Support positive arity typealias in arity checker (#2021)

Currently the arity checker assumes that applications within a type
signature have arity unit. This is not the case where a type alias
function is used within a type signature that returns a positive arity
function type.

For example:

```
type T :=
  | t : T;

funAlias : Type -> Type;
funAlias a := a -> a;

f : funAlias T;
f t := t;
```

* Closes https://github.com/anoma/juvix/issues/2020

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

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

@@ -435,7 +435,7 @@ typeArity = go
     go :: Expression -> Arity
     go = \case
       ExpressionIden i -> goIden i
-      ExpressionApplication {} -> ArityUnit
+      ExpressionApplication a -> goApplication a
       ExpressionLiteral {} -> ArityUnknown
       ExpressionFunction f -> ArityFunction (goFun f)
       ExpressionHole {} -> ArityUnknown
@@ -445,6 +445,14 @@ typeArity = go
       ExpressionSimpleLambda {} -> simplelambda
       ExpressionLet l -> goLet l
 
+    goApplication :: Application -> Arity
+    goApplication a = case lhs of
+      ExpressionIden IdenInductive {} -> ArityUnit
+      _ -> ArityUnknown
+      where
+        lhs :: Expression
+        lhs = fst (unfoldApplication a)
+
     goLet :: Let -> Arity
     goLet l = typeArity (l ^. letExpression)
 

tests/positive/TypeAlias.juvix

@@ -34,3 +34,15 @@ p a := mkPair t a a;
 
 x' : flip Pair (id _) T2;
 x' := mkPair x t2 t;
+
+funAlias : Type -> Type;
+funAlias a := a -> a;
+
+f : funAlias T;
+f :=
+  \ {
+    | t := t
+  };
+
+f' : funAlias T;
+f' t := t;