Bind typed fact admission to module builders

3 files changed, 598 insertions, 261 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index e94aa3f..9491f5f 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -2049,34 +2049,24 @@ prepareTypedGroundReflexivity context staged st = do
             (checkingOwnedSymbols st)
             (checkingDependencies st)
             (Facts.stagedFactSemantic staged)
-        admitted <-
-            first
-                (checkingErrorAt context
-                    . ("typed reflexivity replay failed: "
-                        <>)
-                    . Text.pack
-                    . show)
-                (Transition.authorizeTransitionKernelFact
-                    (TypedReflexivity.groundReflexivityTarget
-                        typed)
-                    (TypedReflexivity.groundReflexivityDerivation
-                        typed)
-                    builder)
         builder' <-
             first
                 (checkingErrorAt context
-                    . ("typed reflexivity registration failed: "
+                    . ("typed reflexivity admission failed: "
                         <>)
                     . Text.pack
                     . show)
-                (Transition.commitTransitionTypedFact
+                (Transition.commitTransitionKernelFact
                     (blockContextMarker context :| [])
                     (Transition.origin
                         (blockContextLocation context)
                         Nothing
                         (Just
                             (blockContextMarker context)))
-                    admitted
+                    (TypedReflexivity.groundReflexivityTarget
+                        typed)
+                    (TypedReflexivity.groundReflexivityDerivation
+                        typed)
                     builder)
         pure
             st
@@ -2110,14 +2100,6 @@ prepareTypedAtomicAssumption context staged st = do
                     context
                     "typed atomic preparation failed: ")
                 preparation
-        semantic <-
-            first
-                (typedFactError
-                    context
-                    "typed atomic fact preparation failed: ")
-                (Transition.prepareTypedSemanticFact
-                    (TypedAtomic.closedAtomicStatement
-                        prepared))
         markers' <-
             validateTypedFactState
                 context
@@ -2132,7 +2114,8 @@ prepareTypedAtomicAssumption context staged st = do
                     (blockContextMarker context :| [])
                     (typedFactOrigin context)
                     DeclaredUserAxiom
-                    semantic
+                    (TypedAtomic.closedAtomicStatement
+                        prepared)
                     builder)
         pure
             (publishTypedFactState
@@ -2185,27 +2168,19 @@ prepareTypedAtomicReuse context staged st = do
                                 context
                                 staged
                                 st
-                        admitted <-
+                        builder' <-
                             first
                                 (typedFactError
                                     context
-                                    "typed imported-fact replay failed: ")
-                                (Transition.authorizeTransitionKernelFactWithImports
+                                    "typed imported-fact admission failed: ")
+                                (Transition.commitTransitionKernelFactWithImports
+                                    (blockContextMarker context :| [])
+                                    (typedFactOrigin context)
                                     (Vector.singleton imported)
                                     target
                                     (importedFactDerivation
                                         (importIx 0))
                                     builder)
-                        builder' <-
-                            first
-                                (typedFactError
-                                    context
-                                    "typed imported-fact registration failed: ")
-                                (Transition.commitTransitionTypedFact
-                                    (blockContextMarker context :| [])
-                                    (typedFactOrigin context)
-                                    admitted
-                                    builder)
                         pure
                             (publishTypedFactState
                                 context
@@ -3363,34 +3338,23 @@ commitTypedInductiveFact
     -> TypedInductive.PreparedTypedInductiveFact
     -> CheckingM Transition.TransitionModuleBuilder
 commitTypedInductiveFact context imports builder fact = do
-    admitted <-
-        either
-            ( throwIO
-                . typedInductiveError
-                    context
-                    "typed inductive replay failed: "
-            )
-            pure
-            (Transition.authorizeTransitionKernelFactWithImports
-                imports
-                (TypedInductive.typedInductiveFactTarget
-                    fact)
-                (TypedInductive.typedInductiveFactDerivation
-                    fact)
-                builder)
     either
         ( throwIO
             . typedInductiveError
                 context
-                "typed inductive fact registration failed: "
+                "typed inductive fact admission failed: "
         )
         pure
-        (Transition.commitTransitionTypedFact
+        (Transition.commitTransitionKernelFactWithImports
             (TypedInductive.typedInductiveFactMarker
                 fact
                 :| [])
             (typedFactOrigin context)
-            admitted
+            imports
+            (TypedInductive.typedInductiveFactTarget
+                fact)
+            (TypedInductive.typedInductiveFactDerivation
+                fact)
             builder)
 
 commitTypedInductiveState
diff --git a/source/Checking/Transition.hs b/source/Checking/Transition.hs
index 31c14cd..f406a5d 100644
--- a/source/Checking/Transition.hs
+++ b/source/Checking/Transition.hs
@@ -27,10 +27,6 @@ module Checking.Transition
     , factReferenceOrdinal
     , TransitionFactRef
     , transitionTypedFactReference
-    , TypedSemanticFact
-    , prepareTypedSemanticFact
-    , typedSemanticStatement
-    , typedSemanticFofCapability
     , TypedDirectAxiomManifestEntry
     , typedDirectAssumptionFact
     , typedDirectAssumptionKind
@@ -47,14 +43,9 @@ module Checking.Transition
     , typedVampireLoweringUses
     , typedFoundationUses
     , typedKernelRuleUses
-    , TypedAdmittedFact
-    , authorizeTransitionKernelFact
     , TransitionDerivationImport
     , transitionDerivationImport
     , lookupTransitionTypedImport
-    , authorizeTransitionKernelFactWithImports
-    , typedAdmittedStatement
-    , typedAdmittedTrustDependencies
     , AdmittedFact
     , admittedFactReference
     , admittedFactIsKernelProof
@@ -72,7 +63,8 @@ module Checking.Transition
     , transitionCurrentDeclarationReference
     , commitTransitionOpaqueGlobal
     , commitTransitionTransparentGlobal
-    , commitTransitionTypedFact
+    , commitTransitionKernelFact
+    , commitTransitionKernelFactWithImports
     , commitTransitionTypedVampireFact
     , commitTransitionTypedDeclaredAssumption
     , transitionBuilderWithLegacyStage
@@ -269,29 +261,35 @@ data TypedSemanticFact = TypedSemanticFact
     deriving stock (Eq)
 
 prepareTypedSemanticFact
-    :: FrozenCheckedCore CheckedGlobalRef
+    :: TransitionModuleBuilder
+    -> FrozenCheckedCore CheckedGlobalRef
     -> Either TransitionModuleError TypedSemanticFact
-prepareTypedSemanticFact statement
-    | frozenCoreType statement /= TyProp =
-        Left
-            (TransitionTypedFactIsNotProposition
-                (frozenCoreType statement))
-    | otherwise = do
-        proposition <-
-            first TransitionTypedFactSupportError
-                (Backend.supportedProposition
-                    Vector.empty
-                    (embedClosedCore [] statement))
-        capability <-
-            first TransitionTypedFactClassificationError
-                (Backend.classifySupportedProposition
-                    (Just . checkedGlobalType)
-                    proposition)
-        Right
-            (TypedSemanticFact
-                statement
-                proposition
-                capability)
+prepareTypedSemanticFact builder supplied = do
+    statement <-
+        recheckBuilderFrozenCore builder supplied
+    prepare statement
+  where
+    prepare statement
+        | frozenCoreType statement /= TyProp =
+            Left
+                (TransitionTypedFactIsNotProposition
+                    (frozenCoreType statement))
+        | otherwise = do
+            proposition <-
+                first TransitionTypedFactSupportError
+                    (Backend.supportedProposition
+                        Vector.empty
+                        (embedClosedCore [] statement))
+            capability <-
+                first TransitionTypedFactClassificationError
+                    (Backend.classifySupportedProposition
+                        (builderGlobalType builder)
+                        proposition)
+            Right
+                (TypedSemanticFact
+                    statement
+                    proposition
+                    capability)
 
 typedSemanticStatement
     :: TypedSemanticFact
@@ -508,18 +506,49 @@ data TypedAdmittedFact = TypedAdmittedFact
     !FactAuthorization
     deriving stock (Eq)
 
-authorizeTransitionKernelFact
-    :: FrozenCheckedCore CheckedGlobalRef
+commitTransitionKernelFact
+    :: NonEmpty Marker
+    -> Origin
+    -> FrozenCheckedCore CheckedGlobalRef
     -> KernelDerivation CheckedGlobalRef
     -> TransitionModuleBuilder
-    -> Either TransitionModuleError TypedAdmittedFact
-authorizeTransitionKernelFact target derivation builder =
-    authorizeTransitionKernelFactWithImports
+    -> Either TransitionModuleError TransitionModuleBuilder
+commitTransitionKernelFact aliases factOrigin target derivation builder =
+    commitTransitionKernelFactWithImports
+        aliases
+        factOrigin
         Vector.empty
         target
         derivation
         builder
 
+commitTransitionKernelFactWithImports
+    :: NonEmpty Marker
+    -> Origin
+    -> Vector TransitionDerivationImport
+    -> FrozenCheckedCore CheckedGlobalRef
+    -> KernelDerivation CheckedGlobalRef
+    -> TransitionModuleBuilder
+    -> Either TransitionModuleError TransitionModuleBuilder
+commitTransitionKernelFactWithImports
+        aliases
+        factOrigin
+        imports
+        target
+        derivation
+        builder = do
+    admitted <-
+        authorizeTransitionKernelFactWithImports
+            imports
+            target
+            derivation
+            builder
+    insertTransitionTypedFact
+        aliases
+        factOrigin
+        admitted
+        builder
+
 data TransitionDerivationImport =
     TransitionDerivationImport
         !TransitionFactRef
@@ -603,16 +632,18 @@ authorizeTransitionKernelFactWithImportsAndProvenance
         derivation
         builder = do
     semantic <-
-        prepareTypedSemanticFact target
+        prepareTypedSemanticFact builder target
+    let checkedTarget =
+            typedSemanticStatement semantic
     replayed <-
         first TransitionKernelReplayError
             (replayKernelDerivation
                 (builderFoundation builder)
                 defaultKernelReplayLimits
-                (Just . checkedGlobalType)
+                (builderGlobalType builder)
                 (derivationImport
                     <$> imports)
-                target
+                checkedTarget
                 derivation)
     inheritedTrust <-
         foldM
@@ -927,6 +958,8 @@ data TransitionModuleBuilder = TransitionModuleBuilder
     , builderEnvironmentDeltas
         :: !(Vector TypedModuleEnvironmentDelta)
     , builderGlobals :: !(Map Symbol TypedGlobalBinding)
+    , builderGlobalDeclarations
+        :: !(Map OpaqueDeclarationRef TypedGlobalBinding)
     , builderLocalGlobalsReversed :: ![TypedGlobalBinding]
     , builderImportedFacts :: !(Vector TransitionFactEntry)
     , builderLocalFactsReversed :: ![TransitionFactEntry]
@@ -958,7 +991,7 @@ openTransitionModuleBuilder
                 (legacyImportedView
                     foundation
                     (transitionAdmittedLegacyModule <$> directImports))
-        (environmentDeltas, globals) <-
+        (environmentDeltas, globals, globalDeclarations) <-
             mergeTypedEnvironments directImports
         (importedFacts, factAliases) <-
             mergeTransitionFacts directImports
@@ -977,6 +1010,8 @@ openTransitionModuleBuilder
                 , builderEnvironmentDeltas =
                     environmentDeltas
                 , builderGlobals = globals
+                , builderGlobalDeclarations =
+                    globalDeclarations
                 , builderLocalGlobalsReversed = []
                 , builderImportedFacts = importedFacts
                 , builderLocalFactsReversed = []
@@ -1008,6 +1043,107 @@ transitionBuilderFoundation
 transitionBuilderFoundation =
     builderFoundation
 
+builderGlobalType
+    :: TransitionModuleBuilder
+    -> CheckedGlobalRef
+    -> Maybe CoreType
+builderGlobalType builder reference =
+    case Map.lookup
+            (checkedGlobalReference reference)
+            (builderGlobalDeclarations builder) of
+        Just
+            (TypedGlobalBinding
+                _symbol
+                authoritative
+                _origin
+                _body)
+            | checkedGlobalType reference
+                == checkedGlobalType authoritative ->
+                    Just (checkedGlobalType authoritative)
+        _ ->
+            Nothing
+
+validateBuilderGlobalReference
+    :: TransitionModuleBuilder
+    -> CheckedGlobalRef
+    -> Either TransitionModuleError CoreType
+validateBuilderGlobalReference builder reference =
+    case Map.lookup
+            (checkedGlobalReference reference)
+            (builderGlobalDeclarations builder) of
+        Nothing ->
+            Left
+                (TransitionGlobalReferenceNotVisible
+                    reference)
+        Just
+            (TypedGlobalBinding
+                _symbol
+                authoritative
+                _origin
+                _body)
+            | checkedGlobalType reference
+                == checkedGlobalType authoritative ->
+                    Right (checkedGlobalType authoritative)
+            | otherwise ->
+                Left
+                    (TransitionGlobalReferenceTypeMismatch
+                        reference
+                        (checkedGlobalType authoritative))
+
+validateBuilderCanonicalGlobals
+    :: TransitionModuleBuilder
+    -> CanonicalTerm CheckedGlobalRef
+    -> Either TransitionModuleError ()
+validateBuilderCanonicalGlobals builder =
+    traverse_
+        (void . validateBuilderGlobalReference builder)
+        . Set.toAscList
+        . canonicalTermGlobals
+
+recheckBuilderFrozenCore
+    :: TransitionModuleBuilder
+    -> FrozenCheckedCore CheckedGlobalRef
+    -> Either
+        TransitionModuleError
+        (FrozenCheckedCore CheckedGlobalRef)
+recheckBuilderFrozenCore builder supplied = do
+    validateBuilderCanonicalGlobals
+        builder
+        (frozenCoreTerm supplied)
+    first TransitionCoreCheckError
+        (checkCanonicalCore
+            (builderGlobalType builder)
+            (frozenCoreTerm supplied))
+
+canonicalTermGlobals
+    :: Ord global
+    => CanonicalTerm global
+    -> Set global
+canonicalTermGlobals = \case
+    CBound{} ->
+        mempty
+    CGlobal global ->
+        Set.singleton global
+    CIntrinsic{} ->
+        mempty
+    COpaqueInteger{} ->
+        mempty
+    CApp function argument ->
+        canonicalTermGlobals function
+            <> canonicalTermGlobals argument
+    CLam _binderType body ->
+        canonicalTermGlobals body
+    CFalsum ->
+        mempty
+    CImp premise conclusion ->
+        canonicalTermGlobals premise
+            <> canonicalTermGlobals conclusion
+    CEq _operandType left right ->
+        canonicalTermGlobals left
+            <> canonicalTermGlobals right
+    CForall _binderType body ->
+        canonicalTermGlobals body
+
 planTransitionTypedProblem
     :: Ord local
     => TransitionModuleBuilder
@@ -1038,15 +1174,26 @@ planTransitionTypedProblem
         auxiliaries
         globalPolicy
         localPolicy = do
+    first TransitionTypedProblemGlobalValidationError
+        (do
+            validateBuilderCanonicalGlobals
+                builder
+                (Backend.supportedPropositionTerm claim)
+            traverse_
+                ( validateBuilderCanonicalGlobals builder
+                    . Backend.supportedPropositionTerm
+                    . Backend.typedLocalPremiseProposition
+                )
+                localPremises)
     validateExplicitTypedDependencies
     inventory <-
         first TransitionTypedProblemInventoryError
             (Backend.prepareTypedFactInventory
-                (Just . checkedGlobalType)
+                (builderGlobalType builder)
                 typedInputs)
     first TransitionTypedProblemPlanningError
         (Backend.planTypedProblem
-            (Just . checkedGlobalType)
+            (builderGlobalType builder)
             inventory
             claim
             localPremises
@@ -1113,7 +1260,9 @@ planTransitionTypedProblem
                         semantic))
 
 data TransitionTypedProblemError local
-    = TransitionTypedProblemDependencyNotMigrated
+    = TransitionTypedProblemGlobalValidationError
+        !TransitionModuleError
+    | TransitionTypedProblemDependencyNotMigrated
         !TransitionFactRef
     | TransitionTypedProblemInventoryError
         !(Backend.TypedFactInventoryError
@@ -1185,37 +1334,20 @@ commitTransitionTransparentGlobal
         body
         bindingOrigin
         builder = do
+    checkedBody <-
+        recheckBuilderFrozenCore builder body
     unless
-        (frozenCoreType body == coreType)
+        (frozenCoreType checkedBody == coreType)
         (Left
             (TransitionTransparentGlobalTypeMismatch
                 symbol
                 coreType
-                (frozenCoreType body)))
-    let visibleReferences =
-            Set.fromList
-                [ reference
-                | TypedGlobalBinding
-                    _visibleSymbol
-                    reference
-                    _visibleOrigin
-                    _visibleBody <-
-                        Map.elems (builderGlobals builder)
-                ]
-        unavailable =
-            frozenCoreGlobals body
-                `Set.difference` visibleReferences
-    unless
-        (Set.null unavailable)
-        (Left
-            (TransitionTransparentGlobalDependencyNotVisible
-                symbol
-                unavailable))
+                (frozenCoreType checkedBody)))
     commitTransitionGlobal
         symbol
         coreType
         bindingOrigin
-        (Just body)
+        (Just checkedBody)
         builder
 
 commitTransitionGlobal
@@ -1234,53 +1366,57 @@ commitTransitionGlobal
     case transitionCurrentDeclarationReference builder of
         Nothing ->
             Left TransitionDeclarationNotOpen
-        Just reference ->
+        Just reference -> do
+            let binding =
+                    TypedGlobalBinding
+                        symbol
+                        (CheckedOpaqueGlobal
+                            reference
+                            coreType)
+                        bindingOrigin
+                        body
             case Map.lookup symbol
                     (builderGlobals builder) of
-                Just (TypedGlobalBinding
-                    _previousSymbol
-                    previousReference
-                    previousOrigin
-                    _previousBody) ->
-                        Left
-                            (TransitionGlobalConflict
-                                symbol
-                                previousReference
-                                previousOrigin
-                                (CheckedOpaqueGlobal
-                                    reference
-                                    coreType)
-                                bindingOrigin)
+                Just previous ->
+                    Left
+                        (globalSymbolConflict
+                            previous
+                            binding)
                 Nothing ->
-                    Right
-                        builder
-                            { builderGlobals =
-                                Map.insert
-                                    symbol
-                                    binding
-                                    (builderGlobals builder)
-                            , builderLocalGlobalsReversed =
-                                binding
-                                    : builderLocalGlobalsReversed
-                                        builder
-                            }
-          where
-            binding =
-                TypedGlobalBinding
-                    symbol
-                    (CheckedOpaqueGlobal
-                        reference
-                        coreType)
-                    bindingOrigin
-                    body
-
-commitTransitionTypedFact
+                    pure ()
+            case Map.lookup reference
+                    (builderGlobalDeclarations builder) of
+                Just previous ->
+                    Left
+                        (globalReferenceConflict
+                            previous
+                            binding)
+                Nothing ->
+                    pure ()
+            (globals, declarations) <-
+                insertVisibleGlobalBinding
+                    ( builderGlobals builder
+                    , builderGlobalDeclarations builder
+                    )
+                    binding
+            Right
+                builder
+                    { builderGlobals = globals
+                    , builderGlobalDeclarations =
+                        declarations
+                    , builderLocalGlobalsReversed =
+                        binding
+                            : builderLocalGlobalsReversed
+                                builder
+                    }
+
+insertTransitionTypedFact
     :: NonEmpty Marker
     -> Origin
     -> TypedAdmittedFact
     -> TransitionModuleBuilder
     -> Either TransitionModuleError TransitionModuleBuilder
-commitTransitionTypedFact aliases factOrigin admitted builder = do
+insertTransitionTypedFact aliases factOrigin admitted builder = do
     factReference <-
         nextTransitionTypedFactReference builder
     let ordinal =
@@ -1332,7 +1468,9 @@ commitTransitionTypedVampireFact
         accepted
         builder = do
     semantic <-
-        prepareTypedSemanticFact target
+        prepareTypedSemanticFact builder target
+    let checkedTarget =
+            typedSemanticStatement semantic
     let problem =
             Provers.preparedTypedProverLogicalProblem
                 preparedTask
@@ -1343,7 +1481,7 @@ commitTransitionTypedVampireFact
             (Backend.supportedPropositionSupport
                 claim)
           && Backend.supportedPropositionTerm claim
-                == frozenCoreTerm target
+                == frozenCoreTerm checkedTarget
         )
         (Left TransitionTypedVampireTargetMismatch)
     unless
