Shift contextual binders under exact binders

1 files changed, 42 insertions, 0 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index e5b8a4f..54238e8 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -1728,6 +1728,48 @@ compilesContextualAbbreviations = do
                 semantic
                 (Module.sealedTypedModuleSemantic cached)
 
+            runsBeforeConsumer <- readIORef runs
+            consumerWorkspace <-
+                parseFinalExactWorkspace prelude mounts
+                    "test/phase5/exact-contextual-abbreviation-consumer.tex"
+            let consumerParsed =
+                    Parse.parsedWorkspaceRootModule consumerWorkspace
+            consumerInput <- expectRight
+                (Module.typedModuleInput
+                    foundation
+                    (Module.finalPreludeReadiness prelude)
+                    resolver
+                    Declaration.FreshValidation
+                    consumerParsed
+                    [cached])
+            consumer <- Module.runTypedModule consumerInput >>= \case
+                Module.TypedModuleSucceeded sealedConsumer ->
+                    pure sealedConsumer
+                Module.TypedModuleOpenFailed failure ->
+                    assertFailure
+                        ("contextual consumer did not open: " <> show failure)
+                        >> fail "unreachable"
+                Module.TypedModuleFailed failure _prefix ->
+                    assertFailure
+                        ("contextual consumer did not seal: " <> show failure)
+                        >> fail "unreachable"
+            let consumerTargets =
+                    [ Semantic.semanticGlobalTargetObject
+                        (Semantic.semanticGlobalBindingTarget binding)
+                    | delta <- localSemanticDeltas consumer
+                    , binding <- Semantic.semanticEnvironmentBindings
+                        (Semantic.declarationDeltaEnvironment delta)
+                    ]
+            assertEqual "two contextual consumer declarations" 2
+                (length consumerTargets)
+            void
+                (sole
+                    "quantified contextual binder matches its explicit parameter"
+                    (nubOrd consumerTargets))
+            runsAfterConsumer <- readIORef runs
+            assertEqual "contextual abbreviations require no prover call"
+                runsBeforeConsumer runsAfterConsumer
+
             verifyFailure foundation resolver prelude mounts sealed
                 "test/phase5/exact-contextual-abbreviation-missing.tex"
                 (\case