[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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Suppose we have

 {{{#!hs
 data G a where
   G1 :: G Char
   G2 :: G Bool
 }}}

 If I now write

 {{{#!hs
 foo x = case x of
   G1 -> 'z'
   G2 -> True
 }}}

 I rightly get an error around untouchable variables.

 If I add the type signature

 {{{#!hs
 foo :: G a -> a
 }}}

 all is well again. So far, so good.

 Now, I write

 {{{#!hs
 foo :: forall a. G a -> a
 foo x = ((case x of
   G1 -> 'z'
   G2 -> True) :: _)
 }}}

 and I get those untouchable errors again. Untouchable-variable errors
 usually arise when there are multiple possible answers to the type
 inference problem. Yet, that isn't the case here: `_` must stand for `a`.

 Solution: mumble mumble bidirectional type inference mumble mumble.

 Part of the problem comes from Note [Partial expression signatures] in
 TcExpr, which states

 {{{
 here is a guiding principile
     e :: ty
 should behave like
     let x :: ty
         x = e
     in x
 }}}

 Indeed, if we behave like that, the untouchable-variable errors are to be
 expected. But I also think that it would be a nice principle to say that
 `:: _` is always a no-op.

 This is not an idle nice-to-have: if we fix this, `singletons` will
 continue to work with GHC. Right now, it doesn't:
 https://github.com/goldfirere/singletons/issues/357

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