@@ -1390,6 +1528,7 @@ commitTransitionTypedVampireFact
             commitReconstructed
                 reconstructionPolicy
                 imports
+                checkedTarget
                 reconstructed
         BackendReconstruction.ReconstructionUnsupported{} ->
             commitTrusted
@@ -1415,6 +1554,7 @@ commitTransitionTypedVampireFact
     commitReconstructed
             policy
             imports
+            checkedTarget
             reconstructed = do
         let connectionReplay =
                 BackendReconstruction.reconstructedConnectionReplay
@@ -1439,11 +1579,11 @@ commitTransitionTypedVampireFact
             authorizeTransitionKernelFactWithImportsAndProvenance
                 (Just provenance)
                 imports
-                target
+                checkedTarget
                 (BackendConnection.replayedConnectionDerivation
                     connectionReplay)
                 builder
-        commitTransitionTypedFact
+        insertTransitionTypedFact
             aliases
             factOrigin
             admitted
@@ -1473,31 +1613,28 @@ commitTransitionTypedVampireFact
                     (TrustedVampire
                         (SessionTypedTrustedVampireEvidence
                             factReference
-                            target
+                            (typedSemanticStatement semantic)
                             (Provers.preparedTypedProverTptpProblem
                                 preparedTask)
                             accepted
                             trust))
