Embeddings using GADT #4

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