diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language.hs b/Pinafore/pinafore-language/lib/Pinafore/Language.hs
index 6476252dd..5c9e5ed37 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language.hs
@@ -38,48 +38,11 @@ module Pinafore.Language
 import Import
 import Pinafore.Language.Convert
 import Pinafore.Language.Error
-import Pinafore.Language.Expression
 import Pinafore.Language.Interpret
 import Pinafore.Language.Interpreter
 import Pinafore.Language.Library
-import Pinafore.Language.Type
 import Pinafore.Language.Var
 
-runPinaforeScoped :: (?library :: LibraryContext) => String -> QInterpreter a -> InterpretResult a
-runPinaforeScoped sourcename ma =
-    runInterpreter (initialPos sourcename) ?library spvals $ do
-        sd <- interpretImportDeclaration builtInModuleName
-        withScopeDocs sd ma
-
-spvals :: (?library :: LibraryContext) => QSpecialVals
-spvals = let
-    specialEvaluate :: forall t. QType 'Positive t -> Text -> IO (Result QError t)
-    specialEvaluate t text = do
-        ier <- evaluate $ runPinaforeScoped "<evaluate>" $ parseToValueSubsume t text
-        runInterpretResult ier
-    in MkQSpecialVals {..}
-
-parseToValue :: Text -> [(ImplicitName, QValue)] -> QInterpreter QValue
-parseToValue text args = do
-    expr <- parseTopExpression text
-    let argExprs = fmap (fmap qConstValue) args
-    expr' <- qImply argExprs expr
-    qEvalExpr expr'
-
-parseToValueUnify ::
-       forall t. (HasQType QPolyShim 'Negative t)
-    => Text
-    -> [(ImplicitName, QValue)]
-    -> QInterpreter t
-parseToValueUnify text args = do
-    val <- parseToValue text args
-    qUnifyValue val
-
-parseToValueSubsume :: forall t. QType 'Positive t -> Text -> QInterpreter t
-parseToValueSubsume t text = do
-    val <- parseToValue text []
-    tsSubsumeValue @QTypeSystem t val
-
 interact :: (?library :: LibraryContext) => Handle -> Handle -> Bool -> View ()
 interact inh outh echo = do
     liftIO $ hSetBuffering outh NoBuffering
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/HasType.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/HasType.hs
index 3d112f692..dc3870036 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/HasType.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Convert/HasType.hs
@@ -64,6 +64,11 @@ class (CoercibleKind (CCRVariancesKind dv), dv ~ HetCCRVariancesOf f, HasCCRVari
     where
     qGroundType :: QGroundType dv f
 
+qSomeGroundType ::
+       forall dv (t :: CCRVariancesKind dv). HasQGroundType dv t
+    => QSomeGroundType
+qSomeGroundType = MkSomeGroundType $ qGroundType @dv @t
+
 type HasQArgumentType :: PolyShimKind -> Polarity -> forall (sv :: CCRVariance) -> CCRVarianceKind sv -> Constraint
 class Is PolarityType polarity => HasQArgumentType pshim polarity sv t | t -> sv where
     qArgumentType :: CCRPolarArgumentShimWit (pshim Type) QType polarity sv t
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Expression.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Expression.hs
index db0b83238..af082bf4b 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Expression.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Expression.hs
@@ -160,6 +160,9 @@ qEvalExpr ::
     -> m QValue
 qEvalExpr expr = tsEval @QTypeSystem expr
 
+qUnifyRigid :: forall a b. QShimWit 'Positive a -> QShimWit 'Negative b -> QInterpreter (QShim a b)
+qUnifyRigid = tsUnifyRigid @QTypeSystem
+
 qUnifyValueTo :: forall t. QShimWit 'Negative t -> QValue -> QInterpreter t
 qUnifyValueTo = tsUnifyValueTo @QTypeSystem
 
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret.hs
index b0422bfba..ec3810797 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Interpret.hs
@@ -2,13 +2,19 @@ module Pinafore.Language.Interpret
     ( parseTopExpression
     , parseModule
     , parseType
+    , parseToValue
+    , parseToValueUnify
+    , parseToValueSubsume
     , interpretImportDeclaration
+    , runPinaforeScoped
     , runInteract
     , showPinaforeModel
     ) where
 
 import Import
+import Pinafore.Language.Convert
 import Pinafore.Language.Error
+import Pinafore.Language.Expression
 import Pinafore.Language.Interpret.Expression
 import Pinafore.Language.Interpret.Interact
 import Pinafore.Language.Interpreter
@@ -36,3 +42,38 @@ parseType ::
 parseType text = do
     st <- parseScopedReaderWhole (fmap return readType) text
     interpretType st
+
+parseToValue :: Text -> [(ImplicitName, QValue)] -> QInterpreter QValue
+parseToValue text args = do
+    expr <- parseTopExpression text
+    let argExprs = fmap (fmap qConstValue) args
+    expr' <- qImply argExprs expr
+    qEvalExpr expr'
+
+parseToValueUnify ::
+       forall t. (HasQType QPolyShim 'Negative t)
+    => Text
+    -> [(ImplicitName, QValue)]
+    -> QInterpreter t
+parseToValueUnify text args = do
+    val <- parseToValue text args
+    qUnifyValue val
+
+parseToValueSubsume :: forall t. QType 'Positive t -> Text -> QInterpreter t
+parseToValueSubsume t text = do
+    val <- parseToValue text []
+    tsSubsumeValue @QTypeSystem t val
+
+spvals :: (?library :: LibraryContext) => QSpecialVals
+spvals = let
+    specialEvaluate :: forall t. QType 'Positive t -> Text -> IO (Result QError t)
+    specialEvaluate t text = do
+        ier <- evaluate $ runPinaforeScoped "<evaluate>" $ parseToValueSubsume t text
+        runInterpretResult ier
+    in MkQSpecialVals {..}
+
+runPinaforeScoped :: (?library :: LibraryContext) => String -> QInterpreter a -> InterpretResult a
+runPinaforeScoped sourcename ma =
+    runInterpreter (initialPos sourcename) ?library spvals $ do
+        sd <- interpretImportDeclaration builtInModuleName
+        withScopeDocs sd ma
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Interpreter/Interpreter.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Interpreter/Interpreter.hs
index 7665723a1..f0e5e08d2 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Interpreter/Interpreter.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Interpreter/Interpreter.hs
@@ -7,6 +7,7 @@ module Pinafore.Language.Interpreter.Interpreter
     , sourcePosParam
     , varIDStateParam
     , scopeParam
+    , loadModuleParam
     , currentNamespaceParam
     , appNotationVarRef
     , appNotationBindsProd
@@ -90,6 +91,15 @@ newtype QInterpreter a = MkQInterpreter
                , MonadTunnelIO
                )
 
+instance RepresentationalRole QInterpreter where
+    representationalCoercion MkCoercion = MkCoercion
+
+instance MaybeRepresentational QInterpreter where
+    maybeRepresentational = Just Dict
+
+instance HasVariance QInterpreter where
+    type VarianceOf QInterpreter = 'Covariance
+
 instance MonadCoroutine QInterpreter where
     coroutineSuspend pqmr =
         hoist MkQInterpreter $ coroutineSuspend $ \pmq -> unInterpreter $ pqmr $ \p -> MkQInterpreter $ pmq p
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library.hs
index 31d19f160..33cd1aff3 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Library.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Library.hs
@@ -17,7 +17,6 @@ import Pinafore.Language.Library.Action
 import Pinafore.Language.Library.Debug
 import Pinafore.Language.Library.Entity
 import Pinafore.Language.Library.Env
-import Pinafore.Language.Library.Eval
 import Pinafore.Language.Library.Function
 import Pinafore.Language.Library.Interpret
 import Pinafore.Language.Library.LibraryModule
@@ -29,6 +28,7 @@ import Pinafore.Language.Library.Maybe
 import Pinafore.Language.Library.Model
 import Pinafore.Language.Library.ModelOrder
 import Pinafore.Language.Library.Optics
+import Pinafore.Language.Library.Pinafore
 import Pinafore.Language.Library.Product
 import Pinafore.Language.Library.Result
 import Pinafore.Language.Library.Storage
@@ -61,7 +61,7 @@ pinaforeLibrary =
     , storageLibSection
     , undoLibSection
     , envLibSection
-    , evalLibSection
+    , pinaforeLibSection
     , debugLibSection
     ]
 
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Eval.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Eval.hs
deleted file mode 100644
index d5c4587e8..000000000
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Eval.hs
+++ /dev/null
@@ -1,38 +0,0 @@
-module Pinafore.Language.Library.Eval
-    ( evalLibSection
-    ) where
-
-import Import
-import Pinafore.Language.Convert.Types
-import Pinafore.Language.Interpreter
-import Pinafore.Language.Library.Convert ()
-import Pinafore.Language.Library.Defs
-import Pinafore.Language.Library.LibraryModule
-import Pinafore.Language.Library.Types
-import Pinafore.Language.SpecialForm
-import Pinafore.Language.Type
-
-evalLibSection :: LibraryStuff
-evalLibSection =
-    headingBDS "Eval" "" $
-    pure $
-    namespaceBDS
-        "Eval"
-        [ specialFormBDS
-              "evaluate"
-              "A function that evaluates text as a Pinafore expression to be subsumed to positive type `A`.\n\n\
-                \The local scope is not in any way transmitted to the evaluation."
-              ["@A"]
-              "Text -> Action (Result Text A)" $
-          MkQSpecialForm (ConsListType AnnotPositiveType NilListType) $ \(MkSome (tp :: _ t), ()) -> do
-              spvals <- getSpecialVals
-              let
-                  stype :: QShimWit 'Positive (Text -> Action (Result Text t))
-                  stype = funcShimWit textShimWit $ actionShimWit $ resultShimWit textShimWit $ mkPolarShimWit tp
-                  sval :: Text -> Action (Result Text t)
-                  sval src =
-                      liftIO $ do
-                          result <- specialEvaluate spvals tp src
-                          return $ mapResultFailure showText result
-              return $ constSealedExpression $ MkSomeOf stype sval
-        ]
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs
new file mode 100644
index 000000000..0b258f615
--- /dev/null
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Pinafore.hs
@@ -0,0 +1,122 @@
+{-# OPTIONS -fno-warn-orphans #-}
+
+module Pinafore.Language.Library.Pinafore
+    ( pinaforeLibSection
+    ) where
+
+import Import
+import Pinafore.Language.Convert
+import Pinafore.Language.Error
+import Pinafore.Language.Expression
+import Pinafore.Language.Interpret
+import Pinafore.Language.Interpreter
+import Pinafore.Language.Library.Convert ()
+import Pinafore.Language.Library.Defs
+import Pinafore.Language.Library.LibraryModule
+import Pinafore.Language.Library.Types
+import Pinafore.Language.SpecialForm
+import Pinafore.Language.Type
+import Pinafore.Language.Var
+
+-- QContext
+newtype QContext =
+    MkQContext LibraryContext
+
+instance HasQGroundType '[] QContext where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily QContext)|]) "Context.Pinafore."
+
+thisContext :: QSpecialForm
+thisContext =
+    MkQSpecialForm NilListType $ \() -> do
+        lm <- paramAsk loadModuleParam
+        let
+            sval :: QContext
+            sval = MkQContext $ MkLibraryContext lm
+        return $ constSealedExpression $ MkSomeOf qType sval
+
+-- QInterpreter
+instance HasQGroundType '[ CoCCRVariance] QInterpreter where
+    qGroundType =
+        stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily QInterpreter)|]) "Interpreter.Pinafore."
+
+langRunInterpreter :: QContext -> QInterpreter A -> Action (Result Text A)
+langRunInterpreter (MkQContext lc) ia = let
+    ?library = lc
+    in do
+           rea <- runInterpretResult $ runPinaforeScoped "<evaluate>" ia
+           return $ mapResultFailure showText rea
+
+-- LangType
+data LangType (pq :: (Type, Type)) =
+    forall a. MkLangType (QRange a pq)
+                         (QNonpolarType a)
+
+instance CatFunctor (CatRange (->)) (->) LangType where
+    cfmap f (MkLangType r v) = MkLangType (cfmap f r) v
+
+instance ShowText (LangType pq) where
+    showText (MkLangType _ v) = toText $ exprShow v
+
+instance MaybeRepresentational LangType where
+    maybeRepresentational = Nothing
+
+instance HasCCRVariance 'RangeCCRVariance LangType
+
+instance HasQGroundType '[ RangeCCRVariance] LangType where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangType)|]) "Type.Pinafore."
+
+langTypePositive :: LangType '( p, q) -> QShimWit 'Positive p
+langTypePositive (MkLangType r t) = mapShimWit (MkPolarShim $ rangeContra r) $ nonpolarToPositive @QTypeSystem t
+
+langTypeNegative :: LangType '( p, q) -> QShimWit 'Negative q
+langTypeNegative (MkLangType r t) = mapShimWit (MkPolarShim $ rangeCo r) $ nonpolarToNegative @QTypeSystem t
+
+langUnifyTypes :: LangType '( A, TopType) -> LangType '( BottomType, B) -> QInterpreter (A -> B)
+langUnifyTypes ta tb = fmap shimToFunction $ qUnifyRigid (langTypePositive ta) (langTypeNegative tb)
+
+-- LangValue
+newtype LangValue =
+    MkLangValue QValue
+
+instance HasQGroundType '[] LangValue where
+    qGroundType = stdSingleGroundType $(iowitness [t|'MkWitKind (SingletonFamily LangValue)|]) "Value.Pinafore."
+
+mkLangValue :: LangType '( A, TopType) -> A -> LangValue
+mkLangValue t v = MkLangValue $ MkSomeOf (langTypePositive t) v
+
+interpretToValue :: Text -> QInterpreter LangValue
+interpretToValue src = fmap MkLangValue $ parseToValue src []
+
+langUnifyValue :: LangType '( BottomType, A) -> LangValue -> QInterpreter A
+langUnifyValue t (MkLangValue v) = qUnifyValueTo (langTypeNegative t) v
+
+pinaforeLibSection :: LibraryStuff
+pinaforeLibSection =
+    headingBDS "Pinafore" "" $
+    pure $
+    namespaceBDS
+        "Pinafore"
+        [ typeBDS "Context" "" (qSomeGroundType @_ @QContext) []
+        , namespaceBDS
+              "Context"
+              [specialFormBDS "this" "The context at this point in source." [] "Context.Pinafore" thisContext]
+        , typeBDS "Interpreter" "" (qSomeGroundType @_ @QInterpreter) []
+        , namespaceBDS "Interpreter" $ monadEntries @Interpreter <> [valBDS "run" "" langRunInterpreter]
+        , typeBDS "Type" "" (qSomeGroundType @_ @LangType) []
+        , specialFormBDS "const.Type" "" ["@A"] "Type.Pinafore A" $
+          MkQSpecialForm (ConsListType AnnotNonpolarType NilListType) $ \(MkSome (tw :: _ t), ()) -> let
+              stype :: QShimWit 'Positive (LangType '( t, t))
+              stype = rangeShimWit qGroundType (nonpolarToNegative @QTypeSystem tw) (nonpolarToPositive @QTypeSystem tw)
+              sval :: LangType '( t, t)
+              sval = MkLangType identityRange tw
+              in return $ constSealedExpression $ MkSomeOf stype sval
+        , hasSubtypeRelationBDS @(LangType '( P, Q)) @Showable Verify "" $ functionToShim "show" textShowable
+        , namespaceBDS "Type" [valBDS "unify" "Unify two types." langUnifyTypes]
+        , typeBDS "Value" "" (qSomeGroundType @_ @LangValue) []
+        , namespaceBDS
+              "Value"
+              [ valBDS "mk" "" mkLangValue
+              , valBDS "unify" "Unify type with value." langUnifyValue
+              , valBDS "interpret" "Interpret Pinafore source." interpretToValue
+              ]
+        ]
diff --git a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Types.hs b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Types.hs
index e7f2c32fc..9bbf02629 100644
--- a/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Types.hs
+++ b/Pinafore/pinafore-language/lib/Pinafore/Language/Library/Types.hs
@@ -1,5 +1,9 @@
 module Pinafore.Language.Library.Types
-    ( openEntityShimWit
+    ( coShimWit
+    , contraShimWit
+    , rangeShimWit
+    , cocoShimWit
+    , openEntityShimWit
     , maybeShimWit
     , listShimWit
     , list1ShimWit
@@ -17,41 +21,62 @@ import Pinafore.Language.Type
 openEntityShimWit :: forall tid. OpenEntityType tid -> QShimWit 'Positive (OpenEntity tid)
 openEntityShimWit tp = typeToDolan $ MkDolanGroundedType (openEntityGroundType tp) NilCCRArguments
 
-coFShimWit ::
+coShimWit ::
        forall f polarity a. (HasVariance f, VarianceOf f ~ Covariance, Is PolarityType polarity)
     => QGroundType '[ CoCCRVariance] f
     -> QShimWit polarity a
     -> QShimWit polarity (f a)
-coFShimWit gt wa =
+coShimWit gt wa =
     shimWitToDolan $
     mkDolanGroundedShimWit gt $
     consCCRPolarArgumentsShimWit (qgtVarianceMap gt) (coCCRArgument wa) nilCCRPolarArgumentsShimWit
 
+contraShimWit ::
+       forall f polarity a. (HasVariance f, VarianceOf f ~ Contravariance, Is PolarityType polarity)
+    => QGroundType '[ ContraCCRVariance] f
+    -> QShimWit (InvertPolarity polarity) a
+    -> QShimWit polarity (f a)
+contraShimWit gt wa =
+    shimWitToDolan $
+    mkDolanGroundedShimWit gt $
+    consCCRPolarArgumentsShimWit (qgtVarianceMap gt) (contraCCRArgument wa) nilCCRPolarArgumentsShimWit
+
+rangeShimWit ::
+       forall f polarity p q. Is PolarityType polarity
+    => QGroundType '[ RangeCCRVariance] f
+    -> QShimWit (InvertPolarity polarity) p
+    -> QShimWit polarity q
+    -> QShimWit polarity (f '( p, q))
+rangeShimWit gt wp wq =
+    shimWitToDolan $
+    mkDolanGroundedShimWit gt $
+    consCCRPolarArgumentsShimWit (qgtVarianceMap gt) (rangeCCRArgument wp wq) nilCCRPolarArgumentsShimWit
+
 maybeShimWit ::
        forall polarity a. Is PolarityType polarity
     => QShimWit polarity a
     -> QShimWit polarity (Maybe a)
-maybeShimWit = coFShimWit maybeGroundType
+maybeShimWit = coShimWit maybeGroundType
 
 listShimWit ::
        forall polarity a. Is PolarityType polarity
     => QShimWit polarity a
     -> QShimWit polarity [a]
-listShimWit = coFShimWit listGroundType
+listShimWit = coShimWit listGroundType
 
 list1ShimWit ::
        forall polarity a. Is PolarityType polarity
     => QShimWit polarity a
     -> QShimWit polarity (NonEmpty a)
-list1ShimWit = coFShimWit list1GroundType
+list1ShimWit = coShimWit list1GroundType
 
-cocoFShimWit ::
+cocoShimWit ::
        forall f polarity a b. Is PolarityType polarity
     => QGroundType '[ CoCCRVariance, CoCCRVariance] f
     -> QShimWit polarity a
     -> QShimWit polarity b
     -> QShimWit polarity (f a b)
-cocoFShimWit gt wa wb =
+cocoShimWit gt wa wb =
     shimWitToDolan $
     mkDolanGroundedShimWit gt $
     consCCRPolarArgumentsShimWit (qgtVarianceMap gt) (coCCRArgument wa) $
@@ -63,21 +88,21 @@ eitherShimWit ::
     => QShimWit polarity a
     -> QShimWit polarity b
     -> QShimWit polarity (Either a b)
-eitherShimWit = cocoFShimWit eitherGroundType
+eitherShimWit = cocoShimWit eitherGroundType
 
 resultShimWit ::
        forall polarity a b. Is PolarityType polarity
     => QShimWit polarity a
     -> QShimWit polarity b
     -> QShimWit polarity (Result a b)
-resultShimWit = cocoFShimWit resultGroundType
+resultShimWit = cocoShimWit resultGroundType
 
 pairShimWit ::
        forall polarity a b. Is PolarityType polarity
     => QShimWit polarity a
     -> QShimWit polarity b
     -> QShimWit polarity (a, b)
-pairShimWit = cocoFShimWit pairGroundType
+pairShimWit = cocoShimWit pairGroundType
 
 funcShimWit ::
        forall polarity (pshim :: PolyShimKind) a b.
diff --git a/Pinafore/pinafore-language/package.yaml b/Pinafore/pinafore-language/package.yaml
index 2ef462bec..dd8b60178 100644
--- a/Pinafore/pinafore-language/package.yaml
+++ b/Pinafore/pinafore-language/package.yaml
@@ -133,7 +133,7 @@ library:
       - Pinafore.Language.Library.Storage
       - Pinafore.Language.Library.Undo
       - Pinafore.Language.Library.Env
-      - Pinafore.Language.Library.Eval
+      - Pinafore.Language.Library.Pinafore
       - Pinafore.Language.Library.Debug
       - Pinafore.Language.Library
       - Pinafore.Language
diff --git a/Pinafore/pinafore-language/pinafore-language.cabal b/Pinafore/pinafore-language/pinafore-language.cabal
index b7ba4ae8e..408df6bab 100644
--- a/Pinafore/pinafore-language/pinafore-language.cabal
+++ b/Pinafore/pinafore-language/pinafore-language.cabal
@@ -123,7 +123,7 @@ library
       Pinafore.Language.Library.Storage
       Pinafore.Language.Library.Undo
       Pinafore.Language.Library.Env
-      Pinafore.Language.Library.Eval
+      Pinafore.Language.Library.Pinafore
       Pinafore.Language.Library.Debug
       Pinafore.Language.Library
       Pinafore.Language
diff --git a/Pinafore/typed-expression/lib/Language/Expression/TypeSystem/Complete.hs b/Pinafore/typed-expression/lib/Language/Expression/TypeSystem/Complete.hs
index f28c8eabf..2a21a190f 100644
--- a/Pinafore/typed-expression/lib/Language/Expression/TypeSystem/Complete.hs
+++ b/Pinafore/typed-expression/lib/Language/Expression/TypeSystem/Complete.hs
@@ -44,6 +44,17 @@ tsEval ::
     -> m (TSValue ts)
 tsEval = evalSealedExpression
 
+tsUnifyRigid ::
+       forall ts a b. CompleteTypeSystem ts
+    => TSPosShimWit ts a
+    -> TSNegShimWit ts b
+    -> TSInner ts (TSShim ts a b)
+tsUnifyRigid witp witn =
+    runRenamer @ts (renameableVars witp <> renameableVars witn) [] $ do
+        uconv <- unifyPosNegShimWit @ts (uuLiftPosShimWit @ts witp) (uuLiftNegShimWit @ts witn)
+        convexpr <- unifierSolve @ts uconv return
+        lift $ evalExpression convexpr
+
 -- | for debugging
 tsUnifyRigidValue ::
        forall ts t. (CompleteTypeSystem ts, FromPolarShimWit (TSShim ts) (TSNegWitness ts) t)
@@ -51,10 +62,8 @@ tsUnifyRigidValue ::
     -> TSInner ts t
 tsUnifyRigidValue (MkSomeOf witp val) = let
     witn = fromPolarShimWit
-    in runRenamer @ts (renameableVars witp <> renameableVars witn) [] $ do
-           uconv <- unifyPosNegShimWit @ts (uuLiftPosShimWit @ts witp) (uuLiftNegShimWit @ts witn)
-           convexpr <- unifierSolve @ts uconv return
-           conv <- lift $ evalExpression convexpr
+    in do
+           conv <- tsUnifyRigid @ts witp witn
            return $ shimToFunction conv val
 
 tsUnifyExpressionTo ::