Migrate to `Felix` namespaceHEADhotg

1 files changed, 1604 insertions, 0 deletions

diff --git a/source/Felix/Checking/Core.hs b/source/Felix/Checking/Core.hs
new file mode 100644
index 0000000..13ec218
--- /dev/null
+++ b/source/Felix/Checking/Core.hs
@@ -0,0 +1,1604 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Checked monomorphic HOL syntax and its nameless in-memory form.
+--
+-- Scoped syntax is an operational construction language.  Only a checked,
+-- frozen value is semantic input to later kernel and backend boundaries.
+module Felix.Checking.Core
+    ( CoreType(..)
+    , CoreIntrinsicTag(..)
+    , coreIntrinsicType
+    , CoreSyntax
+    , coreLocal
+    , coreGlobal
+    , coreIntrinsic
+    , coreOpaqueInteger
+    , coreApply
+    , coreLambda
+    , coreFalsum
+    , coreImplication
+    , coreEquality
+    , coreForall
+    , CheckedCore
+    , checkedCoreType
+    , checkCore
+    , checkClosedCore
+    , ClosedCheckedProposition
+    , checkedPropositionCore
+    , checkClosedProposition
+    , CoreCheckError(..)
+    , CanonicalTerm(..)
+    , canonicalSetInsert
+    , FrozenCheckedCore
+    , frozenCoreType
+    , frozenCoreTerm
+    , thawFrozenCore
+    , frozenCoreGlobals
+    , mapFrozenGlobals
+    , ScopedCheckedCore
+    , scopedCoreContext
+    , scopedCoreType
+    , scopedCoreTerm
+    , mapScopedGlobals
+    , checkScopedCanonicalCore
+    , embedClosedCore
+    , weakenCheckedScopedCore
+    , weakenScopedCore
+    , scopedSetDefinition
+    , scopedCharacteristicDefinition
+    , scopedReplacementGraph
+    , implyScopedCore
+    , equalScopedCore
+    , conjoinScopedCore
+    , disjoinScopedCore
+    , negateScopedCore
+    , falsumScopedCore
+    , splitScopedSetEquality
+    , scopedSetInductionInstance
+    , closeScopedForall
+    , closeScopedExists
+    , openScopedForall
+    , openScopedImplication
+    , openScopedAssumption
+    , closeScopedCore
+    , betaNormalizeCanonical
+    , instantiateCanonical
+    , shiftCanonical
+    , mapCanonicalGlobals
+    , canonicalTermGlobals
+    , checkCanonicalCore
+    , freezeClosed
+    , FreezeError(..)
+    , referenceFreezeClosed
+    ) where
+
+import Base hiding (Empty)
+
+import Bound
+import Control.DeepSeq (NFData)
+import Control.Monad (ap, unless)
+import Data.Set qualified as Set
+import Numeric.Natural (Natural)
+
+
+-- | The complete monomorphic type grammar of the checked core.
+data CoreType
+    = TyProp
+    | TySet
+    | TyArrow !CoreType !CoreType
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+
+-- | The complete set-forming primitive inventory.
+data CoreIntrinsicTag
+    = Member
+    | Empty
+    | PairSet
+    | FamilyUnion
+    | PowerSet
+    | Sep
+    | Repl
+    | SetChoose
+    | UnivOf
+    -- | The bounded set-valued least fixed point. It denotes the elements of
+    -- its bound that belong to every bounded pre-fixed point of its operator.
+    | ISetLfp
+    deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
+    deriving anyclass (NFData)
+
+coreIntrinsicType :: CoreIntrinsicTag -> CoreType
+coreIntrinsicType = \case
+    Member ->
+        TySet `TyArrow` (TySet `TyArrow` TyProp)
+    Empty ->
+        TySet
+    PairSet ->
+        TySet `TyArrow` (TySet `TyArrow` TySet)
+    FamilyUnion ->
+        TySet `TyArrow` TySet
+    PowerSet ->
+        TySet `TyArrow` TySet
+    Sep ->
+        TySet
+            `TyArrow`
+                ((TySet `TyArrow` TyProp) `TyArrow` TySet)
+    Repl ->
+        TySet
+            `TyArrow`
+                ((TySet `TyArrow` TySet) `TyArrow` TySet)
+    SetChoose ->
+        (TySet `TyArrow` TyProp) `TyArrow` TySet
+    UnivOf ->
+        TySet `TyArrow` TySet
+    ISetLfp ->
+        TySet
+            `TyArrow`
+                ((TySet `TyArrow` TySet) `TyArrow` TySet)
+
+
+-- | Operational scoped syntax.  Its constructors remain private because this
+-- value is neither a typing certificate nor an authority-bearing term.
+data CoreSyntax global local
+    = CoreLocal local
+    | CoreGlobal global
+    | CoreIntrinsic CoreIntrinsicTag
+    | CoreOpaqueInteger !Integer
+    | CoreApply
+        !(CoreSyntax global local)
+        !(CoreSyntax global local)
+    | CoreLambda
+        !CoreType
+        !(Scope () (CoreSyntax global) local)
+    | CoreFalsum
+    | CoreImplication
+        !(CoreSyntax global local)
+        !(CoreSyntax global local)
+    | CoreEquality
+        !CoreType
+        !(CoreSyntax global local)
+        !(CoreSyntax global local)
+    | CoreForall
+        !CoreType
+        !(Scope () (CoreSyntax global) local)
+    deriving stock (Functor, Foldable, Traversable)
+
+instance Applicative (CoreSyntax global) where
+    pure = CoreLocal
+    (<*>) = ap
+
+instance Monad (CoreSyntax global) where
+    CoreLocal local >>= replace =
+        replace local
+    CoreGlobal global >>= _replace =
+        CoreGlobal global
+    CoreIntrinsic intrinsic >>= _replace =
+        CoreIntrinsic intrinsic
+    CoreOpaqueInteger integer >>= _replace =
+        CoreOpaqueInteger integer
+    CoreApply function argument >>= replace =
+        CoreApply
+            (function >>= replace)
+            (argument >>= replace)
+    CoreLambda binderType body >>= replace =
+        CoreLambda binderType (body >>>= replace)
+    CoreFalsum >>= _replace =
+        CoreFalsum
+    CoreImplication premise conclusion >>= replace =
+        CoreImplication
+            (premise >>= replace)
+            (conclusion >>= replace)
+    CoreEquality operandType left right >>= replace =
+        CoreEquality
+            operandType
+            (left >>= replace)
+            (right >>= replace)
+    CoreForall binderType body >>= replace =
+        CoreForall binderType (body >>>= replace)
+
+coreLocal :: local -> CoreSyntax global local
+coreLocal = CoreLocal
+
+coreGlobal :: global -> CoreSyntax global local
+coreGlobal = CoreGlobal
+
+coreIntrinsic :: CoreIntrinsicTag -> CoreSyntax global local
+coreIntrinsic = CoreIntrinsic
+
+coreOpaqueInteger :: Integer -> CoreSyntax global local
+coreOpaqueInteger = CoreOpaqueInteger
+
+coreApply
+    :: CoreSyntax global local
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+coreApply = CoreApply
+
+coreLambda
+    :: Eq local
+    => CoreType
+    -> local
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+coreLambda binderType local body =
+    CoreLambda binderType (abstract1 local body)
+
+coreFalsum :: CoreSyntax global local
+coreFalsum = CoreFalsum
+
+coreImplication
+    :: CoreSyntax global local
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+coreImplication = CoreImplication
+
+coreEquality
+    :: CoreType
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+coreEquality = CoreEquality
+
+coreForall
+    :: Eq local
+    => CoreType
+    -> local
+    -> CoreSyntax global local
+    -> CoreSyntax global local
+coreForall binderType local body =
+    CoreForall binderType (abstract1 local body)
+
+
+data CoreCheckError
+    = UnknownCoreGlobal
+    | UnboundCoreLocal
+    | UnboundCoreIndex !Natural
+    | AppliedNonFunction !CoreType
+    | ApplicationArgumentTypeMismatch
+        !CoreType
+        !CoreType
+    | ImplicationOperandTypeMismatch
+        !CoreType
+    | EqualityOperandTypeMismatch
+        !CoreType
+        !CoreType
+    | QuantifierBodyTypeMismatch
+        !CoreType
+    | ExpectedCoreType
+        !CoreType
+        !CoreType
+    deriving stock (Show, Eq)
+
+
+-- | A scoped term whose complete tree has been type checked.
+data CheckedCore global local = CheckedCore
+    !CoreType
+    !(CoreSyntax global local)
+
+checkedCoreType :: CheckedCore global local -> CoreType
+checkedCoreType (CheckedCore coreType _syntax) =
+    coreType
+
+checkCore
+    :: (global -> Maybe CoreType)
+    -> (local -> Maybe CoreType)
+    -> CoreSyntax global local
+    -> Either CoreCheckError (CheckedCore global local)
+checkCore globalType localType syntax = do
+    coreType <-
+        inferCore globalType localType syntax
+    pure (CheckedCore coreType syntax)
+
+checkClosedCore
+    :: (global -> Maybe CoreType)
+    -> CoreSyntax global local
+    -> Either CoreCheckError (CheckedCore global Void)
+checkClosedCore globalType syntax = do
+    closedSyntax <-
+        maybe
+            (Left UnboundCoreLocal)
+            Right
+            (traverse (const Nothing) syntax)
+    checkCore globalType absurd closedSyntax
+
+newtype ClosedCheckedProposition global =
+    ClosedCheckedProposition (CheckedCore global Void)
+
+checkedPropositionCore
+    :: ClosedCheckedProposition global
+    -> CheckedCore global Void
+checkedPropositionCore
+    (ClosedCheckedProposition proposition) =
+        proposition
+
+checkClosedProposition
+    :: (global -> Maybe CoreType)
+    -> CoreSyntax global local
+    -> Either CoreCheckError (ClosedCheckedProposition global)
+checkClosedProposition globalType syntax = do
+    checked <-
+        checkClosedCore globalType syntax
+    unless
+        (checkedCoreType checked == TyProp)
+        (Left
+            (ExpectedCoreType
+                TyProp
+                (checkedCoreType checked)))
+    pure (ClosedCheckedProposition checked)
+
+inferCore
+    :: forall global local
+     . (global -> Maybe CoreType)
+    -> (local -> Maybe CoreType)
+    -> CoreSyntax global local
+    -> Either CoreCheckError CoreType
+inferCore globalType localType =
+    infer
+        (maybe
+            (Left UnboundCoreLocal)
+            Right
+            . localType)
+  where
+    infer
+        :: forall local'
+         . (local' -> Either CoreCheckError CoreType)
+        -> CoreSyntax global local'
+        -> Either CoreCheckError CoreType
+    infer resolveLocal = \case
+        CoreLocal local ->
+            resolveLocal local
+        CoreGlobal global ->
+            maybe
+                (Left UnknownCoreGlobal)
+                Right
+                (globalType global)
+        CoreIntrinsic intrinsic ->
+            Right (coreIntrinsicType intrinsic)
+        CoreOpaqueInteger{} ->
+            Right TySet
+        CoreApply function argument -> do
+            functionType <-
+                infer resolveLocal function
+            argumentType <-
+                infer resolveLocal argument
+            case functionType of
+                TyArrow expectedArgument resultType
+                    | expectedArgument == argumentType ->
+                        Right resultType
+                    | otherwise ->
+                        Left
+                            (ApplicationArgumentTypeMismatch
+                                expectedArgument
+                                argumentType)
+                other ->
+                    Left (AppliedNonFunction other)
+        CoreLambda binderType body -> do
+            bodyType <-
+                infer
+                    (boundLocalType binderType resolveLocal)
+                    (unscope body)
+            Right (binderType `TyArrow` bodyType)
+        CoreFalsum ->
+            Right TyProp
+        CoreImplication premise conclusion -> do
+            premiseType <-
+                infer resolveLocal premise
+            unless
+                (premiseType == TyProp)
+                (Left
+                    (ImplicationOperandTypeMismatch
+                        premiseType))
+            conclusionType <-
+                infer resolveLocal conclusion
+            unless
+                (conclusionType == TyProp)
+                (Left
+                    (ImplicationOperandTypeMismatch
+                        conclusionType))
+            Right TyProp
+        CoreEquality operandType left right -> do
+            leftType <-
+                infer resolveLocal left
+            unless
+                (leftType == operandType)
+                (Left
+                    (EqualityOperandTypeMismatch
+                        operandType
+                        leftType))
+            rightType <-
+                infer resolveLocal right
+            unless
+                (rightType == operandType)
+                (Left
+                    (EqualityOperandTypeMismatch
+                        operandType
+                        rightType))
+            Right TyProp
+        CoreForall binderType body -> do
+            bodyType <-
+                infer
+                    (boundLocalType binderType resolveLocal)
+                    (unscope body)
+            unless
+                (bodyType == TyProp)
+                (Left
+                    (QuantifierBodyTypeMismatch bodyType))
+            Right TyProp
+
+    boundLocalType
+        :: forall local'
+         . CoreType
+        -> (local' -> Either CoreCheckError CoreType)
+        -> Var () (CoreSyntax global local')
+        -> Either CoreCheckError CoreType
+    boundLocalType binderType outerType = \case
+        B () ->
+            Right binderType
+        F outerSyntax ->
+            infer outerType outerSyntax
+
+
+-- | Felix-owned explicit-index syntax.  Index zero denotes the nearest
+-- enclosing binder.
+data CanonicalTerm global
+    = CBound !Natural
+    | CGlobal !global
+    | CIntrinsic !CoreIntrinsicTag
+    | COpaqueInteger !Integer
+    | CApp
+        !(CanonicalTerm global)
+        !(CanonicalTerm global)
+    | CLam
+        !CoreType
+        !(CanonicalTerm global)
+    | CFalsum
+    | CImp
+        !(CanonicalTerm global)
+        !(CanonicalTerm global)
+    | CEq
+        !CoreType
+        !(CanonicalTerm global)
+        !(CanonicalTerm global)
+    | CForall
+        !CoreType
+        !(CanonicalTerm global)
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+-- | The fixed checked-core interpretation of set insertion.
+--
+-- Finite-set notation uses this intrinsic HOTG adjunction directly.  The
+-- ordinary source-owned @cons@ function is not consulted during lowering.
+canonicalSetInsert
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+canonicalSetInsert element set =
+    CApp
+        (CIntrinsic FamilyUnion)
+        (CApp
+            (CApp
+                (CIntrinsic PairSet)
+                (CApp
+                    (CApp
+                        (CIntrinsic PairSet)
+                        element)
+                    element))
+            set)
+
+data FrozenCheckedCore global = FrozenCheckedCore
+    !CoreType
+    !(CanonicalTerm global)
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+frozenCoreType :: FrozenCheckedCore global -> CoreType
+frozenCoreType (FrozenCheckedCore coreType _term) =
+    coreType
+
+frozenCoreTerm :: FrozenCheckedCore global -> CanonicalTerm global
+frozenCoreTerm (FrozenCheckedCore _coreType term) =
+    term
+
+mapFrozenGlobals
+    :: (global -> global')
+    -> FrozenCheckedCore global
+    -> FrozenCheckedCore global'
+mapFrozenGlobals transform
+        (FrozenCheckedCore coreType term) =
+    FrozenCheckedCore
+        coreType
+        (mapCanonicalGlobals transform term)
+
+-- | Recover an operational closed term from a checked frozen value. Any caller
+-- that extends or substitutes it must check the resulting term again.
+thawFrozenCore
+    :: FrozenCheckedCore global
+    -> CoreSyntax global Void
+thawFrozenCore (FrozenCheckedCore _coreType term) =
+    case traverse (const Nothing) (go [] term) of
+        Just closedSyntax ->
+            closedSyntax
+        Nothing ->
+            impossible
+                "a frozen core term became open while being thawed"
+  where
+    go
+        :: [Natural]
+        -> CanonicalTerm global
+        -> CoreSyntax global Natural
+    go binders = \case
+        CBound index ->
+            case lookupBinder index binders of
+                Just local ->
+                    coreLocal local
+                Nothing ->
+                    impossible
+                        "a frozen core term contains an unbound index"
+        CGlobal global ->
+            coreGlobal global
+        CIntrinsic intrinsic ->
+            coreIntrinsic intrinsic
+        COpaqueInteger integer ->
+            coreOpaqueInteger integer
+        CApp function argument ->
+            coreApply
+                (go binders function)
+                (go binders argument)
+        CLam binderType body ->
+            let local =
+                    fromIntegral (length binders)
+            in coreLambda
+                binderType
+                local
+                (go (local : binders) body)
+        CFalsum ->
+            coreFalsum
+        CImp premise conclusion ->
+            coreImplication
+                (go binders premise)
+                (go binders conclusion)
+        CEq operandType left right ->
+            coreEquality
+                operandType
+                (go binders left)
+                (go binders right)
+        CForall binderType body ->
+            let local =
+                    fromIntegral (length binders)
+            in coreForall
+                binderType
+                local
+                (go (local : binders) body)
+
+    lookupBinder
+        :: Natural
+        -> [Natural]
+        -> Maybe Natural
+    lookupBinder _index [] =
+        Nothing
+    lookupBinder 0 (local : _rest) =
+        Just local
+    lookupBinder index (_local : rest) =
+        lookupBinder (index - 1) rest
+
+frozenCoreGlobals
+    :: Ord global
+    => FrozenCheckedCore global
+    -> Set.Set global
+frozenCoreGlobals =
+    canonicalTermGlobals . frozenCoreTerm
+
+canonicalTermGlobals
+    :: Ord global
+    => CanonicalTerm global
+    -> Set.Set global
+canonicalTermGlobals = \case
+    CBound{} ->
+        mempty
+    CGlobal global ->
+        Set.singleton global
+    CIntrinsic{} ->
+        mempty
+    COpaqueInteger{} ->
+        mempty
+    CApp function argument ->
+        canonicalTermGlobals function
+            <> canonicalTermGlobals argument
+    CLam _binderType body ->
+        canonicalTermGlobals body
+    CFalsum ->
+        mempty
+    CImp premise conclusion ->
+        canonicalTermGlobals premise
+            <> canonicalTermGlobals conclusion
+    CEq _operandType left right ->
+        canonicalTermGlobals left
+            <> canonicalTermGlobals right
+    CForall _binderType body ->
+        canonicalTermGlobals body
+
+-- | A checked canonical term relative to the listed nearest-first binders.
+-- This is the construction boundary used by kernel replay; it carries no fact
+-- authority.
+data ScopedCheckedCore global = ScopedCheckedCore
+    ![CoreType]
+    !CoreType
+    !(CanonicalTerm global)
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+scopedCoreContext
+    :: ScopedCheckedCore global
+    -> [CoreType]
+scopedCoreContext
+        (ScopedCheckedCore context _coreType _term) =
+    context
+
+scopedCoreType
+    :: ScopedCheckedCore global
+    -> CoreType
+scopedCoreType
+        (ScopedCheckedCore _context coreType _term) =
+    coreType
+
+scopedCoreTerm
+    :: ScopedCheckedCore global
+    -> CanonicalTerm global
+scopedCoreTerm
+        (ScopedCheckedCore _context _coreType term) =
+    term
+
+mapScopedGlobals
+    :: (left -> right)
+    -> ScopedCheckedCore left
+    -> ScopedCheckedCore right
+mapScopedGlobals transform
+        (ScopedCheckedCore context coreType term) =
+    ScopedCheckedCore
+        context
+        coreType
+        (mapCanonicalGlobals transform term)
+
+checkScopedCanonicalCore
+    :: (global -> Maybe CoreType)
+    -> [CoreType]
+    -> CanonicalTerm global
+    -> Either CoreCheckError (ScopedCheckedCore global)
+checkScopedCanonicalCore globalType context term =
+    ScopedCheckedCore context
+        <$> inferCanonicalCore globalType context term
+        <*> pure term
+
+-- | Regard a closed term under a larger lexical context. Closed canonical
+-- terms contain no indices, so this does not shift the term.
+embedClosedCore
+    :: [CoreType]
+    -> FrozenCheckedCore global
+    -> ScopedCheckedCore global
+embedClosedCore context
+        (FrozenCheckedCore coreType term) =
+    ScopedCheckedCore context coreType term
+
+-- | Add one nearest binder to an already checked lexical context.
+weakenCheckedScopedCore
+    :: CoreType
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+weakenCheckedScopedCore binderType scoped =
+    ScopedCheckedCore
+        (binderType : scopedCoreContext scoped)
+        (scopedCoreType scoped)
+        (shiftCanonical 1 0 (scopedCoreTerm scoped))
+
+-- | Add one nearest binder to a checked lexical context.
+weakenScopedCore
+    :: (global -> Maybe CoreType)
+    -> CoreType
+    -> ScopedCheckedCore global
+    -> Either CoreCheckError (ScopedCheckedCore global)
+weakenScopedCore globalType binderType scoped =
+    checkScopedCanonicalCore
+        globalType
+        (binderType : scopedCoreContext scoped)
+        (shiftCanonical 1 0
+            (scopedCoreTerm scoped))
+
+-- | Introduce a fresh set-valued local definition. Separation specializes
+-- the checked foundation characteristic so its local premise remains
+-- first-order.
+scopedSetDefinition
+    :: Eq global
+    => FrozenCheckedCore Void
+    -> ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+scopedSetDefinition
+        characteristic
+        expression@(ScopedCheckedCore context TySet term) =
+    case term of
+        CApp
+                (CApp (CIntrinsic Sep) bound)
+                predicate@(CLam TySet _body) ->
+            scopedCharacteristicDefinition
+                characteristic
+                expression
+                ( ScopedCheckedCore context TySet bound
+                    :| [ ScopedCheckedCore
+                            context
+                            (TySet `TyArrow` TyProp)
+                            predicate
+                       ]
+                )
+        _ ->
+            Just
+                (ScopedCheckedCore
+                    (TySet : context)
+                    TyProp
+                    (CEq
+                        TySet
+                        (CBound 0)
+                        (shiftCanonical 1 0 term)))
+scopedSetDefinition _characteristic _expression =
+    Nothing
+
+-- | Specialize a checked characteristic and abstract its set-valued target
+-- into one fresh nearest binder. Checked substitution and beta reduction
+-- preserve the foundation row's proposition type.
+scopedCharacteristicDefinition
+    :: Eq global
+    => FrozenCheckedCore Void
+    -> ScopedCheckedCore global
+    -> NonEmpty (ScopedCheckedCore global)
+    -> Maybe (ScopedCheckedCore global)
+scopedCharacteristicDefinition
+        (FrozenCheckedCore TyProp frozen)
+        (ScopedCheckedCore context TySet target)
+        arguments
+    | all ((== context) . scopedCoreContext) arguments = do
+        specialized <-
+            specialize
+                (mapCanonicalGlobals absurd frozen)
+                (toList arguments)
+        let normalized = betaNormalizeCanonical specialized
+            (found, abstracted) = abstractTarget 0 normalized
+        guard found
+        pure
+            (ScopedCheckedCore
+                (TySet : context)
+                TyProp
+                abstracted)
+  where
+    specialize term [] =
+        Just term
+    specialize (CForall binderType body)
+            (ScopedCheckedCore _ argumentType argument : rest)
+        | binderType == argumentType =
+            specialize
+                (instantiateCanonical argument body)
+                rest
+    specialize _term _arguments =
+        Nothing
+
+    abstractTarget depth term
+        | term == shiftCanonical depth 0 target =
+            (True, CBound (fromIntegral depth))
+        | otherwise =
+            case term of
+                CBound index
+                    | index < fromIntegral depth ->
+                        (False, CBound index)
+                    | otherwise ->
+                        (False, CBound (index + 1))
+                CGlobal global ->
+                    (False, CGlobal global)
+                CIntrinsic intrinsic ->
+                    (False, CIntrinsic intrinsic)
+                COpaqueInteger integer ->
+                    (False, COpaqueInteger integer)
+                CApp function argument ->
+                    combine CApp
+                        (abstractTarget depth function)
+                        (abstractTarget depth argument)
+                CLam binderType body ->
+                    let (found, abstracted) =
+                            abstractTarget (depth + 1) body
+                    in (found, CLam binderType abstracted)
+                CFalsum ->
+                    (False, CFalsum)
+                CImp premise conclusion ->
+                    combine CImp
+                        (abstractTarget depth premise)
+                        (abstractTarget depth conclusion)
+                CEq operandType left right ->
+                    combine (CEq operandType)
+                        (abstractTarget depth left)
+                        (abstractTarget depth right)
+                CForall binderType body ->
+                    let (found, abstracted) =
+                            abstractTarget (depth + 1) body
+                    in (found, CForall binderType abstracted)
+
+    combine constructor (leftFound, left) (rightFound, right) =
+        (leftFound || rightFound, constructor left right)
+scopedCharacteristicDefinition _characteristic _target _arguments =
+    Nothing
+
+-- | Build the replacement graph of one checked set-valued local function.
+-- The ordered-pair constructor is an ordinary checked source object.
+scopedReplacementGraph
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+scopedReplacementGraph
+        (ScopedCheckedCore context pairType pair)
+        domain@(ScopedCheckedCore domainContext TySet domainTerm)
+        (ScopedCheckedCore valueContext TySet value)
+    | pairType == TySet `TyArrow` (TySet `TyArrow` TySet)
+    , domainContext == context
+    , valueContext == TySet : context =
+        let pairValue =
+                CApp
+                    (CApp
+                        (shiftCanonical 1 0 pair)
+                        (CBound 0))
+                    value
+            function = CLam TySet pairValue
+            graph =
+                CApp
+                    (CApp (CIntrinsic Repl) domainTerm)
+                    function
+        in Just
+            ( ScopedCheckedCore context TySet graph
+            , domain
+            , ScopedCheckedCore
+                context
+                (TySet `TyArrow` TySet)
+                function
+            )
+scopedReplacementGraph _pair _domain _value =
+    Nothing
+
+betaNormalizeCanonical
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+betaNormalizeCanonical = \case
+    CApp function argument ->
+        case betaNormalizeCanonical function of
+            CLam _binderType body ->
+                betaNormalizeCanonical
+                    (instantiateCanonical
+                        (betaNormalizeCanonical argument)
+                        body)
+            normalizedFunction ->
+                CApp
+                    normalizedFunction
+                    (betaNormalizeCanonical argument)
+    CLam binderType body ->
+        CLam binderType (betaNormalizeCanonical body)
+    CImp premise conclusion ->
+        CImp
+            (betaNormalizeCanonical premise)
+            (betaNormalizeCanonical conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (betaNormalizeCanonical left)
+            (betaNormalizeCanonical right)
+    CForall binderType body ->
+        CForall binderType (betaNormalizeCanonical body)
+    term -> term
+
+-- | Combine two checked propositions under the same lexical context.
+implyScopedCore
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+implyScopedCore
+        (ScopedCheckedCore premiseContext TyProp premise)
+        (ScopedCheckedCore conclusionContext TyProp conclusion)
+    | premiseContext == conclusionContext =
+        Just
+            (ScopedCheckedCore
+                premiseContext
+                TyProp
+                (CImp premise conclusion))
+implyScopedCore _premise _conclusion =
+    Nothing
+
+-- | Form an equality between checked operands under the same lexical
+-- context.  This preserves the checked-core invariant without requiring a
+-- caller to recover global types merely to combine already checked terms.
+equalScopedCore
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+equalScopedCore
+        (ScopedCheckedCore leftContext leftType left)
+        (ScopedCheckedCore rightContext rightType right)
+    | leftContext == rightContext
+    , leftType == rightType =
+        Just
+            (ScopedCheckedCore
+                leftContext
+                TyProp
+                (CEq leftType left right))
+equalScopedCore _left _right =
+    Nothing
+
+-- | Conjoin two checked propositions under the same lexical context.  Truth
+-- is normalized away so callers can build an optional source guard without
+-- retaining an inert conjunct.
+conjoinScopedCore
+    :: Eq global
+    => ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+conjoinScopedCore
+        left@(ScopedCheckedCore leftContext TyProp leftTerm)
+        right@(ScopedCheckedCore rightContext TyProp rightTerm)
+    | leftContext == rightContext
+    , leftTerm == truth = Just right
+    | leftContext == rightContext
+    , rightTerm == truth = Just left
+    | leftContext == rightContext =
+        Just
+            (ScopedCheckedCore
+                leftContext
+                TyProp
+                (CImp
+                    (CImp leftTerm (CImp rightTerm CFalsum))
+                    CFalsum))
+  where
+    truth = CImp CFalsum CFalsum
+conjoinScopedCore _left _right =
+    Nothing
+
+-- | Disjoin two checked propositions under the same lexical context using
+-- the fixed classical encoding owned by the checked core.
+disjoinScopedCore
+    :: ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+disjoinScopedCore
+        (ScopedCheckedCore leftContext TyProp left)
+        (ScopedCheckedCore rightContext TyProp right)
+    | leftContext == rightContext =
+        Just
+            (ScopedCheckedCore
+                leftContext
+                TyProp
+                (CImp (CImp left CFalsum) right))
+disjoinScopedCore _left _right =
+    Nothing
+
+-- | Negate a checked proposition without changing its lexical context.
+negateScopedCore
+    :: ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+negateScopedCore (ScopedCheckedCore context TyProp proposition) =
+    Just
+        (ScopedCheckedCore
+            context
+            TyProp
+            (CImp proposition CFalsum))
+negateScopedCore _proposition =
+    Nothing
+
+-- | Checked falsum at an already established lexical context.
+falsumScopedCore :: [CoreType] -> ScopedCheckedCore global
+falsumScopedCore context =
+    ScopedCheckedCore context TyProp CFalsum
+
+-- | Split a checked set equality into its two extensionality directions.
+splitScopedSetEquality
+    :: ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+splitScopedSetEquality
+        (ScopedCheckedCore context TyProp (CEq TySet left right)) =
+    Just (subset left right, subset right left)
+  where
+    subset source target =
+        ScopedCheckedCore
+            context
+            TyProp
+            (CForall
+                TySet
+                (CImp
+                    (memberOf (shiftCanonical 1 0 source))
+                    (memberOf (shiftCanonical 1 0 target))))
+
+    memberOf set =
+        CApp
+            (CApp
+                (CIntrinsic Member)
+                (CBound 0))
+            set
+splitScopedSetEquality _proposition =
+    Nothing
+
+-- | Derive the exact predicate, member-wise hypothesis, induction step, and
+-- binder-level result for one set-valued ambient binder. The selected binder
+-- is replaced by the newly introduced set variable; every other ambient
+-- binder remains a parameter.
+scopedSetInductionInstance
+    :: Natural
+    -> ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        , ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+scopedSetInductionInstance selected
+        (ScopedCheckedCore context TyProp property)
+    | binderTypeAt selected context == Just TySet =
+        Just (predicate, hypothesis, step, result)
+  where
+    abstractedProperty = abstractSelected 0 property
+    predicate =
+        ScopedCheckedCore
+            context
+            (TySet `TyArrow` TyProp)
+            (CLam TySet abstractedProperty)
+    hypothesis =
+        ScopedCheckedCore
+            context
+            TyProp
+            (CForall
+                TySet
+                (CImp
+                    (CApp
+                        (CApp
+                            (CIntrinsic Member)
+                            (CBound 0))
+                        (CBound (selected + 1)))
+                    abstractedProperty))
+    step =
+        ScopedCheckedCore
+            context
+            TyProp
+            (CForall
+                TySet
+                (CImp
+                    (abstractSelected
+                        0
+                        (scopedCoreTerm hypothesis))
+                    abstractedProperty))
+    result =
+        ScopedCheckedCore
+            context
+            TyProp
+            (CForall TySet abstractedProperty)
+
+    abstractSelected depth = \case
+        CBound index
+            | index == depth + selected ->
+                CBound depth
+            | index >= depth ->
+                CBound (index + 1)
+            | otherwise ->
+                CBound index
+        CGlobal global ->
+            CGlobal global
+        CIntrinsic intrinsic ->
+            CIntrinsic intrinsic
+        COpaqueInteger integer ->
+            COpaqueInteger integer
+        CApp function argument ->
+            CApp
+                (abstractSelected depth function)
+                (abstractSelected depth argument)
+        CLam binderType body ->
+            CLam binderType
+                (abstractSelected (depth + 1) body)
+        CFalsum ->
+            CFalsum
+        CImp premise conclusion ->
+            CImp
+                (abstractSelected depth premise)
+                (abstractSelected depth conclusion)
+        CEq operandType left right ->
+            CEq operandType
+                (abstractSelected depth left)
+                (abstractSelected depth right)
+        CForall binderType body ->
+            CForall binderType
+                (abstractSelected (depth + 1) body)
+scopedSetInductionInstance _selected _property =
+    Nothing
+
+-- | Close the nearest checked binder as one leading universal.
+closeScopedForall
+    :: ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+closeScopedForall
+        (ScopedCheckedCore (binderType : context) TyProp body) =
+    Just
+        (ScopedCheckedCore
+            context
+            TyProp
+            (CForall binderType body))
+closeScopedForall _scoped =
+    Nothing
+
+-- | Close the nearest checked binder as one leading existential.
+closeScopedExists
+    :: ScopedCheckedCore global
+    -> Maybe (ScopedCheckedCore global)
+closeScopedExists
+        (ScopedCheckedCore (binderType : context) TyProp body) =
+    Just
+        (ScopedCheckedCore
+            context
+            TyProp
+            (CImp
+                (CForall binderType (CImp body CFalsum))
+                CFalsum))
+closeScopedExists _scoped =
+    Nothing
+
+-- | Open one checked leading universal without rechecking its body.
+openScopedForall
+    :: ScopedCheckedCore global
+    -> Maybe (CoreType, ScopedCheckedCore global)
+openScopedForall
+        (ScopedCheckedCore context TyProp
+            (CForall binderType body)) =
+    Just
+        ( binderType
+        , ScopedCheckedCore
+            (binderType : context)
+            TyProp
+            body
+        )
+openScopedForall _scoped =
+    Nothing
+
+-- | Split one checked implication under its unchanged ambient context.
+openScopedImplication
+    :: ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+openScopedImplication
+        (ScopedCheckedCore context TyProp
+            (CImp premise conclusion)) =
+    Just
+        ( ScopedCheckedCore context TyProp premise
+        , ScopedCheckedCore context TyProp conclusion
+        )
+openScopedImplication _scoped =
+    Nothing
+
+-- | Open a checked proof assumption against the current goal.  Besides a
+-- direct implication antecedent, the source language historically permits
+-- either immediate side of one binary conjunction antecedent to be assumed
+-- first.  The other side remains the next implication antecedent.  This is a
+-- deliberately shallow structural rule: it neither flattens conjunctions nor
+-- treats disjunction as an eliminable assumption.
+openScopedAssumption
+    :: Eq global
+    => ScopedCheckedCore global
+    -> ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+openScopedAssumption supplied goal = do
+    (antecedent, conclusion) <- openScopedImplication goal
+    if supplied == antecedent
+        then pure (antecedent, conclusion)
+        else do
+            (left, right) <- splitScopedConjunction antecedent
+            if supplied == left
+                then do
+                    remaining <- implyScopedCore right conclusion
+                    pure (left, remaining)
+                else if supplied == right
+                    then do
+                        remaining <- implyScopedCore left conclusion
+                        pure (right, remaining)
+                    else Nothing
+
+splitScopedConjunction
+    :: ScopedCheckedCore global
+    -> Maybe
+        ( ScopedCheckedCore global
+        , ScopedCheckedCore global
+        )
+splitScopedConjunction
+        (ScopedCheckedCore context TyProp
+            (CImp (CImp left (CImp right CFalsum)) CFalsum)) =
+    Just
+        ( ScopedCheckedCore context TyProp left
+        , ScopedCheckedCore context TyProp right
+        )
+splitScopedConjunction _scoped =
+    Nothing
+
+closeScopedCore
+    :: ScopedCheckedCore global
+    -> Maybe (FrozenCheckedCore global)
+closeScopedCore
+        (ScopedCheckedCore [] coreType term) =
+    Just (FrozenCheckedCore coreType term)
+closeScopedCore ScopedCheckedCore{} =
+    Nothing
+
+-- | Substitute an outer-context term for index zero and remove that binder.
+instantiateCanonical
+    :: CanonicalTerm global
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+instantiateCanonical argument =
+    instantiateAt 0
+  where
+    instantiateAt depth = \case
+        CBound index
+            | index == depth ->
+                shiftCanonical depth 0 argument
+            | index > depth ->
+                CBound (index - 1)
+            | otherwise ->
+                CBound index
+        CGlobal global ->
+            CGlobal global
+        CIntrinsic intrinsic ->
+            CIntrinsic intrinsic
+        COpaqueInteger integer ->
+            COpaqueInteger integer
+        CApp function operand ->
+            CApp
+                (instantiateAt depth function)
+                (instantiateAt depth operand)
+        CLam binderType body ->
+            CLam binderType
+                (instantiateAt (depth + 1) body)
+        CFalsum ->
+            CFalsum
+        CImp premise conclusion ->
+            CImp
+                (instantiateAt depth premise)
+                (instantiateAt depth conclusion)
+        CEq operandType left right ->
+            CEq operandType
+                (instantiateAt depth left)
+                (instantiateAt depth right)
+        CForall binderType body ->
+            CForall binderType
+                (instantiateAt (depth + 1) body)
+
+mapCanonicalGlobals
+    :: (global -> global')
+    -> CanonicalTerm global
+    -> CanonicalTerm global'
+mapCanonicalGlobals transform = \case
+    CBound index ->
+        CBound index
+    CGlobal global ->
+        CGlobal (transform global)
+    CIntrinsic intrinsic ->
+        CIntrinsic intrinsic
+    COpaqueInteger integer ->
+        COpaqueInteger integer
+    CApp function argument ->
+        CApp
+            (mapCanonicalGlobals transform function)
+            (mapCanonicalGlobals transform argument)
+    CLam binderType body ->
+        CLam binderType
+            (mapCanonicalGlobals transform body)
+    CFalsum ->
+        CFalsum
+    CImp premise conclusion ->
+        CImp
+            (mapCanonicalGlobals transform premise)
+            (mapCanonicalGlobals transform conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (mapCanonicalGlobals transform left)
+            (mapCanonicalGlobals transform right)
+    CForall binderType body ->
+        CForall binderType
+            (mapCanonicalGlobals transform body)
+
+-- | Recheck a nameless term without exposing the checked wrapper constructor.
+checkCanonicalCore
+    :: (global -> Maybe CoreType)
+    -> CanonicalTerm global
+    -> Either CoreCheckError (FrozenCheckedCore global)
+checkCanonicalCore globalType term =
+    FrozenCheckedCore
+        <$> inferCanonicalCore globalType [] term
+        <*> pure term
+
+inferCanonicalCore
+    :: (global -> Maybe CoreType)
+    -> [CoreType]
+    -> CanonicalTerm global
+    -> Either CoreCheckError CoreType
+inferCanonicalCore globalType binders = \case
+    CBound index ->
+        maybe
+            (Left (UnboundCoreIndex index))
+            Right
+            (binderTypeAt index binders)
+    CGlobal global ->
+        maybe
+            (Left UnknownCoreGlobal)
+            Right
+            (globalType global)
+    CIntrinsic intrinsic ->
+        Right (coreIntrinsicType intrinsic)
+    COpaqueInteger{} ->
+        Right TySet
+    CApp function argument -> do
+        functionType <-
+            inferCanonicalCore globalType binders function
+        argumentType <-
+            inferCanonicalCore globalType binders argument
+        case functionType of
+            TyArrow expectedArgument resultType
+                | expectedArgument == argumentType ->
+                    Right resultType
+                | otherwise ->
+                    Left
+                        (ApplicationArgumentTypeMismatch
+                            expectedArgument
+                            argumentType)
+            other ->
+                Left (AppliedNonFunction other)
+    CLam binderType body -> do
+        bodyType <-
+            inferCanonicalCore
+                globalType
+                (binderType : binders)
+                body
+        Right (binderType `TyArrow` bodyType)
+    CFalsum ->
+        Right TyProp
+    CImp premise conclusion -> do
+        premiseType <-
+            inferCanonicalCore globalType binders premise
+        unless
+            (premiseType == TyProp)
+            (Left
+                (ImplicationOperandTypeMismatch
+                    premiseType))
+        conclusionType <-
+            inferCanonicalCore globalType binders conclusion
+        unless
+            (conclusionType == TyProp)
+            (Left
+                (ImplicationOperandTypeMismatch
+                    conclusionType))
+        Right TyProp
+    CEq operandType left right -> do
+        leftType <-
+            inferCanonicalCore globalType binders left
+        unless
+            (leftType == operandType)
+            (Left
+                (EqualityOperandTypeMismatch
+                    operandType
+                    leftType))
+        rightType <-
+            inferCanonicalCore globalType binders right
+        unless
+            (rightType == operandType)
+            (Left
+                (EqualityOperandTypeMismatch
+                    operandType
+                    rightType))
+        Right TyProp
+    CForall binderType body -> do
+        bodyType <-
+            inferCanonicalCore
+                globalType
+                (binderType : binders)
+                body
+        unless
+            (bodyType == TyProp)
+            (Left
+                (QuantifierBodyTypeMismatch bodyType))
+        Right TyProp
+
+binderTypeAt :: Natural -> [CoreType] -> Maybe CoreType
+binderTypeAt _index [] =
+    Nothing
+binderTypeAt 0 (binderType : _rest) =
+    Just binderType
+binderTypeAt index (_binderType : rest) =
+    binderTypeAt (index - 1) rest
+
+shiftCanonical
+    :: Natural
+    -> Natural
+    -> CanonicalTerm global
+    -> CanonicalTerm global
+shiftCanonical amount cutoff = \case
+    CBound index
+        | index >= cutoff ->
+            CBound (index + amount)
+        | otherwise ->
+            CBound index
+    CGlobal global ->
+        CGlobal global
+    CIntrinsic intrinsic ->
+        CIntrinsic intrinsic
+    COpaqueInteger integer ->
+        COpaqueInteger integer
+    CApp function argument ->
+        CApp
+            (shiftCanonical amount cutoff function)
+            (shiftCanonical amount cutoff argument)
+    CLam binderType body ->
+        CLam binderType
+            (shiftCanonical amount (cutoff + 1) body)
+    CFalsum ->
+        CFalsum
+    CImp premise conclusion ->
+        CImp
+            (shiftCanonical amount cutoff premise)
+            (shiftCanonical amount cutoff conclusion)
+    CEq operandType left right ->
+        CEq operandType
+            (shiftCanonical amount cutoff left)
+            (shiftCanonical amount cutoff right)
+    CForall binderType body ->
+        CForall binderType
+            (shiftCanonical amount (cutoff + 1) body)
+
+data FreezeError
+    = FreeLocalInClosedCore
+    deriving stock (Show, Eq)
+
+-- | Freeze a checked closed term in one traversal of the operational syntax.
+freezeClosed
+    :: CheckedCore global Void
+    -> Either FreezeError (FrozenCheckedCore global)
+freezeClosed (CheckedCore coreType syntax) =
+    FrozenCheckedCore coreType
+        <$> optimizedFreeze 0 rootResolver syntax
+  where
+    rootResolver _depth =
+        absurd
+
+-- | Bounded executable oracle for tests.  Production code uses 'freezeClosed'.
+referenceFreezeClosed
+    :: CheckedCore global Void
+    -> Either FreezeError (FrozenCheckedCore global)
+referenceFreezeClosed (CheckedCore coreType syntax) =
+    FrozenCheckedCore coreType
+        <$> referenceFreeze 0 rootResolver syntax
+  where
+    rootResolver _depth =
+        absurd
+
+type VariableResolver local global =
+    Natural
+    -> local
+    -> Either FreezeError (CanonicalTerm global)
+
+optimizedFreeze
+    :: Natural
+    -> VariableResolver local global
+    -> CoreSyntax global local
+    -> Either FreezeError (CanonicalTerm global)
+optimizedFreeze depth resolve = \case
+    CoreLocal local ->
+        resolve depth local
+    CoreGlobal global ->
+        Right (CGlobal global)
+    CoreIntrinsic intrinsic ->
+        Right (CIntrinsic intrinsic)
+    CoreOpaqueInteger integer ->
+        Right (COpaqueInteger integer)
+    CoreApply function argument ->
+        CApp
+            <$> optimizedFreeze depth resolve function
+            <*> optimizedFreeze depth resolve argument
+    CoreLambda binderType body ->
+        CLam binderType
+            <$> optimizedFreeze
+                (depth + 1)
+                (resolveGeneralized depth resolve)
+                (unscope body)
+    CoreFalsum ->
+        Right CFalsum
+    CoreImplication premise conclusion ->
+        CImp
+            <$> optimizedFreeze depth resolve premise
+            <*> optimizedFreeze depth resolve conclusion
+    CoreEquality operandType left right ->
+        CEq operandType
+            <$> optimizedFreeze depth resolve left
+            <*> optimizedFreeze depth resolve right
+    CoreForall binderType body ->
+        CForall binderType
+            <$> optimizedFreeze
+                (depth + 1)
+                (resolveGeneralized depth resolve)
+                (unscope body)
+  where
+    resolveGeneralized
+        :: Natural
+        -> VariableResolver local global
+        -> VariableResolver
+            (Var () (CoreSyntax global local))
+            global
+    resolveGeneralized binderLevel outerResolve currentDepth = \case
+        B () ->
+            Right
+                (CBound
+                    (currentDepth - binderLevel - 1))
+        F outerSyntax ->
+            optimizedFreeze
+                currentDepth
+                outerResolve
+                outerSyntax
+
+referenceFreeze
+    :: Natural
+    -> VariableResolver local global
+    -> CoreSyntax global local
+    -> Either FreezeError (CanonicalTerm global)
+referenceFreeze depth resolve = \case
+    CoreLocal local ->
+        resolve depth local
+    CoreGlobal global ->
+        Right (CGlobal global)
+    CoreIntrinsic intrinsic ->
+        Right (CIntrinsic intrinsic)
+    CoreOpaqueInteger integer ->
+        Right (COpaqueInteger integer)
+    CoreApply function argument ->
+        CApp
+            <$> referenceFreeze depth resolve function
+            <*> referenceFreeze depth resolve argument
+    CoreLambda binderType body ->
+        CLam binderType
+            <$> referenceFreeze
+                (depth + 1)
+                (resolveNormalized depth resolve)
+                (fromScope body)
+    CoreFalsum ->
+        Right CFalsum
+    CoreImplication premise conclusion ->
+        CImp
+            <$> referenceFreeze depth resolve premise
+            <*> referenceFreeze depth resolve conclusion
+    CoreEquality operandType left right ->
+        CEq operandType
+            <$> referenceFreeze depth resolve left
+            <*> referenceFreeze depth resolve right
+    CoreForall binderType body ->
+        CForall binderType
+            <$> referenceFreeze
+                (depth + 1)
+                (resolveNormalized depth resolve)
+                (fromScope body)
+  where
+    resolveNormalized
+        :: Natural
+        -> VariableResolver local global
+        -> VariableResolver (Var () local) global
+    resolveNormalized binderLevel outerResolve currentDepth = \case
+        B () ->
+            Right
+                (CBound
+                    (currentDepth - binderLevel - 1))
+        F outerLocal ->
+            outerResolve currentDepth outerLocal