Cast :: (Castable a b) => Expr a -> Expr b
So here:
instance (Show a) => Show (Expr a) where
show (Cast e) = "Cast " ++ show e -- ERROR
Cast e
is of type Expr a
. We have a Show a
constraint, and by this very instance that implies Show (Expr a)
, so we can call show
on things of type Expr a
.
But e
is not of type Expr a
. Cast
takes an argument of any type Expr a1
and gives you an Expr a
(renaming the type variables to stay consistent with what we're talking about in the instance), so e
is of type Expr a1
. We don't have a Show
constraint for the type a1
, and we require Show a1
to imply Show (Expr a1)
, so there's no way to show e
.
And there's no way to add such a constraint in the Show
instance, because the type a1
doesn't appear in the type of Cast e
. That seems to be the whole point of using a GADT here; you've deliberately thrown away all information about the type of the thing that Cast
was applied to (other than the fact that Castable a1 a
holds), and declared the result to simply be Expr a
.