From e5771fdba072a7a04c22274879654a013dc7e85f Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 6 Sep 2023 00:16:32 +0200
Subject: [PATCH 1/2] extend test

---
 tests/positive/Internal/Synonyms.juvix | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/positive/Internal/Synonyms.juvix b/tests/positive/Internal/Synonyms.juvix
index dbdb908627..3095d20bcf 100644
--- a/tests/positive/Internal/Synonyms.juvix
+++ b/tests/positive/Internal/Synonyms.juvix
@@ -4,6 +4,8 @@ import Stdlib.Prelude open;
 
 Ty1 : Type := Bool → Bool;
 
+idTy (A : Type) : Type := A;
+
 Ty2 : Type := Ty1;
 
 k : Ty2
@@ -15,5 +17,5 @@ Num : Type := {A : Type} → (A → A) → A → A;
 czero : Num
   | {_} f x := x;
 
-csuc : Num → Num
+csuc : Num → idTy Num
   | n {_} f := f ∘ n {_} f;

From d4aced8636e998925d74c8a8d7bd122cae574145 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 6 Sep 2023 00:35:35 +0200
Subject: [PATCH 2/2] Allow named arguments in type synonyms

---
 .../Analysis/TypeChecking/Data/Inference.hs   | 44 +++++++++++--------
 tests/positive/Internal/Synonyms.juvix        |  9 +++-
 2 files changed, 32 insertions(+), 21 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
index af6ff75558..67c9b2bf16 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
@@ -43,7 +43,11 @@ data InferenceState = InferenceState
 makeLenses ''InferenceState
 
 iniState :: InferenceState
-iniState = InferenceState mempty mempty
+iniState =
+  InferenceState
+    { _inferenceMap = mempty,
+      _inferenceIdens = mempty
+    }
 
 closeState ::
   (Member (Error TypeCheckerError) r) =>
@@ -429,25 +433,27 @@ addIdens idens = do
 -- some condition.
 functionDefEval :: forall r'. (Members '[State FunctionsTable, Termination, Error TypeCheckerError] r') => FunctionDef -> Sem r' (Maybe Expression)
 functionDefEval f = do
-  r <- runFail goTop
-  retTy <- returnsType
+  (params :: [FunctionParameter], ret :: Expression) <- unfoldFunType <$> strongNorm (f ^. funDefType)
+  let retTy = isUniverse ret
+  r <- runFail (goTop params retTy)
   when (isNothing r && retTy) (throw (ErrUnsupportedTypeFunction (UnsupportedTypeFunction f)))
   return r
   where
-    isUniverse :: (Members '[State FunctionsTable] r) => Expression -> Sem r Bool
-    isUniverse e = do
-      e' <- evalState iniState (weakNormalize' e)
-      case e' of
-        ExpressionUniverse {} -> return True
-        _ -> return False
-
-    (params, ret) = unfoldFunType (f ^. funDefType)
-
-    returnsType :: (Members '[State FunctionsTable] r) => Sem r Bool
-    returnsType = isUniverse ret
-
-    goTop :: forall r. (Members '[Fail, State FunctionsTable, Error TypeCheckerError, Termination] r) => Sem r Expression
-    goTop = do
+    strongNorm :: (Members '[State FunctionsTable] r) => Expression -> Sem r Expression
+    strongNorm = evalState iniState . strongNormalize'
+
+    isUniverse :: Expression -> Bool
+    isUniverse = \case
+      ExpressionUniverse {} -> True
+      _ -> False
+
+    goTop ::
+      forall r.
+      (Members '[Fail, State FunctionsTable, Error TypeCheckerError, Termination] r) =>
+      [FunctionParameter] ->
+      Bool ->
+      Sem r Expression
+    goTop params returnsType = do
       checkTerminating
       case f ^. funDefClauses of
         c :| [] -> goClause c
@@ -465,12 +471,12 @@ functionDefEval f = do
             splitExplicitParams :: Sem r [Expression]
             splitExplicitParams = do
               let n = length (c ^. clausePatterns)
-              unlessM returnsType fail
+              unless returnsType fail
               nfirst <- failMaybe (takeExactMay n params)
               mapM simpleExplicitParam nfirst
             simpleExplicitParam :: FunctionParameter -> Sem r Expression
             simpleExplicitParam = \case
-              FunctionParameter Nothing Explicit ty -> return ty
+              FunctionParameter _ Explicit ty -> return ty
               _ -> fail
             goPattern :: (Pattern, Expression) -> Expression -> Sem r Expression
             goPattern (p, ty) = case p of
diff --git a/tests/positive/Internal/Synonyms.juvix b/tests/positive/Internal/Synonyms.juvix
index 3095d20bcf..d216b07028 100644
--- a/tests/positive/Internal/Synonyms.juvix
+++ b/tests/positive/Internal/Synonyms.juvix
@@ -6,7 +6,12 @@ Ty1 : Type := Bool → Bool;
 
 idTy (A : Type) : Type := A;
 
-Ty2 : Type := Ty1;
+idTy2 : typeToType
+  | A := A;
+
+typeToType  : Type := Type -> Type;
+
+Ty2 : idTy Type := Ty1;
 
 k : Ty2
   | x := x;
@@ -17,5 +22,5 @@ Num : Type := {A : Type} → (A → A) → A → A;
 czero : Num
   | {_} f x := x;
 
-csuc : Num → idTy Num
+csuc : idTy2 Num → idTy Num
   | n {_} f := f ∘ n {_} f;