I've been toying with using Data Types a la Carte to get type representations, a `Typeable` class and dynamic types parameterized by a possibly open universe:
If the universe is potentially open, and if we don't care about exhaustive pattern-matching check (which is one of the principal benefits of GADTs -- pronounced in dependently-typed languages), the problem can be solved far more simply. No type classes, no instances, no a la Carte, to packages other than the base. {-# LANGUAGE ScopedTypeVariables #-} module GG where import Data.Typeable argument :: Typeable a => a -> Int argument a | Just (x::Int) <- cast a = x | Just (x::Char) <- cast a = fromEnum x result :: Typeable a => Int -> a result x | Just r <- cast (id x) = r | Just r <- cast ((toEnum x)::Char) = r t1 = argument 'a' t2 = show (result 98 :: Char) That is it, quite symmetrically. This is essentially how type classes are implemented on some systems (Chameleoon, for sure, and probably JHC). By this solution we also gave up on parametricity. Which is why such a solution is probably better kept `under the hood', as an implementation of type classes.