That's right. You may not realize it, but you are trying to do type inference on your language. If you want to convert the expression f x
to your typed GADT, it is not enough simply to know the result type. We could have f :: Bool -> Int
with x :: Bool
, f :: (Int -> Int) -> Int
with x :: Int -> Int
, etc. And your typed representation claims to know that, especially since it requires Typeable
on its constants (you may be able to get away with lying about knowing what type it is if you didn't have the Typeable
constraint).
e2t
requires knowledge of what type the expression is expected to be. You need some way to determine what type the argument of an application is expected to be. Maybe you can get around needing this by saying something different, namely:
e2t :: E -> Maybe (exists a. T a)
That is, you are just trying to see if E
can be given a type, but instead of telling it what type it should be, it tells you. This is bottom-up inference, which is generally easier. To encode this:
data AnyT where
AnyT :: Typeable a => T a -> AnyT
Hmm, after playing with this for a while, I realize you run into exactly the same problem on the way back up. I don't think it's possible to do this using only Data.Typeable
. You need to recreate something like dynApp
from Data.Dynamic
, but for T
s instead of regular Haskell types. I.e. you will have to do some operations on TypeRep
s and then at some point insert a "just trust me" unsafeCoerce
once you know it is safe. But you can't convince the compiler it is safe, as far as I can tell.
This would be possible to do in Agda, because the equivalent said operations on TypeRep
s would be observable to the compiler. It would probably be a good exercise when learning that language.