[GHC] #10729: Type inference in GADT pattern matches

2 Aug 2015

      #10729: Type inference in GADT pattern matches
-------------------------------------+-------------------------------------
              Reporter:  mniip       |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.11
  (Type checker)                     |
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:
Differential Revisions:              |
-------------------------------------+-------------------------------------
 When pattern matching against GADT constructors, GHC seems to have issues
 with inferring the type of the resulting expression.

 Minimal example: Assume the datatype:

 {{{
 data D a where D :: D ()
 }}}
 A simple function that pattern matches on it:
 {{{
 a D = ()
 }}}
 It is expected to have type `D a -> ()` (Note: not `D () -> ()`, existence
 of a `D` should ensure `()`, not the type signature), but instead it
 errors:
 {{{
 error:
     Couldn't match expected type ‘t’ with actual type ‘()’
       ‘t’ is untouchable
         inside the constraints: t1 ~ ()
         bound by a pattern with constructor: D :: D (),
                  in an equation for ‘a’
     ‘t’ is a rigid type variable bound by
         the inferred type of a :: D t1 -> t
 }}}
 Note that the error goes away when we annotate the type of the function:
 {{{
 b :: D a -> () -- no error
 b D = ()
 }}}
 Or if we supply another branch that clarifies the type:
 {{{
 c D = () -- no error
 c _ = ()
 }}}
 But it reappears if the other branch doesn't provide anything to infer
 from:
 {{{
 d D = () -- error
 d _ = undefined
 }}}
 The same issue happens in `case`:
 {{{
 e x = case x of D -> () -- error
 }}}
 But only when the value being matched comes from outside:
 {{{
 f = case D of D -> () -- no error
 }}}

 This behavior is reprooducible and identical in 7.8.4.

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