Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 3936 deletions

diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs
deleted file mode 100644
index 47e3859..0000000
--- a/source/Checking/Exact.hs
+++ /dev/null
@@ -1,3936 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Direct compiler for the first exact monomorphic declaration family.
-module Checking.Exact
-    ( ExactLocalId
-    , exactLocalId
-    , exactLocalIdValue
-    , ExactBinderContext
-    , emptyExactBinderContext
-    , extendExactBinderContext
-    , extendExactAnonymousBinderContext
-    , exactBinderContextSupport
-    , exactBinderContextIndex
-    , PreparedExactProposition
-    , preparedExactPropositionCore
-    , prepareExactProposition
-    , prepareExactSymbolicBoundConstraints
-    , prepareExactSymbolicWitnessConstraints
-    , prepareExactNounWitnessConstraints
-    , PreparedExactSetExpression
-    , PreparedExactSetConstruction(..)
-    , preparedExactSetExpressionCore
-    , preparedExactSetExpressionConstruction
-    , prepareExactSetExpression
-    , PreparedExactLocalFunctionGraph
-    , preparedExactLocalFunctionGraphCore
-    , preparedExactLocalFunctionGraphDomain
-    , preparedExactLocalFunctionGraphMap
-    , prepareExactLocalFunctionGraph
-    , PreparedExactClaimEnvelope
-    , preparedExactClaimTarget
-    , preparedExactClaimVariables
-    , preparedExactClaimContext
-    , preparedExactClaimAntecedentCount
-    , prepareExactClaimEnvelope
-    , PreparedExactDeclaration
-    , preparedExactLocation
-    , preparedExactGlobalKey
-    , preparedExactObjectId
-    , preparedExactObject
-    , preparedExactSyntaxId
-    , preparedExactIsDefinition
-    , prepareExactDeclaration
-    , lowerPreparedExactBinding
-    , CheckedExactBindingAuthorization
-    , authorizeCheckedExactBinding
-    , PreparedExactStructure
-    , prepareExactStructure
-    , CheckedExactStructureAuthorization
-    , lowerPreparedExactStructure
-    , authorizeCheckedExactStructure
-    , PreparedExactSourceAxiom
-    , prepareExactSourceAxiom
-    , lowerPreparedExactSourceAxiom
-    , authorizeCheckedExactSourceAxiom
-    , ExactCompileError(..)
-    , exactCompileErrorLocation
-    , renderExactCompileError
-    ) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Declaration qualified as Declaration
-import Checking.Exact.Vocabulary
-import Checking.Identity
-import Checking.SetConstruction
-import Checking.Semantic
-import Felix.Cache.Codec
-import Felix.Module
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Interface (CanonicalLexicalEntry(..))
-import Syntax.Lexicon qualified as Lexicon
-
-import Control.Monad.Except (ExceptT)
-import Control.Monad.Except (MonadError, throwError)
-import Control.Monad.Except qualified as Except
-import Control.Monad (foldM, unless, when)
-import Control.Monad.State.Strict (StateT)
-import Control.Monad.State.Strict qualified as State
-import Data.ByteString (ByteString)
-import Data.Bifunctor (first)
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-import Data.Maybe (catMaybes)
-import Data.Set qualified as Set
-import Data.Text qualified as Text
-import Data.Vector (Vector)
-import Data.Vector qualified as Vector
-import Numeric.Natural (Natural)
-
-
--- | A disposable identity allocated in source order within one proof.
-newtype ExactLocalId = ExactLocalId Natural
-    deriving stock (Show, Eq, Ord)
-
-exactLocalId :: Natural -> ExactLocalId
-exactLocalId = ExactLocalId
-
-exactLocalIdValue :: ExactLocalId -> Natural
-exactLocalIdValue (ExactLocalId value) = value
-
-data ExactBinder = ExactBinder
-    !ExactLocalId
-    !(Maybe Raw.VarSymbol)
-    !CoreType
-    !(Maybe ExactStructureAnnotation)
-
-data ExactStructureAnnotation = ExactStructureAnnotation
-    !SemanticStructurePhrase
-    !(Maybe ObjectId)
-    !(Map.Map Raw.StructSymbol ObjectId)
-
--- | The active nearest-first binders of one exact proof scope.
-newtype ExactBinderContext = ExactBinderContext [ExactBinder]
-
-emptyExactBinderContext :: ExactBinderContext
-emptyExactBinderContext = ExactBinderContext []
-
-extendExactBinderContext
-    :: NonEmpty (ExactLocalId, Raw.VarSymbol)
-    -> ExactBinderContext
-    -> Either ExactCompileError ExactBinderContext
-extendExactBinderContext additions (ExactBinderContext initial) =
-    ExactBinderContext <$> foldM add initial (toList additions)
-  where
-    add binders (identity, variable)
-        | any (sameVariable variable) binders =
-            Left (ExactDuplicateLocalBinder (locate variable) variable)
-        | any (sameIdentity identity) binders =
-            Left (ExactDuplicateLocalIdentity (locate variable) identity)
-        | otherwise =
-            Right (ExactBinder identity (Just variable) TySet Nothing : binders)
-
-    sameVariable variable (ExactBinder _identity existing _coreType _structure) =
-        existing == Just variable
-
-    sameIdentity identity (ExactBinder existing _variable _coreType _structure) =
-        existing == identity
-
--- | Add one proof-owned binder which deliberately has no source-resolvable
--- spelling.  This is used for a nameless singular witness; it participates in
--- checked support and de Bruijn weakening but cannot shadow or be looked up by
--- a later source variable.
-extendExactAnonymousBinderContext
-    :: ExactLocalId
-    -> ExactBinderContext
-    -> Either ExactCompileError ExactBinderContext
-extendExactAnonymousBinderContext identity (ExactBinderContext binders)
-    | any sameIdentity binders =
-        Left (ExactDuplicateLocalIdentity Nowhere identity)
-    | otherwise =
-        Right
-            (ExactBinderContext
-                (ExactBinder identity Nothing TySet Nothing : binders))
-  where
-    sameIdentity (ExactBinder existing _variable _coreType _structure) =
-        existing == identity
-
-exactBinderContextSupport
-    :: ExactBinderContext
-    -> Vector (ExactLocalId, CoreType)
-exactBinderContextSupport (ExactBinderContext binders) =
-    Vector.fromList
-        [ (identity, coreType)
-        | ExactBinder identity _variable coreType _structure <- binders
-        ]
-
-exactBinderContextIndex
-    :: Raw.VarSymbol
-    -> ExactBinderContext
-    -> Maybe Natural
-exactBinderContextIndex variable (ExactBinderContext binders) =
-    go 0 binders
-  where
-    go _index [] =
-        Nothing
-    go index (ExactBinder _identity candidate _coreType _structure : rest)
-        | candidate == Just variable = Just index
-        | otherwise = go (index + 1) rest
-
-newtype PreparedExactProposition = PreparedExactProposition
-    (ScopedCheckedCore ObjectId)
-
-preparedExactPropositionCore
-    :: PreparedExactProposition
-    -> ScopedCheckedCore ObjectId
-preparedExactPropositionCore (PreparedExactProposition proposition) =
-    proposition
-
-data PreparedExactSetExpression = PreparedExactSetExpression
-    !(ScopedCheckedCore ObjectId)
-    !(Maybe PreparedExactSetConstruction)
-
-data PreparedExactSetConstruction
-    = PreparedUnconditionalSetConstruction
-        !(NamedSetConstruction ObjectId)
-    | PreparedRelationalSetConstruction
-        !(CheckedRelationalSetConstruction ObjectId)
-
-preparedExactSetExpressionCore
-    :: PreparedExactSetExpression
-    -> ScopedCheckedCore ObjectId
-preparedExactSetExpressionCore (PreparedExactSetExpression expression _construction) =
-    expression
-
-preparedExactSetExpressionConstruction
-    :: PreparedExactSetExpression
-    -> Maybe PreparedExactSetConstruction
-preparedExactSetExpressionConstruction
-        (PreparedExactSetExpression _expression construction) =
-    construction
-
--- | A checked replacement graph and the two checked arguments used to
--- specialize its foundation characteristic. This is transient proof
--- preparation data, not a declaration or durable object.
-data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph
-    !(ScopedCheckedCore ObjectId)
-    !(ScopedCheckedCore ObjectId)
-    !(ScopedCheckedCore ObjectId)
-
-preparedExactLocalFunctionGraphCore
-    :: PreparedExactLocalFunctionGraph
-    -> ScopedCheckedCore ObjectId
-preparedExactLocalFunctionGraphCore
-        (PreparedExactLocalFunctionGraph graph _domain _function) =
-    graph
-
-preparedExactLocalFunctionGraphDomain
-    :: PreparedExactLocalFunctionGraph
-    -> ScopedCheckedCore ObjectId
-preparedExactLocalFunctionGraphDomain
-        (PreparedExactLocalFunctionGraph _graph domain _function) =
-    domain
-
-preparedExactLocalFunctionGraphMap
-    :: PreparedExactLocalFunctionGraph
-    -> ScopedCheckedCore ObjectId
-preparedExactLocalFunctionGraphMap
-        (PreparedExactLocalFunctionGraph _graph _domain function) =
-    function
-
--- | One authoritative closed proposition prepared from a top-level claim
--- header and conclusion. The remaining fields are transient opening data for
--- the proof compiler.
-data PreparedExactClaimEnvelope = PreparedExactClaimEnvelope
-    !(ScopedCheckedCore ObjectId)
-    ![Raw.VarSymbol]
-    !ExactBinderContext
-    !Natural
-
-preparedExactClaimTarget
-    :: PreparedExactClaimEnvelope
-    -> ScopedCheckedCore ObjectId
-preparedExactClaimTarget
-        (PreparedExactClaimEnvelope target _variables _context _antecedents) =
-    target
-
-preparedExactClaimVariables
-    :: PreparedExactClaimEnvelope
-    -> [Raw.VarSymbol]
-preparedExactClaimVariables
-        (PreparedExactClaimEnvelope _target variables _context _antecedents) =
-    variables
-
-preparedExactClaimContext
-    :: PreparedExactClaimEnvelope
-    -> ExactBinderContext
-preparedExactClaimContext
-        (PreparedExactClaimEnvelope _target _variables context _antecedents) =
-    context
-
-preparedExactClaimAntecedentCount
-    :: PreparedExactClaimEnvelope
-    -> Natural
-preparedExactClaimAntecedentCount
-        (PreparedExactClaimEnvelope _target _variables _context antecedents) =
-    antecedents
-
-
-data ExactDeclarationFamily
-    = ExactSignature
-    | ExactAbbreviation
-    | ExactDefinition
-    deriving stock (Show, Eq, Ord)
-
-data PreparedExactDeclaration = PreparedExactDeclaration
-    !Location
-    !ExactDeclarationFamily
-    !SemanticGlobalKey
-    !SemanticGlobalTarget
-    !(Maybe AssertedObject)
-    !(Maybe SemanticName)
-    !(Maybe PreparedExactSetConstruction)
-    !DeclarationSyntaxId
-
-preparedExactLocation :: PreparedExactDeclaration -> Location
-preparedExactLocation
-        (PreparedExactDeclaration location _family _key _target _object _alias _construction _syntax) =
-    location
-
-preparedExactGlobalKey :: PreparedExactDeclaration -> SemanticGlobalKey
-preparedExactGlobalKey
-        (PreparedExactDeclaration _location _family key _target _object _alias _construction _syntax) =
-    key
-
-preparedExactObjectId :: PreparedExactDeclaration -> ObjectId
-preparedExactObjectId
-        (PreparedExactDeclaration _location _family _key target _object _alias _construction _syntax) =
-    semanticGlobalTargetObject target
-
-preparedExactObject
-    :: PreparedExactDeclaration
-    -> Maybe AssertedObject
-preparedExactObject
-        (PreparedExactDeclaration _location _family _key _target object _alias _construction _syntax) =
-    object
-
-preparedExactSyntaxId
-    :: PreparedExactDeclaration
-    -> DeclarationSyntaxId
-preparedExactSyntaxId
-        (PreparedExactDeclaration _location _family _key _target _object _alias _construction syntax) =
-    syntax
-
-preparedExactIsDefinition :: PreparedExactDeclaration -> Bool
-preparedExactIsDefinition
-        (PreparedExactDeclaration _location family _key _target _object _alias _construction _syntax) =
-    family == ExactDefinition
-
-preparedExactGlobalTarget
-    :: PreparedExactDeclaration
-    -> SemanticGlobalTarget
-preparedExactGlobalTarget
-        (PreparedExactDeclaration
-            _location _family _key target _object _alias _construction _syntax) =
-    target
-
-preparedDefinitionAlias
-    :: PreparedExactDeclaration
-    -> Maybe SemanticName
-preparedDefinitionAlias
-        (PreparedExactDeclaration
-            _location _family _key _target _object alias _construction _syntax) =
-    alias
-
-preparedDefinitionConstruction
-    :: PreparedExactDeclaration
-    -> Maybe PreparedExactSetConstruction
-preparedDefinitionConstruction
-        (PreparedExactDeclaration
-            _location _family _key _target _object _alias construction _syntax) =
-    construction
-
-data PreparedExactSourceAxiom = PreparedExactSourceAxiom
-    !Location
-    !SemanticName
-    !(ScopedCheckedCore ObjectId)
-    !DeclarationSyntaxId
-
-data PreparedExactStructureFact = PreparedExactStructureFact
-    !Location
-    !(FrozenCheckedCore ObjectId)
-    !SemanticName
-
-data PreparedExactStructure = PreparedExactStructure
-    !Location
-    ![AssertedObject]
-    !ObjectId
-    !SemanticStructureDescriptor
-    !SemanticName
-    ![PreparedExactStructureFact]
-    !DeclarationSyntaxId
-
-data CheckedExactStructureAuthorization =
-    CheckedExactStructureAuthorization
-        !ObjectId
-        ![(Location, Declaration.PreparedVampireObligation Void ())]
-
-data ExactCompileError
-    = ExactUnsupportedDeclaration !Location
-    | ExactUnsupportedDeclarationBody !Location
-    | ExactNonCanonicalSetDefinitionAnnotation !Location
-    | ExactGuardedTransparentDefinition !Location
-    | ExactGuardedOpaqueSignature !Location
-    | ExactDefinitionCombinedSymbolicAlias !Location
-    | ExactRelationalReplacementRequiresNamedDefinition !Location
-    | ExactDeclarationOccurrenceMissing !Location
-    | ExactDeclarationOccurrenceAmbiguous !Location
-    | ExactDeclarationHeadMismatch !Location
-    | ExactFixedSemanticCollision !Location !SemanticGlobalKey
-    | ExactGlobalAlreadyVisible !Location !SemanticGlobalKey
-    | ExactGlobalNotVisible !Location !SemanticGlobalKey
-    | ExactDuplicateParameter !Location !Raw.VarSymbol
-    | ExactDuplicateLocalBinder !Location !Raw.VarSymbol
-    | ExactDuplicateLocalIdentity !Location !ExactLocalId
-    | ExactFreeVariable !Location !Raw.VarSymbol
-    | ExactApplicationExpectedFunction !Location !CoreType
-    | ExactApplicationArgumentMismatch
-        !Location !CoreType !CoreType
-    | ExactExpressionExpectedSet !Location !CoreType
-    | ExactFormulaExpectedProposition !Location !CoreType
-    | ExactCoreCheckFailed !Location !CoreCheckError
-    | ExactObjectTypeMismatch !Location !CoreType !CoreType
-    | ExactUnsupportedHeaderAssumption !Location
-    | ExactQuantifiedTermRequiresPropositionContext !Location
-    | ExactStructureNotVisible !Location !SemanticStructurePhrase
-    | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase
-    | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol
-    | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol
-    | ExactStructureOperationAmbiguous
-        !Location !Raw.StructSymbol ![ObjectId]
-    | ExactContextualExpansionNotAvailable
-        !Location !SemanticGlobalKey
-    | ExactContextualRequirementConflict
-        !Location !Raw.StructSymbol !ObjectId !ObjectId
-    | ExactStructureOccurrenceMismatch !Location
-    | ExactStructureSelfParent !Location !SemanticStructurePhrase
-    | ExactStructureDuplicateParent !Location !SemanticStructurePhrase
-    | ExactStructureAlreadyVisible !Location !SemanticStructurePhrase
-    | ExactStructureDuplicateOperation !Location !Raw.StructSymbol
-    | ExactStructureOperationAlreadyInherited !Location !Raw.StructSymbol
-    | ExactStructureOperationConflict
-        !Location !Raw.StructSymbol
-        !SemanticStructurePhrase !SemanticStructurePhrase
-    | ExactStructureHasNoCarrier !Location !SemanticStructurePhrase
-    | ExactStructureDescriptorInvalid !Location !SemanticEnvironmentError
-    | ExactStructureObjectNotVisible !Location !ObjectId
-    deriving stock (Show, Eq)
-
-exactCompileErrorLocation :: ExactCompileError -> Location
-exactCompileErrorLocation = \case
-    ExactUnsupportedDeclaration location -> location
-    ExactUnsupportedDeclarationBody location -> location
-    ExactNonCanonicalSetDefinitionAnnotation location -> location
-    ExactGuardedTransparentDefinition location -> location
-    ExactGuardedOpaqueSignature location -> location
-    ExactDefinitionCombinedSymbolicAlias location -> location
-    ExactRelationalReplacementRequiresNamedDefinition location -> location
-    ExactDeclarationOccurrenceMissing location -> location
-    ExactDeclarationOccurrenceAmbiguous location -> location
-    ExactDeclarationHeadMismatch location -> location
-    ExactFixedSemanticCollision location _key -> location
-    ExactGlobalAlreadyVisible location _key -> location
-    ExactGlobalNotVisible location _key -> location
-    ExactDuplicateParameter location _parameter -> location
-    ExactDuplicateLocalBinder location _variable -> location
-    ExactDuplicateLocalIdentity location _identity -> location
-    ExactFreeVariable location _variable -> location
-    ExactApplicationExpectedFunction location _actual -> location
-    ExactApplicationArgumentMismatch location _expected _actual -> location
-    ExactExpressionExpectedSet location _actual -> location
-    ExactFormulaExpectedProposition location _actual -> location
-    ExactCoreCheckFailed location _failure -> location
-    ExactObjectTypeMismatch location _expected _actual -> location
-    ExactUnsupportedHeaderAssumption location -> location
-    ExactQuantifiedTermRequiresPropositionContext location -> location
-    ExactStructureNotVisible location _phrase -> location
-    ExactBaseStructureNotAssertable location _phrase -> location
-    ExactDuplicateStructureAnnotation location _variable -> location
-    ExactStructureOperationNotAvailable location _symbol -> location
-    ExactStructureOperationAmbiguous location _symbol _objects -> location
-    ExactContextualExpansionNotAvailable location _key -> location
-    ExactContextualRequirementConflict location _symbol _first _second -> location
-    ExactStructureOccurrenceMismatch location -> location
-    ExactStructureSelfParent location _phrase -> location
-    ExactStructureDuplicateParent location _phrase -> location
-    ExactStructureAlreadyVisible location _phrase -> location
-    ExactStructureDuplicateOperation location _symbol -> location
-    ExactStructureOperationAlreadyInherited location _symbol -> location
-    ExactStructureOperationConflict location _symbol _first _second -> location
-    ExactStructureHasNoCarrier location _phrase -> location
-    ExactStructureDescriptorInvalid location _failure -> location
-    ExactStructureObjectNotVisible location _object -> location
-
-renderExactCompileError :: ExactCompileError -> Text
-renderExactCompileError = \case
-    ExactUnsupportedDeclaration location ->
-        at location <> "this declaration is not yet supported by the typed checker"
-    ExactUnsupportedDeclarationBody location ->
-        at location <> "this source form is not yet supported by exact elaboration"
-    ExactNonCanonicalSetDefinitionAnnotation location ->
-        at location
-            <> "only the unmodified built-in noun `set` is a harmless definition annotation; "
-            <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported"
-    ExactGuardedTransparentDefinition location ->
-        at location
-            <> "a transparent definition cannot have a header assumption; "
-            <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported"
-    ExactGuardedOpaqueSignature location ->
-        at location
-            <> "an opaque signature cannot have a header assumption; "
-            <> "state the condition in a following explicit axiom"
-    ExactDefinitionCombinedSymbolicAlias location ->
-        at location
-            <> "a functional definition cannot declare a symbolic equivalent at the same time; "
-            <> "define the symbolic operator first, then define the functional phrase as an abbreviation applying it"
-    ExactRelationalReplacementRequiresNamedDefinition location ->
-        at location
-            <> "relational replacement is supported only as the outer body of a named definition"
-    ExactDeclarationOccurrenceMissing location ->
-        at location <> "the declaration has no associated syntax occurrence"
-    ExactDeclarationOccurrenceAmbiguous location ->
-        at location <> "the declaration has more than one semantic head"
-    ExactDeclarationHeadMismatch location ->
-        at location <> "the parsed declaration head does not match its syntax occurrence"
-    ExactFixedSemanticCollision location key ->
-        at location <> "the declaration collides with fixed semantics for "
-            <> shown key
-    ExactGlobalAlreadyVisible location key ->
-        at location <> "the global " <> shown key <> " is already declared"
-    ExactGlobalNotVisible location key ->
-        at location <> "the global " <> shown key <> " is not visible"
-    ExactDuplicateParameter location parameter ->
-        at location <> "the declaration parameter " <> shown parameter <> " is repeated"
-    ExactDuplicateLocalBinder location variable ->
-        at location <> "the proof binder " <> shown variable <> " is already active"
-    ExactDuplicateLocalIdentity location identity ->
-        at location <> "the proof-local identity " <> shown identity <> " is already active"
-    ExactFreeVariable location variable ->
-        at location <> "the exact source form contains the free variable " <> shown variable
-    ExactApplicationExpectedFunction location actual ->
-        at location <> "an application expected a function, but found " <> shown actual
-    ExactApplicationArgumentMismatch location expected actual ->
-        at location <> "an application expected " <> shown expected
-            <> ", but found " <> shown actual
-    ExactExpressionExpectedSet location actual ->
-        at location <> "an expression has type " <> shown actual <> " instead of Set"
-    ExactFormulaExpectedProposition location actual ->
-        at location <> "a formula has type " <> shown actual <> " instead of Prop"
-    ExactCoreCheckFailed location failure ->
-        at location <> "the checked declaration core is invalid: " <> shown failure
-    ExactObjectTypeMismatch location expected actual ->
-        at location <> "the declaration object has type " <> shown actual
-            <> " instead of " <> shown expected
-    ExactUnsupportedHeaderAssumption location ->
-        at location <> "this top-level header assumption is not yet supported by exact elaboration"
-    ExactQuantifiedTermRequiresPropositionContext location ->
-        at location
-            <> "a quantified term requires a containing proposition"
-    ExactStructureNotVisible location structurePhrase ->
-        at location <> "the structure " <> shown structurePhrase <> " is not visible"
-    ExactBaseStructureNotAssertable location structurePhrase ->
-        at location <> "the metadata-only structure " <> shown structurePhrase
-            <> " cannot be asserted"
-    ExactDuplicateStructureAnnotation location variable ->
-        at location <> "the structure binder " <> shown variable
-            <> " is annotated more than once"
-    ExactStructureOperationNotAvailable location symbol ->
-        at location <> "the structure operation " <> shown symbol
-            <> " is not available in the active structure scope"
-    ExactStructureOperationAmbiguous location symbol objects ->
-        at location <> "the structure operation " <> shown symbol
-            <> " is ambiguous between " <> shown objects
-    ExactContextualExpansionNotAvailable location key ->
-        at location <> "the contextual abbreviation " <> shown key
-            <> " has no compatible active structure"
-    ExactContextualRequirementConflict location symbol firstObject secondObject ->
-        at location <> "the contextual abbreviation requires incompatible "
-            <> shown symbol <> " operations " <> shown firstObject
-            <> " and " <> shown secondObject
-    ExactStructureOccurrenceMismatch location ->
-        at location <> "the structure syntax occurrences do not match the declaration"
-    ExactStructureSelfParent location structurePhrase ->
-        at location <> "the structure " <> shown structurePhrase
-            <> " cannot inherit from itself"
-    ExactStructureDuplicateParent location structurePhrase ->
-        at location <> "the parent structure " <> shown structurePhrase
-            <> " is repeated"
-    ExactStructureAlreadyVisible location structurePhrase ->
-        at location <> "the structure " <> shown structurePhrase
-            <> " is already declared"
-    ExactStructureDuplicateOperation location symbol ->
-        at location <> "the structure operation " <> shown symbol
-            <> " is repeated"
-    ExactStructureOperationAlreadyInherited location symbol ->
-        at location <> "the structure operation " <> shown symbol
-            <> " is already inherited"
-    ExactStructureOperationConflict location symbol firstOrigin secondOrigin ->
-        at location <> "the inherited structure operation " <> shown symbol
-            <> " conflicts between " <> shown firstOrigin
-            <> " and " <> shown secondOrigin
-    ExactStructureHasNoCarrier location structurePhrase ->
-        at location <> "the structure " <> shown structurePhrase
-            <> " does not inherit the base carrier operation"
-    ExactStructureDescriptorInvalid location _failure ->
-        at location <> "the canonical structure descriptor is inconsistent"
-    ExactStructureObjectNotVisible location identity ->
-        at location <> "the structure fact mentions unavailable object "
-            <> shown identity
-  where
-    at location = locationToText location <> ": "
-    shown :: Show value => value -> Text
-    shown = Text.pack . show
-
-data ElaborationState = ElaborationState
-    { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural)
-    -- Counts every active de Bruijn binder, including anonymous and
-    -- contextual binders which have no entry in 'elaborationBinders'.
-    , elaborationBinderDepth :: !Natural
-    , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation)
-    , elaborationGlobals :: !(Map.Map ObjectId CoreType)
-    , elaborationContextualBinder :: !(Maybe Natural)
-    , elaborationContextualRequirements
-        :: !(Map.Map Raw.StructSymbol ObjectId)
-    }
-
-type Elaborate =
-    StateT
-        ElaborationState
-        (ExceptT ExactCompileError (Declaration.LoweringDriver))
-
-data PreparedHead = PreparedHead
-    !SemanticGlobalKey
-    ![Raw.VarSymbol]
-    !CoreType
-
-data PreparedBody
-    = OpaqueBody
-    | TransparentBody
-        !(CanonicalTerm ObjectId)
-        !(Maybe PreparedExactSetConstruction)
-    | ContextualTransparentBody
-        !(Map.Map Raw.StructSymbol ObjectId)
-        !(CanonicalTerm ObjectId)
-
-data CompiledBody = CompiledBody
-    !(CanonicalTerm ObjectId)
-    !(Maybe CompiledNamedSetConstruction)
-
-data CompiledNamedSetConstruction
-    = CompiledSeparationConstruction
-        !(CanonicalTerm ObjectId)
-        !(CanonicalTerm ObjectId)
-    | CompiledFunctionalReplacementConstruction
-        !(NonEmpty (CanonicalTerm ObjectId))
-        !(CanonicalTerm ObjectId)
-        !(Maybe (CanonicalTerm ObjectId))
-    | CompiledRelationalReplacementConstruction
-        !(CanonicalTerm ObjectId)
-        !(CanonicalTerm ObjectId)
-
-prepareExactProposition
-    :: ExactBinderContext
-    -> Raw.Stmt
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactProposition)
-prepareExactProposition context statement =
-    prepareExactPropositionTerm
-        context
-        (locate statement)
-        (compileStatement statement)
-
--- | Compile the source bound of already-opened symbolic binders.  This is the
--- shared checked constraint seam used by quantified statements and proof
--- binders, so relation signs, carrier casts, and global occurrences are
--- elaborated exactly once by the ordinary expression compiler.
-prepareExactSymbolicBoundConstraints
-    :: ExactBinderContext
-    -> NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactProposition)
-prepareExactSymbolicBoundConstraints context variables bound =
-    prepareExactPropositionTerm
-        context
-        (case bound of
-            Raw.Unbounded -> locate (NonEmpty.head variables)
-            _ -> locate bound)
-        (logicalConjunction
-            <$> compileSymbolicBoundConstraintList variables bound)
-
--- | Compile the opened body used by a symbolic existential witness.  Its
--- grouping is deliberately identical to 'SymbolicExists': all bound
--- constraints form the existential restriction and the stated proposition is
--- its body.
-prepareExactSymbolicWitnessConstraints
-    :: ExactBinderContext
-    -> NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Raw.Stmt
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactProposition)
-prepareExactSymbolicWitnessConstraints context variables bound statement =
-    prepareExactPropositionTerm context (locate statement) do
-        constraints <-
-            logicalConjunction
-                <$> compileSymbolicBoundConstraintList variables bound
-        body <- compileStatement statement
-        pure
-            (if constraints == logicalTruth
-                then body
-                else logicalAnd constraints body)
-
--- | Compile the checked constraint of an already-opened noun witness.  Named
--- binders are resolved normally; a nameless singular noun uses the nearest
--- anonymous binder and therefore introduces no lookup spelling.
-prepareExactNounWitnessConstraints
-    :: ExactBinderContext
-    -> Raw.NounPhrase []
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactProposition)
-prepareExactNounWitnessConstraints context nounPhrase =
-    case nounPhrase of
-        Raw.NounPhrase left noun variables right suchThat ->
-            prepareExactPropositionTerm context (locate noun) do
-                subjects <-
-                    case NonEmpty.nonEmpty variables of
-                        Just binders ->
-                            toList
-                                <$> traverse compileIntroducedVariable binders
-                        Nothing ->
-                            pure [CBound 0]
-                compileNounPhraseConstraints
-                    subjects left noun right suchThat
-
-prepareExactPropositionTerm
-    :: ExactBinderContext
-    -> Location
-    -> Elaborate (CanonicalTerm ObjectId)
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactProposition)
-prepareExactPropositionTerm context location compile =
-    Except.runExceptT do
-        let initialElaboration = initialElaborationState context
-        (term, finalElaboration) <-
-            State.runStateT compile initialElaboration
-        checked <-
-            either
-                (Except.throwError . ExactCoreCheckFailed location)
-                pure
-                (checkScopedCanonicalCore
-                    (`Map.lookup` elaborationGlobals finalElaboration)
-                    (binderTypes context)
-                    term)
-        unless (scopedCoreType checked == TyProp)
-            (Except.throwError
-                (ExactFormulaExpectedProposition
-                    location
-                    (scopedCoreType checked)))
-        pure (PreparedExactProposition checked)
-
-prepareExactSetExpression
-    :: ExactBinderContext
-    -> Raw.Expr
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactSetExpression)
-prepareExactSetExpression context expression =
-    Except.runExceptT do
-        let initialElaboration = initialElaborationState context
-        (compiled, finalElaboration) <-
-            State.runStateT
-                (compileNamedSetExpression expression)
-                initialElaboration
-        let CompiledBody term rawConstruction = compiled
-        checked <-
-            either
-                (Except.throwError
-                    . ExactCoreCheckFailed (locate expression))
-                pure
-                (checkScopedCanonicalCore
-                    (`Map.lookup` elaborationGlobals finalElaboration)
-                    (binderTypes context)
-                    term)
-        unless (scopedCoreType checked == TySet)
-            (Except.throwError
-                (ExactExpressionExpectedSet
-                    (locate expression)
-                    (scopedCoreType checked)))
-        construction <-
-            Except.liftEither
-                (traverse
-                    (checkCompiledNamedSetConstruction
-                        (`Map.lookup` elaborationGlobals finalElaboration)
-                        (binderTypes context))
-                    rawConstruction)
-        traverse_
-            (\checkedConstruction ->
-                unless
-                    (preparedSetConstructionTerm checkedConstruction == checked)
-                    (impossible
-                        "exact named construction disagrees with its checked expression"))
-            construction
-        pure (PreparedExactSetExpression checked construction)
-
-checkCompiledNamedSetConstruction
-    :: (ObjectId -> Maybe CoreType)
-    -> [CoreType]
-    -> CompiledNamedSetConstruction
-    -> Either ExactCompileError PreparedExactSetConstruction
-checkCompiledNamedSetConstruction globalType context = \case
-    CompiledSeparationConstruction bound predicate -> do
-        checkedBound <- checkAt context TySet bound
-        checkedPredicate <- checkAt (TySet : context) TyProp predicate
-        maybe
-            (Left
-                (ExactCoreCheckFailed
-                    Nowhere
-                    (ExpectedCoreType TySet TyProp)))
-            (Right . PreparedUnconditionalSetConstruction)
-            (checkedSeparationConstruction
-                globalType checkedBound checkedPredicate)
-    CompiledFunctionalReplacementConstruction domains value condition -> do
-        let domainList = NonEmpty.toList domains
-            fullContext = replicate (length domainList) TySet <> context
-        checkedDomains <-
-            traverse
-                (\(depth, domain) ->
-                    checkAt
-                        (replicate depth TySet <> context)
-                        TySet
-                        domain)
-                (zip [0..] domainList)
-        checkedValue <- checkAt fullContext TySet value
-        checkedCondition <- traverse (checkAt fullContext TyProp) condition
-        maybe
-            (Left
-                (ExactCoreCheckFailed
-                    Nowhere
-                    (ExpectedCoreType TySet TyProp)))
-            (Right . PreparedUnconditionalSetConstruction)
-            (checkedFunctionalReplacementConstruction
-                globalType
-                (NonEmpty.fromList checkedDomains)
-                checkedValue
-                checkedCondition)
-    CompiledRelationalReplacementConstruction domain relation -> do
-        checkedDomain <- checkAt context TySet domain
-        checkedRelation <- checkAt (TySet : TySet : context) TyProp relation
-        maybe
-            (Left
-                (ExactCoreCheckFailed
-                    Nowhere
-                    (ExpectedCoreType TySet TyProp)))
-            (Right . PreparedRelationalSetConstruction)
-            (checkedRelationalReplacementConstruction
-                globalType checkedDomain checkedRelation)
-  where
-    checkAt expectedContext expectedType term = do
-        checked <-
-            first
-                (ExactCoreCheckFailed Nowhere)
-                (checkScopedCanonicalCore globalType expectedContext term)
-        unless
-            (scopedCoreType checked == expectedType)
-            (Left
-                (ExactCoreCheckFailed
-                    Nowhere
-                    (ExpectedCoreType
-                        expectedType
-                        (scopedCoreType checked))))
-        pure checked
-
-preparedSetConstructionTerm
-    :: PreparedExactSetConstruction
-    -> ScopedCheckedCore ObjectId
-preparedSetConstructionTerm = \case
-    PreparedUnconditionalSetConstruction construction ->
-        namedSetConstructionTerm construction
-    PreparedRelationalSetConstruction construction ->
-        relationalSetConstructionTerm construction
-
-preparedSetConstructionClosedBody
-    :: PreparedExactSetConstruction
-    -> FrozenCheckedCore ObjectId
-preparedSetConstructionClosedBody = \case
-    PreparedUnconditionalSetConstruction construction ->
-        namedSetConstructionClosedBody construction
-    PreparedRelationalSetConstruction construction ->
-        relationalSetConstructionClosedBody construction
-
-prepareExactLocalFunctionGraph
-    :: Location
-    -> ExactBinderContext
-    -> ExactBinderContext
-    -> Raw.Expr
-    -> Raw.Expr
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactLocalFunctionGraph)
-prepareExactLocalFunctionGraph
-        location context argumentContext domainExpression valueExpression =
-    Except.runExceptT do
-        domain <-
-            preparedExactSetExpressionCore
-                <$> ( Except.lift
-                        (prepareExactSetExpression context domainExpression)
-                        >>= Except.liftEither
-                    )
-        value <-
-            preparedExactSetExpressionCore
-                <$> ( Except.lift
-                        (prepareExactSetExpression
-                            argumentContext valueExpression)
-                        >>= Except.liftEither
-                    )
-        pair <- prepareOrderedPair
-        case scopedReplacementGraph pair domain value of
-            Just (graph, checkedDomain, function) ->
-                pure
-                    (PreparedExactLocalFunctionGraph
-                        graph checkedDomain function)
-            Nothing ->
-                impossible
-                    "checked local-function components did not form a replacement graph"
-  where
-    prepareOrderedPair = do
-        let initialElaboration = initialElaborationState context
-            key =
-                SemanticExpressionFunction
-                    (Raw.mixfixPattern Raw.PairSymbol)
-            expected = TySet `TyArrow` (TySet `TyArrow` TySet)
-        ((term, actual), finalElaboration) <-
-            State.runStateT
-                (applyResolvedTyped location key [])
-                initialElaboration
-        unless (actual == expected)
-            (Except.throwError
-                (ExactObjectTypeMismatch location expected actual))
-        either
-            (Except.throwError . ExactCoreCheckFailed location)
-            pure
-            (checkScopedCanonicalCore
-                (`Map.lookup` elaborationGlobals finalElaboration)
-                (binderTypes context)
-                term)
-
-prepareExactClaimEnvelope
-    :: [Raw.Asm]
-    -> Raw.Stmt
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactClaimEnvelope)
-prepareExactClaimEnvelope assumptions statement =
-    discover [] emptyExactBinderContext
-  where
-    discover variables context = do
-        attempted <- prepareExactClaimAttempt context assumptions statement
-        case attempted of
-            Left (ExactFreeVariable _location variable)
-                | variable `elem` variables ->
-                    impossible
-                        "exact claim discovery repeated an active free variable"
-                | otherwise ->
-                    case extendExactBinderContext
-                            ( ( exactLocalId
-                                    (fromIntegral (length variables))
-                              , variable
-                              ) :| []
-                            )
-                            context of
-                        Left failure ->
-                            pure (Left failure)
-                        Right extended ->
-                            discover (variables <> [variable]) extended
-            Left failure ->
-                pure (Left failure)
-            Right (target, antecedentCount, structures) ->
-                pure
-                    (Right
-                        (PreparedExactClaimEnvelope
-                            target
-                            variables
-                            (annotateBinderContext structures context)
-                            antecedentCount))
-
-prepareExactClaimAttempt
-    :: ExactBinderContext
-    -> [Raw.Asm]
-    -> Raw.Stmt
-    -> Declaration.LoweringDriver
-        (Either
-            ExactCompileError
-            ( ScopedCheckedCore ObjectId
-            , Natural
-            , Map.Map Natural ExactStructureAnnotation
-            ))
-prepareExactClaimAttempt context assumptions statement =
-    Except.runExceptT do
-        let initialElaboration = initialElaborationState context
-        ((antecedents, conclusion), finalElaboration) <-
-            State.runStateT
-                ( do
-                    antecedents <-
-                        concat <$> traverse compileHeaderAssumption assumptions
-                    conclusion <- compileStatement statement
-                    pure (antecedents, conclusion)
-                )
-                initialElaboration
-        checkedAntecedents <-
-            traverse
-                (uncurry
-                    (checkEnvelopeProposition
-                        finalElaboration
-                        context))
-                antecedents
-        checkedConclusion <-
-            checkEnvelopeProposition
-                finalElaboration
-                context
-                (locate statement)
-                conclusion
-        let implication =
-                foldr
-                    (\antecedent continuation ->
-                        fromMaybe
-                            (impossible
-                                "checked claim antecedents have unequal contexts")
-                            (implyScopedCore antecedent continuation))
-                    checkedConclusion
-                    checkedAntecedents
-            closed = closeClaimBinders implication
-        unless (null (scopedCoreContext closed))
-            (impossible "exact claim closure retained a binder")
-        pure
-            ( closed
-            , fromIntegral (length antecedents)
-            , elaborationStructures finalElaboration
-            )
-
-checkEnvelopeProposition
-    :: ElaborationState
-    -> ExactBinderContext
-    -> Location
-    -> CanonicalTerm ObjectId
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        (ScopedCheckedCore ObjectId)
-checkEnvelopeProposition elaboration context location term = do
-    checked <-
-        either
-            (Except.throwError . ExactCoreCheckFailed location)
-            pure
-            (checkScopedCanonicalCore
-                (`Map.lookup` elaborationGlobals elaboration)
-                (binderTypes context)
-                term)
-    unless (scopedCoreType checked == TyProp)
-        (Except.throwError
-            (ExactFormulaExpectedProposition
-                location
-                (scopedCoreType checked)))
-    pure checked
-
-closeClaimBinders
-    :: ScopedCheckedCore global
-    -> ScopedCheckedCore global
-closeClaimBinders scoped =
-    case scopedCoreContext scoped of
-        [] -> scoped
-        _binder : _remaining ->
-            closeClaimBinders
-                (fromMaybe
-                    (impossible
-                        "a checked claim binder could not be closed")
-                    (closeScopedForall scoped))
-
-binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural
-binderIndices (ExactBinderContext binders) =
-    Map.fromList
-        [ (variable, fromIntegral index)
-        | (index, ExactBinder _identity (Just variable) _coreType _structure) <-
-            zip [0 :: Int ..] binders
-        ]
-
-binderStructures
-    :: ExactBinderContext
-    -> Map.Map Natural ExactStructureAnnotation
-binderStructures (ExactBinderContext binders) =
-    Map.fromList
-        [ (fromIntegral index, structure)
-        | (index, ExactBinder _identity _variable _coreType (Just structure)) <-
-            zip [0 :: Int ..] binders
-        ]
-
-binderTypes :: ExactBinderContext -> [CoreType]
-binderTypes (ExactBinderContext binders) =
-    [ coreType
-    | ExactBinder _identity _variable coreType _structure <- binders
-    ]
-
-initialElaborationState :: ExactBinderContext -> ElaborationState
-initialElaborationState context =
-    ElaborationState
-        { elaborationBinders = binderIndices context
-        , elaborationBinderDepth =
-            fromIntegral (length (binderTypes context))
-        , elaborationStructures = binderStructures context
-        , elaborationGlobals = mempty
-        , elaborationContextualBinder = Nothing
-        , elaborationContextualRequirements = mempty
-        }
-
-annotateBinderContext
-    :: Map.Map Natural ExactStructureAnnotation
-    -> ExactBinderContext
-    -> ExactBinderContext
-annotateBinderContext structures (ExactBinderContext binders) =
-    ExactBinderContext
-        [ ExactBinder identity variable coreType
-            (Map.lookup (fromIntegral index) structures)
-        | (index, ExactBinder identity variable coreType _old) <-
-            zip [0 :: Int ..] binders
-        ]
-
-compileHeaderAssumption
-    :: Raw.Asm
-    -> Elaborate [(Location, CanonicalTerm ObjectId)]
-compileHeaderAssumption = \case
-    Raw.AsmSuppose statement -> do
-        proposition <- compileStatement statement
-        pure [(locate statement, proposition)]
-    Raw.AsmLetNoun variables nounPhrase
-        | exactSetNounPhrase nounPhrase -> do
-            traverse_ compileIntroducedVariable variables
-            pure []
-        | otherwise -> do
-            subjects <- traverse compileIntroducedVariable variables
-            constraints <-
-                traverse (`compileNounPhraseMaybe` nounPhrase) subjects
-            pure
-                [ (locate variable, constraint)
-                | (variable, constraint) <-
-                    zip (toList variables) (toList constraints)
-                ]
-    Raw.AsmLetIn variables domain -> do
-        variableTerms <- traverse compileIntroducedVariable variables
-        domainTerm <- compileExpressionAsSet domain
-        traverse
-            (\(variable, variableTerm) -> do
-                proposition <-
-                    compileMembership
-                        (locate domain)
-                        Raw.Positive
-                        variableTerm
-                        domainTerm
-                pure (locate variable, proposition))
-            (zip (toList variables) (toList variableTerms))
-    Raw.AsmLetEq variable expression -> do
-        variableTerm <- compileIntroducedVariable variable
-        expressionTerm <- compileExpressionAsSet expression
-        pure
-            [ ( locate variable
-              , CEq TySet variableTerm expressionTerm
-              )
-            ]
-    Raw.AsmLetThe variable _function ->
-        Except.throwError
-            (ExactUnsupportedHeaderAssumption (locate variable))
-    Raw.AsmLetStruct variable structure -> do
-        subject <- compileIntroducedVariable variable
-        annotation <-
-            resolveStructureAnnotation
-                (locate variable)
-                structure
-        index <-
-            maybe
-                (impossible "an introduced structure variable is unbound")
-                pure
-                =<< Map.lookup variable <$> State.gets elaborationBinders
-        existing <- State.gets (Map.lookup index . elaborationStructures)
-        when
-            (isJust existing)
-            (Except.throwError
-                (ExactDuplicateStructureAnnotation
-                    (locate variable) variable))
-        State.modify' \state ->
-            state
-                { elaborationStructures =
-                    Map.insert index annotation
-                        (elaborationStructures state)
-                }
-        predicate <-
-            maybe
-                (impossible "an assertable structure has no predicate")
-                pure
-                (structureAnnotationPredicate annotation)
-        recordExactGlobal
-            predicate
-            (TyArrow TySet TyProp)
-        pure
-            [ ( locate variable
-              , CApp
-                    (CGlobal predicate)
-                    subject
-              )
-            ]
-
-compileIntroducedVariable
-    :: Raw.VarSymbol
-    -> Elaborate (CanonicalTerm ObjectId)
-compileIntroducedVariable variable =
-    compileExpressionAsSet (Raw.ExprVar variable)
-
-resolveStructureAnnotation
-    :: Location
-    -> Raw.StructPhrase
-    -> Elaborate ExactStructureAnnotation
-resolveStructureAnnotation location rawPhrase = do
-    let structurePhrase = semanticStructurePhrase rawPhrase
-    resolved <-
-        State.lift
-            (Except.lift
-                (Declaration.resolveVisibleStructureLowering structurePhrase))
-    structure <-
-        maybe
-            (Except.throwError
-                (ExactStructureNotVisible location structurePhrase))
-            pure
-            resolved
-    predicate <-
-        maybe
-            (Except.throwError
-                (ExactBaseStructureNotAssertable location structurePhrase))
-            pure
-            (Declaration.resolvedStructurePredicate structure)
-    pure
-        (ExactStructureAnnotation
-            structurePhrase
-            (Just predicate)
-            (Declaration.resolvedStructureOperations structure))
-
-structureAnnotationPredicate :: ExactStructureAnnotation -> Maybe ObjectId
-structureAnnotationPredicate
-        (ExactStructureAnnotation _ predicate _operations) =
-    predicate
-
-structureAnnotationOperation
-    :: Raw.StructSymbol
-    -> ExactStructureAnnotation
-    -> Maybe ObjectId
-structureAnnotationOperation symbol
-        (ExactStructureAnnotation _phrase _predicate operations) =
-    Map.lookup symbol operations
-
-recordExactGlobal :: ObjectId -> CoreType -> Elaborate ()
-recordExactGlobal identity coreType = do
-    existing <- State.gets (Map.lookup identity . elaborationGlobals)
-    case existing of
-        Nothing ->
-            State.modify' \state ->
-                state
-                    { elaborationGlobals =
-                        Map.insert identity coreType
-                            (elaborationGlobals state)
-                    }
-        Just actual
-            | actual == coreType -> pure ()
-            | otherwise ->
-                impossible "one exact global acquired two checked types"
-
-prepareExactSourceAxiom
-    :: Raw.Block
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactSourceAxiom)
-prepareExactSourceAxiom = \case
-    Raw.BlockAxiom
-            location _title (Raw.Marker marker)
-            (Raw.Axiom assumptions statement) -> do
-            prepared <- prepareExactClaimEnvelope assumptions statement
-            pure do
-                envelope <- prepared
-                let core = preparedExactClaimTarget envelope
-                    alias = semanticName marker
-                unless (null (scopedCoreContext core))
-                    (Left (ExactUnsupportedDeclarationBody location))
-                pure
-                    (PreparedExactSourceAxiom
-                        location
-                        alias
-                        core
-                        (declarationSyntaxId
-                            (encodePreparedSourceAxiom core alias)))
-    block ->
-        pure (Left (ExactUnsupportedDeclaration (locate block)))
-
-lowerPreparedExactSourceAxiom
-    :: PreparedExactSourceAxiom
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration ()))
-lowerPreparedExactSourceAxiom
-        (PreparedExactSourceAxiom _location alias target syntax) =
-    fmap
-        (\spec ->
-            Declaration.checkedCompiledDeclaration
-                syntax [] [] [] []
-                [ Declaration.checkedCandidate
-                    spec
-                    Declaration.checkedSourceAxiomPlanning
-                    :| []
-                ]
-                ())
-        <$> Declaration.prepareCandidateSpecLowering
-            [] target SearchEligible [alias]
-
-authorizeCheckedExactSourceAxiom
-    :: ()
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedExactSourceAxiom () = \case
-    [candidate :| []] ->
-        Declaration.authorizeSourceAxiomCandidate candidate
-    stages ->
-        Declaration.failDeclaration
-            (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                1 (length stages))
-
-prepareExactDeclaration
-    :: Raw.Block
-    -> [CanonicalLexicalEntry]
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactDeclaration)
-prepareExactDeclaration block entries =
-    Except.runExceptT do
-        entry <-
-            case entries of
-                [] -> Except.throwError
-                    (ExactDeclarationOccurrenceMissing (locate block))
-                [single] -> pure single
-                _ -> Except.throwError
-                    (ExactDeclarationOccurrenceAmbiguous (locate block))
-        key <-
-            maybe
-                (Except.throwError
-                    (ExactUnsupportedDeclaration (locate block)))
-                pure
-                (semanticGlobalKeyFromLexicalEntry entry)
-        when
-            (isJust (fixedSemanticMeaning key))
-            (Except.throwError
-                (ExactFixedSemanticCollision (locate block) key))
-        visible <- Except.lift
-            (Declaration.resolveVisibleGlobalLowering key)
-        when
-            (isJust visible)
-            (Except.throwError
-                (ExactGlobalAlreadyVisible (locate block) key))
-        (head', family, rawBody) <-
-            prepareHead block key
-        slot <- Except.lift Declaration.nextDeclarationSlotLowering
-        theory <- Except.lift Declaration.currentTheoryLowering
-        (body, globals) <-
-            case rawBody of
-                Nothing -> pure (OpaqueBody, Map.empty)
-                Just buildBody -> do
-                    let initialElaboration =
-                            ElaborationState
-                                { elaborationBinders = mempty
-                                , elaborationBinderDepth = 0
-                                , elaborationStructures = mempty
-                                , elaborationGlobals = mempty
-                                , elaborationContextualBinder = Nothing
-                                , elaborationContextualRequirements = mempty
-                                }
-                    (CompiledBody canonical rawConstruction, finalElaboration) <-
-                        State.runStateT buildBody initialElaboration
-                    let PreparedHead _semanticKey parameters _coreType = head'
-                    construction <-
-                        Except.liftEither
-                            (traverse
-                                (checkCompiledNamedSetConstruction
-                                    (`Map.lookup`
-                                        elaborationGlobals finalElaboration)
-                                    (replicate (length parameters) TySet))
-                                rawConstruction)
-                    traverse_
-                        (\checkedConstruction ->
-                            unless
-                                (frozenCoreTerm
-                                    (preparedSetConstructionClosedBody
-                                        checkedConstruction)
-                                    == canonical)
-                                (impossible
-                                    "exact named construction disagrees with its transparent body"))
-                        construction
-                    let requirements =
-                            elaborationContextualRequirements finalElaboration
-                        body
-                            | Map.null requirements =
-                                TransparentBody canonical construction
-                            | family == ExactAbbreviation =
-                                ContextualTransparentBody
-                                    requirements
-                                    (CLam TySet canonical)
-                            | otherwise =
-                                impossible
-                                    "a non-abbreviation acquired contextual requirements"
-                    pure (body, elaborationGlobals finalElaboration)
-        let PreparedHead semanticKey _parameters coreType = head'
-        unless (semanticKey == key)
-            (Except.throwError
-                (ExactDeclarationHeadMismatch (locate block)))
-        (target, content) <-
-            case body of
-                OpaqueBody -> do
-                    let seed =
-                            opaqueDeclarationSeed
-                                (declarationSlotModule slot)
-                                (declarationSlotOrdinal slot)
-                                SignatureDeclaration
-                                (generatedObjectSlot 0)
-                        content' =
-                            OpaqueObjectContent theory seed coreType
-                        identity = opaqueObjectId theory seed coreType
-                    pure (GlobalReference identity, content')
-                TransparentBody canonical _construction -> do
-                    checked <-
-                        either
-                            (Except.throwError
-                                . ExactCoreCheckFailed (locate block))
-                            pure
-                            (checkCanonicalCore
-                                (`Map.lookup` globals)
-                                canonical)
-                    unless
-                        (frozenCoreType checked == coreType)
-                        (Except.throwError
-                            (ExactObjectTypeMismatch
-                                (locate block)
-                                coreType
-                                (frozenCoreType checked)))
-                    let content' =
-                            TransparentObjectContent
-                                theory
-                                coreType
-                                canonical
-                    let identity =
-                            transparentObjectId theory coreType canonical
-                        semanticTarget =
-                            case family of
-                                ExactAbbreviation ->
-                                    TransparentExpansion identity
-                                ExactDefinition -> GlobalReference identity
-                                ExactSignature ->
-                                    impossible
-                                        "a signature acquired a transparent body"
-                    pure (semanticTarget, content')
-                ContextualTransparentBody requirements canonical -> do
-                    let contextualType = TyArrow TySet coreType
-                    checked <-
-                        either
-                            (Except.throwError
-                                . ExactCoreCheckFailed (locate block))
-                            pure
-                            (checkCanonicalCore
-                                (`Map.lookup` globals)
-                                canonical)
-                    unless
-                        (frozenCoreType checked == contextualType)
-                        (Except.throwError
-                            (ExactObjectTypeMismatch
-                                (locate block)
-                                contextualType
-                                (frozenCoreType checked)))
-                    let content' =
-                            TransparentObjectContent
-                                theory
-                                contextualType
-                                canonical
-                        identity =
-                            transparentObjectId
-                                theory contextualType canonical
-                    pure
-                        ( ContextualTransparentExpansion
-                            identity requirements
-                        , content'
-                        )
-        let targetObject = semanticGlobalTargetObject target
-        available <-
-            Except.lift (Declaration.objectAvailableLowering targetObject)
-        let alias = definitionAlias block
-            asserted
-                | available = Nothing
-                | otherwise = Just (assertedObject targetObject content)
-            syntax =
-                declarationSyntaxId
-                    (encodePreparedSyntax family head' body alias)
-        pure
-            (PreparedExactDeclaration
-                (locate block)
-                family
-                key
-                target
-                asserted
-                alias
-                (case family of
-                    ExactDefinition -> case body of
-                        TransparentBody _canonical construction -> construction
-                        _ -> Nothing
-                    _ -> Nothing)
-                syntax)
-
-lowerPreparedExactBinding
-    :: PreparedExactDeclaration
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration CheckedExactBindingAuthorization))
-lowerPreparedExactBinding prepared =
-    case preparedDefinitionAlias prepared of
-        Nothing ->
-            pure
-                (Right
-                    (checked [] CheckedExactBindingNone))
-        Just alias -> case preparedDefinitionConstruction prepared of
-            Nothing ->
-                fmap
-                    (\spec ->
-                        checked
-                            [ Declaration.checkedCandidate
-                                spec
-                                (Declaration.checkedDefinitionEquationPlanning
-                                    identity)
-                                :| []
-                            ]
-                            (CheckedExactBindingDefinition identity))
-                    <$> Declaration.prepareDefinitionEquationSpecLowering
-                        objects identity alias
-            Just (PreparedUnconditionalSetConstruction construction) ->
-                Except.runExceptT do
-                    equation <-
-                        Except.lift
-                            (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering
-                                objects identity SearchIneligible alias)
-                            >>= Except.liftEither
-                    (extensional, descriptor) <-
-                        Except.lift
-                            (Declaration.prepareNamedSetConstructionSpecLowering
-                                objects identity construction)
-                            >>= Except.liftEither
-                    pure
-                        (checked
-                            [ Declaration.checkedCandidate
-                                equation
-                                (Declaration.checkedDefinitionEquationPlanning
-                                    identity)
-                                :| [ Declaration.checkedCandidate
-                                        extensional
-                                        (Declaration.checkedKernelPlanning
-                                            descriptor [])
-                                   ]
-                            ]
-                            (CheckedExactBindingConstruction
-                                identity construction))
-            Just (PreparedRelationalSetConstruction construction) ->
-                Except.runExceptT do
-                    equation <-
-                        Except.lift
-                            (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering
-                                objects identity SearchIneligible alias)
-                            >>= Except.liftEither
-                    let functionality =
-                            relationalSetConstructionClosedFunctionality
-                                construction
-                        functionalityScoped =
-                            embedClosedCore [] functionality
-                    functionalitySpec <-
-                        Except.lift
-                            (Declaration.prepareFrozenCandidateSpecLowering
-                                objects functionality SearchIneligible [])
-                            >>= Except.liftEither
-                    obligation <-
-                        Except.lift
-                            (Declaration.prepareScopedVampireObligationLowering
-                                Vector.empty
-                                functionalityScoped
-                                []
-                                []
-                                Declaration.VampireImplicitPremises)
-                            >>= either
-                                (Except.throwError
-                                    . Declaration.ProofObligationFailedAt location
-                                    . Declaration.CurrentCandidateVampirePreparationFailed)
-                                pure
-                    (extensional, descriptor) <-
-                        Except.lift
-                            (Declaration.prepareRelationalSetConstructionSpecLowering
-                                objects identity construction functionality)
-                            >>= Except.liftEither
-                    pure
-                        (checked
-                            [ Declaration.checkedCandidate
-                                equation
-                                (Declaration.checkedDefinitionEquationPlanning
-                                    identity)
-                                :| [ Declaration.checkedCandidate
-                                        functionalitySpec
-                                        (Declaration.checkedSourceProofPlanning
-                                            [Declaration.checkedPlannedVampireRequest
-                                                location obligation]
-                                            [])
-                                   ]
-                            , Declaration.checkedCandidate
-                                extensional
-                                (Declaration.checkedStagedKernelPlanning
-                                    descriptor
-                                    [Declaration.plannedEarlierCandidate 0 1])
-                                :| []
-                            ]
-                            (CheckedExactBindingRelationalConstruction
-                                identity construction obligation))
-  where
-    identity = preparedExactObjectId prepared
-    objects = maybeToList (preparedExactObject prepared)
-    location = preparedExactLocation prepared
-    checked stages body =
-        Declaration.checkedCompiledDeclaration
-            (preparedExactSyntaxId prepared)
-            objects
-            []
-            [semanticGlobalBinding
-                (preparedExactGlobalKey prepared)
-                (preparedExactGlobalTarget prepared)]
-            []
-            stages
-            body
-
-data CheckedExactBindingAuthorization
-    = CheckedExactBindingNone
-    | CheckedExactBindingDefinition !ObjectId
-    | CheckedExactBindingConstruction
-        !ObjectId
-        !(NamedSetConstruction ObjectId)
-    | CheckedExactBindingRelationalConstruction
-        !ObjectId
-        !(CheckedRelationalSetConstruction ObjectId)
-        !(Declaration.PreparedVampireObligation Void ())
-
-authorizeCheckedExactBinding
-    :: CheckedExactBindingAuthorization
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedExactBinding body stages =
-    case (body, stages) of
-        (CheckedExactBindingNone, []) -> pure ()
-        (CheckedExactBindingDefinition identity, [candidate :| []]) ->
-            Declaration.authorizeDefinitionEquationCandidate
-                identity candidate
-        ( CheckedExactBindingConstruction identity construction
-          , [equation :| [extensional]]
-          ) -> do
-            Declaration.authorizeDefinitionEquationCandidate
-                identity equation
-            Declaration.authorizeNamedSetConstructionCandidate
-                identity construction extensional
-        ( CheckedExactBindingRelationalConstruction
-                identity construction obligation
-          , [equation :| [functionality], extensional :| []]
-          ) -> do
-            Declaration.authorizeDefinitionEquationCandidate
-                identity equation
-            Declaration.authorizeVampireCandidate
-                functionality
-                (Declaration.acceptPreparedVampireObligation obligation)
-            Declaration.authorizeRelationalSetConstructionCandidate
-                identity construction functionality extensional
-        _ ->
-            Declaration.failDeclaration
-                (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                    (case body of
-                        CheckedExactBindingNone -> 0
-                        CheckedExactBindingDefinition{} -> 1
-                        CheckedExactBindingConstruction{} -> 1
-                        CheckedExactBindingRelationalConstruction{} -> 2)
-                    (length stages))
-
-prepareExactStructure
-    :: Raw.Block
-    -> [CanonicalLexicalEntry]
-    -> Declaration.LoweringDriver
-        (Either ExactCompileError PreparedExactStructure)
-prepareExactStructure block entries =
-    Except.runExceptT do
-        (location, marker, structure) <-
-            case block of
-                Raw.BlockStruct location _title (Raw.Marker marker) structure ->
-                    pure (location, marker, structure)
-                _ -> Except.throwError
-                    (ExactUnsupportedDeclaration (locate block))
-        validateStructureOccurrences location structure entries
-        let structurePhrase =
-                semanticStructurePhrase (Raw.structPhrase structure)
-            parentPhrases =
-                semanticStructurePhrase <$> Raw.structParents structure
-        when
-            (structurePhrase `elem` parentPhrases)
-            (Except.throwError
-                (ExactStructureSelfParent location structurePhrase))
-        case firstDuplicate parentPhrases of
-            Just duplicate ->
-                Except.throwError
-                    (ExactStructureDuplicateParent location duplicate)
-            Nothing -> pure ()
-        visible <- Except.lift
-            (Declaration.resolveVisibleStructureLowering structurePhrase)
-        when
-            (isJust visible)
-            (Except.throwError
-                (ExactStructureAlreadyVisible location structurePhrase))
-        parents <- traverse (resolveParent location) parentPhrases
-        inherited <-
-            foldM mergeParentOperations Map.empty
-                (zip parentPhrases parents)
-        case firstDuplicate (Raw.structFixes structure) of
-            Just duplicate ->
-                Except.throwError
-                    (ExactStructureDuplicateOperation location duplicate)
-            Nothing -> pure ()
-        traverse_
-            (\symbol ->
-                when
-                    (Map.member symbol inherited)
-                    (Except.throwError
-                        (ExactStructureOperationAlreadyInherited
-                            location symbol)))
-            (Raw.structFixes structure)
-        slot <- Except.lift Declaration.nextDeclarationSlotLowering
-        theory <- Except.lift Declaration.currentTheoryLowering
-        let operationType = TyArrow TySet TySet
-            makeOperation index symbol =
-                let seed =
-                        opaqueDeclarationSeed
-                            (declarationSlotModule slot)
-                            (declarationSlotOrdinal slot)
-                            StructureDeclaration
-                            (generatedObjectSlot index)
-                    content = OpaqueObjectContent theory seed operationType
-                    identity = opaqueObjectId theory seed operationType
-                in ( symbol
-                   , identity
-                   , assertedObject identity content
-                   )
-            ownOperations =
-                zipWith makeOperation [0 ..] (Raw.structFixes structure)
-            operationObjects =
-                [ asserted
-                | (_symbol, _identity, asserted) <- ownOperations
-                ]
-            completeOperations =
-                Map.union
-                    (Map.fromList
-                        [ (symbol, identity)
-                        | (symbol, identity, _asserted) <- ownOperations
-                        ])
-                    (fst <$> inherited)
-        unless
-            (Map.member Raw.CarrierSymbol completeOperations)
-            (Except.throwError
-                (ExactStructureHasNoCarrier location structurePhrase))
-        context <-
-            either Except.throwError pure
-                (extendExactBinderContext
-                    ((exactLocalId 0, Raw.structLabel structure) :| [])
-                    emptyExactBinderContext)
-        let provisionalAnnotation =
-                ExactStructureAnnotation
-                    structurePhrase Nothing completeOperations
-            structureContext =
-                annotateBinderContext
-                    (Map.singleton 0 provisionalAnnotation)
-                    context
-        checkedAssumptions <-
-            traverse
-                (\(assumptionMarker, assumption) -> do
-                    prepared <- Except.lift
-                        (prepareExactProposition structureContext assumption)
-                    proposition <- Except.liftEither prepared
-                    pure
-                        ( locate assumption
-                        , assumptionMarker
-                        , preparedExactPropositionCore proposition
-                        ))
-                (Raw.structAssumes structure)
-        parentTerms <-
-            fmap catMaybes
-                (traverse
-                    (\parent ->
-                        case Declaration.resolvedStructurePredicate parent of
-                            Nothing -> pure Nothing
-                            Just predicate ->
-                                pure
-                                    (Just
-                                        (CApp
-                                            (CGlobal predicate)
-                                            (CBound 0))))
-                    parents)
-        let assumptionTerms =
-                [ scopedCoreTerm proposition
-                | (_assumptionLocation, _assumptionMarker, proposition) <-
-                    checkedAssumptions
-                ]
-            predicateBody =
-                CLam TySet
-                    (logicalConjunction
-                        (parentTerms <> assumptionTerms))
-            predicateType = TyArrow TySet TyProp
-            predicateContent =
-                TransparentObjectContent theory predicateType predicateBody
-            predicate =
-                transparentObjectId theory predicateType predicateBody
-        predicateAvailable <-
-            Except.lift (Declaration.objectAvailableLowering predicate)
-        let predicateObject =
-                [ assertedObject predicate predicateContent
-                | not predicateAvailable
-                ]
-            ownBindings =
-                [ semanticStructureOperation symbol identity
-                | (symbol, identity, _asserted) <- ownOperations
-                ]
-        descriptor <-
-            Except.liftEither
-                (first
-                    (ExactStructureDescriptorInvalid location)
-                    (semanticStructureDescriptor
-                        structurePhrase
-                        (Just predicate)
-                        parentPhrases
-                        ownBindings))
-        let structureApplication =
-                CApp (CGlobal predicate) (CBound 0)
-            inheritance =
-                [ ( location
-                  , semanticName (marker <> "inherit")
-                  , CForall TySet
-                        (CImp structureApplication
-                            (logicalConjunction parentTerms))
-                  )
-                | not (null parentTerms)
-                ]
-            projections =
-                [ ( assumptionLocation
-                  , semanticName assumptionMarker
-                  , CForall TySet
-                        (CImp structureApplication
-                            (scopedCoreTerm proposition))
-                  )
-                | ( assumptionLocation
-                  , Raw.Marker assumptionMarker
-                  , proposition
-                  ) <- checkedAssumptions
-                ]
-            generatedTerms = inheritance <> projections
-            localTypes =
-                Map.fromList
-                    ((predicate, predicateType)
-                        : [ (identity, operationType)
-                          | (_symbol, identity, _asserted) <- ownOperations
-                          ])
-        resolvedTypes <-
-            resolveStructureGlobalTypes
-                localTypes
-                [ term
-                | (_factLocation, _alias, term) <- generatedTerms
-                ]
-        generated <-
-            traverse
-                (\(factLocation, alias, term) -> do
-                    frozen <-
-                        either
-                            (Except.throwError
-                                . ExactCoreCheckFailed factLocation)
-                            pure
-                            (checkCanonicalCore
-                                (`Map.lookup` resolvedTypes)
-                                term)
-                    pure
-                        (PreparedExactStructureFact
-                            factLocation frozen alias))
-                generatedTerms
-        environment <-
-            Except.liftEither
-                (first
-                    (ExactStructureDescriptorInvalid location)
-                    (semanticEnvironmentWithStructures [] [descriptor]))
-        let syntax =
-                declarationSyntaxId
-                    (encodePreparedStructure
-                        environment
-                        predicate
-                        generated)
-        pure
-            (PreparedExactStructure
-                location
-                (operationObjects <> predicateObject)
-                predicate
-                descriptor
-                (semanticName marker)
-                generated
-                syntax)
-  where
-    resolveParent location structurePhrase = do
-        resolved <- Except.lift
-            (Declaration.resolveVisibleStructureLowering structurePhrase)
-        maybe
-            (Except.throwError
-                (ExactStructureNotVisible location structurePhrase))
-            pure
-            resolved
-
-    mergeParentOperations inherited (parentPhrase, parent) =
-        foldM
-            (insertParentOperation parentPhrase)
-            inherited
-            (Map.toAscList
-                (Declaration.resolvedStructureOperations parent))
-
-    insertParentOperation parentPhrase inherited (symbol, identity) =
-        case Map.lookup symbol inherited of
-            Nothing ->
-                pure
-                    (Map.insert symbol (identity, parentPhrase) inherited)
-            Just (existing, existingOrigin)
-                | existing == identity -> pure inherited
-                | otherwise ->
-                    Except.throwError
-                        (ExactStructureOperationConflict
-                            (locate block)
-                            symbol
-                            existingOrigin
-                            parentPhrase)
-
-    resolveStructureGlobalTypes localTypes terms = do
-        let dependencies = Set.unions (canonicalTermGlobals <$> terms)
-        foldM
-            (\types identity ->
-                case Map.lookup identity types of
-                    Just{} -> pure types
-                    Nothing -> do
-                        coreType <- Except.lift
-                            (Declaration.objectTypeLowering identity)
-                        case coreType of
-                            Nothing ->
-                                Except.throwError
-                                    (ExactStructureObjectNotVisible
-                                        (locate block) identity)
-                            Just actual ->
-                                pure (Map.insert identity actual types))
-            localTypes
-            (Set.toAscList dependencies)
-
-lowerPreparedExactStructure
-    :: PreparedExactStructure
-    -> Declaration.LoweringDriver
-        (Either
-            Declaration.DeclarationError
-            (Declaration.CheckedDeclaration
-                CheckedExactStructureAuthorization))
-lowerPreparedExactStructure
-        (PreparedExactStructure
-            _location objects predicate descriptor alias generatedFacts syntax) =
-    Except.runExceptT do
-        definition <-
-            Except.lift
-                (Declaration.preparePointwiseDefinitionEquationSpecLowering
-                    objects predicate alias)
-                >>= Except.liftEither
-        generatedCandidates <-
-            traverse
-                (\(PreparedExactStructureFact
-                        factLocation target factAlias) -> do
-                    generatedSpec <- Except.lift
-                        (Declaration.prepareFrozenCandidateSpecLowering
-                            objects target SearchEligible [factAlias])
-                        >>= Except.liftEither
-                    obligation <- Except.lift
-                        (Declaration.prepareStagedCandidateVampireLowering
-                            factLocation objects definition generatedSpec)
-                        >>= Except.liftEither
-                    pure
-                        ( Declaration.checkedCandidate generatedSpec
-                            (Declaration.checkedSourceProofPlanning
-                                [ Declaration.checkedPlannedVampireRequest
-                                    factLocation obligation
-                                ]
-                                [ Declaration.plannedEarlierCandidate 0 0
-                                ])
-                        , (factLocation, obligation)
-                        ))
-                generatedFacts
-        let generatedAuthorizations =
-                snd <$> generatedCandidates
-            stages =
-                [ Declaration.checkedCandidate definition
-                    (Declaration.checkedDefinitionEquationPlanning predicate)
-                    :| []
-                ]
-                    <> maybeToList
-                        (NonEmpty.nonEmpty
-                            (fst <$> generatedCandidates))
-            body =
-                CheckedExactStructureAuthorization
-                    predicate
-                    generatedAuthorizations
-        pure
-            (Declaration.checkedCompiledDeclaration
-                syntax objects [] [] [descriptor] stages
-                body)
-
-authorizeCheckedExactStructure
-    :: CheckedExactStructureAuthorization
-    -> [NonEmpty Declaration.ReservedCandidate]
-    -> Declaration.Declaration ()
-authorizeCheckedExactStructure
-        (CheckedExactStructureAuthorization predicate obligations)
-        stages =
-    case (obligations, stages) of
-        ([], [definition :| []]) ->
-            Declaration.authorizeDefinitionEquationCandidate
-                predicate definition
-        (_, [definition :| [], generatedCandidates])
-            | length obligations == NonEmpty.length generatedCandidates -> do
-                Declaration.authorizeDefinitionEquationCandidate
-                    predicate definition
-                Declaration.authorizeVampireCandidateBatch
-                    (NonEmpty.zipWith
-                        (\candidate (factLocation, obligation) ->
-                            ( factLocation
-                            , candidate
-                            , do
-                                void
-                                    (Declaration.useStagedCandidate
-                                        definition)
-                                pure obligation
-                            ))
-                        generatedCandidates
-                        (NonEmpty.fromList obligations))
-        _ ->
-            Declaration.failDeclaration
-                (Declaration.CheckedAuthorizationCandidateShapeMismatch
-                    (if null obligations then 1 else 2)
-                    (length stages))
-
-validateStructureOccurrences
-    :: Location
-    -> Raw.StructDefn
-    -> [CanonicalLexicalEntry]
-    -> ExceptT ExactCompileError (Declaration.LoweringDriver) ()
-validateStructureOccurrences location structure entries = do
-    let Raw.LexicalItemSgPl forms structureMarker =
-            Raw.structPhrase structure
-        expected =
-            CanonicalStructureNoun
-                (Raw.sg forms)
-                (Raw.pl forms)
-                structureMarker
-                : [ CanonicalStructureOperation command
-                  | Raw.StructSymbol command <- Raw.structFixes structure
-                  ]
-    unless
-        (entries == expected)
-        (Except.throwError
-            (ExactStructureOccurrenceMismatch location))
-
-encodePreparedStructure
-    :: SemanticEnvironmentDelta
-    -> ObjectId
-    -> [PreparedExactStructureFact]
-    -> ByteString
-encodePreparedStructure environment predicate generated =
-    encodeCache do
-        putCacheTag 0x04
-        putSemanticEnvironmentDeltaCache environment
-        putObjectIdCache predicate
-        putCacheList
-            (\(PreparedExactStructureFact _location target alias) -> do
-                putCanonicalTermCache putObjectIdCache
-                    (frozenCoreTerm target)
-                putCacheText (semanticNameText alias))
-            generated
-
-prepareHead
-    :: Raw.Block
-    -> SemanticGlobalKey
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , ExactDeclarationFamily
-        , Maybe (Elaborate CompiledBody)
-        )
-prepareHead block key =
-    case block of
-        Raw.BlockSig location _title _marker assumptions signature -> do
-            rejectHeaderAssumptions ExactGuardedOpaqueSignature assumptions
-            head' <- prepareSignature location key signature
-            pure (head', ExactSignature, Nothing)
-        Raw.BlockAbbr location _title _marker abbreviation -> do
-            (head', buildBody) <-
-                prepareAbbreviation location key abbreviation
-            pure (head', ExactAbbreviation, Just buildBody)
-        Raw.BlockDefn location _title _marker definition -> do
-            (head', buildBody) <-
-                prepareDefinition location key definition
-            pure (head', ExactDefinition, Just buildBody)
-        _ ->
-            Except.throwError (ExactUnsupportedDeclaration (locate block))
-
-prepareSignature
-    :: Location
-    -> SemanticGlobalKey
-    -> Raw.Signature
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        PreparedHead
-prepareSignature location key = \case
-    Raw.SignatureAdj subject (Raw.Adj _ item arguments) -> do
-        ensureAdjectiveKey location item key
-        makePreparedHead
-            location key (subject : arguments) TyProp
-    Raw.SignatureSymbolic (Raw.SymbolPattern symbol parameters) nounPhrase -> do
-        unless
-            ( key
-                == SemanticExpressionFunction
-                    (Raw.mixfixPattern symbol)
-            )
-            (Except.throwError (ExactDeclarationHeadMismatch location))
-        unless
-            (exactSetNounPhrase nounPhrase)
-            (Except.throwError (ExactUnsupportedDeclarationBody location))
-        makePreparedHead location key parameters TySet
-    _ ->
-        Except.throwError (ExactUnsupportedDeclaration location)
-
-prepareAbbreviation
-    :: Location
-    -> SemanticGlobalKey
-    -> Raw.Abbreviation
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , Elaborate CompiledBody
-        )
-prepareAbbreviation location key = \case
-    Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do
-        ensureExpressionKey location symbol key
-        makeContextualTransparentHead
-            location key parameters TySet
-            (ordinaryCompiledBody <$> compileExpressionAsSet expression)
-    Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do
-        ensureFunctionPhraseKey location item key
-        makeContextualTransparentHead
-            location key parameters TySet
-            (ordinaryCompiledBody <$> compileTermAsSet term)
-    Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do
-        ensureAdjectiveKey location item key
-        makeContextualTransparentHead
-            location key (subject : arguments) TyProp
-            (ordinaryCompiledBody <$> compileStatement statement)
-    Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do
-        ensureVerbKey location item key
-        makeContextualTransparentHead
-            location key (subject : arguments) TyProp
-            (ordinaryCompiledBody <$> compileStatement statement)
-    Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do
-        ensureNounKey location item key
-        makeContextualTransparentHead
-            location key (subject : arguments) TyProp
-            (ordinaryCompiledBody <$> compileStatement statement)
-    Raw.AbbreviationRel left relation parameters right statement -> do
-        ensureRelationKey location relation key
-        makeContextualTransparentHead
-            location key (parameters <> [left, right]) TyProp
-            (ordinaryCompiledBody <$> compileStatement statement)
-
-prepareDefinition
-    :: Location
-    -> SemanticGlobalKey
-    -> Raw.Defn
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , Elaborate CompiledBody
-        )
-prepareDefinition location key = \case
-    Raw.Defn assumptions head' statement -> do
-        rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions
-        (parameters, resultType) <-
-            definitionHead location key head'
-        makeTransparentHead
-            location key parameters resultType
-            (ordinaryCompiledBody <$> compileStatement statement)
-    Raw.DefnFun assumptions (Raw.Fun _ item parameters) symbolic term -> do
-        rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions
-        traverse_
-            (Except.throwError
-                . ExactDefinitionCombinedSymbolicAlias
-                . locate)
-            symbolic
-        ensureFunctionPhraseKey location item key
-        makeTransparentHead
-            location key parameters TySet
-            (compileNamedSetTerm term)
-    Raw.DefnOp (Raw.SymbolPattern symbol parameters) expression -> do
-        ensureExpressionKey location symbol key
-        makeTransparentHead
-            location key parameters TySet
-            (compileNamedSetExpression expression)
-
-definitionHead
-    :: Location
-    -> SemanticGlobalKey
-    -> Raw.DefnHead
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ([Raw.VarSymbol], CoreType)
-definitionHead location key = \case
-    Raw.DefnAdj annotation subject (Raw.Adj _ item arguments) -> do
-        validateDefinitionAnnotation annotation
-        ensureAdjectiveKey location item key
-        pure (subject : arguments, TyProp)
-    Raw.DefnVerb annotation subject (Raw.Verb _ item arguments) -> do
-        validateDefinitionAnnotation annotation
-        ensureVerbKey location item key
-        pure (subject : arguments, TyProp)
-    Raw.DefnNoun subject (Raw.Noun _ item arguments) -> do
-        ensureNounKey location item key
-        pure (subject : arguments, TyProp)
-    Raw.DefnRel left relation parameters right -> do
-        ensureRelationKey location relation key
-        pure (parameters <> [left, right], TyProp)
-    Raw.DefnSymbolicPredicate
-            (Raw.PrefixPredicate command arity)
-            _marker
-            parameters -> do
-        unless
-            ( key
-                == SemanticPrefixPredicate
-                    command
-                    (fromIntegral arity)
-            )
-            (Except.throwError (ExactDeclarationHeadMismatch location))
-        pure (toList parameters, TyProp)
-
-validateDefinitionAnnotation
-    :: MonadError ExactCompileError monad
-    => Maybe (Raw.NounPhrase Maybe)
-    -> monad ()
-validateDefinitionAnnotation = traverse_ \nounPhrase ->
-    unless (exactSetNounPhrase nounPhrase)
-        (throwError
-            (ExactNonCanonicalSetDefinitionAnnotation
-                (exactNounPhraseLocation nounPhrase)))
-
-rejectHeaderAssumptions
-    :: MonadError ExactCompileError monad
-    => (Location -> ExactCompileError)
-    -> [Raw.Asm]
-    -> monad ()
-rejectHeaderAssumptions makeError = \case
-    [] -> pure ()
-    assumption : _ ->
-        throwError (makeError (exactAssumptionLocation assumption))
-
-exactAssumptionLocation :: Raw.Asm -> Location
-exactAssumptionLocation = \case
-    Raw.AsmSuppose statement -> locate statement
-    Raw.AsmLetNoun variables _nounPhrase -> locate variables
-    Raw.AsmLetIn variables _expression -> locate variables
-    Raw.AsmLetThe variable _function -> locate variable
-    Raw.AsmLetEq variable _expression -> locate variable
-    Raw.AsmLetStruct variable _structure -> locate variable
-
-exactNounPhraseLocation :: Raw.NounPhraseOf t argument -> Location
-exactNounPhraseLocation
-        (Raw.NounPhrase _left noun _variables _right _suchThat) =
-    locate noun
-
-makeTransparentHead
-    :: Location
-    -> SemanticGlobalKey
-    -> [Raw.VarSymbol]
-    -> CoreType
-    -> Elaborate CompiledBody
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , Elaborate CompiledBody
-        )
-makeTransparentHead location key parameters resultType body = do
-    (prepared, binders) <-
-        prepareParameters location key parameters resultType
-    let close = do
-            State.modify' \state ->
-                state
-                    { elaborationBinders = binders
-                    , elaborationBinderDepth =
-                        fromIntegral (length parameters)
-                    }
-            CompiledBody body' construction <- body
-            pure
-                (CompiledBody
-                    (foldr (const (CLam TySet)) body' parameters)
-                    construction)
-    pure (prepared, close)
-
-makeContextualTransparentHead
-    :: Location
-    -> SemanticGlobalKey
-    -> [Raw.VarSymbol]
-    -> CoreType
-    -> Elaborate CompiledBody
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , Elaborate CompiledBody
-        )
-makeContextualTransparentHead location key parameters resultType body = do
-    (prepared, binders) <-
-        prepareParameters location key parameters resultType
-    let close = do
-            State.modify' \state ->
-                state
-                    { elaborationBinders = binders
-                    , elaborationBinderDepth =
-                        fromIntegral (length parameters) + 1
-                    , elaborationContextualBinder =
-                        Just (fromIntegral (length parameters))
-                    }
-            CompiledBody body' _construction <- body
-            pure
-                (CompiledBody
-                    (foldr (const (CLam TySet)) body' parameters)
-                    Nothing)
-    pure (prepared, close)
-
-makePreparedHead
-    :: Location
-    -> SemanticGlobalKey
-    -> [Raw.VarSymbol]
-    -> CoreType
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        PreparedHead
-makePreparedHead location key parameters resultType = do
-    (prepared, _binders) <-
-        prepareParameters location key parameters resultType
-    pure prepared
-
-prepareParameters
-    :: Location
-    -> SemanticGlobalKey
-    -> [Raw.VarSymbol]
-    -> CoreType
-    -> ExceptT
-        ExactCompileError
-        (Declaration.LoweringDriver)
-        ( PreparedHead
-        , Map.Map Raw.VarSymbol Natural
-        )
-prepareParameters
-        location key parameters resultType = do
-    case firstDuplicate parameters of
-        Just duplicate ->
-            Except.throwError
-                (ExactDuplicateParameter location duplicate)
-        Nothing -> pure ()
-    let indices =
-            reverse (take (length parameters) [0 ..])
-        binders =
-            Map.fromList
-                (zip parameters indices)
-        coreType = foldr (const (TyArrow TySet)) resultType parameters
-    pure
-        ( PreparedHead key parameters coreType
-        , binders
-        )
-
-compileExpressionAsSet
-    :: Raw.Expr
-    -> Elaborate (CanonicalTerm ObjectId)
-compileExpressionAsSet expression = do
-    (term, actual) <- compileExpression expression
-    unless (actual == TySet)
-        (Except.throwError
-            (ExactExpressionExpectedSet (locate expression) actual))
-    pure term
-
--- | Compile one set expression once while retaining the checked-source shape
--- needed only when that expression is subsequently named by a definition.
--- Nested constructions remain ordinary exact terms.
-compileNamedSetExpression
-    :: Raw.Expr
-    -> Elaborate CompiledBody
-compileNamedSetExpression = \case
-    Raw.ExprSep _location variable bound predicate -> do
-        (term, bound', predicate') <-
-            compileSeparation variable bound predicate
-        pure
-            (CompiledBody term
-                (Just
-                    (CompiledSeparationConstruction
-                        bound' predicate')))
-    Raw.ExprReplace _location value bounds condition -> do
-        replacement <-
-            compileFunctionalReplacement value bounds condition
-        pure
-            (CompiledBody
-                (compiledFunctionalReplacementTerm replacement)
-                (Just
-                    (CompiledFunctionalReplacementConstruction
-                        (compiledFunctionalReplacementDomains replacement)
-                        (compiledFunctionalReplacementValue replacement)
-                        (compiledFunctionalReplacementCondition replacement))))
-    Raw.ExprReplacePred _location range domainVariable bound predicate -> do
-        (term, domain, relation) <-
-            compileRelationalReplacement
-                range domainVariable bound predicate
-        pure
-            (CompiledBody term
-                (Just
-                    (CompiledRelationalReplacementConstruction
-                        domain relation)))
-    expression ->
-        (`CompiledBody` Nothing)
-            <$> compileExpressionAsSet expression
-
-compileNamedSetTerm :: Raw.Term -> Elaborate CompiledBody
-compileNamedSetTerm = \case
-    Raw.TermExpr expression -> compileNamedSetExpression expression
-    term -> ordinaryCompiledBody <$> compileTermAsSet term
-
-ordinaryCompiledBody :: CanonicalTerm ObjectId -> CompiledBody
-ordinaryCompiledBody term = CompiledBody term Nothing
-
-compileTermAsSet
-    :: Raw.Term
-    -> Elaborate (CanonicalTerm ObjectId)
-compileTermAsSet = \case
-    Raw.TermExpr expression ->
-        compileExpressionAsSet expression
-    Raw.TermFun (Raw.Fun location item arguments) -> do
-        let patterns = Raw.lexicalItemSgPlPattern item
-            key = SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)
-        compiled <- traverse compileTermAsSet arguments
-        applyResolved location key compiled
-    Raw.TermQuantified _quantifier location _nounPhrase ->
-        Except.throwError
-            (ExactQuantifiedTermRequiresPropositionContext location)
-    term ->
-        Except.throwError
-            (ExactUnsupportedDeclarationBody (locate term))
-
--- | Compile a source term only at a proposition consumer.  Indefinite terms
--- own the continuation, so their noun constraints and quantifier surround
--- exactly the proposition which consumes the resulting set.  Function-phrase
--- arguments recurse through the same seam and therefore never masquerade as
--- independently set-valued terms.
-compileTermInProposition
-    :: Raw.Term
-    -> (CanonicalTerm ObjectId
-        -> Elaborate (CanonicalTerm ObjectId))
-    -> Elaborate (CanonicalTerm ObjectId)
-compileTermInProposition term continuation =
-    case term of
-        Raw.TermExpr expression ->
-            compileExpressionAsSet expression >>= continuation
-        Raw.TermFun (Raw.Fun location item arguments) -> do
-            let patterns = Raw.lexicalItemSgPlPattern item
-                key =
-                    SemanticFunctionPhrase
-                        (Raw.sg patterns)
-                        (Raw.pl patterns)
-            compileTermsInProposition arguments \compiled -> do
-                value <- applyResolved location key compiled
-                continuation value
-        Raw.TermQuantified quantifier _location nounPhrase ->
-            compileQuantifiedTermInProposition
-                quantifier nounPhrase continuation
-        Raw.TermIota location _variable _statement ->
-            Except.throwError (ExactUnsupportedDeclarationBody location)
-
--- | Compile source-ordered proposition terms.  The first source occurrence
--- receives the outermost continuation and therefore the widest scope.
-compileTermsInProposition
-    :: [Raw.Term]
-    -> ([CanonicalTerm ObjectId]
-        -> Elaborate (CanonicalTerm ObjectId))
-    -> Elaborate (CanonicalTerm ObjectId)
-compileTermsInProposition terms continuation =
-    case terms of
-        [] -> continuation []
-        term : remaining ->
-            compileTermInProposition term \compiled -> do
-                compiledDepth <- State.gets elaborationBinderDepth
-                compileTermsInProposition remaining \rest -> do
-                    compiled' <-
-                        weakenElaboratedTermFrom compiledDepth compiled
-                    continuation (compiled' : rest)
-
-weakenElaboratedTermFrom
-    :: Natural
-    -> CanonicalTerm ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-weakenElaboratedTermFrom originalDepth term = do
-    currentDepth <- State.gets elaborationBinderDepth
-    when (currentDepth < originalDepth)
-        (impossible
-            "a proposition-term continuation escaped its binder scope")
-    pure
-        (shiftCanonical
-            (currentDepth - originalDepth)
-            0
-            term)
-
-compileExpression
-    :: Raw.Expr
-    -> Elaborate (CanonicalTerm ObjectId, CoreType)
-compileExpression = \case
-    Raw.ExprVar variable -> do
-        binders <- State.gets elaborationBinders
-        case Map.lookup variable binders of
-            Just index ->
-                pure (CBound index, TySet)
-            Nothing ->
-                Except.throwError
-                    (ExactFreeVariable (locate variable) variable)
-    Raw.ExprInteger _location integer ->
-        pure (COpaqueInteger (toInteger integer), TySet)
-    Raw.ExprOp location symbol arguments -> do
-        let key =
-                SemanticExpressionFunction
-                    (Raw.mixfixPattern symbol)
-        compiled <- traverse compileExpression arguments
-        case fixedSemanticMeaning key of
-            Just (FixedIntrinsic intrinsic) ->
-                applyTyped
-                    location
-                    (CIntrinsic intrinsic)
-                    (coreIntrinsicType intrinsic)
-                    compiled
-            Just (FixedNegatedIntrinsic _intrinsic) ->
-                impossible
-                    "expression key resolved to a negated intrinsic"
-            Just FixedEquality ->
-                impossible
-                    "expression key resolved to fixed equality"
-            Just FixedDisequality ->
-                impossible
-                    "expression key resolved to fixed disequality"
-            Nothing ->
-                applyResolvedTyped
-                    location
-                    key
-                    compiled
-    Raw.ExprStructOp location symbol maybeArgument ->
-        compileStructureOperation location symbol maybeArgument
-    Raw.ExprFiniteSet _location elements -> do
-        compiled <- traverse compileExpressionAsSet elements
-        pure
-            ( foldr
-                canonicalSetInsert
-                (CIntrinsic Empty)
-                compiled
-            , TySet
-            )
-    Raw.ExprSep _location variable bound predicate -> do
-        (term, _bound, _predicate) <-
-            compileSeparation variable bound predicate
-        pure (term, TySet)
-    Raw.ExprReplace _location value bounds condition -> do
-        replacement <-
-            compileFunctionalReplacement value bounds condition
-        pure (compiledFunctionalReplacementTerm replacement, TySet)
-    Raw.ExprReplacePred location _value _variable _bound _predicate ->
-        Except.throwError
-            (ExactRelationalReplacementRequiresNamedDefinition location)
-
-compileStructureOperation
-    :: Location
-    -> Raw.StructSymbol
-    -> Maybe Raw.Expr
-    -> Elaborate (CanonicalTerm ObjectId, CoreType)
-compileStructureOperation location symbol maybeArgument = do
-    (argument, object) <-
-        case maybeArgument of
-            Just expression -> do
-                term <- compileExpressionAsSet expression
-                structures <- State.gets elaborationStructures
-                case termStructureAnnotation term structures of
-                    Just annotation -> do
-                        object <-
-                            maybe
-                                (Except.throwError
-                                    (ExactStructureOperationNotAvailable
-                                        location symbol))
-                                pure
-                                (structureAnnotationOperation
-                                    symbol annotation)
-                        pure (term, object)
-                    Nothing -> do
-                        object <-
-                            resolveUniqueStructureOperation location symbol
-                        pure (term, object)
-            Nothing -> do
-                structures <- State.gets elaborationStructures
-                case
-                    [ (CBound index, object)
-                    | (index, structure) <- Map.toAscList structures
-                    , Just object <-
-                        [structureAnnotationOperation symbol structure]
-                    ] of
-                    firstMatch : _ -> pure firstMatch
-                    [] -> do
-                        contextual <- State.gets elaborationContextualBinder
-                        case contextual of
-                            Nothing ->
-                                Except.throwError
-                                    (ExactStructureOperationNotAvailable
-                                        location symbol)
-                            Just index -> do
-                                object <-
-                                    resolveUniqueStructureOperation
-                                        location symbol
-                                recordContextualRequirement
-                                    location symbol object
-                                pure (CBound index, object)
-    recordExactGlobal object (TyArrow TySet TySet)
-    pure (CApp (CGlobal object) argument, TySet)
-  where
-    termStructureAnnotation term structures =
-        case term of
-            CBound index -> Map.lookup index structures
-            _ -> Nothing
-
-resolveUniqueStructureOperation
-    :: Location
-    -> Raw.StructSymbol
-    -> Elaborate ObjectId
-resolveUniqueStructureOperation location symbol = do
-    objects <-
-        State.lift
-            (Except.lift
-                (Declaration.resolveVisibleStructureOperationObjectsLowering
-                    symbol))
-    case objects of
-        [] ->
-            Except.throwError
-                (ExactStructureOperationNotAvailable location symbol)
-        [object] -> pure object
-        _ ->
-            Except.throwError
-                (ExactStructureOperationAmbiguous location symbol objects)
-
-recordContextualRequirement
-    :: Location
-    -> Raw.StructSymbol
-    -> ObjectId
-    -> Elaborate ()
-recordContextualRequirement location symbol object = do
-    existing <-
-        State.gets
-            (Map.lookup symbol . elaborationContextualRequirements)
-    case existing of
-        Nothing ->
-            State.modify' \state ->
-                state
-                    { elaborationContextualRequirements =
-                        Map.insert symbol object
-                            (elaborationContextualRequirements state)
-                    }
-        Just actual
-            | actual == object -> pure ()
-            | otherwise ->
-                Except.throwError
-                    (ExactContextualRequirementConflict
-                        location symbol actual object)
-
-structureCarrierCast
-    :: Location
-    -> CanonicalTerm ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-structureCarrierCast location term =
-    case term of
-        CBound index -> do
-            annotation <- State.gets (Map.lookup index . elaborationStructures)
-            case annotation of
-                Nothing -> pure term
-                Just structure -> do
-                    carrier <-
-                        maybe
-                            (Except.throwError
-                                (ExactStructureOperationNotAvailable
-                                    location Raw.CarrierSymbol))
-                            pure
-                            (structureAnnotationOperation
-                                Raw.CarrierSymbol structure)
-                    recordExactGlobal carrier (TyArrow TySet TySet)
-                    pure (CApp (CGlobal carrier) term)
-        _ -> pure term
-
-compileMembership
-    :: Location
-    -> Raw.Sign
-    -> CanonicalTerm ObjectId
-    -> CanonicalTerm ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-compileMembership location sign element set = do
-    checkedSet <- structureCarrierCast location set
-    let proposition =
-            CApp
-                (CApp (CIntrinsic Member) element)
-                checkedSet
-    pure case sign of
-        Raw.Positive -> proposition
-        Raw.Negative -> logicalNot proposition
-
-compileSeparation
-    :: Raw.VarSymbol
-    -> Raw.Expr
-    -> Raw.Stmt
-    -> Elaborate
-        ( CanonicalTerm ObjectId
-        , CanonicalTerm ObjectId
-        , CanonicalTerm ObjectId
-        )
-compileSeparation variable bound predicate = do
-    bound' <- compileExpressionAsSet bound
-    predicate' <-
-        withSetBinders (variable :| [])
-            (compileStatement predicate)
-    pure
-        ( CApp
-            (CApp (CIntrinsic Sep) bound')
-            (CLam TySet predicate')
-        , bound'
-        , predicate'
-        )
-
-compileRelationalReplacement
-    :: Raw.VarSymbol
-    -> Raw.VarSymbol
-    -> Raw.Expr
-    -> Raw.Stmt
-    -> Elaborate
-        ( CanonicalTerm ObjectId
-        , CanonicalTerm ObjectId
-        , CanonicalTerm ObjectId
-        )
-compileRelationalReplacement range domainVariable bound predicate = do
-    domain <- compileExpressionAsSet bound
-    relation <-
-        withSetBinders (domainVariable :| [range])
-            (compileStatement predicate)
-    let restrictedDomain =
-            CApp
-                (CApp (CIntrinsic Sep) domain)
-                (CLam TySet (logicalExists relation))
-        choiceFunction =
-            CLam TySet
-                (CApp (CIntrinsic SetChoose) (CLam TySet relation))
-        replacement =
-            CApp
-                (CApp (CIntrinsic Repl) restrictedDomain)
-                choiceFunction
-    pure (replacement, domain, relation)
-
-data CompiledFunctionalReplacement = CompiledFunctionalReplacement
-    !(CanonicalTerm ObjectId)
-    !(NonEmpty (CanonicalTerm ObjectId))
-    !(CanonicalTerm ObjectId)
-    !(Maybe (CanonicalTerm ObjectId))
-
-compiledFunctionalReplacementTerm
-    :: CompiledFunctionalReplacement
-    -> CanonicalTerm ObjectId
-compiledFunctionalReplacementTerm
-        (CompiledFunctionalReplacement term _domains _value _condition) =
-    term
-
-compiledFunctionalReplacementDomains
-    :: CompiledFunctionalReplacement
-    -> NonEmpty (CanonicalTerm ObjectId)
-compiledFunctionalReplacementDomains
-        (CompiledFunctionalReplacement _term domains _value _condition) =
-    domains
-
-compiledFunctionalReplacementValue
-    :: CompiledFunctionalReplacement
-    -> CanonicalTerm ObjectId
-compiledFunctionalReplacementValue
-        (CompiledFunctionalReplacement _term _domains value _condition) =
-    value
-
-compiledFunctionalReplacementCondition
-    :: CompiledFunctionalReplacement
-    -> Maybe (CanonicalTerm ObjectId)
-compiledFunctionalReplacementCondition
-        (CompiledFunctionalReplacement _term _domains _value condition) =
-    condition
-
-compileFunctionalReplacement
-    :: Raw.Expr
-    -> NonEmpty (Raw.VarSymbol, Raw.Expr)
-    -> Maybe Raw.Stmt
-    -> Elaborate CompiledFunctionalReplacement
-compileFunctionalReplacement
-        value ((variable, domain) :| remaining) condition = do
-    domain' <- compileExpressionAsSet domain
-    case remaining of
-        [] -> do
-            (value', condition') <-
-                withSetBinders (variable :| []) do
-                    value' <- compileExpressionAsSet value
-                    condition' <- traverse compileStatement condition
-                    pure (value', condition')
-            let filteredDomain =
-                    case condition' of
-                        Nothing -> domain'
-                        Just predicate ->
-                            CApp
-                                (CApp (CIntrinsic Sep) domain')
-                                (CLam TySet predicate)
-            pure
-                (CompiledFunctionalReplacement
-                    (CApp
-                        (CApp (CIntrinsic Repl) filteredDomain)
-                        (CLam TySet value'))
-                    (domain' :| [])
-                    value'
-                    condition')
-        next : rest -> do
-            nested <-
-                withSetBinders (variable :| [])
-                    (compileFunctionalReplacement
-                        value (next :| rest) condition)
-            pure
-                (CompiledFunctionalReplacement
-                    (CApp
-                        (CIntrinsic FamilyUnion)
-                        (CApp
-                            (CApp (CIntrinsic Repl) domain')
-                            (CLam TySet
-                                (compiledFunctionalReplacementTerm nested))))
-                    (domain'
-                        NonEmpty.<|
-                            compiledFunctionalReplacementDomains nested)
-                    (compiledFunctionalReplacementValue nested)
-                    (compiledFunctionalReplacementCondition nested))
-
-compileStatement
-    :: Raw.Stmt
-    -> Elaborate (CanonicalTerm ObjectId)
-compileStatement = \case
-    Raw.StmtFormula formula ->
-        compileFormula formula
-    Raw.StmtVerbPhrase terms verbPhrase ->
-        compileTermsInProposition (toList terms) \subjects ->
-            logicalConjunction
-                <$> traverse (`compileVerbPhrase` verbPhrase) subjects
-    Raw.StmtNoun terms nounPhrase ->
-        compileTermsInProposition (toList terms) \subjects ->
-            logicalConjunction
-                <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects
-    Raw.StmtExists _location nounPhrase ->
-        compileExistentialNounPhrase nounPhrase
-    Raw.StmtQuantPhrase
-            _location
-            (Raw.QuantPhrase quantifier nounPhrase)
-            statement ->
-        compileQuantifiedNounPhrase quantifier nounPhrase statement
-    Raw.StmtConnected connective location left right ->
-        compileConnective
-            (fromMaybe (locate left) location)
-            connective
-            compileStatement
-            left
-            right
-    Raw.StmtNeg _location statement ->
-        logicalNot <$> compileStatement statement
-    Raw.SymbolicQuantified
-            _location quantifier variables bound suchThat statement ->
-        compileSymbolicQuantified
-            quantifier variables bound suchThat (compileStatement statement)
-    Raw.StmtStruct term rawPhrase ->
-        compileTermInProposition term \subject -> do
-            annotation <-
-                resolveStructureAnnotation (locate term) rawPhrase
-            predicate <-
-                maybe
-                    (impossible "an assertable structure has no predicate")
-                    pure
-                    (structureAnnotationPredicate annotation)
-            recordExactGlobal
-                predicate
-                (TyArrow TySet TyProp)
-            pure
-                (CApp
-                    (CGlobal predicate)
-                    subject)
-
-compileQuantifiedTermInProposition
-    :: Raw.Quantifier
-    -> Raw.NounPhrase Maybe
-    -> (CanonicalTerm ObjectId
-        -> Elaborate (CanonicalTerm ObjectId))
-    -> Elaborate (CanonicalTerm ObjectId)
-compileQuantifiedTermInProposition quantifier
-        (Raw.NounPhrase left noun named right suchThat)
-        compileBody =
-    case named of
-        Nothing ->
-            withAnonymousSetBinder compileFor
-        Just variable ->
-            withSetBinders (variable :| []) do
-                subject <- compileIntroducedVariable variable
-                compileFor subject
-  where
-    compileFor subject = do
-        constraints <-
-            compileNounPhraseConstraints
-                [subject] left noun right suchThat
-        body <- compileBody subject
-        pure (quantifyNounPhrase quantifier 1 constraints body)
-
-compileSymbolicQuantified
-    :: Raw.Quantifier
-    -> NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Maybe Raw.Stmt
-    -> Elaborate (CanonicalTerm ObjectId)
-    -> Elaborate (CanonicalTerm ObjectId)
-compileSymbolicQuantified quantifier variables bound suchThat compileBody =
-    withSetBinders variables do
-        boundConstraints <-
-            compileSymbolicBoundConstraintList variables bound
-        suchThatConstraints <-
-            maybeToList <$> traverse compileStatement suchThat
-        body <- compileBody
-        pure
-            (quantifyNounPhrase
-                quantifier
-                (length (toList variables))
-                (logicalConjunction
-                    (boundConstraints <> suchThatConstraints))
-                body)
-
-compileSymbolicBoundConstraintList
-    :: NonEmpty Raw.VarSymbol
-    -> Raw.Bound
-    -> Elaborate [CanonicalTerm ObjectId]
-compileSymbolicBoundConstraintList variables = \case
-    Raw.Unbounded ->
-        pure []
-    Raw.Bounded _location sign relation domain -> do
-        subjects <- traverse compileIntroducedVariable variables
-        domain' <- compileExpressionAsSet domain
-        traverse
-            (\subject -> do
-                proposition <-
-                    compileAtomicRelationTerms subject relation domain'
-                pure case sign of
-                    Raw.Positive -> proposition
-                    Raw.Negative -> logicalNot proposition)
-            (toList subjects)
-
-compileAtomicRelationTerms
-    :: CanonicalTerm ObjectId
-    -> Raw.Relation
-    -> CanonicalTerm ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-compileAtomicRelationTerms left relation right =
-    case relation of
-        Raw.Relation location symbol parameters -> do
-            let key =
-                    SemanticRelation
-                        (Raw.relationSymbolToken symbol)
-                        (Raw.relationSymbolParameterArity symbol)
-            compiledParameters <- traverse compileExpressionAsSet parameters
-            case fixedSemanticMeaning key of
-                Just FixedEquality
-                    | null parameters -> pure (CEq TySet left right)
-                Just FixedDisequality
-                    | null parameters ->
-                        pure (logicalNot (CEq TySet left right))
-                Just (FixedIntrinsic Member)
-                    | null parameters ->
-                        compileMembership location Raw.Positive left right
-                Just (FixedNegatedIntrinsic Member)
-                    | null parameters ->
-                        compileMembership location Raw.Negative left right
-                Just (FixedIntrinsic intrinsic) -> do
-                    (term, actual) <-
-                        applyTyped
-                            location
-                            (CIntrinsic intrinsic)
-                            (coreIntrinsicType intrinsic)
-                            ((\term -> (term, TySet))
-                                <$> (compiledParameters <> [left, right]))
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-                Just (FixedNegatedIntrinsic intrinsic) -> do
-                    (term, actual) <-
-                        applyTyped
-                            location
-                            (CIntrinsic intrinsic)
-                            (coreIntrinsicType intrinsic)
-                            ((\term -> (term, TySet))
-                                <$> (compiledParameters <> [left, right]))
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure (logicalNot term)
-                _ -> do
-                    (term, actual) <-
-                        applyResolvedTyped
-                            location key
-                            ((\term -> (term, TySet))
-                                <$> (compiledParameters <> [left, right]))
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-        Raw.RelationExpr location expression ->
-            compileRelationExpression location expression left right
-
-compileVerbPhrase
-    :: CanonicalTerm ObjectId
-    -> Raw.VerbPhrase
-    -> Elaborate (CanonicalTerm ObjectId)
-compileVerbPhrase subject = \case
-    Raw.VPVerb verb ->
-        compileVerb subject verb
-    Raw.VPVerbNot verb ->
-        logicalNot <$> compileVerb subject verb
-    Raw.VPAdj adjectives ->
-        logicalConjunction
-            <$> traverse (compileAdjective subject) adjectives
-    Raw.VPAdjNot adjectives ->
-        logicalNot . logicalConjunction
-            <$> traverse (compileAdjective subject) adjectives
-
-compilePredicateArguments
-    :: CanonicalTerm ObjectId
-    -> [Raw.Term]
-    -> ( CanonicalTerm ObjectId
-        -> [CanonicalTerm ObjectId]
-        -> Elaborate (CanonicalTerm ObjectId)
-       )
-    -> Elaborate (CanonicalTerm ObjectId)
-compilePredicateArguments subject arguments continuation = do
-    subjectDepth <- State.gets elaborationBinderDepth
-    compileTermsInProposition arguments \compiled -> do
-        subject' <- weakenElaboratedTermFrom subjectDepth subject
-        continuation subject' compiled
-
-compileVerb
-    :: CanonicalTerm ObjectId
-    -> Raw.Verb
-    -> Elaborate (CanonicalTerm ObjectId)
-compileVerb subject (Raw.Verb location item arguments) = do
-    let patterns = Raw.lexicalItemSgPlPattern item
-    compilePredicateArguments subject arguments \subject' compiled ->
-        applyResolvedPredicate
-            location
-            (SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
-            (subject' : compiled)
-
-compileAdjective
-    :: CanonicalTerm ObjectId
-    -> Raw.Adj
-    -> Elaborate (CanonicalTerm ObjectId)
-compileAdjective subject (Raw.Adj location item arguments) =
-    compilePredicateArguments subject arguments \subject' compiled ->
-        applyResolvedPredicateChoice
-            location
-            ( SemanticRightAdjective (Raw.lexicalItemPattern item)
-                :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)]
-            )
-            (subject' : compiled)
-
-compileLeftAdjective
-    :: CanonicalTerm ObjectId
-    -> Raw.AdjL
-    -> Elaborate (CanonicalTerm ObjectId)
-compileLeftAdjective subject (Raw.AdjL location item arguments) =
-    compilePredicateArguments subject arguments \subject' compiled ->
-        applyResolvedPredicate
-            location
-            (SemanticLeftAdjective (Raw.lexicalItemPattern item))
-            (subject' : compiled)
-
-compileRightAttribute
-    :: CanonicalTerm ObjectId
-    -> Raw.AdjR
-    -> Elaborate (CanonicalTerm ObjectId)
-compileRightAttribute subject = \case
-    Raw.AdjR location item arguments ->
-        compilePredicateArguments subject arguments \subject' compiled ->
-            applyResolvedPredicate
-                location
-                (SemanticRightAdjective (Raw.lexicalItemPattern item))
-                (subject' : compiled)
-    Raw.AttrRThat verbPhrase ->
-        compileVerbPhrase subject verbPhrase
-
-compileNoun
-    :: CanonicalTerm ObjectId
-    -> Raw.Noun
-    -> Elaborate (CanonicalTerm ObjectId)
-compileNoun subject (Raw.Noun location item arguments)
-    | Lexicon.isBuiltinSetNoun item =
-        pure logicalTruth
-    | otherwise = do
-        let patterns = Raw.lexicalItemSgPlPattern item
-            key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
-        compilePredicateArguments subject arguments \subject' compiled ->
-            case fixedSemanticMeaning key of
-                Just (FixedIntrinsic Member) ->
-                    case compiled of
-                        [set] ->
-                            compileMembership
-                                location Raw.Positive subject' set
-                        _ ->
-                            impossible
-                                "the fixed element noun does not have one argument"
-                Just (FixedIntrinsic intrinsic) -> do
-                    (term, actual) <-
-                        applyTyped
-                            location
-                            (CIntrinsic intrinsic)
-                            (coreIntrinsicType intrinsic)
-                            ((\argument -> (argument, TySet))
-                                <$> (subject' : compiled))
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-                Just{} ->
-                    impossible "a fixed noun is not a predicate intrinsic"
-                Nothing ->
-                    applyResolvedPredicate
-                        location key (subject' : compiled)
-
-compileNounPhraseConstraints
-    :: [CanonicalTerm ObjectId]
-    -> [Raw.AdjL]
-    -> Raw.Noun
-    -> [Raw.AdjR]
-    -> Maybe Raw.Stmt
-    -> Elaborate (CanonicalTerm ObjectId)
-compileNounPhraseConstraints subjects left noun right suchThat = do
-    nounConstraints <- traverse (`compileNoun` noun) subjects
-    leftConstraints <- concat
-        <$> traverse
-            (\subject -> traverse (compileLeftAdjective subject) left)
-            subjects
-    rightConstraints <- concat
-        <$> traverse
-            (\subject -> traverse (compileRightAttribute subject) right)
-            subjects
-    suchThatConstraint <- traverse compileStatement suchThat
-    pure
-        (logicalConjunction
-            ( nounConstraints
-                <> leftConstraints
-                <> rightConstraints
-                <> maybeToList suchThatConstraint
-            ))
-
-compileNounPhraseMaybe
-    :: CanonicalTerm ObjectId
-    -> Raw.NounPhrase Maybe
-    -> Elaborate (CanonicalTerm ObjectId)
-compileNounPhraseMaybe subject
-        (Raw.NounPhrase left noun named right suchThat) =
-    case named of
-        Nothing ->
-            compileNounPhraseConstraints
-                [subject] left noun right suchThat
-        Just variable -> do
-            abstracted <-
-                withSetBinders (variable :| [])
-                    (compileNounPhraseConstraints
-                        [CBound 0] left noun right suchThat)
-            pure (instantiateCanonical subject abstracted)
-
-compileExistentialNounPhrase
-    :: Raw.NounPhrase []
-    -> Elaborate (CanonicalTerm ObjectId)
-compileExistentialNounPhrase
-        (Raw.NounPhrase left noun variables right suchThat) =
-    case NonEmpty.nonEmpty variables of
-        Just binders ->
-            withSetBinders binders do
-                subjects <- traverse compileIntroducedVariable binders
-                constraints <-
-                    compileNounPhraseConstraints
-                        (toList subjects) left noun right suchThat
-                pure
-                    (foldr
-                        (const logicalExists)
-                        constraints
-                        binders)
-        Nothing ->
-            withAnonymousSetBinder \subject ->
-                logicalExists
-                    <$> compileNounPhraseConstraints
-                        [subject] left noun right suchThat
-
-compileQuantifiedNounPhrase
-    :: Raw.Quantifier
-    -> Raw.NounPhrase []
-    -> Raw.Stmt
-    -> Elaborate (CanonicalTerm ObjectId)
-compileQuantifiedNounPhrase quantifier
-        (Raw.NounPhrase left noun variables right suchThat)
-        statement =
-    case NonEmpty.nonEmpty variables of
-        Just binders ->
-            withSetBinders binders do
-                subjects <- traverse compileIntroducedVariable binders
-                constraints <-
-                    compileNounPhraseConstraints
-                        (toList subjects) left noun right suchThat
-                body <- compileStatement statement
-                pure
-                    (quantifyNounPhrase
-                        quantifier
-                        (length (toList binders))
-                        constraints
-                        body)
-        Nothing ->
-            withAnonymousSetBinder \subject -> do
-                constraints <-
-                    compileNounPhraseConstraints
-                        [subject] left noun right suchThat
-                body <- compileStatement statement
-                pure (quantifyNounPhrase quantifier 1 constraints body)
-
-quantifyNounPhrase
-    :: Raw.Quantifier
-    -> Int
-    -> CanonicalTerm ObjectId
-    -> CanonicalTerm ObjectId
-    -> CanonicalTerm ObjectId
-quantifyNounPhrase quantifier binderCount constraints body =
-    case quantifier of
-        Raw.Universally ->
-            quantify
-                (if constraints == logicalTruth
-                    then body
-                    else CImp constraints body)
-        Raw.Existentially ->
-            quantify
-                (if constraints == logicalTruth
-                    then body
-                    else logicalAnd constraints body)
-        Raw.Nonexistentially ->
-            logicalNot
-                (quantify
-                    (if constraints == logicalTruth
-                        then body
-                        else logicalAnd constraints body))
-  where
-    quantify scoped =
-        foldr (const binder) scoped [1 .. binderCount]
-    binder = case quantifier of
-        Raw.Universally -> CForall TySet
-        Raw.Existentially -> logicalExists
-        Raw.Nonexistentially -> logicalExists
-
-withAnonymousSetBinder
-    :: (CanonicalTerm ObjectId -> Elaborate value)
-    -> Elaborate value
-withAnonymousSetBinder action = do
-    outer <- State.gets elaborationBinders
-    outerDepth <- State.gets elaborationBinderDepth
-    outerStructures <- State.gets elaborationStructures
-    outerContextual <- State.gets elaborationContextualBinder
-    State.modify' \state ->
-        state
-            { elaborationBinders = (+ 1) <$> outer
-            , elaborationBinderDepth = outerDepth + 1
-            , elaborationStructures =
-                Map.mapKeysMonotonic (+ 1) outerStructures
-            , elaborationContextualBinder = (+ 1) <$> outerContextual
-            }
-    result <- action (CBound 0)
-    State.modify' \state ->
-        state
-            { elaborationBinders = outer
-            , elaborationBinderDepth = outerDepth
-            , elaborationStructures = outerStructures
-            , elaborationContextualBinder = outerContextual
-            }
-    pure result
-
-withSetBinders
-    :: NonEmpty Raw.VarSymbol
-    -> Elaborate value
-    -> Elaborate value
-withSetBinders variables action = do
-    outer <- State.gets elaborationBinders
-    outerDepth <- State.gets elaborationBinderDepth
-    outerStructures <- State.gets elaborationStructures
-    outerContextual <- State.gets elaborationContextualBinder
-    case firstDuplicate (toList variables) of
-        Just duplicate ->
-            Except.throwError
-                (ExactDuplicateLocalBinder
-                    (locate duplicate)
-                    duplicate)
-        Nothing -> pure ()
-    case find (`Map.member` outer) (toList variables) of
-        Just shadowed ->
-            Except.throwError
-                (ExactDuplicateLocalBinder
-                    (locate shadowed)
-                    shadowed)
-        Nothing -> pure ()
-    let binderCount = fromIntegral (length (toList variables))
-        shifted = (+ binderCount) <$> outer
-        introduced =
-            Map.fromList
-                (zip
-                    (toList variables)
-                    (reverse [0 .. binderCount - 1]))
-    State.modify' \state ->
-        state
-            { elaborationBinders = introduced <> shifted
-            , elaborationBinderDepth = outerDepth + binderCount
-            , elaborationStructures =
-                Map.mapKeysMonotonic (+ binderCount) outerStructures
-            , elaborationContextualBinder =
-                (+ binderCount) <$> outerContextual
-            }
-    result <- action
-    State.modify' \state ->
-        state
-            { elaborationBinders = outer
-            , elaborationBinderDepth = outerDepth
-            , elaborationStructures = outerStructures
-            , elaborationContextualBinder = outerContextual
-            }
-    pure result
-
-compileFormula
-    :: Raw.Formula
-    -> Elaborate (CanonicalTerm ObjectId)
-compileFormula = \case
-    Raw.FormulaChain chain ->
-        compileRelationChain chain
-    Raw.PropositionalConstant _ Raw.IsBottom ->
-        pure CFalsum
-    Raw.PropositionalConstant _ Raw.IsTop ->
-        pure (CImp CFalsum CFalsum)
-    Raw.FormulaNeg _ formula ->
-        logicalNot <$> compileFormula formula
-    Raw.FormulaPredicate
-            location
-            (Raw.PrefixPredicate command arity)
-            _marker
-            arguments -> do
-        compiled <- traverse compileExpression arguments
-        (term, actual) <-
-            applyResolvedTyped
-                location
-                (SemanticPrefixPredicate
-                    command
-                    (fromIntegral arity))
-                (toList compiled)
-        unless (actual == TyProp)
-            (Except.throwError
-                (ExactFormulaExpectedProposition location actual))
-        pure term
-    Raw.Connected location connective left right ->
-        compileConnective
-            location
-            connective
-            compileFormula
-            left
-            right
-    Raw.FormulaQuantified
-            _location quantifier variables bound formula ->
-        compileSymbolicQuantified
-            quantifier variables bound Nothing (compileFormula formula)
-compileConnective
-    :: Location
-    -> Raw.Connective
-    -> (input -> Elaborate (CanonicalTerm ObjectId))
-    -> input
-    -> input
-    -> Elaborate (CanonicalTerm ObjectId)
-compileConnective _location connective compile left right = do
-    left' <- compile left
-    right' <- compile right
-    case connective of
-        Raw.Conjunction ->
-            pure (logicalAnd left' right')
-        Raw.Disjunction ->
-            pure (logicalOr left' right')
-        Raw.Implication ->
-            pure (CImp left' right')
-        Raw.Equivalence ->
-            pure (CEq TyProp left' right')
-        Raw.ExclusiveOr ->
-            pure
-                (logicalAnd
-                    (logicalOr left' right')
-                    (logicalNot (logicalAnd left' right')))
-        Raw.NegatedDisjunction ->
-            pure (logicalNot (logicalOr left' right'))
-
-logicalAnd
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-logicalAnd left right =
-    logicalNot (CImp left (logicalNot right))
-
-logicalTruth :: CanonicalTerm global
-logicalTruth =
-    CImp CFalsum CFalsum
-
-logicalConjunction
-    :: (Foldable collection, Eq global)
-    => collection (CanonicalTerm global)
-    -> CanonicalTerm global
-logicalConjunction =
-    foldr combine logicalTruth
-  where
-    combine proposition remaining
-        | proposition == logicalTruth = remaining
-        | remaining == logicalTruth = proposition
-        | otherwise = logicalAnd proposition remaining
-
-logicalOr
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-    -> CanonicalTerm global
-logicalOr left right =
-    CImp (logicalNot left) right
-
-logicalExists
-    :: CanonicalTerm global
-    -> CanonicalTerm global
-logicalExists body =
-    logicalNot (CForall TySet (logicalNot body))
-
-compileAtomicRelation
-    :: NonEmpty Raw.Expr
-    -> Raw.Relation
-    -> NonEmpty Raw.Expr
-    -> Elaborate (CanonicalTerm ObjectId)
-compileAtomicRelation left relation right =
-    case (toList left, relation, toList right) of
-        ([leftExpression], Raw.Relation location symbol parameters, [rightExpression]) -> do
-            let key =
-                    SemanticRelation
-                        (Raw.relationSymbolToken symbol)
-                        (Raw.relationSymbolParameterArity symbol)
-            case fixedSemanticMeaning key of
-                Just FixedEquality
-                    | null parameters -> do
-                        left' <- compileExpressionAsSet leftExpression
-                        right' <- compileExpressionAsSet rightExpression
-                        pure (CEq TySet left' right')
-                    | otherwise ->
-                        Except.throwError
-                            (ExactUnsupportedDeclarationBody location)
-                Just FixedDisequality
-                    | null parameters -> do
-                        left' <- compileExpressionAsSet leftExpression
-                        right' <- compileExpressionAsSet rightExpression
-                        pure (logicalNot (CEq TySet left' right'))
-                    | otherwise ->
-                        Except.throwError
-                            (ExactUnsupportedDeclarationBody location)
-                Just (FixedIntrinsic Member)
-                    | null parameters -> do
-                        left' <- compileExpressionAsSet leftExpression
-                        right' <- compileExpressionAsSet rightExpression
-                        compileMembership
-                            location Raw.Positive left' right'
-                Just (FixedNegatedIntrinsic Member)
-                    | null parameters -> do
-                        left' <- compileExpressionAsSet leftExpression
-                        right' <- compileExpressionAsSet rightExpression
-                        compileMembership
-                            location Raw.Negative left' right'
-                Just (FixedIntrinsic intrinsic) -> do
-                    compiled <- traverse compileExpression
-                        (parameters <> [leftExpression, rightExpression])
-                    (term, actual) <-
-                        applyTyped
-                            location
-                            (CIntrinsic intrinsic)
-                            (coreIntrinsicType intrinsic)
-                            compiled
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-                Just (FixedNegatedIntrinsic intrinsic) -> do
-                    compiled <- traverse compileExpression
-                        (parameters <> [leftExpression, rightExpression])
-                    (term, actual) <-
-                        applyTyped
-                            location
-                            (CIntrinsic intrinsic)
-                            (coreIntrinsicType intrinsic)
-                            compiled
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure (logicalNot term)
-                Nothing -> do
-                    compiled <- traverse compileExpression
-                        (parameters <> [leftExpression, rightExpression])
-                    (term, actual) <-
-                        applyResolvedTyped location key compiled
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-        ([leftExpression], Raw.RelationExpr location expression, [rightExpression]) -> do
-            left' <- compileExpressionAsSet leftExpression
-            right' <- compileExpressionAsSet rightExpression
-            compileRelationExpression location expression left' right'
-        _ ->
-            Except.throwError
-                (ExactUnsupportedDeclarationBody (locate relation))
-
-compileRelationExpression
-    :: Location
-    -> Raw.Expr
-    -> CanonicalTerm ObjectId
-    -> CanonicalTerm ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-compileRelationExpression location expression left right = do
-    relation <- compileExpressionAsSet expression
-    pair <-
-        applyResolved
-            location
-            (SemanticExpressionFunction
-                (Raw.mixfixPattern Raw.PairSymbol))
-            [left, right]
-    compileMembership location Raw.Positive pair relation
-
-compileRelationChain
-    :: Raw.Chain
-    -> Elaborate (CanonicalTerm ObjectId)
-compileRelationChain chain =
-    logicalConjunction <$> traverse compileLink (chainLinks chain)
-  where
-    compileLink (sign, relation, left, right) = do
-        proposition <-
-            compileAtomicRelation
-                (left :| []) relation (right :| [])
-        pure case sign of
-            Raw.Positive -> proposition
-            Raw.Negative -> logicalNot proposition
-
-    chainLinks = \case
-        Raw.ChainBase left sign relation right ->
-            [ (sign, relation, leftExpression, rightExpression)
-            | leftExpression <- toList left
-            , rightExpression <- toList right
-            ]
-        Raw.ChainCons left sign relation rest ->
-            let firstRight = chainFirstLeft rest
-            in
-                [ (sign, relation, leftExpression, rightExpression)
-                | leftExpression <- toList left
-                , rightExpression <- toList firstRight
-                ]
-                <> chainLinks rest
-
-    chainFirstLeft = \case
-        Raw.ChainBase left _sign _relation _right -> left
-        Raw.ChainCons left _sign _relation _rest -> left
-
-applyResolved
-    :: Location
-    -> SemanticGlobalKey
-    -> [CanonicalTerm ObjectId]
-    -> Elaborate (CanonicalTerm ObjectId)
-applyResolved location key arguments = do
-    (term, actual) <-
-        applyResolvedTyped
-            location key ((\argument -> (argument, TySet)) <$> arguments)
-    unless (actual == TySet)
-        (Except.throwError
-            (ExactExpressionExpectedSet location actual))
-    pure term
-
-applyResolvedPredicate
-    :: Location
-    -> SemanticGlobalKey
-    -> [CanonicalTerm ObjectId]
-    -> Elaborate (CanonicalTerm ObjectId)
-applyResolvedPredicate location key =
-    applyResolvedPredicateChoice location (key :| [])
-
-applyResolvedPredicateChoice
-    :: Location
-    -> NonEmpty SemanticGlobalKey
-    -> [CanonicalTerm ObjectId]
-    -> Elaborate (CanonicalTerm ObjectId)
-applyResolvedPredicateChoice location keys arguments = do
-    case firstFixedMeaning (toList keys) of
-        Just meaning ->
-            maybe
-                (impossible
-                    "a fixed equality predicate has an invalid source arity")
-                pure
-                (lowerFixedEqualityPredicate meaning arguments)
-        Nothing -> do
-            visible <- for (toList keys) \key -> do
-                found <-
-                    State.lift
-                        (Except.lift
-                            (Declaration.resolveVisibleGlobalLowering key))
-                pure ((\target -> (key, target)) <$> found)
-            case catMaybes visible of
-                [(key, _target)] -> do
-                    (term, actual) <-
-                        applyResolvedTyped
-                            location key
-                            ((\argument -> (argument, TySet)) <$> arguments)
-                    unless (actual == TyProp)
-                        (Except.throwError
-                            (ExactFormulaExpectedProposition location actual))
-                    pure term
-                [] ->
-                    Except.throwError
-                        (ExactGlobalNotVisible location (NonEmpty.head keys))
-                _ ->
-                    impossible
-                        "one adjective surface resolves to several exact globals"
-  where
-    firstFixedMeaning =
-        foldr
-            (\key found -> fixedSemanticMeaning key <|> found)
-            Nothing
-
-applyResolvedTyped
-    :: Location
-    -> SemanticGlobalKey
-    -> [(CanonicalTerm ObjectId, CoreType)]
-    -> Elaborate (CanonicalTerm ObjectId, CoreType)
-applyResolvedTyped location key arguments = do
-    visible <-
-        State.lift
-            (Except.lift
-                (Declaration.resolveVisibleGlobalContentLowering key))
-    (target, content, dependencies) <-
-        maybe
-            (Except.throwError (ExactGlobalNotVisible location key))
-            pure
-            visible
-    case target of
-        GlobalReference identity -> do
-            let coreType = objectContentType content
-            State.modify' \state ->
-                state
-                    { elaborationGlobals =
-                        Map.insert
-                            identity coreType
-                            (elaborationGlobals state)
-                    }
-            applyTyped location (CGlobal identity) coreType arguments
-        TransparentExpansion _identity ->
-            case content of
-                TransparentObjectContent _theory coreType body -> do
-                    State.modify' \state ->
-                        state
-                            { elaborationGlobals =
-                                Map.union
-                                    dependencies
-                                    (elaborationGlobals state)
-                            }
-                    applyExpandedTyped
-                        location body coreType arguments
-                _ ->
-                    impossible
-                        "validated transparent expansion has opaque content"
-        ContextualTransparentExpansion _identity requirements ->
-            case content of
-                TransparentObjectContent _theory coreType body -> do
-                    State.modify' \state ->
-                        state
-                            { elaborationGlobals =
-                                Map.union
-                                    dependencies
-                                    (elaborationGlobals state)
-                            }
-                    contextArgument <-
-                        resolveContextualExpansionArgument
-                            location key requirements
-                    applyExpandedTyped
-                        location body coreType
-                        ((contextArgument, TySet) : arguments)
-                _ ->
-                    impossible
-                        "validated contextual expansion has opaque content"
-
-resolveContextualExpansionArgument
-    :: Location
-    -> SemanticGlobalKey
-    -> Map.Map Raw.StructSymbol ObjectId
-    -> Elaborate (CanonicalTerm ObjectId)
-resolveContextualExpansionArgument location key requirements = do
-    contextual <- State.gets elaborationContextualBinder
-    case contextual of
-        Just index -> do
-            traverse_
-                (uncurry (recordContextualRequirement location))
-                (Map.toAscList requirements)
-            pure (CBound index)
-        Nothing -> do
-            structures <- State.gets elaborationStructures
-            case
-                [ CBound index
-                | (index, structure) <- Map.toAscList structures
-                , all
-                    (\(symbol, object) ->
-                        structureAnnotationOperation symbol structure
-                            == Just object)
-                    (Map.toAscList requirements)
-                ] of
-                firstMatch : _ -> pure firstMatch
-                [] ->
-                    Except.throwError
-                        (ExactContextualExpansionNotAvailable location key)
-
-applyExpandedTyped
-    :: Location
-    -> CanonicalTerm ObjectId
-    -> CoreType
-    -> [(CanonicalTerm ObjectId, CoreType)]
-    -> Elaborate (CanonicalTerm ObjectId, CoreType)
-applyExpandedTyped location body coreType arguments =
-    foldM step (body, coreType) arguments
-  where
-    step (current, currentType) (argument, argumentType) =
-        case currentType of
-            TyArrow expected result
-                | expected == argumentType ->
-                    pure
-                        ( case current of
-                            CLam binderType lambdaBody
-                                | binderType == expected ->
-                                    instantiateCanonical
-                                        argument lambdaBody
-                            _ -> CApp current argument
-                        , result
-                        )
-                | otherwise ->
-                    Except.throwError
-                        (ExactApplicationArgumentMismatch
-                            location expected argumentType)
-            actual ->
-                Except.throwError
-                    (ExactApplicationExpectedFunction location actual)
-
-applyTyped
-    :: Location
-    -> CanonicalTerm ObjectId
-    -> CoreType
-    -> [(CanonicalTerm ObjectId, CoreType)]
-    -> Elaborate (CanonicalTerm ObjectId, CoreType)
-applyTyped location function functionType arguments =
-    foldM step (function, functionType) arguments
-  where
-    step (currentFunction, currentType) (argument, argumentType) =
-        case currentType of
-            TyArrow expected result
-                | expected == argumentType ->
-                    pure (CApp currentFunction argument, result)
-                | otherwise ->
-                    Except.throwError
-                        (ExactApplicationArgumentMismatch
-                            location expected argumentType)
-            actual ->
-                Except.throwError
-                    (ExactApplicationExpectedFunction location actual)
-
-logicalNot :: CanonicalTerm global -> CanonicalTerm global
-logicalNot proposition =
-    CImp proposition CFalsum
-
-ensureExpressionKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.FunctionSymbol
-    -> SemanticGlobalKey
-    -> monad ()
-ensureExpressionKey location symbol key =
-    unless
-        (key == SemanticExpressionFunction (Raw.mixfixPattern symbol))
-        (throwError (ExactDeclarationHeadMismatch location))
-
-ensureAdjectiveKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.LexicalItem
-    -> SemanticGlobalKey
-    -> monad ()
-ensureAdjectiveKey location item key =
-    unless
-        ( key == SemanticLeftAdjective (Raw.lexicalItemPattern item)
-          || key == SemanticRightAdjective (Raw.lexicalItemPattern item)
-        )
-        (throwError (ExactDeclarationHeadMismatch location))
-
-ensureFunctionPhraseKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.LexicalItemSgPl
-    -> SemanticGlobalKey
-    -> monad ()
-ensureFunctionPhraseKey location item key =
-    let patterns = Raw.lexicalItemSgPlPattern item
-    in unless
-        (key == SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns))
-        (throwError (ExactDeclarationHeadMismatch location))
-
-ensureNounKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.LexicalItemSgPl
-    -> SemanticGlobalKey
-    -> monad ()
-ensureNounKey location item key =
-    let patterns = Raw.lexicalItemSgPlPattern item
-    in unless
-        (key == SemanticNoun (Raw.sg patterns) (Raw.pl patterns))
-        (throwError (ExactDeclarationHeadMismatch location))
-
-ensureVerbKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.LexicalItemSgPl
-    -> SemanticGlobalKey
-    -> monad ()
-ensureVerbKey location item key =
-    let patterns = Raw.lexicalItemSgPlPattern item
-    in unless
-        (key == SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
-        (throwError (ExactDeclarationHeadMismatch location))
-
-ensureRelationKey
-    :: MonadError ExactCompileError monad
-    => Location
-    -> Raw.RelationSymbol
-    -> SemanticGlobalKey
-    -> monad ()
-ensureRelationKey location relation key =
-    unless
-        ( key
-            == SemanticRelation
-                (Raw.relationSymbolToken relation)
-                (Raw.relationSymbolParameterArity relation)
-        )
-        (throwError (ExactDeclarationHeadMismatch location))
-
-exactSetNounPhrase :: Raw.NounPhrase Maybe -> Bool
-exactSetNounPhrase = \case
-    Raw.NounPhrase
-            []
-            (Raw.Noun _ item [])
-            Nothing
-            []
-            Nothing ->
-        Lexicon.isBuiltinSetNoun item
-    _ -> False
-
-encodePreparedSyntax
-    :: ExactDeclarationFamily
-    -> PreparedHead
-    -> PreparedBody
-    -> Maybe SemanticName
-    -> ByteString
-encodePreparedSyntax
-        family (PreparedHead key _parameters coreType) body alias =
-    encodeCache do
-        putCacheTag case family of
-            ExactSignature -> 0x00
-            ExactAbbreviation -> 0x01
-            ExactDefinition -> 0x02
-        putSemanticGlobalKeyCache key
-        putCoreTypeCache coreType
-        case body of
-            OpaqueBody -> putCacheTag 0x00
-            TransparentBody canonical _construction -> do
-                putCacheTag 0x01
-                putCanonicalTermCache putObjectIdCache canonical
-            ContextualTransparentBody requirements canonical -> do
-                putCacheTag 0x02
-                putCanonicalCacheMap
-                    (\(Raw.StructSymbol symbol) -> putCacheText symbol)
-                    putObjectIdCache
-                    requirements
-                putCanonicalTermCache putObjectIdCache canonical
-        putCacheMaybe
-            (putCacheText . semanticNameText)
-            alias
-
-encodePreparedSourceAxiom
-    :: ScopedCheckedCore ObjectId
-    -> SemanticName
-    -> ByteString
-encodePreparedSourceAxiom proposition alias =
-    encodeCache do
-        putCacheTag 0x03
-        putCanonicalTermCache putObjectIdCache
-            (scopedCoreTerm proposition)
-        putCacheText (semanticNameText alias)
-
-definitionAlias :: Raw.Block -> Maybe SemanticName
-definitionAlias = \case
-    Raw.BlockDefn _location _title (Raw.Marker marker) _definition ->
-        Just (semanticName marker)
-    _ -> Nothing
-
-firstDuplicate :: Ord value => [value] -> Maybe value
-firstDuplicate =
-    go Set.empty
-  where
-    go _seen [] = Nothing
-    go seen (value : rest)
-        | value `Set.member` seen = Just value
-        | otherwise = go (Set.insert value seen) rest