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 |