Improvement to 'Embeddable' typeclass through 'Embedding' GADT - #21

Merged

RobinWebbers merged 7 commits into

mainfrom

Jul 31, 2026

Commits on Jul 30, 2026

Stub for heterogeneous embedding using 'Embed'
RobinWebbers
committed
2ef46c0

Commits on Jul 31, 2026

WIP embeddings. This implements the improved API for type embeddings. We have yet to resolve the term embeddings. The fresh variable generation probably also needs to be changed afterwards.
RobinWebbers
committed
74cd929
Changed type embeddings interface to allow for a type alias that we simply expand. Makes the declarations a lot easier, as everything is now Haskell and we just pass in a Template Haskell name. Imp…
RobinWebbers
committed
f6f6259
Added some comments to changes in expression subsumption.
RobinWebbers
committed
bf5f4a4
Adjusted fresh variable instantiation to use the new embeddings. Bugfixed the 'Embedding' datatype instance, which got the wrong coercion.
RobinWebbers
committed
cb002b2
Adjusted fresh variable generation to work with the InstEnvs. Fixed bug in generate Embedding instance where we used the wrong destination type. Added functional dependency on 'Embeddable', locking…
RobinWebbers
committed
2297f5f
Typo in commit
RobinWebbers
committed
0a83fe0