Check for syntactically invalid constraint guards in the parser (#1686)

Numeric constraint guards have very particular syntactic requirements:

* They must always be used in top-level definitions.
* Their definitions must always be accompanied by a top-level type signature.

Previously, we checked these requirements in a combination of places in the
parser and the typechecker. The checks in the typechecker weren't very
thorough, however, and they failed to catch local definitions without type
signatures that use constraint guards, as seen in #1685.

This patch moves all of these syntactic checks to the parser (in
`Cryptol.Parser.ExpandPropGuards`). We now recurse into expressions to check
for local definition that use constraint guards and error if we encounter one.
This ensures that by the time we reach the typechecker, all constraint guard
expressions are at least syntactically valid.

Fixes #1685.

CHANGES.md

@@ -1,3 +1,10 @@
+# next -- TBA
+
+## Bug fixes
+
+* Fix #1685, which caused Cryptol to panic when given a local definition without
+  a type signature that uses numeric constraint guards.
+
 # 3.1.0 -- 2024-02-05
 
 ## Language changes

src/Cryptol/Parser/ExpandPropGuards.hs

@@ -22,6 +22,7 @@ import Control.DeepSeq
 import Cryptol.Parser.AST
 import Cryptol.Utils.PP
 import Cryptol.Utils.Panic (panic)
+import Data.Foldable (traverse_)
 import Data.Text (pack)
 import GHC.Generics (Generic)
 
@@ -31,15 +32,35 @@ type ExpandPropGuardsM a = Either Error a
 runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a
 runExpandPropGuardsM m = m
 
--- | Error
+-- | Errors that can happen while expanding constraint guards.
 data Error = NoSignature (Located PName)
+             -- ^ A declaration using constraints guard lacks an explicit type
+             -- signature, which is a requirement.
+           | NestedConstraintGuard (Located PName)
+             -- ^ Constraint guards appear somewhere other than the top level,
+             -- which is not allowed.
   deriving (Show, Generic, NFData)
 
 instance PP Error where
   ppPrec _ err = case err of
     NoSignature x ->
-      text "At" <+> pp (srcRange x) <.> colon
-        <+> text "Declarations using constraint guards require an explicit type signature."
+      hang
+        (text "At" <+> pp (srcRange x) <.> colon)
+        2
+        (vcat [ text "Declaration" <+> backticks (pp (thing x)) <+>
+                text "lacks a type signature."
+              , text "Declarations using constraint guards require an" <+>
+                text "explicit type signature."
+              ])
+    NestedConstraintGuard x ->
+      hang
+        (text "At" <+> pp (srcRange x) <.> colon)
+        2
+        (vcat [ text "Local declaration" <+> backticks (pp (thing x)) <+>
+                text "may not use constraint guards."
+              , text "Constraint guards may only appear at the top-level of" <+>
+                text "a module."
+              ])
 
 expandPropGuards :: ModuleG mname PName -> ExpandPropGuardsM (ModuleG mname PName)
 expandPropGuards m =
@@ -69,16 +90,23 @@ expandTopDecl topDecl =
 expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
 expandDecl decl =
   case decl of
-    DBind bind -> do bs <- expandBind bind
-                     pure (map DBind bs)
-    _          -> pure [decl]
+    DBind bind ->
+      do bs <- expandBind bind
+         pure (map DBind bs)
+    DLocated d rng ->
+      do ds <- expandDecl d
+         pure $ map (`DLocated` rng) ds
+    _ ->
+      pure [decl]
 
 expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
 expandBind bind =
   case thing (bDef bind) of
     DImpl (DPropGuards guards) -> expand (DImpl . DPropGuards) guards
     DForeign (Just (DPropGuards guards)) -> expand (DForeign . Just . DPropGuards) guards
-    _ -> pure [bind]
+    _ ->
+      do checkNestedGuardsInBind bind
+         pure [bind]
 
   where
   expand def guards = do
@@ -90,6 +118,7 @@ expandBind bind =
           PropGuardCase PName ->
           ExpandPropGuardsM (PropGuardCase PName, Bind PName)
         goGuard (PropGuardCase props' e) = do
+          checkNestedGuardsInExpr e
           bName' <- newName (bName bind) (thing <$> props')
           -- call to generated function
           tParams <- case bSignature bind of
@@ -117,6 +146,123 @@ expandBind bind =
       bind {bDef = def guards' <$ bDef bind} :
       binds'
 
+-- | Check for nested uses of constraint guards in an expression (e.g.,
+-- in a local definition bound with @where@).
+checkNestedGuardsInExpr :: Expr PName -> ExpandPropGuardsM ()
+checkNestedGuardsInExpr expr =
+  case expr of
+    EVar {} ->
+      pure ()
+    ELit {} ->
+      pure ()
+    EGenerate e ->
+      checkNestedGuardsInExpr e
+    ETuple es ->
+      traverse_ checkNestedGuardsInExpr es
+    ERecord r ->
+      traverse_ (checkNestedGuardsInExpr . snd) r
+    ESel e _ ->
+      checkNestedGuardsInExpr e
+    EUpd mbE upds ->
+      do traverse_ checkNestedGuardsInExpr mbE
+         traverse_ checkNestedGuardsInUpdField upds
+    EList es ->
+      traverse_ checkNestedGuardsInExpr es
+    EFromTo {} ->
+      pure ()
+    EFromToBy {} ->
+      pure ()
+    EFromToDownBy {} ->
+      pure ()
+    EFromToLessThan {} ->
+      pure ()
+    EInfFrom _ mbE ->
+      traverse_ checkNestedGuardsInExpr mbE
+    EComp e mss ->
+      do checkNestedGuardsInExpr e
+         traverse_ (traverse_ checkNestedGuardsInMatch) mss
+    EApp e1 e2 ->
+      do checkNestedGuardsInExpr e1
+         checkNestedGuardsInExpr e2
+    EAppT e _ ->
+      checkNestedGuardsInExpr e
+    EIf e1 e2 e3 ->
+      do checkNestedGuardsInExpr e1
+         checkNestedGuardsInExpr e2
+         checkNestedGuardsInExpr e3
+    EWhere e ds ->
+      do checkNestedGuardsInExpr e
+         traverse_ checkNestedGuardsInDecl ds
+    ETyped e _ ->
+      checkNestedGuardsInExpr e
+    ETypeVal _ ->
+      pure ()
+    EFun _ _ e ->
+      checkNestedGuardsInExpr e
+    ELocated e _ ->
+      checkNestedGuardsInExpr e
+    ESplit e ->
+      checkNestedGuardsInExpr e
+    EParens e ->
+      checkNestedGuardsInExpr e
+    EInfix e1 _ _ e2 ->
+      do checkNestedGuardsInExpr e1
+         checkNestedGuardsInExpr e2
+    EPrefix _ e ->
+      checkNestedGuardsInExpr e
+    ECase e ca ->
+      do checkNestedGuardsInExpr e
+         traverse_ checkNestedGuardsInCaseAlt ca
+  where
+    checkNestedGuardsInUpdField :: UpdField PName -> ExpandPropGuardsM ()
+    checkNestedGuardsInUpdField (UpdField _ _ e) =
+      checkNestedGuardsInExpr e
+
+    checkNestedGuardsInMatch :: Match PName -> ExpandPropGuardsM ()
+    checkNestedGuardsInMatch match =
+      case match of
+        Match _ e ->
+          checkNestedGuardsInExpr e
+        MatchLet b ->
+          checkNestedGuardsInBind b
+
+    checkNestedGuardsInCaseAlt :: CaseAlt PName -> ExpandPropGuardsM ()
+    checkNestedGuardsInCaseAlt (CaseAlt _ e) =
+      checkNestedGuardsInExpr e
+
+-- | Check for nested uses of constraint guards in a local declaration.
+checkNestedGuardsInDecl :: Decl PName -> ExpandPropGuardsM ()
+checkNestedGuardsInDecl decl =
+  case decl of
+    DSignature {} -> pure ()
+    DPatBind _ e  -> checkNestedGuardsInExpr e
+    DBind b       -> checkNestedGuardsInBind b
+    DRec bs       -> traverse_ checkNestedGuardsInBind bs
+    DFixity {}    -> pure ()
+    DPragma {}    -> pure ()
+    DType {}      -> pure ()
+    DProp {}      -> pure ()
+    DLocated d _  -> checkNestedGuardsInDecl d
+
+-- | Check for nested uses of constraint guards in a local bind.
+checkNestedGuardsInBind :: Bind PName -> ExpandPropGuardsM ()
+checkNestedGuardsInBind bind =
+  case thing (bDef bind) of
+    DPrim         -> pure ()
+    DImpl bi      -> checkNestedGuardsInBindImpl bi
+    DForeign mbBi -> traverse_ checkNestedGuardsInBindImpl mbBi
+  where
+    nestedConstraintGuards :: ExpandPropGuardsM ()
+    nestedConstraintGuards = Left . NestedConstraintGuard $ bName bind
+
+    checkNestedGuardsInBindImpl :: BindImpl PName -> ExpandPropGuardsM ()
+    checkNestedGuardsInBindImpl bi =
+      case bi of
+        DPropGuards _ ->
+          nestedConstraintGuards
+        DExpr e ->
+          checkNestedGuardsInExpr e
+
 patternToExpr :: Pattern PName -> Expr PName
 patternToExpr (PVar locName) = EVar (thing locName)
 patternToExpr _ =

src/Cryptol/TypeCheck/Error.hs

@@ -171,13 +171,6 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
               | UnsupportedFFIType TypeSource FFITypeError
                 -- ^ Type is not supported for FFI
 
-              | NestedConstraintGuard Ident
-                -- ^ Constraint guards may only apper at the top-level
-
-              | DeclarationRequiresSignatureCtrGrd Ident
-                -- ^ All declarataions in a recursive group involving
-                -- constraint guards should have signatures
-
               | InvalidConstraintGuard Prop
                 -- ^ The given constraint may not be used as a constraint guard
 
@@ -273,8 +266,6 @@ errorImportance err =
     UnsupportedFFIType {}                            -> 7
     -- less than UnexpectedTypeWildCard
 
-    NestedConstraintGuard {}                         -> 10
-    DeclarationRequiresSignatureCtrGrd {}            -> 9
     InvalidConstraintGuard {}                        -> 5
 
 
@@ -342,8 +333,6 @@ instance TVars Error where
       UnsupportedFFIKind {}    -> err
       UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
 
-      NestedConstraintGuard {} -> err
-      DeclarationRequiresSignatureCtrGrd {} -> err
       InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p
 
       TemporaryError {} -> err
@@ -395,8 +384,6 @@ instance FVS Error where
       UnsupportedFFIKind {}  -> Set.empty
       UnsupportedFFIType _ t -> fvs t
 
-      NestedConstraintGuard {} -> Set.empty
-      DeclarationRequiresSignatureCtrGrd {} -> Set.empty
       InvalidConstraintGuard p -> fvs p
 
       TemporaryError {} -> Set.empty
@@ -688,18 +675,6 @@ instance PP (WithNames Error) where
         [ ppWithNames names t
         , "When checking" <+> pp src ]
 
-      NestedConstraintGuard d ->
-        vcat [ "Local declaration" <+> backticks (pp d)
-                                   <+> "may not use constraint guards."
-             , "Constraint guards may only appear at the top-level of a module."
-             ]
-
-      DeclarationRequiresSignatureCtrGrd d ->
-        vcat [ "The declaration of" <+> backticks (pp d) <+>
-                                            "requires a full type signature,"
-             , "because it is part of a recursive group with constraint guards."
-             ]
-
       InvalidConstraintGuard p ->
         let d = case tNoUser p of
                   TCon tc _ -> pp tc

src/Cryptol/TypeCheck/Infer.hs

@@ -956,8 +956,6 @@ inferBinds isTopLevel isRec binds =
                      genCs     <- generalize bs1 cs
                      return (done,genCs)
 
-     checkNumericConstraintGuardsOK isTopLevel sigs noSigs
-
      rec
        let exprMap = Map.fromList (map monoUse genBs)
        (doneBs, genBs) <- check exprMap
@@ -985,40 +983,6 @@ inferBinds isTopLevel isRec binds =
     withQs   = foldl' appP withTys  qs
 
 
-{-
-Here we also check that:
-  * Numeric constraint guards appear only at the top level
-  * All definitions in a recursive groups with numberic constraint guards
-    have signatures
-
-The reason is to avoid interference between local constraints coming
-from the guards and type inference.  It might be possible to
-relex these requirements, but this requires some more careful thought on
-the interaction between the two, and the effects on pricniple types.
--}
-checkNumericConstraintGuardsOK ::
-  Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()
-checkNumericConstraintGuardsOK isTopLevel haveSig noSig =
-  do unless isTopLevel
-            (mapM_ (mkErr NestedConstraintGuard) withGuards)
-     unless (null withGuards)
-            (mapM_ (mkErr DeclarationRequiresSignatureCtrGrd) noSig)
-  where
-  mkErr f b =
-    do let nm = P.bName b
-       inRange (srcRange nm) (recordError (f (nameIdent (thing nm))))
-
-  withGuards = filter hasConstraintGuards haveSig
-  -- When desugaring constraint guards we check that they have signatures,
-  -- so no need to look at noSig
-
-  hasConstraintGuards b =
-    case P.bindImpl b of
-      Just (P.DPropGuards {}) -> True
-      _                       -> False
-
-
-
 {- | Come up with a type for recursive calls to a function, and decide
      how we are going to be checking the binding.
      Returns: (Name, type or schema, computation to check binding)
@@ -1178,6 +1142,9 @@ checkMonoB b t =
                          , dDoc = thing <$> P.bDoc b
                          }
 
+        -- The pass in Cryptol.Parser.ExpandPropGuards ensures that by the time
+        -- we reach this code, all definitions that use constraint guards will
+        -- have a type signature, so this case should be unreachable.
         P.DPropGuards _ ->
           tcPanic "checkMonoB"
             [ "Used constraint guards without a signature at "

tests/constraint-guards/noNested.icry.stdout

@@ -2,6 +2,6 @@ Loading module Cryptol
 Loading module Cryptol
 Loading module Main
 
-[error] at noNested.cry:6:3--6:9:
+At noNested.cry:6:3--6:9:
   Local declaration `nested` may not use constraint guards.
   Constraint guards may only appear at the top-level of a module.

tests/constraint-guards/noTypeSig.cry

@@ -0,0 +1 @@
+f | 0 == 0 => ()

tests/constraint-guards/noTypeSig.icry

@@ -0,0 +1 @@
+:load noTypeSig.cry

tests/constraint-guards/noTypeSig.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+At noTypeSig.cry:1:1--1:2:
+  Declaration `f` lacks a type signature.
+  Declarations using constraint guards require an explicit type signature.

tests/constraint-guards/noTypeSigNested.cry

@@ -0,0 +1,5 @@
+// A regression test for #1685.
+f : ()
+f = g
+  where
+    g | 0 == 0 => ()

tests/constraint-guards/noTypeSigNested.icry

@@ -0,0 +1 @@
+:load noTypeSigNested.cry

tests/constraint-guards/noTypeSigNested.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+At noTypeSigNested.cry:5:5--5:6:
+  Local declaration `g` may not use constraint guards.
+  Constraint guards may only appear at the top-level of a module.