-        commitTransitionTypedFact
+        insertTransitionTypedFact
             aliases
             factOrigin
             admitted
             builder
 
-    validateGlobalType (global, reportedType) =
-        if global `Set.notMember` visibleGlobals
-            then
-                Left
-                    (TransitionTypedVampireGlobalNotVisible
-                        global)
-            else
-                unless
-                    (checkedGlobalType global
-                        == reportedType)
-                    (Left
-                        (TransitionTypedVampireGlobalTypeMismatch
-                            global
-                            reportedType))
+    validateGlobalType (global, reportedType) = do
+        authoritativeType <-
+            validateBuilderGlobalReference
+                builder
+                global
+        unless
+            (authoritativeType == reportedType)
+            (Left
+                (TransitionTypedVampireGlobalTypeMismatch
+                    global
+                    reportedType))
 
     validateSelectedFact selected =
         case lookupBuilderFact reference builder of
@@ -1518,6 +1655,11 @@ commitTransitionTypedVampireFact
                         rowReference
                         admitted)
                     _registration) -> do
+                        semantic <-
+                            prepareTypedSemanticFact
+                                builder
+                                (typedAdmittedStatement
+                                    admitted)
                         let selectedProposition =
                                 Backend.typedBackendFactProposition
                                     selected
@@ -1527,12 +1669,12 @@ commitTransitionTypedVampireFact
                         unless
                             ( rowReference == reference
                               && frozenCoreTerm
-                                    (typedAdmittedStatement
-                                        admitted)
+                                    (typedSemanticStatement
+                                        semantic)
                                     == Backend.supportedPropositionTerm
                                         selectedProposition
                               && typedSemanticFofCapability
-                                    (admittedSemantic admitted)
+                                    semantic
                                     == selectedCapability
                             )
                             (Left
@@ -1541,8 +1683,8 @@ commitTransitionTypedVampireFact
                         typedImport <-
                             transitionDerivationImport
                                 reference
-                                (typedAdmittedStatement
-                                    admitted)
+                                (typedSemanticStatement
+                                    semantic)
                         pure
                             ( typedImport
                             , typedAdmittedTrustDependencies
@@ -1575,22 +1717,6 @@ commitTransitionTypedVampireFact
                     tag))
         pure (Set.singleton tag)
 
