Implement some error messages (#1396) (#1400)

* Implement error message for double braces
* Implement error message for implicit pattern on the left of an application
* Implement error message for constructor expected on the left of an application 

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>

src/Juvix/Syntax/Concrete/Scoped/Error.hs

@@ -33,6 +33,9 @@ data ScoperError
   | ErrMultipleCompileRuleSameBackend MultipleCompileRuleSameBackend
   | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock
   | ErrDuplicateInductiveParameterName DuplicateInductiveParameterName
+  | ErrDoubleBracesPattern DoubleBracesPattern
+  | ErrImplicitPatternLeftApplication ImplicitPatternLeftApplication
+  | ErrConstructorExpectedLeftApplication ConstructorExpectedLeftApplication
   deriving stock (Show)
 
 instance ToGenericError ScoperError where
@@ -60,3 +63,6 @@ instance ToGenericError ScoperError where
     ErrMultipleCompileRuleSameBackend e -> genericError e
     ErrWrongKindExpressionCompileBlock e -> genericError e
     ErrDuplicateInductiveParameterName e -> genericError e
+    ErrDoubleBracesPattern e -> genericError e
+    ErrImplicitPatternLeftApplication e -> genericError e
+    ErrConstructorExpectedLeftApplication e -> genericError e

src/Juvix/Syntax/Concrete/Scoped/Error/Types.hs

@@ -546,3 +546,70 @@ instance ToGenericError DuplicateInductiveParameterName where
             <> "."
             <> line
             <> "Inductive parameter names can not be repeated."
+
+newtype DoubleBracesPattern = DoubleBracesPattern
+  { _doubleBracesPatternArg :: PatternArg
+  }
+  deriving stock (Show)
+
+makeLenses ''DoubleBracesPattern
+
+instance ToGenericError DoubleBracesPattern where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      pat :: PatternArg
+      pat = e ^. doubleBracesPatternArg
+      i = getLoc pat
+      msg =
+        "Double braces are not valid:"
+          -- TODO add bold to braces
+          <+> braces (ppCode pat)
+
+newtype ImplicitPatternLeftApplication = ImplicitPatternLeftApplication
+  { _implicitPatternLeftApplication :: PatternApp
+  }
+  deriving stock (Show)
+
+makeLenses ''ImplicitPatternLeftApplication
+
+instance ToGenericError ImplicitPatternLeftApplication where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      pat :: PatternApp
+      pat = e ^. implicitPatternLeftApplication
+      i = getLoc pat
+      msg =
+        "Pattern matching an implicit argument cannot occur on the left of an application:"
+          <+> ppCode pat
+
+newtype ConstructorExpectedLeftApplication = ConstructorExpectedLeftApplication
+  { _constructorExpectedLeftApplicationPattern :: Pattern
+  }
+  deriving stock (Show)
+
+makeLenses ''ConstructorExpectedLeftApplication
+
+instance ToGenericError ConstructorExpectedLeftApplication where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = prettyError msg,
+        _genericErrorIntervals = [i]
+      }
+    where
+      pat :: Pattern
+      pat = e ^. constructorExpectedLeftApplicationPattern
+      i = getLoc pat
+      msg =
+        "Constructor expected on the left of a pattern application:"
+          <+> ppCode pat

src/Juvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -660,6 +660,12 @@ instance PrettyCode PatternArg where
     p <- ppCode (a ^. patternArgPattern)
     return (bracesIf (Implicit == a ^. patternArgIsImplicit) p)
 
+instance PrettyCode PatternApp where
+  ppCode (PatternApp l r) = do
+    l' <- ppLeftExpression appFixity l
+    r' <- ppRightExpression appFixity r
+    return $ l' <+> r'
+
 ppPatternParenType :: forall s r. (SingI s, Member (Reader Options) r) => PatternParensType s -> Sem r (Doc Ann)
 ppPatternParenType p = case sing :: SStage s of
   SParsed -> ppCode p

src/Juvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -1420,7 +1420,7 @@ parseTerm =
 -- Infix Patterns
 -------------------------------------------------------------------------------
 
-type ParsePat = P.Parsec () [PatternAtom 'Scoped]
+type ParsePat = P.ParsecT () [PatternAtom 'Scoped] (Sem '[Error ScoperError])
 
 makePatternTable ::
   PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]]
@@ -1543,11 +1543,18 @@ parsePatternTerm = do
           _ -> Nothing
 
     parseBraces :: ParsePat PatternArg
-    parseBraces = P.token bracesPat mempty
+    parseBraces = do
+      res <- P.token bracesPat mempty
+      case res of
+        Left er -> P.lift (throw er)
+        Right a -> return a
       where
-        bracesPat :: PatternAtom 'Scoped -> Maybe PatternArg
+        bracesPat :: PatternAtom 'Scoped -> Maybe (Either ScoperError PatternArg)
         bracesPat s = case s of
-          PatternAtomBraces r -> Just (set patternArgIsImplicit Implicit r)
+          PatternAtomBraces r
+            | Implicit <- r ^. patternArgIsImplicit ->
+                Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r)))
+            | otherwise -> Just (Right (set patternArgIsImplicit Implicit r))
           _ -> Nothing
 
     parseParens :: ParsePat PatternArg
