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