Fix arity checker bug (#1546)

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

@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.C
 where
 
 import Juvix.Compiler.Internal.Extra
+import Juvix.Compiler.Internal.Pretty
 import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types
@@ -319,7 +320,7 @@ checkLambda ari (Lambda cl) = Lambda <$> mapM goClause cl
                   -- TODO. think what to do in this case
                   return (pats, as)
                 (_ : _, []) -> case rest of
-                  ArityRestUnit -> error "too many patterns in lambda"
+                  ArityRestUnit -> error ("too many patterns in lambda: " <> ppTrace (Lambda cl) <> "\n" <> prettyText ari)
                   ArityRestUnknown -> return (pats, [])
 
 idenArity :: Members '[Reader LocalVars, Reader InfoTable] r => Iden -> Sem r Arity
@@ -422,10 +423,10 @@ checkExpression hintArity expr = case expr of
               toArity = \case
                 ParamExplicit a -> a
                 ParamImplicit -> ArityUnit
-          mapM
-            (secondM (uncurry checkExpression))
-            [(i', (a, e')) | (a, (i', e')) <- zip (argsAris ++ repeat ArityUnknown) args]
-            >>= addHoles i hintArity ari
+          argsWithHoles :: [(IsImplicit, Expression)] <- addHoles i hintArity ari args
+          let argsWithAris :: [(IsImplicit, (Arity, Expression))]
+              argsWithAris = [(i', (a, e')) | (a, (i', e')) <- zip (argsAris ++ repeat ArityUnknown) argsWithHoles]
+          mapM (secondM (uncurry checkExpression)) argsWithAris
         addHoles ::
           Interval ->
           Arity ->

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

@@ -1,6 +1,7 @@
 module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types where
 
 import Juvix.Prelude
+import Juvix.Prelude.Pretty
 
 data Arity
   = ArityUnit
@@ -74,3 +75,32 @@ foldArity UnfoldedArity {..} = go _ufoldArityParams
           l = case a of
             ParamExplicit e -> ParamExplicit e
             ParamImplicit -> ParamImplicit
+
+instance HasAtomicity FunctionArity where
+  atomicity = const (Aggregate funFixity)
+
+instance HasAtomicity Arity where
+  atomicity = \case
+    ArityUnit -> Atom
+    ArityUnknown -> Atom
+    ArityFunction f -> atomicity f
+
+instance Pretty ArityParameter where
+  pretty = \case
+    ParamImplicit -> "{𝟙}"
+    ParamExplicit f -> pretty f
+
+instance Pretty FunctionArity where
+  pretty f@(FunctionArity l r) =
+    parensCond (atomParens (const True) (atomicity f) funFixity) (pretty l)
+      <> " → "
+      <> pretty r
+    where
+      parensCond :: Bool -> Doc a -> Doc a
+      parensCond t d = if t then parens d else d
+
+instance Pretty Arity where
+  pretty = \case
+    ArityUnit -> "𝟙"
+    ArityUnknown -> "?"
+    ArityFunction f -> pretty f

tests/positive/Internal/Lambda.juvix

@@ -109,4 +109,14 @@ zipWith := λ {_ nil _ := nil;
 t : {A : Type} → {B : Type} → ({X : Type} → List X) → List A × List B;
 t := id {({X : Type} → List X) → _} λ { f := f {_} , f {_} };
 
+inductive Box (A : Type) {
+  b : A → Box A;
+};
+
+x : Box ((A : Type) → A → A);
+x := b λ {A a := a};
+
+t1 : {A : Type} → Box ((A : Type) → A → A) → A → A;
+t1 {A} := λ {(b f) := f A};
+
 end;