Transform a GADT without constraints to another GADT with constraints when such constraints hold

Question

Can we transform a GADT without a given constraint on its constructors to a GADT that does have the said constraint? I want to do this because I want to get a deep-embedding of Arrows and do some interesting things with the representation that (for now) seem to require `Typeable`. (One reason) ``` data DSL a b where Id :: DSL a a Comp :: DSL b c -> DSL a b -> DSL a c -- Other constructors for Arrow(Loop,Apply,etc) data DSL2 a b where Id2 :: (Typeable a, Typeable b) => DSL2 a a Comp2 :: (Typeable a, Typeable b, Typeable c) => DSL2 b c -> DSL2 a b -> DSL2 a c -- ... ``` We could try the following `from` function but that breaks quickly as we don't have the `Typeable` information for the recursive point ``` from :: (Typeable a, Typeable b) => DSL a b -> DSL2 a b from (Id) = Id2 from (Comp g f) = Comp2 (from g) (from f) ``` So instead we try to capture the transformation in a type class. However, that will break as well as we will be missing the `Typeable b` information as `b` is an exist…

Accepted Answer

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.

Transform a GADT without constraints to another GADT with constraints when such constraints hold

Solution

Problem

Related problems