parse error for missing types on quantifier-bound variables

Closes #314.
disco-lang · Mar 28, 2022 · 82c9994 · 82c9994
1 parent fe646fb
commit 82c9994
Show file tree

Hide file tree

Showing 3 changed files with 94 additions and 43 deletions.
diff --git a/docs/reference/no-search.rst b/docs/reference/no-search.rst
@@ -26,26 +26,3 @@ The below property is in fact false, but Disco can't handle it:
    Error: the type
      ℕ → ℕ
    is not searchable (i.e. it cannot be used in a forall).
-
-This error can also occur when you forget to put a type on a variable
-in a ``forall``.  For example:
-
-::
-
-   Disco> :test forall x. x == x
-   Error: the type
-     a1
-   is not searchable (i.e. it cannot be used in a forall).
-
-The problem here is really that Disco does not know what type ``x``
-should be.  If we add a type annotation on ``x``, it works fine:
-
-::
-
-   Disco> :test forall x: Bool. x == x
-     - Test passed: ∀x. x == x
-       No counterexamples exist.
-   Disco> :test forall x: N. x == x
-     - Test passed: ∀x. x == x
-       Checked 100 possibilities without finding a counterexample.
-
diff --git a/src/Disco/Parser.hs b/src/Disco/Parser.hs
@@ -121,13 +121,16 @@ instance Ord OpaqueTerm where
 data DiscoParseError
   = ReservedVarName String
   | InvalidPattern OpaqueTerm
+  | MissingAscr
   deriving (Show, Eq, Ord)
 
 instance ShowErrorComponent DiscoParseError where
   showErrorComponent (ReservedVarName x)     = "keyword \"" ++ x ++ "\" cannot be used as a variable name"
   showErrorComponent (InvalidPattern (OT t)) = "Invalid pattern: " ++ run (prettyStr t)
+  showErrorComponent MissingAscr        = "Variables introduced by ∀ or ∃ must have a type"
   errorComponentLen (ReservedVarName x) = length x
   errorComponentLen (InvalidPattern _)  = 1
+  errorComponentLen MissingAscr         = 1
 
 -- | A parser is a megaparsec parser of strings, with an extra layer
 --   of state to keep track of the current indentation level and
@@ -752,9 +755,9 @@ tuple t   = TTup t
 
 -- | Parse a quantified abstraction (λ, ∀, ∃).
 parseQuantified :: Parser Term
-parseQuantified =
-  TAbs <$> parseQuantifier
-       <*> (bind <$> parsePattern `sepBy` comma <*> (dot *> parseTerm))
+parseQuantified = do
+  q <- parseQuantifier
+  TAbs q <$> (bind <$> parsePattern (q /= Lam) `sepBy` comma <*> (dot *> parseTerm))
 
 -- | Parse a quantifier symbol (lambda, forall, or exists).
 parseQuantifier :: Parser Quantifier
@@ -801,7 +804,7 @@ parseGuard = try parseGPat <|> parseGBool <|> parseGLet
     guardWord = reserved "if" <|> reserved "when"
     parseGBool = GBool <$> (embed <$> (guardWord *> parseTerm))
     parseGPat  = GPat <$> (embed <$> (guardWord *> parseTerm))
-                      <*> (reserved "is" *> parsePattern)
+                      <*> (reserved "is" *> parsePattern False)
     parseGLet  = GLet <$> (reserved "let" *> parseBinding)
 
 -- | Parse an atomic pattern, by parsing a term and then attempting to
@@ -814,13 +817,24 @@ parseAtomicPattern = label "pattern" $ do
     Just p  -> return p
 
 -- | Parse a pattern, by parsing a term and then attempting to convert
---   it to a pattern.
-parsePattern :: Parser Pattern
-parsePattern = label "pattern" $ do
+--   it to a pattern.  The Bool parameter says whether to require
+--   a type ascription.
+parsePattern :: Bool -> Parser Pattern
+parsePattern requireAscr = label "pattern" $ do
   t <- parseTerm
   case termToPattern t of
     Nothing -> customFailure $ InvalidPattern (OT t)
-    Just p  -> return p
+    Just p
+      | not requireAscr || hasAscr p -> return p
+      | otherwise -> customFailure MissingAscr
+
+-- | Does a pattern either have a top-level ascription, or consist of
+--   a tuple with each component recursively having ascriptions?
+--   This is required for patterns bound by ∀ and ∃ quantifiers.
+hasAscr :: Pattern -> Bool
+hasAscr PAscr{}   = True
+hasAscr (PTup ps) = all hasAscr ps
+hasAscr _         = False
 
 -- | Attempt converting a term to a pattern.
 termToPattern :: Term -> Maybe Pattern

diff --git a/test/parse-quantifiers/expected b/test/parse-quantifiers/expected
@@ -14,24 +14,84 @@ https://disco-lang.readthedocs.io/en/latest/reference/shape-mismatch.html
 8
 8
 8
-TAbs_ Ex () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
+1:16:
+  |
+1 | :parse exists x. x > 3
+  |                ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
-TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
+1:23:
+  |
+1 | :parse exists (x:N), y. x > y
+  |                       ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ Ex () (<[PVar_ () x,PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ Ex () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
+1:16:
+  |
+1 | :parse exists x, (y:F). x > y
+  |                ^
+Variables introduced by ∀ or ∃ must have a type
+
+1:11:
+  |
+1 | :parse ∃ x. x > 3
+  |           ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
-TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
+1:18:
+  |
+1 | :parse ∃ (x:N), y. x > y
+  |                  ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ Ex () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ Ex () (<[PVar_ () x,PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ All () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
+1:11:
+  |
+1 | :parse ∃ x, (y:F). x > y
+  |           ^
+Variables introduced by ∀ or ∃ must have a type
+
+1:16:
+  |
+1 | :parse forall x. x > 3
+  |                ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
-TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
+1:23:
+  |
+1 | :parse forall (x:N), y. x > y
+  |                       ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ All () (<[PVar_ () x,PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ All () (<[PVar_ () x]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
+1:16:
+  |
+1 | :parse forall x, (y:F). x > y
+  |                ^
+Variables introduced by ∀ or ∃ must have a type
+
+1:11:
+  |
+1 | :parse ∀ x. x > 3
+  |           ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TNat_ () 3]))
-TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PVar_ () y]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
+1:18:
+  |
+1 | :parse ∀ (x:N), y. x > y
+  |                  ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ All () (<[PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
-TAbs_ All () (<[PVar_ () x,PAscr_ () (PVar_ () y) (TyAtom (ABase F))]> TApp_ () (TPrim_ () (PrimBOp Gt)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1]))
+1:11:
+  |
+1 | :parse ∀ x, (y:F). x > y
+  |           ^
+Variables introduced by ∀ or ∃ must have a type
+
 TAbs_ All () (<[PTup_ () [PAscr_ () (PVar_ () x) (TyAtom (ABase N)),PAscr_ () (PVar_ () y) (TyAtom (ABase N)),PAscr_ () (PVar_ () z) (TyAtom (ABase N))]]> TApp_ () (TPrim_ () (PrimBOp Impl)) (TTup_ () [TApp_ () (TPrim_ () (PrimBOp And)) (TTup_ () [TParens_ () (TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@1])),TParens_ () (TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@1,TVar_ () 0@2]))]),TApp_ () (TPrim_ () (PrimBOp Eq)) (TTup_ () [TVar_ () 0@0,TVar_ () 0@2])]))