@@ -1587,15 +1594,16 @@ parsePatternAtoms ::
   PatternAtoms 'Scoped ->
   Sem r PatternArg
 parsePatternAtoms atoms@(PatternAtoms sec' _) = do
-  case res of
-    Left {} -> throw (ErrInfixPattern (InfixErrorP atoms))
-    Right r -> return r
+  case run (runError res) of
+    Left e -> throw e -- Scoper effect error
+    Right Left {} -> throw (ErrInfixPattern (InfixErrorP atoms)) -- Megaparsec error
+    Right (Right r) -> return r
   where
     sec = toList sec'
     tbl = makePatternTable atoms
     parser :: ParsePat PatternArg
     parser = runM (mkPatternParser tbl) <* P.eof
-    res = P.parse parser filePath sec
+    res = P.runParserT parser filePath sec
 
     filePath :: FilePath
     filePath = "tmp"

src/Juvix/Translation/ScopedToAbstract.hs

@@ -341,31 +341,35 @@ goFunctionParameter (FunctionParameter {..}) = do
       }
 
 goPatternApplication ::
+  Member (Error ScoperError) r =>
   PatternApp ->
   Sem r Abstract.ConstructorApp
 goPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternApplication a)
 
 goPatternConstructor ::
+  Member (Error ScoperError) r =>
   ConstructorRef ->
   Sem r Abstract.ConstructorApp
 goPatternConstructor a = uncurry Abstract.ConstructorApp <$> viewApp (PatternConstructor a)
 
 goInfixPatternApplication ::
+  Member (Error ScoperError) r =>
   PatternInfixApp ->
   Sem r Abstract.ConstructorApp
 goInfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternInfixApplication a)
 
 goPostfixPatternApplication ::
+  Member (Error ScoperError) r =>
   PatternPostfixApp ->
   Sem r Abstract.ConstructorApp
 goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a)
 
-viewApp :: forall r. Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
-viewApp = \case
+viewApp :: forall r. Member (Error ScoperError) r => Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
+viewApp p = case p of
   PatternConstructor c -> return (goConstructorRef c, [])
-  PatternApplication (PatternApp l r) -> do
+  PatternApplication app@(PatternApp _ r) -> do
     r' <- goPatternArg r
-    second (`snoc` r') <$> viewAppLeft l
+    second (`snoc` r') <$> viewAppLeft app
   PatternInfixApplication (PatternInfixApp l c r) -> do
     l' <- goPatternArg l
     r' <- goPatternArg r
@@ -377,19 +381,16 @@ viewApp = \case
   PatternWildcard {} -> err
   PatternEmpty {} -> err
   where
-    viewAppLeft :: PatternArg -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
-    viewAppLeft p
-      -- TODO proper error
-      | Implicit <- p ^. patternArgIsImplicit = error "An implicit pattern cannot be on the left of an application"
-      | otherwise = viewApp (p ^. patternArgPattern)
-    -- TODO proper error
-    err :: a
-    err = error "constructor expected on the left of a pattern application"
+    viewAppLeft :: PatternApp -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
+    viewAppLeft app@(PatternApp l _)
+      | Implicit <- l ^. patternArgIsImplicit = throw (ErrImplicitPatternLeftApplication (ImplicitPatternLeftApplication app))
+      | otherwise = viewApp (l ^. patternArgPattern)
+    err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p))
 
 goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef
 goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n)
 
-goPatternArg :: PatternArg -> Sem r Abstract.PatternArg
+goPatternArg :: Member (Error ScoperError) r => PatternArg -> Sem r Abstract.PatternArg
 goPatternArg p = do
   pat' <- goPattern (p ^. patternArgPattern)
   return
@@ -398,7 +399,7 @@ goPatternArg p = do
         _patternArgPattern = pat'
       }
 
-goPattern :: Pattern -> Sem r Abstract.Pattern
+goPattern :: Member (Error ScoperError) r => Pattern -> Sem r Abstract.Pattern
 goPattern p = case p of
   PatternVariable a -> return $ Abstract.PatternVariable (goSymbol a)
   PatternConstructor c -> Abstract.PatternConstructorApp <$> goPatternConstructor c

test/Scope/Negative.hs

@@ -205,6 +205,27 @@ scoperErrorTests =
       $ \case
         ErrQualSymNotInScope {} -> Nothing
         _ -> wrongError,
+    NegTest
+      "Double braces in pattern"
+      "."
+      "NestedPatternBraces.juvix"
+      $ \case
+        ErrDoubleBracesPattern {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Pattern matching an implicit argument on the left of an application"
+      "."
+      "ImplicitPatternLeftApplication.juvix"
+      $ \case
+        ErrImplicitPatternLeftApplication {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Constructor expected on the left of a pattern application"
+      "."
+      "ConstructorExpectedLeftApplication.juvix"
+      $ \case
+        ErrConstructorExpectedLeftApplication {} -> Nothing
+        _ -> wrongError,
     NegTest
       "Compile block for a unsupported kind of expression"
       "CompileBlocks"

tests/negative/ConstructorExpectedLeftApplication.juvix

@@ -0,0 +1,6 @@
+module ConstructorExpectedLeftApplication;
+
+f : {A : Type} -> A -> A;
+f (x y) := x;
+
+end;

tests/negative/ImplicitPatternLeftApplication.juvix

@@ -0,0 +1,6 @@
+module ImplicitPatternLeftApplication;
+
+f : {A : Type} -> A -> A;
+f ({x} y) := y;
+
+end;

tests/negative/NestedPatternBraces.juvix

@@ -0,0 +1,6 @@
+module NestedPatternBraces;
+
+a : {A : Type} → Type;
+a {{A}} ≔ a;
+
+end;