Type inference in presence of pattern matching on GADTs

This small example

{-# LANGUAGE GADTs #-}

data G a where
   I :: G Integer

f g = case g of I -> ()

yields

    • Couldn't match expected type ‘p’ with actual type ‘()’
        ‘p’ is untouchable
          inside the constraints: a ~ Integer
          bound by a pattern with constructor: I :: G Integer,
                   in a case alternative
          at gadtsInference.hs:6:17
      ‘p’ is a rigid type variable bound by
        the inferred type of f :: G a -> p
        at gadtsInference.hs:6:1-23
      Possible fix: add a type signature for ‘f’
    • In the expression: ()
      In a case alternative: I -> ()
      In the expression: case g of { I -> () }
    • Relevant bindings include
        f :: G a -> p (bound at gadtsInference.hs:6:1)
  |
6 | f g = case g of I -> ()
  |                      ^^

Without providing the type annotation for f f :: G a -> () GHC cannot infer the correct result type.

Trac metadata

Trac field	Value
Version	8.6.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	low
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 3

added GADTs Tfeature request Trac import labels

closed

This is expected behavior. Per the 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

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 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.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid

added Plow label