[GHC] #16146: Trivial partial type signature kills type inference in the presence of GADTs

[GHC]

#16146: Trivial partial type signature kills type inference in the presence of
GADTs
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 The real use case isn't `:: _` -- it's `:: Sing @_ (Something Big &&
 Obnoxious)`. The right value for the `_` is being pushed down, but it
 can't be inferred from the expression in the signature. The signature is
 needed in some scenarios... not actually the one that's causing trouble,
 though. The problem is that I think it will be impossible for `singletons`
 to tell the difference between scenarios where it's needed and those where
 it isn't, so we need it not to interfere.

 The signature in question indeed does no quantification.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16146#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler