fix type synonyms

anoma · May 13, 2024 · 73d855b · 73d855b
1 parent bfce447
commit 73d855b
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
@@ -490,8 +490,8 @@ checkFunctionParameter ::
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter FunctionParameter {..} = do
-  let ty = _paramType
-  ty' <- checkIsType (getLoc ty) ty
+  ty <- checkIsType (getLoc _paramType) _paramType
+  ty' <- strongNormalize ty
   when (_paramImplicit == ImplicitInstance) $ do
     tab <- ask
     checkInstanceParam tab ty'

diff --git a/tests/Compilation/positive/test061.juvix b/tests/Compilation/positive/test061.juvix
@@ -6,11 +6,14 @@ import Stdlib.Prelude open hiding {Show; mkShow; module Show};
 trait
 type Show A := mkShow {show : A → String};
 
+Show' : Type -> Type := Show;
+Bool' : Type := Bool;
+
 instance
 showStringI : Show String := mkShow (show := id);
 
 instance
-showBoolI : Show Bool :=
+showBoolI : Show' Bool' :=
   mkShow@{
     show (x : Bool) : String := if x "true" "false"
   };
@@ -21,9 +24,9 @@ showNatI : Show Nat := mkShow (show := natToString);
 g : {A : Type} → {{Show A}} → Nat := 5;
 
 instance
-showListI {A} {{Show A}} : Show (List A) :=
+showListI {A} {{Show' A}} : Show (List A) :=
   mkShow@{
-    show {A} : {{Show A}} → List A → String
+    show {A} : {{Show' A}} → List A → String
       | nil := "nil"
       | (h :: t) := Show.show h ++str " :: " ++str show t
   };
@@ -49,7 +52,7 @@ f'3 {A} {{M : Show A}} : A → String := Show.show {{M}};
 
 f'4 {A} {{_ : Show A}} : A → String := Show.show;
 
-f5 {A} {{Show A}} (n : String) (a : A) : String :=
+f5 {A} {{Show' A}} (n : String) (a : A) : String :=
   n ++str Show.show a;
 
 instance
@@ -63,7 +66,7 @@ showBoolFunI : Show (Bool → Bool) := mkShow@{
 };
 
 instance
-showPairI {A B} {{Show A}} {{Show B}} : Show (A × B) :=
+showPairI {A B} {{Show A}} {{Show' B}} : Show' (A × B) :=
   mkShow λ {(x, y) := Show.show x ++str ", " ++str Show.show y};
 
 trait