The Embeddable typeclass as is, is not great... Ideally it works like Coercible, but actually implementing a typecheck plugin for this is both fragile and a lot of work. Instead, we can bring in a nominal coercion that two runtime reps are equivalent through an GADT, which can then also contain Coercible instances like so:
data Embedding (a :: k1) (b :: k2) where
Embedding :: Coercible a b => Embedding a b
We can supply these instances to term embeddings which may pattern match to get the coercible instances between different kinded types (which of course is sound under the symbolic evaluation).
The
Embeddabletypeclass as is, is not great... Ideally it works like Coercible, but actually implementing a typecheck plugin for this is both fragile and a lot of work. Instead, we can bring in a nominal coercion that two runtime reps are equivalent through an GADT, which can then also containCoercibleinstances like so:We can supply these instances to term embeddings which may pattern match to get the coercible instances between different kinded types (which of course is sound under the symbolic evaluation).