Pattern matching against GADTs without -XGADTs has odd behavior.

I'm getting a weird error message declaring a function in GHCi, but the same function declared in the source file works.

Repro case:

{-# LANGUAGE GADTs #-}
module Bug where

data Witness a b c where
   Z :: Witness a as (a,as)
   P :: Witness a as xs -> Witness a (b,as) (b,xs)

data Expr a vars where
   Lam :: String -> Expr a (b,vars) -> Expr (b -> a) vars
   Ap :: Expr (b -> a) vars -> Expr b vars -> Expr a vars

subst :: Witness a vs vsa -> Expr a vs -> Expr b vsa -> Expr b vs
subst = undefined

subAp :: Expr a vs -> Expr a vs
subAp (Ap (Lam _ e) v) = subst Z v e

This compiles fine. But in GHCi:

> let { subAp2 :: Expr a vs -> Expr a vs ; subAp2 (Ap (Lam _ e) v) = subst Z v e }

<interactive>:1:79:
    Couldn't match expected type `a1' against inferred type `a2'
      `a1' is a rigid type variable bound by
           the type signature for `subAp2' at <interactive>:1:21
      `a2' is a rigid type variable bound by
           the constructor `Lam' at <interactive>:1:54
      Expected type: Expr a1 (Decl b vs)
      Inferred type: Expr a2 (Decl b1 vs)
    In the third argument of `subst', namely `e'
    In the expression: subst Z v e

Interestingly, if I do :set -XGADTs followed by that declaration, it works.

Trac metadata

Trac field	Value
Version	6.8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Unknown
Architecture	Unknown