Give proper errors for incorrect application of lazy builtins (#1830)

* Closes #1828

examples/milestone/TicTacToe/Web/TicTacToe.juvix

@@ -23,8 +23,11 @@ module Web.TicTacToe;
     IOUnit : IO;
   IOUnit := printString "";
 
+  ioseq : IO → IO → IO;
+  ioseq x y := x >> y;
+
   sequenceIO : List IO → IO;
-  sequenceIO := foldr (>>) IOUnit;
+  sequenceIO := foldr ioseq IOUnit;
 
   mapIO : {A : Type} → (A → IO) → List A → IO;
   mapIO f xs := sequenceIO (map f xs);

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -624,7 +624,7 @@ goExpression' = \case
       varsNum <- asks (^. indexTableVarsNum)
       return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1))
     Internal.IdenFunction n -> do
-      funInfoBuiltin <- getFunctionBuiltinInfo n
+      funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
       case funInfoBuiltin of
         Just Internal.BuiltinBoolIf -> error "if must be called with 3 arguments"
         Just Internal.BuiltinBoolOr -> error "|| must be called with 2 arguments"
@@ -655,7 +655,7 @@ goExpression' = \case
         Just _ -> error ("internal to core: not a constructor " <> txt)
         Nothing -> error ("internal to core: undeclared identifier: " <> txt)
     Internal.IdenAxiom n -> do
-      axiomInfoBuiltin <- getAxiomBuiltinInfo n
+      axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n
       case axiomInfoBuiltin of
         Just Internal.BuiltinIOSequence -> error ">> must be called with 2 arguments"
         Just Internal.BuiltinTrace -> error "trace must be called with 2 arguments"
@@ -721,7 +721,7 @@ goApplication a = do
 
   case f of
     Internal.ExpressionIden (Internal.IdenAxiom n) -> do
-      axiomInfoBuiltin <- getAxiomBuiltinInfo n
+      axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n
       case axiomInfoBuiltin of
         Just Internal.BuiltinNatPrint -> app
         Just Internal.BuiltinStringPrint -> app
@@ -748,7 +748,7 @@ goApplication a = do
         Just Internal.BuiltinFail -> app
         Nothing -> app
     Internal.ExpressionIden (Internal.IdenFunction n) -> do
-      funInfoBuiltin <- getFunctionBuiltinInfo n
+      funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
       case funInfoBuiltin of
         Just Internal.BuiltinBoolIf -> do
           sym <- getBoolSymbol
@@ -778,17 +778,3 @@ goLiteral intToNat l = case l ^. withLocParam of
   where
     mkLitConst :: ConstantValue -> Node
     mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt)))
-
-getAxiomBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom)
-getAxiomBuiltinInfo n = do
-  maybeAxiomInfo <- HashMap.lookup n <$> asks (^. Internal.infoAxioms)
-  return $ case maybeAxiomInfo of
-    Just axiomInfo -> axiomInfo ^. Internal.axiomInfoBuiltin
-    Nothing -> Nothing
-
-getFunctionBuiltinInfo :: Member (Reader Internal.InfoTable) r => Name -> Sem r (Maybe BuiltinFunction)
-getFunctionBuiltinInfo n = do
-  maybeFunInfo <- HashMap.lookup n <$> asks (^. Internal.infoFunctions)
-  return $ case maybeFunInfo of
-    Just funInfo -> funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin
-    Nothing -> Nothing

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -196,3 +196,17 @@ constructorReturnType c = do
           ind
           inductiveParams
   return saturatedTy
+
+getAxiomBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinAxiom)
+getAxiomBuiltinInfo n = do
+  maybeAxiomInfo <- HashMap.lookup n <$> asks (^. infoAxioms)
+  return $ case maybeAxiomInfo of
+    Just axiomInfo -> axiomInfo ^. axiomInfoBuiltin
+    Nothing -> Nothing
+
+getFunctionBuiltinInfo :: Member (Reader InfoTable) r => Name -> Sem r (Maybe BuiltinFunction)
+getFunctionBuiltinInfo n = do
+  maybeFunInfo <- HashMap.lookup n <$> asks (^. infoFunctions)
+  return $ case maybeFunInfo of
+    Just funInfo -> funInfo ^. functionInfoDef . funDefBuiltin
+    Nothing -> Nothing

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -477,8 +477,8 @@ checkExpression ::
   Expression ->
   Sem r Expression
 checkExpression hintArity expr = case expr of
-  ExpressionIden {} -> appHelper expr []
+  ExpressionIden {} -> goApp expr []
-  ExpressionApplication a -> goApp a
+  ExpressionApplication a -> uncurry goApp $ second toList (unfoldApplication' a)
   ExpressionLiteral {} -> appHelper expr []
   ExpressionFunction {} -> return expr
   ExpressionUniverse {} -> return expr
@@ -488,8 +488,41 @@ checkExpression hintArity expr = case expr of
   ExpressionLet l -> ExpressionLet <$> checkLet hintArity l
   ExpressionCase l -> ExpressionCase <$> checkCase hintArity l
   where
-    goApp :: Application -> Sem r Expression
+    goApp :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
-    goApp = uncurry appHelper . second toList . unfoldApplication'
+    goApp f args = do
+      case f of
+        ExpressionIden (IdenAxiom n) -> do
+          blt <- getAxiomBuiltinInfo n
+          case blt of
+            Just BuiltinIOSequence -> goBuiltinApp n 0 2 f args
+            Just BuiltinTrace -> goBuiltinApp n 2 2 f args
+            _ -> appHelper f args
+        ExpressionIden (IdenFunction n) -> do
+          blt <- getFunctionBuiltinInfo n
+          case blt of
+            Just BuiltinBoolIf -> goBuiltinApp n 1 3 f args
+            Just BuiltinBoolOr -> goBuiltinApp n 0 2 f args
+            Just BuiltinBoolAnd -> goBuiltinApp n 0 2 f args
+            _ -> appHelper f args
+        _ -> appHelper f args
+
+    goBuiltinApp :: Name -> Int -> Int -> Expression -> [(IsImplicit, Expression)] -> Sem r Expression
+    goBuiltinApp n implArgsNum argsNum f args = do
+      args' <- goImplArgs implArgsNum args
+      if
+          | length args' >= argsNum -> appHelper f args
+          | otherwise ->
+              throw $
+                ErrBuiltinNotFullyApplied
+                  BuiltinNotFullyApplied
+                    { _builtinNotFullyAppliedName = n,
+                      _builtinNotFullyAplliedExpectedArgsNum = argsNum
+                    }
+      where
+        goImplArgs :: Int -> [(IsImplicit, Expression)] -> Sem r [(IsImplicit, Expression)]
+        goImplArgs 0 as = return as
+        goImplArgs k ((Implicit, _) : as) = goImplArgs (k - 1) as
+        goImplArgs _ as = return as
 
     appHelper :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
     appHelper fun0 args = do

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error.hs

@@ -15,6 +15,7 @@ data ArityCheckerError
   | ErrPatternFunction PatternFunction
   | ErrTooManyArguments TooManyArguments
   | ErrFunctionApplied FunctionApplied
+  | ErrBuiltinNotFullyApplied BuiltinNotFullyApplied
 
 instance ToGenericError ArityCheckerError where
   genericError :: (Member (Reader GenericOptions) r) => ArityCheckerError -> Sem r GenericError
@@ -26,3 +27,4 @@ instance ToGenericError ArityCheckerError where
     ErrPatternFunction e -> genericError e
     ErrTooManyArguments e -> genericError e
     ErrFunctionApplied e -> genericError e
+    ErrBuiltinNotFullyApplied e -> genericError e

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Error/Types.hs

@@ -232,3 +232,31 @@ instance ToGenericError FunctionApplied where
               <> softline
               <> "In the application"
               <+> ppApp opts' (fun, args)
+
+data BuiltinNotFullyApplied = BuiltinNotFullyApplied
+  { _builtinNotFullyAppliedName :: Name,
+    _builtinNotFullyAplliedExpectedArgsNum :: Int
+  }
+
+makeLenses ''BuiltinNotFullyApplied
+
+instance ToGenericError BuiltinNotFullyApplied where
+  genericError e = ask >>= generr
+    where
+      generr opts =
+        return
+          GenericError
+            { _genericErrorLoc = i,
+              _genericErrorMessage = ppOutput msg,
+              _genericErrorIntervals = [i]
+            }
+        where
+          opts' = fromGenericOptions opts
+          i = getLoc (e ^. builtinNotFullyAppliedName)
+          argsNum = e ^. builtinNotFullyAplliedExpectedArgsNum
+          msg =
+            "The lazy builtin"
+              <+> ppCode opts' (e ^. builtinNotFullyAppliedName)
+              <+> "must be applied to exactly"
+              <+> pretty argsNum
+              <+> "arguments"

test/Arity/Negative.hs

@@ -92,5 +92,12 @@ tests =
       $(mkRelFile "WrongReturnTypeTooManyArguments.juvix")
       $ \case
         ErrTooManyArguments {} -> Nothing
+        _ -> wrongError,
+    NegTest
+      "Lazy builtin not fully applied"
+      $(mkRelDir "Internal")
+      $(mkRelFile "LazyBuiltin.juvix")
+      $ \case
+        ErrBuiltinNotFullyApplied {} -> Nothing
         _ -> wrongError
   ]

tests/negative/Internal/LazyBuiltin.juvix

@@ -0,0 +1,14 @@
+module LazyBuiltin;
+
+builtin bool type Bool :=
+  | true : Bool
+  | false : Bool;
+
+builtin bool-if if : {A : Type} -> Bool -> A -> A -> A;
+if true x _ := x;
+if false _ x := x;
+
+f : Bool -> Bool;
+f x := if x;
+
+end;