-    admittedSemantic
-            (TypedAdmittedFact semantic _authorization) =
-        semantic
-
-    visibleGlobals =
-        Set.fromList
-            [ reference
-            | TypedGlobalBinding
-                _symbol
-                reference
-                _origin
-                _body <-
-                    Map.elems
-                        (builderGlobals builder)
-            ]
-
 nextTransitionTypedFactReference
     :: TransitionModuleBuilder
     -> Either TransitionModuleError FactRef
@@ -1617,22 +1743,24 @@ commitTransitionTypedDeclaredAssumption
     :: NonEmpty Marker
     -> Origin
     -> AssumptionKind
-    -> TypedSemanticFact
+    -> FrozenCheckedCore CheckedGlobalRef
     -> TransitionModuleBuilder
     -> Either TransitionModuleError TransitionModuleBuilder
 commitTransitionTypedDeclaredAssumption
         aliases
         factOrigin
         kind
-        semantic
+        statement
         builder = do
+    semantic <-
+        prepareTypedSemanticFact builder statement
     factReference <-
         nextTransitionTypedFactReference builder
     let factOrdinal =
             builderNextTypedFact builder
         reference =
             TransitionTypedFactRef factReference
-        statement =
+        checkedStatement =
             typedSemanticStatement semantic
         assumptionOrdinal =
             LocalAssumptionOrdinal
