#2004: Pattern matching against GADTs without -XGADTs has odd behavior.
----------------------------------------+-----------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.8.1
Severity: normal | Keywords:
Difficulty: Unknown | Testcase:
Architecture: Unknown | Os: Unknown
----------------------------------------+-----------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2004>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
