Opened 5 years ago

Closed 5 years ago

#2899 closed bug (invalid)

GADT type inference with existentials

Reported by: jochemb Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 6.10.1
Keywords: GADT, existential types Cc: jochem@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:


The following code works in GHC 6.8.2:

{-# OPTIONS -fglasgow-exts #-}
module Test where

data Existential = forall a. Ex (GADT a)

data GADT :: * -> * where
        GCon :: Int -> GADT ()

-- g :: Existential -> Int
g (Ex (GCon x)) = x

The compiler correctly infers the type of x in the definition of g, and correctly infers the type of g.

In GHC 6.10.1, however, this fails with:

    GADT pattern match with non-rigid result type `t'
      Solution: add a type signature
    In the definition of `g': g (Ex (GCon x)) = x
Failed, modules loaded: none.

The solution, to include the type signature of g (that I have commented out), works, but why can't GHC figure out the type of g? GHC 6.8.2 could!

An equivalent version with a non-GADT instead, works correctly:

data GADT a = GCon Int

Ticket #2206 might be related.

Change History (2)

comment:1 Changed 5 years ago by jochemb

  • Cc jochem@… added

comment:2 Changed 5 years ago by simonpj

  • Difficulty set to Unknown
  • Resolution set to invalid
  • Status changed from new to closed

This is by design, I'm afraid. See

The trouble with 6.8.2 is that while it would sometimes guess right, it could also fail in an unpredictable way, so 6.10 is a bit more conservative, but also a bit more predictable.


Note: See TracTickets for help on using tickets.