@@ -1641,13 +1769,13 @@ commitTransitionTypedDeclaredAssumption
             TypedDirectAxiomManifestEntry
                 factReference
                 kind
-                statement
+                checkedStatement
         sessionReference =
             SessionTypedDeclaredAssumptionRef
                 factReference
                 assumptionOrdinal
                 kind
-                statement
+                checkedStatement
         admitted =
             TypedAdmittedFact
                 semantic
@@ -2082,6 +2210,106 @@ validateTypedDirectAxiomManifest localFacts manifest =
             zip [0 ..] (Vector.toList manifest)
         ]
 
+insertVisibleGlobalBinding
+    :: ( Map Symbol TypedGlobalBinding
+       , Map OpaqueDeclarationRef TypedGlobalBinding
+       )
+    -> TypedGlobalBinding
+    -> Either
+        TransitionModuleError
+        ( Map Symbol TypedGlobalBinding
+        , Map OpaqueDeclarationRef TypedGlobalBinding
+        )
+insertVisibleGlobalBinding
+        (globals, declarations)
+        binding@(TypedGlobalBinding
+            symbol
+            reference
+            _bindingOrigin
+            _body) = do
+    globals' <-
+        case Map.lookup symbol globals of
+            Nothing ->
+                Right (Map.insert symbol binding globals)
+            Just previous@(TypedGlobalBinding
+                    _previousSymbol
+                    _previousReference
+                    _previousOrigin
+                    _previousBody)
+                | previous == binding ->
+                    Right globals
+                | otherwise ->
+                    Left
+                        (globalSymbolConflict
+                            previous
+                            binding)
+    declarations' <-
+        case Map.lookup declaration declarations of
+            Nothing ->
+                Right
+                    (Map.insert
+                        declaration
+                        binding
+                        declarations)
+            Just previous
+                | previous == binding ->
+                    Right declarations
+                | otherwise ->
+                    Left
+                        (globalReferenceConflict
+                            previous
+                            binding)
+    pure (globals', declarations')
+  where
+    declaration =
+        checkedGlobalReference reference
+
+globalSymbolConflict
+    :: TypedGlobalBinding
+    -> TypedGlobalBinding
+    -> TransitionModuleError
+globalSymbolConflict
+        (TypedGlobalBinding
+            previousSymbol
+            previousReference
+            previousOrigin
+            _previousBody)
+        (TypedGlobalBinding
+            _incomingSymbol
+            incomingReference
+            incomingOrigin
+            _incomingBody) =
+    TransitionGlobalConflict
+        previousSymbol
+        previousReference
+        previousOrigin
+        incomingReference
+        incomingOrigin
+
+globalReferenceConflict
+    :: TypedGlobalBinding
+    -> TypedGlobalBinding
+    -> TransitionModuleError
+globalReferenceConflict
+        (TypedGlobalBinding
+            previousSymbol
+            previousReference
+            previousOrigin
+            _previousBody)
+        (TypedGlobalBinding
+            incomingSymbol
+            incomingReference
+            incomingOrigin
+            _incomingBody) =
+    TransitionGlobalReferenceConflict
+        (checkedGlobalReference incomingReference)
+        previousSymbol
+        (checkedGlobalType previousReference)
+        previousOrigin
+        incomingSymbol
+        (checkedGlobalType incomingReference)
+        incomingOrigin
+
 
 mergeTypedEnvironments
     :: [TransitionAdmittedModule]
