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-
#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.... #extension-GADTs users' guide section on GADTs]: 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