Implement error messages (#1396)

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

@@ -34,6 +34,8 @@ data ScoperError
   | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock
   | ErrDuplicateInductiveParameterName DuplicateInductiveParameterName
   | ErrDoubleBracesPattern DoubleBracesPattern
+  | ErrImplicitPatternLeftApplication ImplicitPatternLeftApplication
+  | ErrConstructorExpectedLeftApplication ConstructorExpectedLeftApplication
   deriving stock (Show)
 
 instance ToGenericError ScoperError where
@@ -62,3 +64,5 @@ instance ToGenericError ScoperError where
     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

@@ -564,8 +564,52 @@ instance ToGenericError DoubleBracesPattern where
     where
       pat :: PatternArg
       pat = e ^. doubleBracesPatternArg
-      i = getLoc (e ^. doubleBracesPatternArg)
+      i = getLoc pat
       msg =
         "Double braces are not valid:"
-        -- TODO add bold to braces
+          -- 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

@@ -1553,7 +1553,7 @@ parsePatternTerm = do
         bracesPat s = case s of
           PatternAtomBraces r
             | Implicit <- r ^. patternArgIsImplicit ->
-              Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r)))
+                Just (Left (ErrDoubleBracesPattern (DoubleBracesPattern r)))
             | otherwise -> Just (Right (set patternArgIsImplicit Implicit r))
           _ -> Nothing
 

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

@@ -212,6 +212,20 @@ scoperErrorTests =
       $ \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;