@@ -2089,6 +2317,7 @@ mergeTypedEnvironments
         TransitionModuleError
         ( Vector TypedModuleEnvironmentDelta
         , Map Symbol TypedGlobalBinding
+        , Map OpaqueDeclarationRef TypedGlobalBinding
         )
 mergeTypedEnvironments directImports = do
     (_deltasByModule, reversedDeltas) <-
@@ -2096,14 +2325,15 @@ mergeTypedEnvironments directImports = do
             importModule
             (Map.empty, [])
             directImports
-    globals <-
+    (globals, globalDeclarations) <-
         foldM
             applyDelta
-            Map.empty
+            (Map.empty, Map.empty)
             (reverse reversedDeltas)
     pure
         ( Vector.fromList (reverse reversedDeltas)
         , globals
+        , globalDeclarations
         )
   where
     importModule imported admitted =
@@ -2133,35 +2363,9 @@ mergeTypedEnvironments directImports = do
                         (TransitionImportedModuleConflict
                             name)
 
-    applyDelta globals
+    applyDelta environment
             (TypedModuleEnvironmentDelta _name bindings) =
-        foldM insertBinding globals bindings
-
-    insertBinding globals
-            binding@(TypedGlobalBinding
-                symbol
-                reference
-                bindingOrigin
-                _body) =
-        case Map.lookup symbol globals of
-            Nothing ->
-                Right (Map.insert symbol binding globals)
-            Just
-                (TypedGlobalBinding
-                    _previousSymbol
-                    previousReference
-                    previousOrigin
-                    _previousBody)
-                | previousReference == reference ->
-                    Right globals
-                | otherwise ->
-                    Left
-                        (TransitionGlobalConflict
-                            symbol
-                            previousReference
-                            previousOrigin
-                            reference
-                            bindingOrigin)
+        foldM insertVisibleGlobalBinding environment bindings
 
 mergeTransitionFacts
     :: [TransitionAdmittedModule]
