From 2ef46c0f25fcda403bc424056a63c59adb7d1521 Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Mon, 20 Jul 2026 10:51:16 +0200
Subject: [PATCH 1/7] Stub for heterogeneous embedding using 'Embed'

---
 src/Pantomime/BuiltIn.hs | 33 +++++++++++++++++++++++++++++----
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs
index cb2e43d..9c84c75 100644
--- a/src/Pantomime/BuiltIn.hs
+++ b/src/Pantomime/BuiltIn.hs
@@ -22,6 +22,7 @@
 module Pantomime.BuiltIn
   -- | Embeddable constraint for user interpretations.
   ( Embeddable (..)
+  , Embed (..)
 
   -- | Typeclass to differentiate primitive types.
   , Primitive (..)
@@ -174,7 +175,7 @@ module Pantomime.BuiltIn
 
 import Control.Monad.Identity (Identity (..))
 import Data.Bits qualified as Prelude (Bits (..))
-import Data.Coerce (coerce)
+import Data.Coerce (Coercible, coerce)
 import Data.Constraint (Dict (..), HasDict (..))
 import Data.Constraint.Unsafe qualified as Prelude (unsafeSNat)
 import Data.Composition ((.:))
@@ -218,7 +219,7 @@ import GHC.Word
   , Word64 (..)
   )
 import Grisette
