The problem with the recursive case is fatal to transforming DSL a b
into DSL2 a b
.
To do this transformation would require finding the Typeable
dictionary for the existential type b
in the Comp
case - but what b
actually is has already been forgotten.
For example consider the following program:
data X = X Int
-- No Typeable instance for X
dsl1 :: DSL X Char
dsl1 = -- DSL needs to have some way to make non-identity terms,
-- use whatever mechanism it offers for this.
dsl2 :: DSL Int X
dsl2 = -- DSL needs to have some way to make non-identity terms,
-- use whatever mechanism it offers for this.
v :: DSL Int Char
v = Comp dsl1 dsl2
v2 :: DSL2 Int Char
v2 = -- made by converting v from DSL to DSL2, note that Int and Char are Typeable
typeOfIntermediate :: DSL a c -> TypeRep
typeOfIntermediate int =
case int of
Comp (bc :: DSL2 b c) (ab :: DSL2 a b) ->
typeOf (undefined :: b)
typeOfX = typeOfIntermediate v2
In other words if there was a way to do the conversion in general, you could somehow invent a Typeable
instance for a type that doesn't actually have one.