@@ -2278,13 +2482,25 @@ data TransitionModuleError
         !Origin
         !CheckedGlobalRef
         !Origin
-    | TransitionTransparentGlobalTypeMismatch
+    | TransitionGlobalReferenceConflict
+        !OpaqueDeclarationRef
         !Symbol
         !CoreType
+        !Origin
+        !Symbol
+        !CoreType
+        !Origin
+    | TransitionGlobalReferenceNotVisible
+        !CheckedGlobalRef
+    | TransitionGlobalReferenceTypeMismatch
+        !CheckedGlobalRef
         !CoreType
-    | TransitionTransparentGlobalDependencyNotVisible
+    | TransitionCoreCheckError
+        !CoreCheckError
+    | TransitionTransparentGlobalTypeMismatch
         !Symbol
-        !(Set CheckedGlobalRef)
+        !CoreType
+        !CoreType
     | TransitionTypedFactIsNotProposition
         !CoreType
     | TransitionTypedFactSupportError
@@ -2295,8 +2511,6 @@ data TransitionModuleError
     | TransitionTypedVampireTargetMismatch
     | TransitionTypedVampireRequestMismatch
     | TransitionTypedVampireHasOpenLocalPremises
-    | TransitionTypedVampireGlobalNotVisible
-        !CheckedGlobalRef
     | TransitionTypedVampireGlobalTypeMismatch
         !CheckedGlobalRef
         !CoreType
diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs
index ecac2c7..d216c3b 100644
--- a/source/Test/Unit/Source.hs
+++ b/source/Test/Unit/Source.hs
@@ -97,6 +97,8 @@ unitTests = testGroup "Source resolution"
         publishesLegacyImportViews
     , testCase "publishes typed signatures and facts through transition modules"
         publishesTransitionSignatures
+    , testCase "rejects cached global types from another builder"
+        rejectsForeignCachedGlobalType
     , testCase "authorizes exact typed Vampire requests"
         authorizesTypedVampireRequests
     , testCase "enforces and replays direct inductive guards"
@@ -890,14 +892,26 @@ publishesTransitionSignatures =
                             Checking.initialLegacyCheckingEnvironment
                             entryAssignment
                             [])
+                hiddenTarget <-
+                    expectRight
+                        (Core.checkCanonicalCore
+                            (const Nothing)
+                            (Core.CImp
+                                Core.CFalsum
+                                Core.CFalsum))
                 hiddenImport <-
                     expectRight
                         (Transition.transitionDerivationImport
                             sharedReference
-                            sharedStatement)
-                case Transition.authorizeTransitionKernelFactWithImports
+                            hiddenTarget)
+                case Transition.commitTransitionKernelFactWithImports
+                        ("hidden_import" :| [])
+                        (Transition.origin
+                            Nowhere
+                            Nothing
+                            (Just "hidden_import"))
                         (Vector.singleton hiddenImport)
-                        sharedStatement
+                        hiddenTarget
                         (Derivation.importedFactDerivation
                             (Derivation.importIx 0))
                         hiddenBuilder of
@@ -1092,6 +1106,163 @@ publishesTransitionSignatures =
                 (Checking.checkingStateEnvironment checked)
                 finalBuilder)
 
