Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables)
data Exp a where
Tru :: Ty Bool
eval :: Exp a -> a
eval Tru = True
Works fine, as does
eval :: Exp a -> a
eval (Tru :: Exp _) = True
But
eval :: Exp a -> a
eval (Tru :: Exp Bool) = True
doesn't, is this an intended design of GADTs/ScopedTypeVariables that the type equality constraint isn't in scope in the type signature of the pattern match, I would like to match on an existential type in my own code:
compile (ArrIx arr index :: Exp (Sca elt)) = do
...
It can be worked around by writing:
eval a@Tru =
case a :: Exp Bool of
but for my own code it seems I must write
compile uuu@(ArrIx arr index :: Exp a) = do
case uuu :: (a ~ Sca elt) => Exp (Sca elt) of
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | lowest |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |