Arity check types and functions (->) (#2049)

This pr fixes the following:

This example causes the compiler to crash with "implicitness mismatch".
```
f : id Bool -> Bool;
f _ := false;
```
The reason is that `id` expects an implicit argument but finds `Bool`,
which is explicit. The arity checker was not inserting any hole because
it was ignoring the whole type. Moreover the aritychecker was never
checking `->` types as we never expected to
have to insert holes in `->` types (since the only fragment of defined
functions that we accept in types are those which do not have implicit
arguments).

We now properly arity check all types and process the function type `->`
correctly.

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

@@ -103,13 +103,17 @@ checkFunctionDef ::
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
   let arity = typeArity _funDefType
+  _funDefType' <- withEmptyLocalVars (checkType _funDefType)
   _funDefClauses' <- mapM (checkFunctionClause arity) _funDefClauses
   _funDefExamples' <- withEmptyLocalVars (mapM checkExample _funDefExamples)
   return
     FunctionDef
       { _funDefClauses = _funDefClauses',
         _funDefExamples = _funDefExamples',
-        ..
+        _funDefType = _funDefType',
+        _funDefName,
+        _funDefBuiltin,
+        _funDefPragmas
       }
 
 checkFunctionClause ::
@@ -134,6 +138,12 @@ checkFunctionClause ari cl = do
 simplelambda :: a
 simplelambda = error "simple lambda expressions are not supported by the arity checker"
 
+withLocalTypeVar :: Members '[Reader LocalVars] r => VarName -> Sem r a -> Sem r a
+withLocalTypeVar v = withLocalVar v ArityUnit
+
+withLocalVar :: Members '[Reader LocalVars] r => VarName -> Arity -> Sem r a -> Sem r a
+withLocalVar v = local . withArity v
+
 withEmptyLocalVars :: Sem (Reader LocalVars : r) a -> Sem r a
 withEmptyLocalVars = runReader emptyLocalVars
 
@@ -498,14 +508,27 @@ checkExpression hintArity expr = case expr of
   ExpressionIden {} -> goApp expr []
   ExpressionApplication a -> uncurry goApp $ second toList (unfoldApplication' a)
   ExpressionLiteral {} -> appHelper expr []
-  ExpressionFunction {} -> return expr
+  ExpressionFunction f -> ExpressionFunction <$> goFunction f
   ExpressionUniverse {} -> return expr
   ExpressionHole {} -> return expr
   ExpressionSimpleLambda {} -> simplelambda
   ExpressionLambda l -> ExpressionLambda <$> checkLambda hintArity l
   ExpressionLet l -> ExpressionLet <$> checkLet hintArity l
   ExpressionCase l -> ExpressionCase <$> checkCase hintArity l
   where
+    goFunction :: Function -> Sem r Function
+    goFunction (Function l r) = do
+      l' <- goFunctionParameter l
+      r' <- maybe id withLocalTypeVar (l ^. paramName) (checkType r)
+      return (Function l' r')
+      where
+        goFunctionParameter :: FunctionParameter -> Sem r FunctionParameter
+        goFunctionParameter p = do
+          let _paramName = p ^. paramName
+              _paramImplicit = p ^. paramImplicit
+          _paramType <- checkType (p ^. paramType)
+          return FunctionParameter {..}
+
     goApp :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
     goApp f args = do
       case f of

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

@@ -705,7 +705,16 @@ inferExpression' hint e = case e of
           case l'ty of
             ExpressionFunction (Function (FunctionParameter paraName ifun funL) funR) -> do
               r' <- checkExpression funL r
-              unless (iapp == ifun) (error "implicitness mismatch")
+              unless
+                (iapp == ifun)
+                ( error
+                    ( "Impossible: implicitness mismatch"
+                        <> show ifun
+                        <> show iapp
+                        <> "\n"
+                        <> ppTrace (Application l r iapp)
+                    )
+                )
               return
                 TypedExpression
                   { _typedExpression =

test/Typecheck/Positive.hs

@@ -213,6 +213,10 @@ tests =
       "Mutual inference inside let"
       $(mkRelDir ".")
       $(mkRelFile "MutualLet.juvix"),
+    posTest
+      "id application in type"
+      $(mkRelDir ".")
+      $(mkRelFile "IdInType.juvix"),
     posTest
       "Nested pattern match with type variables"
       $(mkRelDir ".")

tests/positive/IdInType.juvix

@@ -0,0 +1,10 @@
+module IdInType;
+
+type Unit :=
+  | unit : Unit;
+
+id : {a : Type} -> a -> a;
+id a := a;
+
+f : id Unit -> Unit;
+f _ := unit;