+rejectsForeignCachedGlobalType :: Assertion
+rejectsForeignCachedGlobalType =
+    withTemporaryDirectory "felix-transition-global-types" \temp -> do
+        writeTheory
+            (temp Posix.</> "entry.tex")
+            []
+            "entry"
+        graph <-
+            buildSearchedGraph temp "entry.tex"
+        workspace <-
+            expectRight
+                =<< Parse.parseResolvedSourceGraph graph
+        assignments <-
+            expectRight
+                (Legacy.assignLegacyModuleOrdinals workspace)
+        assignment <-
+            case toList assignments of
+                [only] ->
+                    pure only
+                actual ->
+                    assertFailure
+                        ("expected one module assignment, got "
+                            <> show (length actual))
+                        >> fail "unreachable"
+        checkedFoundationValue <-
+            expectRight Foundation.checkedFoundation
+        builderA0 <-
+            expectRight
+                (Transition.openTransitionModuleBuilder
+                    checkedFoundationValue
+                    Checking.initialLegacyCheckingEnvironment
+                    assignment
+                    [])
+        builderB0 <-
+            expectRight
+                (Transition.openTransitionModuleBuilder
+                    checkedFoundationValue
+                    Checking.initialLegacyCheckingEnvironment
+                    assignment
+                    [])
+        let symbol =
+                SymbolPredicate
+                    (PredicateSymbol
+                        "same_nominal_global")
+            declarationOrigin =
+                Transition.origin
+                    Nowhere
+                    Nothing
+                    (Just "same_nominal_global")
+        builderA <-
+            expectRight
+                (Transition.commitTransitionOpaqueGlobal
+                    symbol
+                    Core.TySet
+                    declarationOrigin
+                    (Transition.beginTransitionDeclaration
+                        builderA0))
+        builderB <-
+            expectRight
+                (Transition.commitTransitionOpaqueGlobal
+                    symbol
+                    Core.TyProp
+                    declarationOrigin
+                    (Transition.beginTransitionDeclaration
+                        builderB0))
+        globalA <-
+            maybe
+                (assertFailure "builder A lost its global"
+                    >> fail "unreachable")
+                pure
+                (Transition.lookupTransitionGlobal
+                    symbol
+                    builderA)
+        globalB <-
+            maybe
+                (assertFailure "builder B lost its global"
+                    >> fail "unreachable")
+                pure
+                (Transition.lookupTransitionGlobal
+                    symbol
+                    builderB)
+        operand <-
+            expectRight
+                (Core.checkCanonicalCore
+                    (Just . Transition.checkedGlobalType)
+                    (Core.CGlobal globalA))
+        statement <-
+            expectRight
+                (Core.checkCanonicalCore
+                    (Just . Transition.checkedGlobalType)
+                    (Core.CEq
+                        Core.TySet
+                        (Core.CGlobal globalA)
+                        (Core.CGlobal globalA)))
+        case Transition.commitTransitionKernelFact
+                ("foreign_global_type" :| [])
+                (Transition.origin
+                    Nowhere
+                    Nothing
+                    (Just "foreign_global_type"))
+                statement
+                (Derivation.equalityReflexivityDerivation
+                    operand)
+                (Transition.beginTransitionDeclaration
+                    builderB) of
+            Left
+                (Transition.TransitionGlobalReferenceTypeMismatch
+                    actual
+                    authoritativeType) -> do
+                        assertEqual
+                            "cached global reference"
+                            globalA
+                            actual
+                        assertEqual
+                            "builder B authoritative type"
+                            Core.TyProp
+                            authoritativeType
+            Left err ->
+                assertFailure
+                    ("expected cached global type rejection, got "
+                        <> show err)
+            Right _ ->
+                assertFailure
+                    "builder B admitted builder A's cached type"
+        let remappedOperand =
+                Core.mapFrozenGlobals
+                    (const globalB)
+                    operand
+            remappedStatement =
+                Core.mapFrozenGlobals
+                    (const globalB)
+                    statement
+        case Transition.commitTransitionKernelFact
+                ("stale_term_annotation" :| [])
+                (Transition.origin
+                    Nowhere
+                    Nothing
+                    (Just "stale_term_annotation"))
+                remappedStatement
+                (Derivation.equalityReflexivityDerivation
+                    remappedOperand)
+                (Transition.beginTransitionDeclaration
+                    builderB) of
+            Left
+                (Transition.TransitionCoreCheckError
+                    (Core.EqualityOperandTypeMismatch
+                        Core.TySet
+                        Core.TyProp)) ->
+                pure ()
+            Left err ->
+                assertFailure
+                    ("expected fresh builder-relative core check, got "
+                        <> show err)
+            Right _ ->
+                assertFailure
+                    "builder B admitted a stale term annotation"
+
 authorizesTypedVampireRequests :: Assertion
 authorizesTypedVampireRequests =
     withTemporaryDirectory "felix-typed-vampire" \temp -> do
@@ -1176,10 +1347,6 @@ authorizesTypedVampireRequests =
                         :: Vector.Vector
                             (Void, Core.CoreType))
                     (Core.embedClosedCore [] target))
-        fofSemantic <-
-            expectRight
-                (Transition.prepareTypedSemanticFact
-                    target)
         builderWithFof <-
             expectRight
                 (Transition.commitTransitionTypedDeclaredAssumption
@@ -1189,7 +1356,7 @@ authorizesTypedVampireRequests =
                         Nothing
                         (Just "fof_input"))
                     Legacy.DeclaredUserAxiom
-                    fofSemantic
+                    target
                     (Transition.beginTransitionDeclaration
                         builderWithLegacy))
         let higherOrderTarget =
@@ -1198,10 +1365,6 @@ authorizesTypedVampireRequests =
                     (Foundation.foundationAxiomFrozen
                         checkedFoundationValue
                         Foundation.DoubleNegationElim)
-        higherOrderSemantic <-
-            expectRight
-                (Transition.prepareTypedSemanticFact
-                    higherOrderTarget)
         builder <-
             expectRight
                 (Transition.commitTransitionTypedDeclaredAssumption
@@ -1211,7 +1374,7 @@ authorizesTypedVampireRequests =
                         Nothing
                         (Just "th0_input"))
                     Legacy.DeclaredUserAxiom
-                    higherOrderSemantic
+                    higherOrderTarget
                     (Transition.beginTransitionDeclaration
                         builderWithFof))
         implicitProblem <-
@@ -1397,11 +1560,7 @@ authorizesTypedVampireRequests =
                 atom (Core.COpaqueInteger 1)
             atomR =
                 atom (Core.COpaqueInteger 2)
-            declareTyped alias statement current = do
-                semantic <-
-                    expectRight
-                        (Transition.prepareTypedSemanticFact
-                            statement)
+            declareTyped alias statement current =
                 expectRight
                     (Transition.commitTransitionTypedDeclaredAssumption
                         (alias :| [])
@@ -1410,7 +1569,7 @@ authorizesTypedVampireRequests =
                             Nothing
                             (Just alias))
                         Legacy.DeclaredUserAxiom
-                        semantic
+                        statement
                         (Transition.beginTransitionDeclaration
                             current))
         premiseP <-