-  ( SymShift(..)
+  ( SymShift (..)
   , SizedBV (..)
   , SignConversion (..)
   , BitCast (..)
@@ -241,8 +242,13 @@ class (Private a, Private b) => Embeddable (a :: TYPE r1) (b :: TYPE r2) where
   embed :: a -> b
   project :: b -> a
 
--- class Private a b => Embeddable (a :: k1) (b :: k2)
-
+-- If we do go full 'Embeddable' route with a typechecker plugin: we likely want
+-- to call 'solveEquality' from 'GHC.Tc.Solver.Equality' with the given
+-- constraints that all runtime representations are nominally equivalent.
+--
+-- class PrivateEmbeddable
+-- class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2)
+--
 -- embed
 --   :: forall {r1} {r2} (a :: TYPE r1) (b :: TYPE r2)
 --    . Embeddable a b
@@ -250,8 +256,27 @@ class (Private a, Private b) => Embeddable (a :: TYPE r1) (b :: TYPE r2) where
 --   -> b
 -- embed = embed
 
+-- | Evidence of a 'Coercible' instance for different kinded types.
+--
+-- Example embedding of a type to a 64-bit sized bit vector. The evidence
+-- provided by 'Embed' is expected to be generated by the symbolic evaluator.
+--
+-- ```
+-- plus :: forall {r} (a :: TYPE r). Embed a (BitVec 64) -> a -> a -> a
+-- plus Embed = coerce bvadd
+-- ```
+--
+-- Note that only the plugin can safely generate heterogenous coercions. They
+-- are only safe under symbolic evaluation given a coherent set of embeddings.
+--
+-- Of course, a user is free to construct an instance for a homogenous coercion.
+--
+data Embed (a :: k1) (b :: k2) where
+  Embed :: Coercible a b => Embed a b
+
 -- TODO: For now, we'll just have the platform sized as 64-bit. Not sure how
 -- we would handle this correctly? Maybe with a pragma?
+-- | The bit size of this platforms 'Int#' and 'Word#' primitive.
 type PlatformWordSize = 64
 
 -- | Literal construction function for built-in Haskell 'Int#' literal.

From 74cd92900ed3af689cb20738cb7b4f8d55f10884 Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Fri, 24 Jul 2026 11:04:18 +0200
Subject: [PATCH 2/7] 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.

---
 package.yaml                |   1 +
 pantomime.cabal             |   1 +
 src/Pantomime.hs            |   3 +-
 src/Pantomime/Annotation.hs |   4 +-
 src/Pantomime/Axiom.hs      | 502 +++++++++++++++++++++++-------------
 src/Pantomime/BuiltIn.hs    |  55 ++--
 src/Pantomime/Passes.hs     |  18 +-
 src/Pantomime/Solve.hs      |   9 +-
 8 files changed, 375 insertions(+), 218 deletions(-)

diff --git a/package.yaml b/package.yaml
index c8e6337..7eccbb0 100644
--- a/package.yaml
+++ b/package.yaml
@@ -81,6 +81,7 @@ library:
   - hashable
   - deepseq
   - bytestring
+  - syb
 
 tests:
   pantomime-test:
diff --git a/pantomime.cabal b/pantomime.cabal
index 3f92e5e..d4eaf71 100644
--- a/pantomime.cabal
+++ b/pantomime.cabal
@@ -106,6 +106,7 @@ library
     , microlens
     , mtl
     , primitive
+    , syb
     , template-haskell
     , text
     , transformers
diff --git a/src/Pantomime.hs b/src/Pantomime.hs
index e2f1172..21d5ac0 100644
--- a/src/Pantomime.hs
+++ b/src/Pantomime.hs
@@ -4,7 +4,8 @@ module Pantomime
   ( plugin
 
   , Theory (..)
-  , PluginAxioms (..)
+  , Embeddings (..)
+  , ArgType (..)
   , pantomime
   , pantomimeMarker
   , pantomimeNothing
diff --git a/src/Pantomime/Annotation.hs b/src/Pantomime/Annotation.hs
index f2a725f..5f85769 100644
--- a/src/Pantomime/Annotation.hs
+++ b/src/Pantomime/Annotation.hs
@@ -6,13 +6,13 @@ module Pantomime.Annotation
   ) where
 
 import Data.Data (Data)
-import Pantomime.Axiom (PluginAxioms)
+import Pantomime.Axiom (Embeddings)
 import GHC.Utils.Outputable (Outputable (..), hang)
 
 -- TODO: Not sure I like the name. This checks whether an expression whose
 -- result is of type Bool is valid. That is, whether it will always return True.
 data Theory where
-  Theory :: PluginAxioms -> Theory
+  Theory :: Embeddings -> Theory
   deriving (Show, Data)
 
 instance Outputable Theory where
diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 79c04e5..1f9e9d8 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -1,19 +1,21 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Pantomime.Axiom
-  ( PluginAxioms (..)
-  , PluginAxiomsR (..)
+  ( Embeddings (..)
+  , ArgType (..)
+  , EmbeddingsR (..)
   , TypeAxiomsR
   , TermAxiomsR
-  , resolvePluginAxioms
+  , resolveEmbeddings
   ) where
 
 import Prelude hiding (break)
 import Language.Haskell.TH qualified as TH
 
-import GHC.Core.TyCo.Rep (UnivCoProvenance(..))
-import GHC.Core.TyCon.Env (TyConEnv, mkTyConEnv)
-import GHC.Data.TrieMap (TrieMap (..), insertTM)
+import GHC.Core.InstEnv (mkLocalClsInst, emptyInstEnv, extendInstEnv)
+import GHC.Core.TyCo.Rep (UnivCoProvenance (..), Coercion (..))
+import GHC.Core.TyCon.Env (TyConEnv)
+import GHC.Core.Unfold.Make (mkDFunUnfolding)
 import GHC.Plugins
   ( TyCon (..)
   , Name
@@ -23,56 +25,80 @@ import GHC.Plugins
   , Role (..)
   , Expr (..)
   , Var (..)
-  , TypeOrConstraint (..)
+  , Type
+  , MonadUnique (..)
+  , OverlapFlag (..)
+  , OverlapMode (..)
+  , TyVar
+  , Unique
   , mkTyConTy
   , mkUnivCo
   , dataConWorkId
   , mkApps
-  , mkCast
-  , mkSymCo
-  , exprType
+  , mkAppTy
+  , mkTyVarTy
+  , mkVarOccFS
+  , mkSystemName
+  , mkTyVar
   , classDataCon
   , typeKind
-  , unitExpr
-  , unrestricted
-  , emptyInScopeSet
-  , sORTKind_maybe
   , coercibleDataCon
+  , generatedSrcSpan
+  , setIdUnfolding
+  , splitFunTy_maybe
+  , isTypeSynonymTyCon
+  , mkFastString
+  , expandTypeSynonyms
+  , splitTyConAppNoView_maybe
+  , unitDataConId
   )
 import GHC.Tc.Utils.TcType (eqType)
+import GHC.Types.Id.Make (mkDictFunId)
+import GHC.Types.Name (mkInternalName)
 import GHC.Utils.Outputable
   ( Outputable (..)
   , IsDoc (..)
-  , IsLine (fsep, (<+>), text)
+  , IsLine (fsep, (<+>), text, hcat)
+  , SDoc
   , hang
   , punctuate
   , comma
   , brackets
+  , parens
   )
+import GHC.Types.SourceText (SourceText(..))
+import GHC.Types.Unique (incrUnique, minLocalUnique)
 
-import GHC.Exts (IsList (..))
-
-import Control.Monad ((>=>), guard, when)
-import Control.Applicative (Alternative (..))
+import Control.Monad ((>=>), unless)
 
 import Data.Data (Data)
-import Data.Function (on)
-import Data.Map (Map)
+import Data.Foldable (for_)
+import Data.Generics.Aliases (mkQ)
+import Data.Generics.Schemes (something)
+import Data.HashMap.Internal.Strict (HashMap)
+import Data.HashMap.Strict qualified as HashMap
+import Data.List (sort)
+import Data.Text (Text, unpack)
 import Data.Traversable (for)
 
 import Effectful
+import Effectful.Break (runBreak, break)
 import Effectful.Error.Static
 import Effectful.GHC.TH
 import Effectful.GHC.TyThing
+import Effectful.GHC.Unique (HasUnique)
 import Effectful.Context
 
-import Pantomime.BuiltIn (Embeddable)
+import Pantomime.BuiltIn (Embeddable, Embedding (..))
 import Pantomime.Unification (subsumeExpr)
-import Pantomime.Util (foldM', freshId, foldlBy)
+import Pantomime.Util (foldM', dbg, failWith)
 
--- TODO: We're switching away from using 'Coercible' as it requires same runtime
+-- TODO: This should be renamed to 'Embeddings' instead of 'Axioms'. We can
+-- probably drop the 'Plugin' portion as well.
 -- kinded types: something we don't care about within the evaluator. Instead,
 -- we provide a custom typeclass. The comments should mirror this!
+-- TODO: The text below should be updated to reflect the current state of
+-- embeddings. We should at some point link the paper also.
 -- | User axioms only visible to the plugin.
 --
 -- The kinds and types of the mapped terms should match up exactly. The
@@ -112,15 +138,13 @@ import Pantomime.Util (foldM', freshId, foldlBy)
 -- 'BitVec'. The importance lies in using a coercion 'Coercible IntN BitVec'.
 --
 -- > plusInterp
--- >   :: Coercible IntN BitVec
+-- >   :: Embeddable bv BitVec
 -- >   => KnownNat n
--- >   => IntN n
--- >   -> IntN n
--- >   -> IntN n
--- > plusInterp = go
--- >   where
--- >     go :: bv ~ BitVec => bv n -> bv n -> bv n
--- >     go = coerce plusIntN
+-- >   => bv n
+-- >   -> bv n
+-- >   -> bv n
+-- > plusInterp = case embedding @bv @BitVec of
+-- >   Embedding -> coerce SMT.bvadd
 --
 -- Note, the where clause is only to trick Haskell into allowing the coercion
 -- to appear at the top level. With this defintion in place, we supply the
@@ -132,20 +156,24 @@ import Pantomime.Util (foldM', freshId, foldlBy)
 -- one-to-one. That is, to complete the interpretation, we supply 'plusInterp'
 -- with the user-supplied coercion that 'Coercible IntN BitVec'. Afterwards, the
 -- types match up and the function is a valid interpretation.
-data PluginAxioms where
-  PluginAxioms ::
-    { typeAxioms :: Map TH.Name TH.Name
-    -- ^ Type-level representational equivalence axioms.
+data Embeddings where
+  Embeddings ::
+    -- TODO: Probably want to remove the comment about fresh symbolic values
+    -- once we change the interface on this.
+    { typeEmbeddings :: [(ArgType, ArgType)]
+    -- ^ Type-level embeddings.
     --
-    -- Both the key and value of these mappings should be resolvable to 'TyCon'.
-    -- One may think about this as providing an instance 'Coercible' to just the
-    -- plugin between the given 'TyCon'. This instance is used within the solver
-    -- when constructing fresh symbolic values and when resolving instances
-    -- for term-axioms.
+    -- Both the key and value of these mappings should be resolvable to a GHC
+    -- 'Type'. One may think about this as providing an instance 'Embeddable'
+    -- to the plugin between for the given types. This instance is used within
+    -- the solver when constructing fresh symbolic values and when resolving
+    -- instances for term-embeddings.
     -- TODO: Term axioms should allow for recursive definitions also. It
     -- probably won't be used much, but it would be good! I guess we would want
     -- a 'Bind' from GHC, but for template haskell names.
-    , termAxioms :: [(TH.Name, TH.Name)]
+    -- Actually, the above is not really required I think: the embedding can
+    -- always form a local recursive group. Will have to think about this!
+    , termEmbeddings :: [(TH.Name, TH.Name)]
     -- ^ Term-level representational equivalence axioms.
     --
     -- Both the key and value of these mappings should be resolvable to 'Id'.
@@ -157,28 +185,28 @@ data PluginAxioms where
     -- Note that this is a list because the ordering of the definitions does
     -- matter: any later definitions may use ones defined earlier. Duplicate
     -- definitions are considered an error.
-    } -> PluginAxioms
+    } -> Embeddings
   deriving (Show, Data)
 
-instance Outputable PluginAxioms where
-  ppr PluginAxioms { .. } = do
+instance Outputable Embeddings where
+  ppr Embeddings { .. } = do
     let pprKV (key, value) = text (show key) <+> ":->" <+> text (show value)
     let pprKVList pairs = brackets $ fsep $ punctuate comma $ pprKV <$> pairs
-    hang "PluginAxioms" 2 $ vcat
-      [ hang "Type Axioms:" 2 $ pprKVList (toList typeAxioms)
-      , hang "Term Axioms:" 2 $ pprKVList termAxioms
+    hang "Embeddings" 2 $ vcat
+      [ hang "Type Embeddings:" 2 $ pprKVList typeEmbeddings
+      , hang "Term Embeddings:" 2 $ pprKVList termEmbeddings
       ]
 
-instance Semigroup PluginAxioms where
-  (<>) l r = PluginAxioms
-    { typeAxioms = typeAxioms l <> typeAxioms r
-    , termAxioms = termAxioms l <> termAxioms r
+instance Semigroup Embeddings where
+  (<>) l r = Embeddings
+    { typeEmbeddings = typeEmbeddings l <> typeEmbeddings r
+    , termEmbeddings = termEmbeddings l <> termEmbeddings r
     }
 
-instance Monoid PluginAxioms where
-  mempty = PluginAxioms
-    { typeAxioms = mempty
-    , termAxioms = mempty
+instance Monoid Embeddings where
+  mempty = Embeddings
+    { typeEmbeddings = mempty
+    , termEmbeddings = mempty
     }
 
 type TypeAxiomsR = TyConEnv TyCon
@@ -189,8 +217,8 @@ type TermAxiomsR = [(Id, CoreExpr)]
 -- TODO: I think it would be good to have type synonyms for both of these fields
 -- as we use them independently as well.
 -- | Fully resolved plugin axioms. These may be used as-is by the solver.
-data PluginAxiomsR where
-  PluginAxiomsR ::
+data EmbeddingsR where
+  EmbeddingsR ::
     { typeAxiomsR :: TypeAxiomsR
     -- ^ Type-level axioms, mainly used to construct symbolic values.
     , termAxiomsR :: TermAxiomsR
@@ -198,27 +226,150 @@ data PluginAxiomsR where
     -- resolved by the type-axioms, where applicable.
     --
     -- This may be used to extend substitution environments.
-    } -> PluginAxiomsR
-    deriving (Data)
+    } -> EmbeddingsR
 
-instance Outputable PluginAxiomsR where
-  ppr PluginAxiomsR { .. } = hang "PluginAxiomsR" 2 $ vcat
-    [ hang "Type Axioms:" 2 $ ppr typeAxiomsR
-    , hang "Term Axioms:" 2 $ ppr termAxiomsR
+instance Outputable EmbeddingsR where
+  ppr EmbeddingsR { .. } = hang "EmbeddingsR" 2 $ vcat
+    [ hang "Type Embeddings:" 2 $ ppr typeAxiomsR
+    , hang "Term Embeddings:" 2 $ ppr termAxiomsR
     ]
 
-instance Semigroup PluginAxiomsR where
-  (<>) l r = PluginAxiomsR
+instance Semigroup EmbeddingsR where
+  (<>) l r = EmbeddingsR
+    -- { typeAxiomsR = unionInstEnv (typeAxiomsR l) (typeAxiomsR r)
     { typeAxiomsR = typeAxiomsR l <> typeAxiomsR r
     , termAxiomsR = termAxiomsR l <> termAxiomsR r
     }
 
-instance Monoid PluginAxiomsR where
-  mempty = PluginAxiomsR
+instance Monoid EmbeddingsR where
+  mempty = EmbeddingsR
+    -- { typeAxiomsR = emptyInstEnv
     { typeAxiomsR = mempty
     , termAxiomsR = mempty
     }
 
+-- | A restricted form of types used for user defined 'Embeddable' instances.
+data ArgType where
+  ATApp :: ArgType -> ArgType -> ArgType
+  ATCon :: TH.Name -> ArgType
+  ATVar :: Text -> ArgType -> ArgType
+  deriving (Show, Data)
+
+instance Outputable ArgType where
+  ppr = do
+    let go par = \case
+          ATApp fun arg -> par $ go id fun <+> go parens arg
+          ATCon con -> text $ show con
+          ATVar var _kind -> text $ unpack var
+    go id
+
+-- | Variable store, used to track variable occurences and create new ones.
+--
+-- NOTE: As the uniques in the TyVar's are just incremented local Unique values,
+-- we can get a deterministic order of their occurence by sorting based on the
+-- Unique.
+type VarStore = (HashMap Text TyVar, Unique)
+
+-- | Reify an 'ArgType' for a typeclass instance into a full Haskell type.
+--
+-- The 'Unique' on the 'TyVar' in the 'VarStore' can be sorted for a
+-- deterministic declaration order for the type variables.
+reifyArgType
+  :: HasCallStack
+  => Error SDoc :> es
+  => Error (LookupError TH.Name) :> es
+  => Error (LookupError Name) :> es
+  => THNameToGHCName :> es
+  => HasThings :> es
+  => Context Reader [TyCon] :> es
+  => Context Writer VarStore :> es
+  => Context Reader VarStore :> es
+  => ArgType
+  -> Eff es Type
+-- TODO: Fix call stack growth.
+reifyArgType = \case
+  ATApp fun arg -> do
+    -- Get function type and check if has a function kind.
+    fun' <- reifyArgType fun
+    let err = "Type application function does not have function kind."
+    (_, _, farg, _) <- failWith @SDoc err $ splitFunTy_maybe (typeKind fun')
+
+    -- Get the argument and check if its kind mathes the function argument.
+    arg' <- reifyArgType arg
+    unless (eqType farg $ typeKind arg') do
+      throwError_ @SDoc "Argument kind does not equal expected kind."
+
+    -- Return the application.
+    pure $ mkAppTy fun' arg'
+
+  ATCon name -> do
+    name' <- thNameToGhcName name
+    tc <- lookupTyConAll name'
+    pure $ mkTyConTy tc
+
+  ATVar name kind -> runBreak do
+    -- Fetch the variable store.
+    (mapping, unique) <- get @VarStore
+
+    -- Reify the kind of the variable.
+    kind' <- reifyArgType kind
+
+    -- Early break if we already have a type variable for the name.
+    let existing = HashMap.lookup name mapping
+    for_ existing \tv -> do
+      let kind2 = varType tv
+      unless (eqType kind' kind2) do
+        throwError_ @SDoc $ hcat
+          [ "Type variable '"
+          , text $ unpack name
+          , "' occurs with different kinds '"
+          , ppr kind'
+          , "' and '"
+          , ppr kind2
+          , "'"
+          ]
+      break $ mkTyVarTy tv
+
+    -- Create the fresh type variable.
+    let occ = mkFastString $ unpack name -- TODO: Not the best conversion...
+    let name' = mkSystemName unique $ mkVarOccFS occ
+    let tv = mkTyVar name' kind'
+
+    -- Extend the store with the type variable and increment the unique.
+    let mapping' = HashMap.insert name tv mapping
+    let unique' = incrUnique unique
+    put (mapping', unique')
+
+    -- Return the type variable.
+    pure $ mkTyVarTy tv
+
+-- | Finds a type synonym in a 'Type'.
+hasSynonym :: Type -> Maybe TyCon
+hasSynonym = something $ mkQ Nothing \ty -> do
+  case splitTyConAppNoView_maybe ty of
+    Just (tc, _) | isTypeSynonymTyCon tc -> Just tc
+    _ -> Nothing
+
+-- | Expand all type synonyms from a type.
+--
+-- Throws an error if any type synonym still remains.
+expandTypeSynonyms'
+  :: Error SDoc :> es
+  => Type
+  -> Eff es Type
+expandTypeSynonyms' ty = do
+  let ty' = expandTypeSynonyms ty
+  case hasSynonym ty' of
+    Just tc -> throwError_ @SDoc $ hcat
+      [ "Type '"
+      , ppr ty'
+      , "' contains unsaturated type constructor '"
+      , ppr tc
+      , "' after type alias expansion."
+      ]
+    Nothing -> pure ()
+  pure ty'
+
 -- | Resolve user-supplied axioms in terms of Template Haskell names to their
 -- internal Core representation.
 --
@@ -233,136 +384,120 @@ instance Monoid PluginAxiomsR where
 -- Lastly, this also ensures that mappings are only made for OPAQUE functions.
 -- A special case here we do allow is a NOINLINE function without an unfolding.
 -- For these, we do not use any of the user-provided coercions.
-resolvePluginAxioms
+resolveEmbeddings
   :: HasCallStack
   -- TODO: Adjust these errors!
   => Error String :> es
+  => Error SDoc :> es
   => Error (LookupError TH.Name) :> es
   => Error (LookupError Name) :> es
   => THNameToGHCName :> es
   => HasThings :> es
+  => HasUnique :> es
   => Context Reader CoreProgram :> es
   => Context Reader [TyCon] :> es
-  => PluginAxioms
-  -> Eff es PluginAxiomsR
-resolvePluginAxioms PluginAxioms { .. } = do
+  => Embeddings
+  -> Eff es EmbeddingsR
+resolveEmbeddings Embeddings { .. } = do
   -- Get the typeclass we want to instantiate.
-  embedCls <- thNameToGhcName >=> lookupClass $ ''Embeddable
-
-  -- Resolve the type-level axioms. This is simply a lookup for the TyCon.
-  typeAxiomsRList <- for (toList typeAxioms) \(orig, interp) -> do
-    let resolve = thNameToGhcName >=> lookupTyConAll
-    -- TODO: Should we ensure that the original TyCon is a data-type or newtype?
-    -- Otherwise, the conversion might be very fragile! Not sure if I'm missing
-    -- any here.
-    orig' <- resolve orig
-    interp' <- resolve interp
-    pure (orig', interp')
+  embeddable <- thNameToGhcName >=> lookupClass $ ''Embeddable
+  embedding <- thNameToGhcName >=> lookupDataCon $ 'Embedding
+
+  -- Gather the instance environment for resolution.
+  instEnv <- foldM' emptyInstEnv typeEmbeddings \instEnv (tyL, tyR) -> do
+    -- Reify the instance head into GHC Types.
+    let runReify = runContextLocal @VarStore (mempty, minLocalUnique)
+    ((tyL', tyR'), store') <- runReify do
+      tyL' <- reifyArgType tyL
+      tyR' <- reifyArgType tyR
+      pure (tyL', tyR')
+
+    -- Expand the type synonyms in the types.
+    tyL'' <- expandTypeSynonyms' tyL'
+    tyR'' <- expandTypeSynonyms' tyR'
+
+    -- FIXME: We should ensure that the kinds for the type match up
+    -- (up to runtime representation).
 
-  -- Gather the dictionary map for instance resolution.
-  dicts <- foldM' emptyTM typeAxiomsRList \dicts (tcR, tcL) -> do
     -- Gather the information to construct the coercion.
-    let prov = PluginProv "pantomime user-defined"
-    let tyL = mkTyConTy tcL
-    let tyR = mkTyConTy tcR
-    let co = mkUnivCo prov [] Representational tyL tyR
-
-    -- Gather the dictionaries for 'Coercible'.
-    let dictCo = do
-          -- Get the kind of the coercible TyCon.
-          let kind = tyConKind tcL
-
-          -- Ensure the kind and roles match up.
-          let eqKind = eqType kind $ tyConKind tcR
-          let eqRoles = all (uncurry (==)) $ on zip tyConRoles tcL tcR
-          guard $ eqKind && eqRoles
-
-          -- Box the coercion.
-          let eqVar = Var $ dataConWorkId coercibleDataCon
-          let dictL = mkApps eqVar
-                [ Type kind
-                , Type tyL
-                , Type tyR
-                , Coercion co
-                ]
-          let dictR = mkApps eqVar
-                [ Type kind
-                , Type tyR
-                , Type tyL
-                , Coercion $ mkSymCo co
-                ]
-          pure (dictL, dictR)
-
-    -- TODO: At some point I want to have 'Embeddable' to act like 'Coercible',
-    -- with the adjustment that we can also generate dictionaries here where
-    -- the final kind can differ. So to be precise, the kinds need to match up
-    -- precisely except the result kind. This one always has to be of kind
-    -- 'TYPE r' but the runtime representations do not have to match.
-    -- Gather the information to construct the final dictionary.
-    --
-    -- Note that for all normal intents and purposes, 'Embeddable' should only
-    -- have instances when the kinds match up exactly. Only axioms may have
-    -- their representation differ, as these will never reach the runtime.
-    --
-    -- At that point, we can also just evict the 'Coercible' instance that we
-    -- build up here.
-    -- Gather the dictionaries for 'Embeddable'.
-    let dictEm = do
-          -- Gather the RuntimeRep of the given types.
-          let runtimeRep ty = do
-                (sort, rty) <- sORTKind_maybe $ typeKind ty
-                case sort of
-                  TypeLike -> pure rty
-                  ConstraintLike -> empty
-
-          repL <- runtimeRep tyL
-          repR <- runtimeRep tyR
-          let con = Var . dataConWorkId . classDataCon $ embedCls
-          -- TODO: For now, we're not really constructing the private typeclass
-          -- correctly. I don't think it's important for our use case, but it is
-          -- not very nice to do it like this.
-          let private = unitExpr
-
-          -- Construct the embed function.
-          let (idE, _) = freshId "arg" (unrestricted tyL) emptyInScopeSet
-          let embed = Lam idE $ mkCast (Var idE) co
-
-          -- Construct the project function.
-          let (idP, _) = freshId "arg" (unrestricted tyR) emptyInScopeSet
-          let project = Lam idP $ mkCast (Var idP) (mkSymCo co)
-
-          -- Construct the typeclass dictionary.
-          pure $ mkApps con
-            [ Type repL
-            , Type repR
-            , Type tyL
-            , Type tyR
-            , private
-            , private
-            , embed
-            , project
-            ]
-
-    -- Actually collect all dictionaries.
-    let dictCo' = maybe [] (\(l, r) -> [l, r]) dictCo
-    let dictEm' = maybe [] (: []) dictEm
-    let dictsNew = dictCo' <> dictEm'
-
-    -- Throw an error if we could not create any.
-    when (null dictsNew) do
-      throwError @String "resolvePluginAxioms: could not create any Embeddable or Coercible dictionaries for the given axioms"
-
-    -- Insert all dictionaries.
-    pure $ foldlBy dicts dictsNew \acc dict -> do
-      let ty = exprType dict
-      insertTM ty dict acc
+    let prov = PluginProv "sym-fc embedding (user-defined)"
+    let kindL = typeKind tyL''
+    let kindR = typeKind tyR''
+    let co = mkUnivCo prov [] Representational tyL'' tyR''
+
+    -- Create a unique name for the embedding.
+    unique <- getUniqueM
+    let occ = mkVarOccFS "embedding"
+    let name = mkInternalName unique occ generatedSrcSpan
+
+    -- Type variables used in the instance declaration.
+    -- NOTE: We can sort the type variables by Unique to get the declaration
+    -- order per 'reifyArgType'.
+    let tvs = sort $ HashMap.elems (fst store')
+
+    -- We don't support typeclass requirements (not sure if we ever need them)?
+    let theta = []
+
+    -- Construct the initial 'DFunId', without unfolding.
+    let tys = [kindL, kindR, tyL'', tyR'']
+    let dfun = mkDictFunId name tvs theta embeddable tys
+
+    -- Create the 'Coercible' dictionary.
+    let coercibleDict = mkApps (Var $ dataConWorkId coercibleDataCon)
+          [ Type kindL
+          , Type tyL''
+          , Type tyR''
+          , Coercion co
+          ]
+
+    -- Create the 'Embedding' data type.
+    let coK = mkUnivCo prov [] Nominal kindL kindR
+    let embed = mkApps (Var $ dataConWorkId embedding)
+          [ Type kindL
+          , Type kindR
+          , Type tyL''
+          , Type tyR''
+          , Type tyR''
+          , Coercion coK
+          , Coercion $ Refl tyR''
+          , coercibleDict
+          ]
+
+    -- The 'Embeddable' typeclass has a 'PrivateEmbeddable' requirement that is
+    -- there just so users cannot create an instance manually. It is essentially
+    -- a unit value with a different type, so we just pass in a unit as it is
+    -- never used. Slightly hacky, but it works (we cannot create the instance
+    -- correctly as it is not exported).
+    let private = Var unitDataConId
+
+    -- Create the 'DFunUnfolding'.
+    let bndrs = []
+    let dc = classDataCon embeddable
+    let args = [Type kindL, Type kindR, Type tyL'', Type tyR'', private, embed]
+    let unfolding = mkDFunUnfolding bndrs dc args
+
+    -- Set the unfolding of the 'DFunId'.
+    let dfun' = setIdUnfolding dfun unfolding
+
+    -- Create the local typeclass instance.
+    let overlap = OverlapFlag
+          { overlapMode = NoOverlap NoSourceText
+          , isSafeOverlap = False
+          }
+    let warn = Nothing
+    let inst = mkLocalClsInst dfun' overlap tvs embeddable tys warn
+
+    -- Extend the instance environment with the embedding.
+    pure $ extendInstEnv instEnv inst
+
+  dbg instEnv
 
   -- TODO: We should first ensure that termAxioms do not contain duplicate
   -- definitions.
 
   -- Gather a binder mapping for a substitution. This will use the dictionary
   -- map to supply coercions to any Opaque values that require it.
-  termAxiomsR <- for termAxioms \(orig, interp) -> do
+  _termAxiomsR <- for termEmbeddings \(orig, interp) -> do
     -- Resolve the names as identifiers.
     let resolve = thNameToGhcName >=> lookupIdAll
     orig' <- resolve orig
@@ -401,13 +536,14 @@ resolvePluginAxioms PluginAxioms { .. } = do
     --   _ -> pure emptyTM
 
     -- Check whether the interpretation matches.
+    let dicts = undefined
     expr' <- subsumeExpr dicts (Var interp') $ varType orig'
 
     -- Return the mapping.
     pure (orig', expr')
 
   -- Collect the resolved type and term mappings.
-  pure PluginAxiomsR
-    { typeAxiomsR = mkTyConEnv typeAxiomsRList
-    , termAxiomsR
+  pure EmbeddingsR
+    { typeAxiomsR = mempty
+    , termAxiomsR = mempty
     }
diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs
index 9c84c75..9d08d45 100644
--- a/src/Pantomime/BuiltIn.hs
+++ b/src/Pantomime/BuiltIn.hs
@@ -21,8 +21,9 @@
 -- you're doing!
 module Pantomime.BuiltIn
   -- | Embeddable constraint for user interpretations.
-  ( Embeddable (..)
-  , Embed (..)
+  ( Embeddable
+  , Embedding (..)
+  , embedding
 
   -- | Typeclass to differentiate primitive types.
   , Primitive (..)
@@ -231,22 +232,13 @@ import Pantomime.Util qualified as Util (BitVec, (%+))
 import Prelude qualified
 import Prelude (Applicative (..), Ordering (..), Maybe (..), ($), (.))
 
--- TODO: I guess we could also make this a typeclass without variables?
-class Private a
-
-instance Private a
-
--- TODO: At some point I want this typeclass to have behaviour like 'Coercible'.
--- For now, I'll leave it like this as it eases the implementation quite a bit.
-class (Private a, Private b) => Embeddable (a :: TYPE r1) (b :: TYPE r2) where
-  embed :: a -> b
-  project :: b -> a
-
+-- Below some stubs if we ever want to make 'Embeddable' be like 'Coercible'
+-- without the evidence pattern matching.
+--
 -- If we do go full 'Embeddable' route with a typechecker plugin: we likely want
 -- to call 'solveEquality' from 'GHC.Tc.Solver.Equality' with the given
 -- constraints that all runtime representations are nominally equivalent.
 --
--- class PrivateEmbeddable
 -- class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2)
 --
 -- embed
@@ -254,25 +246,48 @@ class (Private a, Private b) => Embeddable (a :: TYPE r1) (b :: TYPE r2) where
 --    . Embeddable a b
 --   => a
 --   -> b
--- embed = embed
+-- embed = noinline embed
+
+-- | Unexported typeclass that has no instances.
+--
+-- This disallows any instance of 'Embeddable' to be defined as this typeclass
+-- requirement is not exported *and* does not have an instance.
+class PrivateEmbeddable
 
 -- | Evidence of a 'Coercible' instance for different kinded types.
 --
 -- Example embedding of a type to a 64-bit sized bit vector. The evidence
--- provided by 'Embed' is expected to be generated by the symbolic evaluator.
+-- provided by 'Embeddable' is generated by the symbolic evaluator via type
+-- embeddings. Term embeddings can consume these instances of 'Embeddable'.
 --
 -- ```
--- plus :: forall {r} (a :: TYPE r). Embed a (BitVec 64) -> a -> a -> a
--- plus Embed = coerce bvadd
+-- plus64 :: forall {r} (a :: TYPE r). Embeddable a (BitVec 64) => a -> a -> a
+-- plus64 = case embedding of Embedding -> coerce bvadd
 -- ```
 --
 -- Note that only the plugin can safely generate heterogenous coercions. They
 -- are only safe under symbolic evaluation given a coherent set of embeddings.
 --
 -- Of course, a user is free to construct an instance for a homogenous coercion.
+class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2) where
+  -- | Get the 'Embedding' instance of the typeclass.
+  --
+  -- We expose 'embedding' as it keeps the kind arguments invisible, which is
+  -- more ergonomic.
+  embedding' :: Embedding a b
+
+-- | Get the 'Embedding' instance of the typeclass.
+embedding
+  :: forall {k1} {k2} (a :: k1) (b :: k2)
+   . Embeddable a b
+  => Embedding a b
+embedding = embedding'
+
+-- | Data type carrying of a 'Coercible' instance for different kinded types.
 --
-data Embed (a :: k1) (b :: k2) where
-  Embed :: Coercible a b => Embed a b
+-- See 'Embeddable' for more information.
+data Embedding (a :: k1) (b :: k2) where
+  Embedding :: Coercible a b => Embedding a b
 
 -- TODO: For now, we'll just have the platform sized as 64-bit. Not sure how
 -- we would handle this correctly? Maybe with a pragma?
diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs
index 58d47b7..9c08a8a 100644
--- a/src/Pantomime/Passes.hs
+++ b/src/Pantomime/Passes.hs
@@ -7,8 +7,6 @@ import GHC.Plugins hiding (empty, (<>), thNameToGhcName, getFirstAnnotations)
 import GHC.Core.Lint
 import GHC.Driver.Config.Core.Lint (initLintConfig)
 
-import GHC.Core.Make (mkStringExpr)
-
 import Grisette
   ( GrisetteSMTConfig (..)
   , SMTConfig (..)
@@ -28,7 +26,7 @@ import Language.Haskell.TH qualified as TH
 
 import Pantomime.Solve
 import Pantomime.Unification
-import Pantomime.Axiom (resolvePluginAxioms)
+import Pantomime.Axiom (resolveEmbeddings)
 import Pantomime.Annotation
 
 import Effectful
@@ -45,6 +43,7 @@ import Effectful.GHC.Display
 import Effectful.GHC.TyThing
 import Effectful.GHC.External
 import Effectful.GHC.Annotations
+import Effectful.GHC.Unique (HasUnique)
 
 -- | An always non-recursive binder.
 data Bind' a = Bind' a (Expr a)
@@ -106,12 +105,14 @@ runSymbolic
     , Error UnificationError
     , Error SolverError
     , Error String
+    , Error SDoc
     , Provider_ Solver ()
     , HasAnnotations
     , THNameToGHCName
     , HasThings
     , Context Reader CoreProgram
     , Context Reader [TyCon]
+    , HasUnique
     , HasInstEnvs
     , HasFamInstEnvs
     , HasExternalPackageState
@@ -130,12 +131,14 @@ runSymbolic guts
   . runHasExternalPackageState
   . runHasFamInstEnv guts
   . runHasInstEnvs guts
+  . runHasUnique
   . runContextReader (mg_tcs guts)
   . runContextReader (mg_binds guts)
   . runHasThings
   . runThNameToGhcName
   . runHasAnnotations
   . runProvider_ (const $ runSolver solver)
+  . runErrorWith @SDoc propagateError
   . runErrorWith @String propagateErrorShow
   . runErrorWith @SolverError propagateErrorShow
   . runErrorWith @UnificationError propagateError
@@ -201,6 +204,7 @@ printAndLint bind = do
 checkValidityAndEmbed
   :: ( HasCallStack
      , Error String :> es
+     , Error SDoc :> es
      , Error (LookupError Name) :> es
      , Error (LookupError TH.Name) :> es
      , Error SolverError :> es
@@ -209,11 +213,11 @@ checkValidityAndEmbed
      , Provider_ Solver () :> es
      , HasFamInstEnvs :> es
      , HasThings :> es
+     , HasUnique :> es
      , THNameToGHCName :> es
      , HasAnnotations :> es
      , CoreE :> es
      , IOE :> es
-     , HasDynFlagsE :> es
      )
   => ModGuts
   -> Eff es ModGuts
@@ -225,9 +229,9 @@ checkValidityAndEmbed guts = do
   justId <- thNameToGhcName 'pantomimeJust >>= lookupIdAll
 
   (binds, results) <- fmap unzip $ for (mg_binds guts) \case
-    NonRec x e | Just (Theory axioms) <- lookupUFM anns $ varName x -> do
-      axioms' <- resolvePluginAxioms axioms
-      mCounterexample <- checkValid axioms' e
+    NonRec x e | Just (Theory embeddings) <- lookupUFM anns $ varName x -> do
+      embeddings' <- resolveEmbeddings embeddings
+      mCounterexample <- checkValid embeddings' e
       let varNameStr = getOccString x
       case mCounterexample of
         Nothing -> do
diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs
index a6c79f9..2e2f298 100644
--- a/src/Pantomime/Solve.hs
+++ b/src/Pantomime/Solve.hs
@@ -32,7 +32,6 @@ import GHC.Plugins
   , Bind (..)
   , Var
   , exprType
-  , varType
   , vcat
   , emptyInScopeSet
   , getOccString
@@ -71,7 +70,7 @@ import Pantomime.Symbolise
 import Pantomime.Subst
 import Pantomime.Fresh
 import Pantomime.Util (dbg)
-import Pantomime.Axiom (PluginAxiomsR (..))
+import Pantomime.Axiom (EmbeddingsR (..))
 import Pantomime.PrimOps (PrimOp)
 import Pantomime.Defer (defer, withDeferrable)
 import Pantomime.Binding
@@ -128,14 +127,14 @@ construct
   => Context Reader FamInstEnvs :> es
   => Error String :> es
   => [(Var, forall fs. PrimOp fs)]
-  -> PluginAxiomsR
+  -> EmbeddingsR
   -> CoreProgram
   -> CoreExpr
   -- FIXME: This 'Lie' evades the check NFData constraint on 'withDeferrable'.
   -- I'm not sure how to go around this, so for now we just let it crash if it
   -- does occur.. :/
   -> Eff es (SymBool, Lie (Eff SymboliseEff [(Var, Arg)]))
-construct prim PluginAxiomsR { .. } program expr = inject @SymboliseEff $ withDeferrable do
+construct prim EmbeddingsR { .. } program expr = inject @SymboliseEff $ withDeferrable do
   prim' <- for prim \(bndr, rhs) -> do
     rhs' <- defer rhs
     pure (bndr, rhs')
@@ -207,7 +206,7 @@ checkValid
   => THNameToGHCName :> es
   => HasFamInstEnvs :> es
   => Provider_ Solver () :> es
-  => PluginAxiomsR
+  => EmbeddingsR
   -> CoreExpr
   -> Eff es (Maybe Counterexample)
 checkValid axioms expr = runBuiltInTypes do

From f6f62594454b23d82ec3c4977441ec055cf209ad Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Fri, 24 Jul 2026 16:25:08 +0200
Subject: [PATCH 3/7] 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.
 Implemented the term embeddings. TODO: Propagate the usage of these new
 embeddings to the symbolic evaluator!

---
 src/Pantomime.hs             |   1 -
 src/Pantomime/Axiom.hs       | 240 ++++++++---------------------------
 src/Pantomime/Passes.hs      |   1 +
 src/Pantomime/Unification.hs |  76 ++++++-----
 4 files changed, 97 insertions(+), 221 deletions(-)

diff --git a/src/Pantomime.hs b/src/Pantomime.hs
index 21d5ac0..29ea468 100644
--- a/src/Pantomime.hs
+++ b/src/Pantomime.hs
@@ -5,7 +5,6 @@ module Pantomime
 
   , Theory (..)
   , Embeddings (..)
-  , ArgType (..)
   , pantomime
   , pantomimeMarker
   , pantomimeNothing
diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 1f9e9d8..98d3caa 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE OverloadedStrings #-}
 
+-- TODO: We should probably rename this module to 'Embed' at some point, but the
+-- name is already taken by another module. Otherwise, 'Embedding' works. We'll
+-- phase 'Embed' out likely at some point though, so maybe we can switch then.
 module Pantomime.Axiom
   ( Embeddings (..)
-  , ArgType (..)
   , EmbeddingsR (..)
   , TypeAxiomsR
   , TermAxiomsR
@@ -12,7 +14,13 @@ module Pantomime.Axiom
 import Prelude hiding (break)
 import Language.Haskell.TH qualified as TH
 
-import GHC.Core.InstEnv (mkLocalClsInst, emptyInstEnv, extendInstEnv)
+import GHC.Core.InstEnv
+  ( InstEnvs (..)
+  , mkLocalClsInst
+  , emptyInstEnv
+  , extendInstEnv
+  , unionInstEnv
+  )
 import GHC.Core.TyCo.Rep (UnivCoProvenance (..), Coercion (..))
 import GHC.Core.TyCon.Env (TyConEnv)
 import GHC.Core.Unfold.Make (mkDFunUnfolding)
@@ -29,30 +37,23 @@ import GHC.Plugins
   , MonadUnique (..)
   , OverlapFlag (..)
   , OverlapMode (..)
-  , TyVar
-  , Unique
   , mkTyConTy
   , mkUnivCo
   , dataConWorkId
   , mkApps
-  , mkAppTy
+  , mkAppTys
   , mkTyVarTy
   , mkVarOccFS
-  , mkSystemName
-  , mkTyVar
   , classDataCon
   , typeKind
   , coercibleDataCon
   , generatedSrcSpan
   , setIdUnfolding
-  , splitFunTy_maybe
   , isTypeSynonymTyCon
-  , mkFastString
   , expandTypeSynonyms
   , splitTyConAppNoView_maybe
   , unitDataConId
   )
-import GHC.Tc.Utils.TcType (eqType)
 import GHC.Types.Id.Make (mkDictFunId)
 import GHC.Types.Name (mkInternalName)
 import GHC.Utils.Outputable
@@ -64,25 +65,17 @@ import GHC.Utils.Outputable
   , punctuate
   , comma
   , brackets
-  , parens
   )
 import GHC.Types.SourceText (SourceText(..))
-import GHC.Types.Unique (incrUnique, minLocalUnique)
 
-import Control.Monad ((>=>), unless)
+import Control.Monad ((>=>))
 
 import Data.Data (Data)
-import Data.Foldable (for_)
 import Data.Generics.Aliases (mkQ)
 import Data.Generics.Schemes (something)
-import Data.HashMap.Internal.Strict (HashMap)
-import Data.HashMap.Strict qualified as HashMap
-import Data.List (sort)
-import Data.Text (Text, unpack)
 import Data.Traversable (for)
 
 import Effectful
-import Effectful.Break (runBreak, break)
 import Effectful.Error.Static
 import Effectful.GHC.TH
 import Effectful.GHC.TyThing
@@ -91,7 +84,8 @@ import Effectful.Context
 
 import Pantomime.BuiltIn (Embeddable, Embedding (..))
 import Pantomime.Unification (subsumeExpr)
-import Pantomime.Util (foldM', dbg, failWith)
+import Pantomime.Util (foldM')
+import Effectful.GHC.External (HasInstEnvs, getInstEnvs)
 
 -- TODO: This should be renamed to 'Embeddings' instead of 'Axioms'. We can
 -- probably drop the 'Plugin' portion as well.
@@ -160,7 +154,7 @@ data Embeddings where
   Embeddings ::
     -- TODO: Probably want to remove the comment about fresh symbolic values
     -- once we change the interface on this.
-    { typeEmbeddings :: [(ArgType, ArgType)]
+    { typeEmbeddings :: [(TH.Name, TH.Name)]
     -- ^ Type-level embeddings.
     --
     -- Both the key and value of these mappings should be resolvable to a GHC
@@ -248,101 +242,6 @@ instance Monoid EmbeddingsR where
     , termAxiomsR = mempty
     }
 
--- | A restricted form of types used for user defined 'Embeddable' instances.
-data ArgType where
-  ATApp :: ArgType -> ArgType -> ArgType
-  ATCon :: TH.Name -> ArgType
-  ATVar :: Text -> ArgType -> ArgType
-  deriving (Show, Data)
-
-instance Outputable ArgType where
-  ppr = do
-    let go par = \case
-          ATApp fun arg -> par $ go id fun <+> go parens arg
-          ATCon con -> text $ show con
-          ATVar var _kind -> text $ unpack var
-    go id
-
--- | Variable store, used to track variable occurences and create new ones.
---
--- NOTE: As the uniques in the TyVar's are just incremented local Unique values,
--- we can get a deterministic order of their occurence by sorting based on the
--- Unique.
-type VarStore = (HashMap Text TyVar, Unique)
-
--- | Reify an 'ArgType' for a typeclass instance into a full Haskell type.
---
--- The 'Unique' on the 'TyVar' in the 'VarStore' can be sorted for a
--- deterministic declaration order for the type variables.
-reifyArgType
-  :: HasCallStack
-  => Error SDoc :> es
-  => Error (LookupError TH.Name) :> es
-  => Error (LookupError Name) :> es
-  => THNameToGHCName :> es
-  => HasThings :> es
-  => Context Reader [TyCon] :> es
-  => Context Writer VarStore :> es
-  => Context Reader VarStore :> es
-  => ArgType
-  -> Eff es Type
--- TODO: Fix call stack growth.
-reifyArgType = \case
-  ATApp fun arg -> do
-    -- Get function type and check if has a function kind.
-    fun' <- reifyArgType fun
-    let err = "Type application function does not have function kind."
-    (_, _, farg, _) <- failWith @SDoc err $ splitFunTy_maybe (typeKind fun')
-
-    -- Get the argument and check if its kind mathes the function argument.
-    arg' <- reifyArgType arg
-    unless (eqType farg $ typeKind arg') do
-      throwError_ @SDoc "Argument kind does not equal expected kind."
-
-    -- Return the application.
-    pure $ mkAppTy fun' arg'
-
-  ATCon name -> do
-    name' <- thNameToGhcName name
-    tc <- lookupTyConAll name'
-    pure $ mkTyConTy tc
-
-  ATVar name kind -> runBreak do
-    -- Fetch the variable store.
-    (mapping, unique) <- get @VarStore
-
-    -- Reify the kind of the variable.
-    kind' <- reifyArgType kind
-
-    -- Early break if we already have a type variable for the name.
-    let existing = HashMap.lookup name mapping
-    for_ existing \tv -> do
-      let kind2 = varType tv
-      unless (eqType kind' kind2) do
-        throwError_ @SDoc $ hcat
-          [ "Type variable '"
-          , text $ unpack name
-          , "' occurs with different kinds '"
-          , ppr kind'
-          , "' and '"
-          , ppr kind2
-          , "'"
-          ]
-      break $ mkTyVarTy tv
-
-    -- Create the fresh type variable.
-    let occ = mkFastString $ unpack name -- TODO: Not the best conversion...
-    let name' = mkSystemName unique $ mkVarOccFS occ
-    let tv = mkTyVar name' kind'
-
-    -- Extend the store with the type variable and increment the unique.
-    let mapping' = HashMap.insert name tv mapping
-    let unique' = incrUnique unique
-    put (mapping', unique')
-
-    -- Return the type variable.
-    pure $ mkTyVarTy tv
-
 -- | Finds a type synonym in a 'Type'.
 hasSynonym :: Type -> Maybe TyCon
 hasSynonym = something $ mkQ Nothing \ty -> do
@@ -354,7 +253,8 @@ hasSynonym = something $ mkQ Nothing \ty -> do
 --
 -- Throws an error if any type synonym still remains.
 expandTypeSynonyms'
-  :: Error SDoc :> es
+  :: HasCallStack
+  => Error SDoc :> es
   => Type
   -> Eff es Type
 expandTypeSynonyms' ty = do
@@ -386,14 +286,14 @@ expandTypeSynonyms' ty = do
 -- For these, we do not use any of the user-provided coercions.
 resolveEmbeddings
   :: HasCallStack
-  -- TODO: Adjust these errors!
-  => Error String :> es
+  -- TODO: Adjust the opaque SDoc error!
   => Error SDoc :> es
   => Error (LookupError TH.Name) :> es
   => Error (LookupError Name) :> es
   => THNameToGHCName :> es
   => HasThings :> es
   => HasUnique :> es
+  => HasInstEnvs :> es
   => Context Reader CoreProgram :> es
   => Context Reader [TyCon] :> es
   => Embeddings
@@ -404,49 +304,48 @@ resolveEmbeddings Embeddings { .. } = do
   embedding <- thNameToGhcName >=> lookupDataCon $ 'Embedding
 
   -- Gather the instance environment for resolution.
-  instEnv <- foldM' emptyInstEnv typeEmbeddings \instEnv (tyL, tyR) -> do
-    -- Reify the instance head into GHC Types.
-    let runReify = runContextLocal @VarStore (mempty, minLocalUnique)
-    ((tyL', tyR'), store') <- runReify do
-      tyL' <- reifyArgType tyL
-      tyR' <- reifyArgType tyR
-      pure (tyL', tyR')
+  typeEmbeddingsR <- foldM' emptyInstEnv typeEmbeddings \instEnv (tcL, tcR) -> do
+    let lookupTyConTH = thNameToGhcName >=> lookupTyConAll
+    tcL' <- lookupTyConTH tcL
+    tcR' <- lookupTyConTH tcR
 
-    -- Expand the type synonyms in the types.
-    tyL'' <- expandTypeSynonyms' tyL'
-    tyR'' <- expandTypeSynonyms' tyR'
+    -- FIXME: We should ensure that the kinds for the type match up, up to
+    -- runtime representation. This latter part is hard though...
 
-    -- FIXME: We should ensure that the kinds for the type match up
-    -- (up to runtime representation).
+    -- Type variables that we will use in the instance declaration.
+    let tvs = tyConTyVars tcL'
+
+    -- Apply the type variables to both type constructors and expand any type
+    -- synonyms.
+    let expand tc = do
+          let ty = mkAppTys (mkTyConTy tc) $ fmap mkTyVarTy tvs
+          expandTypeSynonyms' ty
+    tyL <- expand tcL'
+    tyR <- expand tcR'
 
     -- Gather the information to construct the coercion.
-    let prov = PluginProv "sym-fc embedding (user-defined)"
-    let kindL = typeKind tyL''
-    let kindR = typeKind tyR''
-    let co = mkUnivCo prov [] Representational tyL'' tyR''
+    let prov = PluginProv "SymFC embedding (user-defined)"
+    let kindL = typeKind tyL
+    let kindR = typeKind tyR
+    let co = mkUnivCo prov [] Representational tyL tyR
 
     -- Create a unique name for the embedding.
     unique <- getUniqueM
     let occ = mkVarOccFS "embedding"
     let name = mkInternalName unique occ generatedSrcSpan
 
-    -- Type variables used in the instance declaration.
-    -- NOTE: We can sort the type variables by Unique to get the declaration
-    -- order per 'reifyArgType'.
-    let tvs = sort $ HashMap.elems (fst store')
-
     -- We don't support typeclass requirements (not sure if we ever need them)?
     let theta = []
 
     -- Construct the initial 'DFunId', without unfolding.
-    let tys = [kindL, kindR, tyL'', tyR'']
+    let tys = [kindL, kindR, tyL, tyR]
     let dfun = mkDictFunId name tvs theta embeddable tys
 
     -- Create the 'Coercible' dictionary.
     let coercibleDict = mkApps (Var $ dataConWorkId coercibleDataCon)
           [ Type kindL
-          , Type tyL''
-          , Type tyR''
+          , Type tyL
+          , Type tyR
           , Coercion co
           ]
 
@@ -455,11 +354,11 @@ resolveEmbeddings Embeddings { .. } = do
     let embed = mkApps (Var $ dataConWorkId embedding)
           [ Type kindL
           , Type kindR
-          , Type tyL''
-          , Type tyR''
-          , Type tyR''
+          , Type tyL
+          , Type tyR
+          , Type tyR
           , Coercion coK
-          , Coercion $ Refl tyR''
+          , Coercion $ Refl tyR
           , coercibleDict
           ]
 
@@ -473,7 +372,7 @@ resolveEmbeddings Embeddings { .. } = do
     -- Create the 'DFunUnfolding'.
     let bndrs = []
     let dc = classDataCon embeddable
-    let args = [Type kindL, Type kindR, Type tyL'', Type tyR'', private, embed]
+    let args = [Type kindL, Type kindR, Type tyL, Type tyR, private, embed]
     let unfolding = mkDFunUnfolding bndrs dc args
 
     -- Set the unfolding of the 'DFunId'.
@@ -490,54 +389,25 @@ resolveEmbeddings Embeddings { .. } = do
     -- Extend the instance environment with the embedding.
     pure $ extendInstEnv instEnv inst
 
-  dbg instEnv
+  -- Construct the instance environment used for subsumption.
+  instEnvs <- getInstEnvs
+  let instEnvs' = instEnvs
+        { ie_local = unionInstEnv typeEmbeddingsR $ ie_local instEnvs
+        }
 
-  -- TODO: We should first ensure that termAxioms do not contain duplicate
+  -- TODO: We should first ensure that type embeddings and termAxioms do not contain duplicate
   -- definitions.
 
   -- Gather a binder mapping for a substitution. This will use the dictionary
   -- map to supply coercions to any Opaque values that require it.
-  _termAxiomsR <- for termEmbeddings \(orig, interp) -> do
+  _termEmbeddingsR <- for termEmbeddings \(orig, interp) -> do
     -- Resolve the names as identifiers.
     let resolve = thNameToGhcName >=> lookupIdAll
     orig' <- resolve orig
     interp' <- resolve interp
 
-    -- TODO: I'm not sure what to do with this. Should we just always resolve
-    -- using the embeddings?
-    -- -- Gather the expression of the interpretation.
-    -- -- TODO: Should we also attempt to get it from the local bindings?
-    -- expr <- case realIdUnfolding interp' of
-    --   CoreUnfolding { uf_tmpl } -> pure uf_tmpl
-    --   _ -> throwError_ ()
-
-    -- -- Check whether the original target can be interpreted.
-    -- dicts' <- case inl_inline $ idInlinePragma orig' of
-    --   -- Opaque values can be fully interpreted. Hence, we resolve any coercions
-    --   -- that were provided by the user.
-    --   Opaque _ -> pure dicts
-
-    --   -- We only want to interpret no-inline if the unfolding was not available.
-    --   NoInline _ | not . hasCoreUnfolding $ realIdUnfolding orig' -> do
-    --     pure emptyTM
-
-    --   -- It is fragile to interpret inlineable instances, as they may already
-    --   -- have been optimised away.
-    --   -- FIXME: It seems that the 'noinline' function has a NOINLINE pragma
-    --   -- but when testing it here, it doesn't. I feel like this test is the
-    --   -- correct one but it doesn't work in this case. I'll leave it like this
-    --   -- for now.
-    --   --
-    --   -- Actually, I ran into an issue where the function I wanted to call had
-    --   -- a NOINLINE on an inner value (that was not exported). Perhaps it still
-    --   -- makes sense to overwrite definitions, even if they can be inlined? I
-    --   -- guess it is still pretty fragile...
-    --   -- _ -> throwError_ ()
-    --   _ -> pure emptyTM
-
     -- Check whether the interpretation matches.
-    let dicts = undefined
-    expr' <- subsumeExpr dicts (Var interp') $ varType orig'
+    expr' <- subsumeExpr instEnvs' (Var interp') $ varType orig'
 
     -- Return the mapping.
     pure (orig', expr')
diff --git a/src/Pantomime/Passes.hs b/src/Pantomime/Passes.hs
index 9c08a8a..51431e0 100644
--- a/src/Pantomime/Passes.hs
+++ b/src/Pantomime/Passes.hs
@@ -212,6 +212,7 @@ checkValidityAndEmbed
      , Context Reader [TyCon] :> es
      , Provider_ Solver () :> es
      , HasFamInstEnvs :> es
+     , HasInstEnvs :> es
      , HasThings :> es
      , HasUnique :> es
      , THNameToGHCName :> es
diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs
index 1462c3b..5c6ff5f 100644
--- a/src/Pantomime/Unification.hs
+++ b/src/Pantomime/Unification.hs
@@ -4,16 +4,15 @@
 -- naming from GHC.
 -- TODO: Add module docs.
 module Pantomime.Unification
-  ( UnificationError (..),
-    OversaturatedError (..),
-    unifyApp,
-    unifyApps,
-    unifyExprs,
-    resolveInstances,
-    resolveInstancesWith,
-    subsumeExpr,
-  )
-where
+  ( UnificationError (..)
+  , OversaturatedError (..)
+  , unifyApp
+  , unifyApps
+  , unifyExprs
+  , resolveInstances
+  , resolveInstancesWith
+  , subsumeExpr
+  ) where
 
 import Control.Applicative (Alternative ((<|>)))
 import Control.Error (LookupError (..))
@@ -26,7 +25,7 @@ import Effectful.Context
 import Effectful.Error.Static
 import Effectful.GHC.External (HasInstEnvs, lookupUniqueInst)
 import GHC.Core.Class (Class)
-import GHC.Core.InstEnv (instanceDFunId)
+import GHC.Core.InstEnv (InstEnvs, instanceDFunId, lookupUniqueInstEnv)
 import GHC.Core.Map.Type (TypeMap)
 import GHC.Core.Predicate (isEvVar)
 import GHC.Core.TyCo.Rep (Scaled (..), Type (..), scaledThing)
@@ -34,7 +33,7 @@ import GHC.Core.Unify (alwaysBindFun, tcMatchTy, tcUnifyTys)
 import GHC.Data.Maybe (rightToMaybe, whenIsJust)
 import GHC.Data.TrieMap (TrieMap (..), insertTM)
 import GHC.Plugins hiding ((<>))
-import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy)
+import GHC.Tc.Utils.TcType (substTy, tcSplitSigmaTy, tcSplitDFunHead)
 import Lens.Micro
 import Lens.Micro.Extras (view)
 import Pantomime.Util
@@ -387,26 +386,27 @@ unifyExprs lhs rhs = do
 -- TODO: Using 'TypeMap CoreExpr' for instances is extremely fragile. It would
 -- be a lot better to use InstEnv to resolve typeclasses. This goes for other
 -- functions in this module as well!
-subsumeExpr ::
-  (HasCallStack) =>
-  (Error String :> es) =>
-  TypeMap CoreExpr ->
-  CoreExpr ->
-  Type ->
-  Eff es CoreExpr
-subsumeExpr dicts expr ty = do
+subsumeExpr
+  :: HasCallStack
+  => Error SDoc :> es
+  => InstEnvs
+  -> CoreExpr
+  -> Type
+  -> Eff es CoreExpr
+subsumeExpr insts expr ty = do
   -- Get the unifiable part of the type.
   let (curTv, curEv, curTy) = splitExprTy expr
   let (reqTv, reqEv, reqTy) = tcSplitSigmaTy ty
 
   -- Match the types and add all dictionaries we care about.
-  let err =
-        "subsumeExpr: type matching failed"
-          <> "\n  current type:  "
-          <> showSDocUnsafe (ppr curTy)
-          <> "\n  required type: "
-          <> showSDocUnsafe (ppr reqTy)
-  subst <- failWith err $ tcMatchTy curTy reqTy
+  let err = hcat
+        [ "Could not match '"
+        , ppr curTy
+        , "' to the required type '"
+        , ppr reqTy
+        , "'."
+        ]
+  subst <- failWith @SDoc err $ tcMatchTy curTy reqTy
 
   -- Make evidence variables.
   let names = ("dict",) . unrestricted <$> reqEv
@@ -414,15 +414,21 @@ subsumeExpr dicts expr ty = do
 
   -- Construct the arguments to supply to the expression to unify.
   let argsTv = substTy subst . mkTyVarTy <$> curTv
-  let dicts' = foldlBy dicts lamEv \acc ev -> do
-        insertTM (varType ev) (Var ev) acc
+  let dicts = foldlBy emptyTM lamEv \acc ev -> do
+        insertTM @TypeMap (varType ev) ev acc
   let curEv' = substTy subst <$> curEv
-  argsEv <- for curEv' \ev -> do
-    let err' =
-          "subsumeExpr: type variable instance not found in dictionary"
-            <> "\n  type: "
-            <> showSDocUnsafe (ppr ev)
-    failWith @String err' $ lookupTM ev dicts'
+  argsEv <- for curEv' \ev -> runBreak do
+    whenIsJust (lookupTM ev dicts) $ break . Var @CoreBndr
+
+    let (cls, args) = tcSplitDFunHead ev
+    case lookupUniqueInstEnv insts cls args of
+      Right (inst, targs) -> pure $ mkTyApps (Var $ instanceDFunId inst) targs
+      -- TODO: Improve error message!
+      Left _err -> throwError_ @SDoc $ hcat
+        [ "Instance lookup of typeclass '"
+        , ppr ev
+        , "' failed when subsuming expression."
+        ]
 
   -- Construct the new expression.
   let open = mkApps expr $ fmap Type argsTv <> argsEv

From bf5f4a4c29241a272aeede56073bdd387d4ff129 Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Mon, 27 Jul 2026 13:30:37 +0200
Subject: [PATCH 4/7] Added some comments to changes in expression subsumption.

---
 src/Pantomime/Axiom.hs       | 4 ++--
 src/Pantomime/Unification.hs | 7 ++++++-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 98d3caa..16da7e4 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -395,8 +395,8 @@ resolveEmbeddings Embeddings { .. } = do
         { ie_local = unionInstEnv typeEmbeddingsR $ ie_local instEnvs
         }
 
-  -- TODO: We should first ensure that type embeddings and termAxioms do not contain duplicate
-  -- definitions.
+  -- TODO: We should ensure that type embeddings and termAxioms do not
+  -- contain duplicate definitions.
 
   -- Gather a binder mapping for a substitution. This will use the dictionary
   -- map to supply coercions to any Opaque values that require it.
diff --git a/src/Pantomime/Unification.hs b/src/Pantomime/Unification.hs
index 5c6ff5f..603ef12 100644
--- a/src/Pantomime/Unification.hs
+++ b/src/Pantomime/Unification.hs
@@ -412,14 +412,19 @@ subsumeExpr insts expr ty = do
   let names = ("dict",) . unrestricted <$> reqEv
   let (lamEv, _) = freshIds names $ mkInScopeSetList reqTv
 
-  -- Construct the arguments to supply to the expression to unify.
+  -- Construct the local arguments to supply to the expression to unify.
   let argsTv = substTy subst . mkTyVarTy <$> curTv
   let dicts = foldlBy emptyTM lamEv \acc ev -> do
         insertTM @TypeMap (varType ev) ev acc
+
+  -- Get the required typeclasses.
   let curEv' = substTy subst <$> curEv
   argsEv <- for curEv' \ev -> runBreak do
+    -- First try to find a local instance that is supplied to the function.
     whenIsJust (lookupTM ev dicts) $ break . Var @CoreBndr
 
+    -- If no local instance exists, try to resolve the through the instance
+    -- environment.
     let (cls, args) = tcSplitDFunHead ev
     case lookupUniqueInstEnv insts cls args of
       Right (inst, targs) -> pure $ mkTyApps (Var $ instanceDFunId inst) targs

From cb002b2c0549c887404123ae646029ee6dd151ca Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Wed, 29 Jul 2026 12:47:56 +0200
Subject: [PATCH 5/7] Adjusted fresh variable instantiation to use the new
 embeddings. Bugfixed the 'Embedding' datatype instance, which got the wrong
 coercion.

---
 src/Pantomime/Axiom.hs   | 91 +++++++++++++++++++++++-----------------
 src/Pantomime/Binding.hs |  3 +-
 src/Pantomime/Fresh.hs   | 48 ++++++++++-----------
 src/Pantomime/Literal.hs |  4 +-
 src/Pantomime/Solve.hs   | 18 +++++---
 5 files changed, 90 insertions(+), 74 deletions(-)

diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 16da7e4..8844473 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -6,8 +6,8 @@
 module Pantomime.Axiom
   ( Embeddings (..)
   , EmbeddingsR (..)
-  , TypeAxiomsR
-  , TermAxiomsR
+  , TypeEmbeddingsR
+  , TermEmbeddingsR
   , resolveEmbeddings
   ) where
 
@@ -16,13 +16,13 @@ import Language.Haskell.TH qualified as TH
 
 import GHC.Core.InstEnv
   ( InstEnvs (..)
+  , InstEnv
   , mkLocalClsInst
   , emptyInstEnv
   , extendInstEnv
   , unionInstEnv
   )
-import GHC.Core.TyCo.Rep (UnivCoProvenance (..), Coercion (..))
-import GHC.Core.TyCon.Env (TyConEnv)
+import GHC.Core.TyCo.Rep (UnivCoProvenance (..))
 import GHC.Core.Unfold.Make (mkDFunUnfolding)
 import GHC.Plugins
   ( TyCon (..)
@@ -44,6 +44,8 @@ import GHC.Plugins
   , mkAppTys
   , mkTyVarTy
   , mkVarOccFS
+  , mkGReflRightCo
+  , mkCastTy
   , classDataCon
   , typeKind
   , coercibleDataCon
@@ -77,6 +79,7 @@ import Data.Traversable (for)
 
 import Effectful
 import Effectful.Error.Static
+import Effectful.GHC.External (HasInstEnvs, getInstEnvs)
 import Effectful.GHC.TH
 import Effectful.GHC.TyThing
 import Effectful.GHC.Unique (HasUnique)
@@ -85,7 +88,6 @@ import Effectful.Context
 import Pantomime.BuiltIn (Embeddable, Embedding (..))
 import Pantomime.Unification (subsumeExpr)
 import Pantomime.Util (foldM')
-import Effectful.GHC.External (HasInstEnvs, getInstEnvs)
 
 -- TODO: This should be renamed to 'Embeddings' instead of 'Axioms'. We can
 -- probably drop the 'Plugin' portion as well.
@@ -203,19 +205,19 @@ instance Monoid Embeddings where
     , termEmbeddings = mempty
     }
 
-type TypeAxiomsR = TyConEnv TyCon
+type TypeEmbeddingsR = InstEnv
 
 -- TODO: I guess these might be better suited as CoreBind no?
-type TermAxiomsR = [(Id, CoreExpr)]
+type TermEmbeddingsR = [(Id, CoreExpr)]
 
 -- TODO: I think it would be good to have type synonyms for both of these fields
 -- as we use them independently as well.
 -- | Fully resolved plugin axioms. These may be used as-is by the solver.
 data EmbeddingsR where
   EmbeddingsR ::
-    { typeAxiomsR :: TypeAxiomsR
+    { typeEmbeddingsR :: TypeEmbeddingsR
     -- ^ Type-level axioms, mainly used to construct symbolic values.
-    , termAxiomsR :: TermAxiomsR
+    , termEmbeddingsR :: TermEmbeddingsR
     -- ^ Term-level axioms, these already have their 'Coercible' instances
     -- resolved by the type-axioms, where applicable.
     --
@@ -224,24 +226,25 @@ data EmbeddingsR where
 
 instance Outputable EmbeddingsR where
   ppr EmbeddingsR { .. } = hang "EmbeddingsR" 2 $ vcat
-    [ hang "Type Embeddings:" 2 $ ppr typeAxiomsR
-    , hang "Term Embeddings:" 2 $ ppr termAxiomsR
+    [ hang "Type Embeddings:" 2 $ ppr typeEmbeddingsR
+    , hang "Term Embeddings:" 2 $ ppr termEmbeddingsR
     ]
 
 instance Semigroup EmbeddingsR where
   (<>) l r = EmbeddingsR
-    -- { typeAxiomsR = unionInstEnv (typeAxiomsR l) (typeAxiomsR r)
-    { typeAxiomsR = typeAxiomsR l <> typeAxiomsR r
-    , termAxiomsR = termAxiomsR l <> termAxiomsR r
+    { typeEmbeddingsR = unionInstEnv (typeEmbeddingsR l) (typeEmbeddingsR r)
+    , termEmbeddingsR = termEmbeddingsR l <> termEmbeddingsR r
     }
 
 instance Monoid EmbeddingsR where
   mempty = EmbeddingsR
-    -- { typeAxiomsR = emptyInstEnv
-    { typeAxiomsR = mempty
-    , termAxiomsR = mempty
+    { typeEmbeddingsR = emptyInstEnv
+    , termEmbeddingsR = mempty
     }
 
+-- TODO: I guess we should change this to 'isValidHeadArg' or something. Then
+-- check if there are not any quantifiers or typeclass constraints in there, as
+-- these are also disallowed!
 -- | Finds a type synonym in a 'Type'.
 hasSynonym :: Type -> Maybe TyCon
 hasSynonym = something $ mkQ Nothing \ty -> do
@@ -313,6 +316,12 @@ resolveEmbeddings Embeddings { .. } = do
     -- runtime representation. This latter part is hard though...
 
     -- Type variables that we will use in the instance declaration.
+    -- TODO: Should there be a functional dependency from the left type to
+    -- the right? I think yes: the left type should uniquely identify the rhs
+    -- (otherwise, the embedding is ambiguous). Would this change what we do
+    -- here? I think the way we instantiate the type variables here, you always
+    -- get the function dependency (unless there is an overlapping instance
+    -- perhaps?)
     let tvs = tyConTyVars tcL'
 
     -- Apply the type variables to both type constructors and expand any type
@@ -323,42 +332,36 @@ resolveEmbeddings Embeddings { .. } = do
     tyL <- expand tcL'
     tyR <- expand tcR'
 
-    -- Gather the information to construct the coercion.
+    -- Construct the kind coercion used to create the 'Embedding' instance.
     let prov = PluginProv "SymFC embedding (user-defined)"
     let kindL = typeKind tyL
     let kindR = typeKind tyR
-    let co = mkUnivCo prov [] Representational tyL tyR
-
-    -- Create a unique name for the embedding.
-    unique <- getUniqueM
-    let occ = mkVarOccFS "embedding"
-    let name = mkInternalName unique occ generatedSrcSpan
+    let coK = mkUnivCo prov [] Nominal kindR kindL
 
-    -- We don't support typeclass requirements (not sure if we ever need them)?
-    let theta = []
+    -- Use the coercion to make a version of the right-hand side that has the
+    -- same kind as the left-hand side.
+    let tyR' = mkCastTy tyR coK
 
-    -- Construct the initial 'DFunId', without unfolding.
-    let tys = [kindL, kindR, tyL, tyR]
-    let dfun = mkDictFunId name tvs theta embeddable tys
+    -- Construct the type coercion that will be exposed by `Coercible`.
+    let co = mkUnivCo prov [] Representational tyL tyR'
 
     -- Create the 'Coercible' dictionary.
     let coercibleDict = mkApps (Var $ dataConWorkId coercibleDataCon)
           [ Type kindL
           , Type tyL
-          , Type tyR
+          , Type tyR'
           , Coercion co
           ]
 
     -- Create the 'Embedding' data type.
-    let coK = mkUnivCo prov [] Nominal kindL kindR
     let embed = mkApps (Var $ dataConWorkId embedding)
           [ Type kindL
           , Type kindR
           , Type tyL
           , Type tyR
-          , Type tyR
+          , Type tyR'
           , Coercion coK
-          , Coercion $ Refl tyR
+          , Coercion $ mkGReflRightCo Nominal tyR coK
           , coercibleDict
           ]
 
@@ -375,6 +378,16 @@ resolveEmbeddings Embeddings { .. } = do
     let args = [Type kindL, Type kindR, Type tyL, Type tyR, private, embed]
     let unfolding = mkDFunUnfolding bndrs dc args
 
+    -- Create a unique name for the embedding.
+    unique <- getUniqueM
+    let occ = mkVarOccFS "embedding"
+    let name = mkInternalName unique occ generatedSrcSpan
+
+    -- Construct the initial 'DFunId', without unfolding.
+    let theta = [] -- No typeclass requirements in embeddings
+    let tys = [kindL, kindR, tyL, tyR']
+    let dfun = mkDictFunId name tvs theta embeddable tys
+
     -- Set the unfolding of the 'DFunId'.
     let dfun' = setIdUnfolding dfun unfolding
 
@@ -400,11 +413,11 @@ resolveEmbeddings Embeddings { .. } = do
 
   -- Gather a binder mapping for a substitution. This will use the dictionary
   -- map to supply coercions to any Opaque values that require it.
-  _termEmbeddingsR <- for termEmbeddings \(orig, interp) -> do
+  termEmbeddingsR <- for termEmbeddings \(orig, interp) -> do
     -- Resolve the names as identifiers.
-    let resolve = thNameToGhcName >=> lookupIdAll
-    orig' <- resolve orig
-    interp' <- resolve interp
+    let lookupIdTH = thNameToGhcName >=> lookupIdAll
+    orig' <- lookupIdTH orig
+    interp' <- lookupIdTH interp
 
     -- Check whether the interpretation matches.
     expr' <- subsumeExpr instEnvs' (Var interp') $ varType orig'
@@ -414,6 +427,6 @@ resolveEmbeddings Embeddings { .. } = do
 
   -- Collect the resolved type and term mappings.
   pure EmbeddingsR
-    { typeAxiomsR = mempty
-    , termAxiomsR = mempty
+    { typeEmbeddingsR
+    , termEmbeddingsR
     }
diff --git a/src/Pantomime/Binding.hs b/src/Pantomime/Binding.hs
index e4ad7e7..a4c28ac 100644
--- a/src/Pantomime/Binding.hs
+++ b/src/Pantomime/Binding.hs
@@ -14,7 +14,7 @@ import Control.Monad ((>=>))
 import Data.Traversable (for)
 import Effectful
 import Effectful.Error.Static
-import Effectful.GHC.TyThing (HasThings, lookupTyCon, lookupId)
+import Effectful.GHC.TyThing (HasThings, lookupTyCon, lookupId, lookupClass)
 import Effectful.GHC.TH (THNameToGHCName, thNameToGhcName)
 import GHC.Plugins (Name, Var, Id)
 import GHC.TypeNats qualified as Builtin (type (<=))
@@ -100,6 +100,7 @@ getBuiltinTyCon = do
   tcKnownNat <- thNameToTyCon ''Builtin.KnownNat
   tcLEqNat <- thNameToTyCon ''(Builtin.<=)
   tcUnsafeEquality <- thNameToTyCon ''Builtin.UnsafeEquality
+  clsEmbeddable <- (thNameToGhcName >=> lookupClass) ''Builtin.Embeddable
   pure BuiltInTyCon { .. }
 
 bindingsTH :: [(TH.Name, forall es. PrimOp es)]
diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs
index e5c5054..28beb90 100644
--- a/src/Pantomime/Fresh.hs
+++ b/src/Pantomime/Fresh.hs
@@ -1,22 +1,20 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Pantomime.Fresh
-  ( FreshInstEnv (..)
-  , freshArgs
+  ( freshArgs
   ) where
 
-import GHC.Builtin.Types.Prim (eqPrimTyCon, eqReprPrimTyCon)
-import GHC.Core.FamInstEnv (topReduceTyFamApp_maybe, FamInstEnvs)
+import GHC.Builtin.Types.Prim (eqPrimTyCon, eqReprPrimTyCon, alphaTy)
+import GHC.Core.FamInstEnv (FamInstEnvs, topReduceTyFamApp_maybe)
+import GHC.Core.InstEnv (InstEnvs (..), lookupUniqueInstEnv, unionInstEnv)
 import GHC.Core.Reduction (Reduction (..), mkReduction, homogeniseHetRedn)
 import GHC.Core.TyCo.Rep (scaledThing, UnivCoProvenance (..))
-import GHC.Core.TyCon.Env (TyConEnv, lookupTyConEnv)
 import GHC.Core.Unify (tcUnifyTysFG, alwaysBindFun, UnifyResultM (..))
 import GHC.Types.Unique (Uniquable (..), getKey)
 import GHC.Utils.Outputable (Outputable (..), text, (<+>), showSDocUnsafe)
 import GHC.Plugins qualified as GHC
 import GHC.Plugins
   ( Var
-  , TyCon
   , Name
   , DataCon
   , InScopeSet
@@ -33,9 +31,7 @@ import GHC.Plugins
   , splitTyConApp_maybe
   , tyConFamilySize
   , tyVarKind
-  , mkTyConTy
   , mkUnivCo
-  , mkAppCos
   , mkReflCo
   , mkSymCo
   , mkSubCo
@@ -62,11 +58,11 @@ import Data.Constraint (Dict (..))
 import Data.Text.Encoding (decodeUtf8)
 import Data.Traversable (for)
 
-import Pantomime.Axiom (TypeAxiomsR)
+import Pantomime.Axiom (TypeEmbeddingsR)
 import Pantomime.Defer (Deferrable, defer)
 import Pantomime.Expr
 import Pantomime.Literal
-  ( BuiltInTyCon
+  ( BuiltInTyCon (..)
   , SomeLiteralType (..)
   , HasDict (..)
   , projectLitTy
@@ -77,11 +73,6 @@ import Effectful
 import Effectful.Error.Static
 import Effectful.Context (Context, ContextMode (..), get)
 
-data FreshInstEnv where
-  FreshInstEnv ::
-    { fieUser :: TyConEnv TyCon
-    } -> FreshInstEnv
-
 data Variable where
   Variable ::
     { varName :: Name
@@ -161,16 +152,22 @@ freshExpr
   => Deferrable es
   => Error String :> es
   => Context Reader FamInstEnvs :> es
+  => Context Reader InstEnvs :> es
   => Context Reader BuiltInTyCon :> es
-  => TyConEnv TyCon
+  => TypeEmbeddingsR
   -> Var
   -> Eval es Expr
-freshExpr axioms root = do
+freshExpr embeddings root = do
   -- TODO: Is it better to this lookup once? Whilst it is a reader-like effect,
   -- it is implemented through IO, so I'm a bit wary of running it in a hot loop
   -- like this one. The only way to know is just to profile I guess, but for now
   -- I'll put it outside.
   fam <- liftEff $ get @FamInstEnvs
+  instEnvs <- liftEff $ get @InstEnvs
+  let instEnvs' = instEnvs
+        { ie_local = unionInstEnv embeddings $ ie_local instEnvs
+        }
+  BuiltInTyCon { clsEmbeddable } <- liftEff $ get @BuiltInTyCon
   -- TODO: Add note on callstack and recursion
   -- TODO: I don't like the nesting this gives. Maybe we should move these
   -- definitions inwards somehow. Perhaps just a standalone helper definition?
@@ -218,14 +215,10 @@ freshExpr axioms root = do
 
           -- User Interpretation:
           -----------------------
-          | Just (tc, args) <- splitTyConApp_maybe ty
-          , Just tc' <- lookupTyConEnv axioms tc -> do
+          | Right (_inst, [tyL, tyR]) <- lookupUniqueInstEnv instEnvs' clsEmbeddable [ty, alphaTy] -> do
             -- Construct the plugin coercion
-            let prov = PluginProv "pantomime user-defined"
-            let tyL = mkTyConTy tc
-            let tyR = mkTyConTy tc'
-            let univ = mkUnivCo prov [] Representational tyL tyR
-            let co = mkAppCos univ $ mkReflCo Nominal <$> args
+            let prov = PluginProv "SymFC embedding (user-defined)"
+            let co = mkUnivCo prov [] Representational tyL tyR
 
             -- Create the final expression.
             mkReductionCast $ mkReduction co (coercionRKind co)
@@ -400,12 +393,13 @@ freshArgs
   => Error String :> es
   => Context Reader BuiltInTyCon :> es
   => Context Reader FamInstEnvs :> es
-  => TypeAxiomsR
+  => Context Reader InstEnvs :> es
+  => TypeEmbeddingsR
   -> [String]
   -> Type
   -> InScopeSet
   -> Eff es ([(Var, Arg)], InScopeSet)
-freshArgs axioms valNames ty scope0 = do
+freshArgs embeddings valNames ty scope0 = do
   -- Gather the argument types.
   let (tyVars, funTy) = splitForAllTyVars ty
   let (argTys, _resTy) = splitFunTys funTy
@@ -425,7 +419,7 @@ freshArgs axioms valNames ty scope0 = do
   let args = tyArgs <> valArgs
 
   -- Create symbolic instance of the arguments.
-  symbolic <- for args $ defer . freshExpr axioms
+  symbolic <- for args $ defer . freshExpr embeddings
 
   -- Zip the binders together with their symbolic instance.
   let binders = zip args symbolic
diff --git a/src/Pantomime/Literal.hs b/src/Pantomime/Literal.hs
index d5d2f16..1d172e0 100644
--- a/src/Pantomime/Literal.hs
+++ b/src/Pantomime/Literal.hs
@@ -27,7 +27,7 @@ module Pantomime.Literal
 import Control.Applicative (Alternative(..))
 import Control.Monad ((>=>))
 
-import Data.Constraint
+import Data.Constraint (Dict (..), HasDict (..), withDict)
 import Data.Functor.Identity (Identity(..))
 import Data.Maybe (isJust)
 import Data.Proxy (Proxy(..))
@@ -37,6 +37,7 @@ import Effectful
 import Effectful.Context
 import Effectful.Error.Static
 
+import GHC.Core.Class (Class)
 import GHC.Core.Reduction (Reduction(..))
 import GHC.Core.FamInstEnv (normaliseType, FamInstEnvs)
 import GHC.Plugins
@@ -306,6 +307,7 @@ data BuiltInTyCon where
     , tcKnownNat :: TyCon
     , tcLEqNat :: TyCon
     , tcUnsafeEquality :: TyCon
+    , clsEmbeddable :: Class
     } -> BuiltInTyCon
 
 -- | Convert a 'LiteralType' into a Haskell 'Type'.
diff --git a/src/Pantomime/Solve.hs b/src/Pantomime/Solve.hs
index 2e2f298..5672354 100644
--- a/src/Pantomime/Solve.hs
+++ b/src/Pantomime/Solve.hs
@@ -89,6 +89,7 @@ import Effectful.GHC.External
 import Effectful.Grisette.Solver
 import Effectful.Provider
 import Effectful.Exception (ErrorCall (..), throwIO)
+import GHC.Core.InstEnv (InstEnvs)
 
 -- TODO: Definitely not the cleanest place to add these effects. I should look
 -- into where to do this.
@@ -96,21 +97,24 @@ runBuiltInTypes
   :: Error (LookupError TH.Name) :> es
   => Error (LookupError Name) :> es
   => HasThings :> es
-  => THNameToGHCName :> es
   => HasFamInstEnvs :> es
-  => Eff (Context Reader BuiltInTyCon : Context Reader InterfaceThings : Context Reader FamInstEnvs : es) a
+  => HasInstEnvs :> es
+  => THNameToGHCName :> es
+  => Eff (Context Reader BuiltInTyCon : Context Reader InterfaceThings : Context Reader FamInstEnvs : Context Reader InstEnvs : es) a
   -> Eff es a
 runBuiltInTypes eff = do
   tys <- getBuiltinTyCon
   ids <- getInterfaceThings
   fam <- getFamInstEnvs
-  runContextReader fam . runContextReader ids . runContextReader tys $ eff
+  env <- getInstEnvs
+  runContextReader env . runContextReader fam . runContextReader ids . runContextReader tys $ eff
 
 type SymboliseEff =
   [ Context Reader BuiltInTyCon
   , Context Reader InterfaceThings
   , Context Reader FamInstEnvs
   , Error String
+  , Context Reader InstEnvs
   ]
 
 newtype Lie a where
@@ -126,6 +130,7 @@ construct
   => Context Reader InterfaceThings :> es
   => Context Reader FamInstEnvs :> es
   => Error String :> es
+  => Context Reader InstEnvs :> es
   => [(Var, forall fs. PrimOp fs)]
   -> EmbeddingsR
   -> CoreProgram
@@ -143,7 +148,7 @@ construct prim EmbeddingsR { .. } program expr = inject @SymboliseEff $ withDefe
   subst0 <- extendIdSubstMany mkEmptySubst prim'
 
   -- Add the term bindings to the substitution.
-  let termAxiomsR' = uncurry NonRec <$> termAxiomsR
+  let termAxiomsR' = uncurry NonRec <$> termEmbeddingsR
   subst1 <- symboliseBindMany subst0 termAxiomsR'
 
   -- TODO: I think there is an ordering problem here between user
@@ -158,7 +163,7 @@ construct prim EmbeddingsR { .. } program expr = inject @SymboliseEff $ withDefe
 
   -- Create fresh arguments.
   let ty = exprType expr
-  (args, _scope) <- freshArgs typeAxiomsR (collectValBinders expr) ty emptyInScopeSet
+  (args, _scope) <- freshArgs typeEmbeddingsR (collectValBinders expr) ty emptyInScopeSet
 
   result <- defer do
     fun <- symbolise subst expr
@@ -202,6 +207,7 @@ checkValid
   => Error (LookupError Name) :> es
   => Error SolverError :> es
   => Context Reader CoreProgram :> es
+  => HasInstEnvs :> es
   => HasThings :> es
   => THNameToGHCName :> es
   => HasFamInstEnvs :> es
@@ -218,7 +224,7 @@ checkValid axioms expr = runBuiltInTypes do
   -- TODO: Is there perhaps a better place to add this? Ideally we just do it
   -- as a normal axiom, but I cannot find where 'nospec' is defined...
   idId <- thNameToGhcName 'id >>= lookupIdAll
-  let axioms' = axioms { termAxiomsR = (nospecId, GHC.Var idId) : termAxiomsR axioms } 
+  let axioms' = axioms { termEmbeddingsR = (nospecId, GHC.Var idId) : termEmbeddingsR axioms } 
 
   (eq, Lie args) <- construct prim axioms' program expr
 

From 2297f5fa44dc7ca1ee99197e44ffef0b1d4ae139 Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Thu, 30 Jul 2026 14:28:52 +0200
Subject: [PATCH 6/7] 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 in to
 the class being non-symmetric. Though the coercion is symmetric, the
 direction of the embedding is not!

---
 src/Pantomime/Axiom.hs   | 25 ++++++++++++++++---------
 src/Pantomime/BuiltIn.hs | 12 +++++++++++-
 src/Pantomime/Fresh.hs   | 29 +++++++++++++++++++++++------
 3 files changed, 50 insertions(+), 16 deletions(-)

diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 8844473..627c051 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -78,12 +78,12 @@ import Data.Generics.Schemes (something)
 import Data.Traversable (for)
 
 import Effectful
+import Effectful.Context
 import Effectful.Error.Static
 import Effectful.GHC.External (HasInstEnvs, getInstEnvs)
 import Effectful.GHC.TH
 import Effectful.GHC.TyThing
 import Effectful.GHC.Unique (HasUnique)
-import Effectful.Context
 
 import Pantomime.BuiltIn (Embeddable, Embedding (..))
 import Pantomime.Unification (subsumeExpr)
@@ -315,19 +315,22 @@ resolveEmbeddings Embeddings { .. } = do
     -- FIXME: We should ensure that the kinds for the type match up, up to
     -- runtime representation. This latter part is hard though...
 
+    -- TODO: There is a note in GHC that says the type variables in instance
+    -- declarations should be completely fresh. I don't think the type variables
+    -- on a TyCon are? If yes, this should be fine. If not, we should swap out
+    -- their 'Unique'.
     -- Type variables that we will use in the instance declaration.
-    -- TODO: Should there be a functional dependency from the left type to
-    -- the right? I think yes: the left type should uniquely identify the rhs
-    -- (otherwise, the embedding is ambiguous). Would this change what we do
-    -- here? I think the way we instantiate the type variables here, you always
-    -- get the function dependency (unless there is an overlapping instance
-    -- perhaps?)
-    let tvs = tyConTyVars tcL'
+    let tvs = case isTypeSynonymTyCon tcL' of
+          True -> tyConTyVars tcL'
+          False -> []
 
     -- Apply the type variables to both type constructors and expand any type
     -- synonyms.
     let expand tc = do
           let ty = mkAppTys (mkTyConTy tc) $ fmap mkTyVarTy tvs
+          -- TODO: Should we ensure that the expansion is actually only a
+          -- newtype or data declaration? I think yes. In fact, we should also
+          -- disallow quantifiers and typeclass requirements in this type!
           expandTypeSynonyms' ty
     tyL <- expand tcL'
     tyR <- expand tcR'
@@ -385,7 +388,7 @@ resolveEmbeddings Embeddings { .. } = do
 
     -- Construct the initial 'DFunId', without unfolding.
     let theta = [] -- No typeclass requirements in embeddings
-    let tys = [kindL, kindR, tyL, tyR']
+    let tys = [kindL, kindR, tyL, tyR]
     let dfun = mkDictFunId name tvs theta embeddable tys
 
     -- Set the unfolding of the 'DFunId'.
@@ -399,6 +402,10 @@ resolveEmbeddings Embeddings { .. } = do
     let warn = Nothing
     let inst = mkLocalClsInst dfun' overlap tvs embeddable tys warn
 
+    -- TODO: We should check whether the function dependency is being upheld.
+    -- We can do so with the function 'checkFundeps' from
+    -- 'GHC.Tc.Instance.FunDeps'
+
     -- Extend the instance environment with the embedding.
     pure $ extendInstEnv instEnv inst
 
diff --git a/src/Pantomime/BuiltIn.hs b/src/Pantomime/BuiltIn.hs
index 9d08d45..c4acc04 100644
--- a/src/Pantomime/BuiltIn.hs
+++ b/src/Pantomime/BuiltIn.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
@@ -269,13 +270,22 @@ class PrivateEmbeddable
 -- are only safe under symbolic evaluation given a coherent set of embeddings.
 --
 -- Of course, a user is free to construct an instance for a homogenous coercion.
-class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2) where
+--
+-- Unlike 'Coercible', 'Embeddable' is not symmetric. The first type argument is
+-- the source type (i.e. the type to embed) and the second type argument is the
+-- destination type (i.e. the interpretation).
+class PrivateEmbeddable => Embeddable (a :: k1) (b :: k2) | a -> b where
   -- | Get the 'Embedding' instance of the typeclass.
   --
   -- We expose 'embedding' as it keeps the kind arguments invisible, which is
   -- more ergonomic.
   embedding' :: Embedding a b
 
+-- Instance to allow resolution of embeddings with more type saturation than
+-- strictly required.
+instance (PrivateEmbeddable, Embeddable a b) => Embeddable (a c) (b c) where
+  embedding' = case embedding @a of Embedding -> Embedding
+
 -- | Get the 'Embedding' instance of the typeclass.
 embedding
   :: forall {k1} {k2} (a :: k1) (b :: k2)
diff --git a/src/Pantomime/Fresh.hs b/src/Pantomime/Fresh.hs
index 28beb90..fc29da9 100644
--- a/src/Pantomime/Fresh.hs
+++ b/src/Pantomime/Fresh.hs
@@ -4,13 +4,15 @@ module Pantomime.Fresh
   ( freshArgs
   ) where
 
-import GHC.Builtin.Types.Prim (eqPrimTyCon, eqReprPrimTyCon, alphaTy)
+import GHC.Builtin.Types.Prim (eqPrimTyCon, eqReprPrimTyCon)
 import GHC.Core.FamInstEnv (FamInstEnvs, topReduceTyFamApp_maybe)
-import GHC.Core.InstEnv (InstEnvs (..), lookupUniqueInstEnv, unionInstEnv)
+import GHC.Core.InstEnv (InstEnvs (..), unionInstEnv)
 import GHC.Core.Reduction (Reduction (..), mkReduction, homogeniseHetRedn)
 import GHC.Core.TyCo.Rep (scaledThing, UnivCoProvenance (..))
 import GHC.Core.Unify (tcUnifyTysFG, alwaysBindFun, UnifyResultM (..))
-import GHC.Types.Unique (Uniquable (..), getKey)
+import GHC.Data.Pair (Pair(..))
+import GHC.Tc.Instance.FunDeps (improveFromInstEnv, FunDepEqn (..))
+import GHC.Types.Unique (Uniquable (..), getKey, minLocalUnique, incrUnique)
 import GHC.Utils.Outputable (Outputable (..), text, (<+>), showSDocUnsafe)
 import GHC.Plugins qualified as GHC
 import GHC.Plugins
@@ -35,11 +37,13 @@ import GHC.Plugins
   , mkReflCo
   , mkSymCo
   , mkSubCo
+  , mkTyConTy
   , coreFullView
   , coercionRKind
   , instNewTyCon_maybe
   , getOccFS
   , bytesFS
+  , tyConKind
   )
 
 import Grisette
@@ -215,13 +219,26 @@ freshExpr embeddings root = do
 
           -- User Interpretation:
           -----------------------
-          | Right (_inst, [tyL, tyR]) <- lookupUniqueInstEnv instEnvs' clsEmbeddable [ty, alphaTy] -> do
+          | Just (tc, targs) <- splitTyConApp_maybe ty
+
+          -- Construct a fresh type and kind variable.
+          , let namekv = GHC.mkSystemName minLocalUnique $ GHC.mkVarOccFS "k"
+          , let k = GHC.mkTyVarTy $ GHC.mkTyVar namekv GHC.liftedTypeKind
+          , let namea = GHC.mkSystemName (incrUnique minLocalUnique) $ GHC.mkVarOccFS "a"
+          , let a = GHC.mkTyVarTy $ GHC.mkTyVar namea k
+
+          -- Lookup an instance using the functional dependency.
+          , let kind = tyConKind tc
+          , let args = [kind, k, mkTyConTy tc, a]
+          , let deps = improveFromInstEnv instEnvs' (const ()) clsEmbeddable args
+          , [FDEqn { fd_eqs = [Pair tyR _]}] <- deps -> do
             -- Construct the plugin coercion
             let prov = PluginProv "SymFC embedding (user-defined)"
-            let co = mkUnivCo prov [] Representational tyL tyR
+            let co = mkUnivCo prov [] Representational (GHC.mkTyConTy tc) tyR
+            let co' = GHC.mkAppCos co $ mkReflCo Nominal <$> targs
 
             -- Create the final expression.
-            mkReductionCast $ mkReduction co (coercionRKind co)
+            mkReductionCast $ mkReduction co' (coercionRKind co')
 
           -- Type-Family:
           ---------------

From 0a83fe03bd84a71b7224fa84329a3448440ea48c Mon Sep 17 00:00:00 2001
From: Robin Webbers <robin_webbers_1@hotmail.com>
Date: Thu, 30 Jul 2026 17:46:09 +0200
Subject: [PATCH 7/7] Typo in commit

---
 src/Pantomime/Axiom.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Pantomime/Axiom.hs b/src/Pantomime/Axiom.hs
index 627c051..a63cb47 100644
--- a/src/Pantomime/Axiom.hs
+++ b/src/Pantomime/Axiom.hs
@@ -402,7 +402,7 @@ resolveEmbeddings Embeddings { .. } = do
     let warn = Nothing
     let inst = mkLocalClsInst dfun' overlap tvs embeddable tys warn
 
-    -- TODO: We should check whether the function dependency is being upheld.
+    -- TODO: We should check whether the functional dependency is being upheld.
     -- We can do so with the function 'checkFundeps' from
     -- 'GHC.Tc.Instance.FunDeps'