Recheck frozen HOL terms canonically

2 files changed, 150 insertions, 0 deletions

diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs
index 27563bd..6329aff 100644
--- a/source/Checking/Core.hs
+++ b/source/Checking/Core.hs
@@ -35,6 +35,7 @@ module Checking.Core
     , FrozenCheckedCore
     , frozenCoreType
     , frozenCoreTerm
+    , checkCanonicalCore
     , freezeClosed
     , FreezeError(..)
     , referenceFreezeClosed
@@ -212,6 +213,7 @@ coreForall binderType local body =
 data CoreCheckError
     = UnknownCoreGlobal
     | UnboundCoreLocal
+    | UnboundCoreIndex !Natural
     | AppliedNonFunction !CoreType
     | ApplicationArgumentTypeMismatch
         !CoreType
@@ -438,6 +440,115 @@ frozenCoreTerm :: FrozenCheckedCore global -> CanonicalTerm global
 frozenCoreTerm (FrozenCheckedCore _coreType term) =
     term
 
+-- | Recheck a nameless term without exposing the checked wrapper constructor.
+checkCanonicalCore
+    :: (global -> Maybe CoreType)
+    -> CanonicalTerm global
+    -> Either CoreCheckError (FrozenCheckedCore global)
+checkCanonicalCore globalType term =
+    FrozenCheckedCore
+        <$> inferCanonicalCore globalType [] term
+        <*> pure term
+
+inferCanonicalCore
+    :: (global -> Maybe CoreType)
+    -> [CoreType]
+    -> CanonicalTerm global
+    -> Either CoreCheckError CoreType
+inferCanonicalCore globalType binders = \case
+    CBound index ->
+        maybe
+            (Left (UnboundCoreIndex index))
+            Right
+            (binderTypeAt index binders)
+    CGlobal global ->
+        maybe
+            (Left UnknownCoreGlobal)
+            Right
+            (globalType global)
+    CIntrinsic intrinsic ->
+        Right (coreIntrinsicType intrinsic)
+    COpaqueInteger{} ->
+        Right TySet
+    CApp function argument -> do
+        functionType <-
+            inferCanonicalCore globalType binders function
+        argumentType <-
+            inferCanonicalCore globalType binders argument
+        case functionType of
+            TyArrow expectedArgument resultType
+                | expectedArgument == argumentType ->
+                    Right resultType
+                | otherwise ->
+                    Left
+                        (ApplicationArgumentTypeMismatch
+                            expectedArgument
+                            argumentType)
+            other ->
+                Left (AppliedNonFunction other)
+    CLam binderType body -> do
+        bodyType <-
+            inferCanonicalCore
+                globalType
+                (binderType : binders)
+                body
+        Right (binderType `TyArrow` bodyType)
+    CFalsum ->
+        Right TyProp
+    CImp premise conclusion -> do
+        premiseType <-
+            inferCanonicalCore globalType binders premise
+        unless
+            (premiseType == TyProp)
+            (Left
+                (ImplicationOperandTypeMismatch
+                    premiseType))
+        conclusionType <-
+            inferCanonicalCore globalType binders conclusion
+        unless
+            (conclusionType == TyProp)
+            (Left
+                (ImplicationOperandTypeMismatch
+                    conclusionType))
+        Right TyProp
+    CEq operandType left right -> do
+        leftType <-
+            inferCanonicalCore globalType binders left
+        unless
+            (leftType == operandType)
+            (Left
+                (EqualityOperandTypeMismatch
+                    operandType
+                    leftType))
+        rightType <-
+            inferCanonicalCore globalType binders right
+        unless
+            (rightType == operandType)
+            (Left
+                (EqualityOperandTypeMismatch
+                    operandType
+                    rightType))
+        Right TyProp
+    CForall binderType body -> do
+        bodyType <-
+            inferCanonicalCore
+                globalType
+                (binderType : binders)
+                body
+        unless
+            (bodyType == TyProp)
+            (Left
+                (QuantifierBodyTypeMismatch bodyType))
+        Right TyProp
+
+binderTypeAt :: Natural -> [CoreType] -> Maybe CoreType
+binderTypeAt _index [] =
+    Nothing
+binderTypeAt 0 (binderType : _rest) =
+    Just binderType
+binderTypeAt index (_binderType : rest) =
+    binderTypeAt (index - 1) rest
+
 data FreezeError
     = FreeLocalInClosedCore
     deriving stock (Show, Eq)
diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs
index cb32323..5de1203 100644
--- a/source/Test/Unit/Core.hs
+++ b/source/Test/Unit/Core.hs
@@ -37,6 +37,9 @@ unitTests =
         , testCase
             "rejects ill-typed and open terms"
             rejectsInvalidTerms
+        , testCase
+            "rechecks canonical terms without unchecked construction"
+            rechecksCanonicalTerms
         , testPropertyNamed
             "optimized freeze agrees with bounded reference"
             "prop_freezeAgreesWithReference"
@@ -149,6 +152,42 @@ rejectsInvalidTerms = do
                     coreFalsum
                     (coreGlobal TestGlobal)))
 
+rechecksCanonicalTerms :: Assertion
+rechecksCanonicalTerms = do
+    let term =
+            CForall TySet
+                (CEq TySet
+                    (CBound 0)
+                    (CBound 0))
+    assertEqual
+        "well-typed canonical proposition"
+        (Right (TyProp, term))
+        ( (\checked ->
+                ( frozenCoreType checked
+                , frozenCoreTerm checked
+                ))
+            <$> checkCanonicalCore testGlobalType term
+        )
+    assertEqual
+        "out-of-scope de Bruijn index"
+        (Left (UnboundCoreIndex 1))
+        (frozenCoreType
+            <$> checkCanonicalCore
+                testGlobalType
+                (CForall TySet (CBound 1)))
+    assertEqual
+        "canonical application still checks argument types"
+        (Left
+            (ApplicationArgumentTypeMismatch
+                TySet
+                TyProp))
+        (frozenCoreType
+            <$> checkCanonicalCore
+                testGlobalType
+                (CApp
+                    (CIntrinsic FamilyUnion)
+                    CFalsum))
+
 prop_freezeAgreesWithReference :: Property
 prop_freezeAgreesWithReference = property do
     depth <-