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