当约束成立时，将没有约束的 GADT 转换为另一个有约束的 GADT

我们能否将构造函数没有给定约束的 GADT 转换为具有上述约束的 GADT？我想这样做是因为我想要深度嵌入箭头并用（目前）似乎需要的表示做一些有趣的事情Typeable. (一个理由 https://stackoverflow.com/a/12232127/682376)

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
  -- ...

我们可以尝试以下方法from功能，但很快就会崩溃，因为我们没有Typeable递归点的信息

from :: (Typeable a, Typeable b) =>  DSL a b -> DSL2 a b
from (Id)       = Id2
from (Comp g f) = Comp2 (from g) (from f)

因此，我们尝试在类型类中捕获转换。然而，这将会被打破，我们也会错过Typeable b信息为b是一个存在主义的。

class From a b where
  from :: a -> b

instance (Typeable a, Typeable b) => From (DSL a b) (DSL2 a b) where
  from (Id)       = Id2
  from (Comp g f) = Comp2 (from g) (from f)

还有其他建议吗？最终我想创建一个深度嵌入Category and Arrow和...一起Typeable有关类型参数的信息。这样我就可以使用箭头语法在 DSL 中构造一个值，并拥有相当标准的 Haskell 代码。也许我必须求助于 Template Haskell？

递归案例的问题对于改造来说是致命的DSL a b into DSL2 a b.

要进行此转换需要找到Typeable存在类型字典b in the Comp案例 - 但什么b其实已经被遗忘了。

例如，考虑以下程序：

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

换句话说，如果有一种方法可以进行一般转换，那么您可以以某种方式发明一种Typeable一种实际上没有类型的实例。