[GHC] #16330: Type inference in presence of pattern matching on GADTs

[GHC]

#16330: Type inference in presence of pattern matching on GADTs
-------------------------------------+-------------------------------------
        Reporter:  v0d1ch            |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  low               |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  invalid           |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 This is expected behavior. Per the
 [https://downloads.haskell.org/~ghc/8.6.3/docs/html/users_guide/glasgow_exts.html
 #extension-GADTs users' guide section on GADTs]:

 > The key point about GADTs is that pattern matching causes type
 refinement. For example, in the right hand side of the equation
 >
 > {{{#!hs
 > eval :: Term a -> a
 > eval (Lit i) =  ...
 > }}}
 >
 > the type `a` is refined to `Int`. That’s the whole point! A precise
 specification of the type rules is beyond what this user manual aspires
 to, but the design closely follows that described in the paper
 [http://research.microsoft.com/%7Esimonpj/papers/gadt/ Simple unification-
 based type inference for GADTs], (ICFP 2006). The general principle is
 this: //type refinement is only carried out based on user-supplied type
 annotations//. So if no type signature is supplied for eval, no type
 refinement happens, and lots of obscure error messages will occur.

 Type inference in the presence of GADT pattern matching is extremely
 difficult in general (for reasons explained in further detail in the
 linked paper), and GHC deliberately requires that you supply a type
 signature to avoid these difficulties.

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