fix negative tests & formatiing

anoma · Oct 19, 2023 · 0e1d18f · 0e1d18f
1 parent e5f603b
commit 0e1d18f
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 8 deletions.
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -940,7 +940,7 @@ instance (SingI s) => PrettyPrint (SigArg s) where
 ppFunctionSignature :: (SingI s) => PrettyPrinting (FunctionDef s)
 ppFunctionSignature FunctionDef {..} = do
   let termin' = (<> line) . ppCode <$> _signTerminating
-      coercion' = (<> line) . ppCode <$> _signCoercion
+      coercion' = (<> if isJust instance' then space else line) . ppCode <$> _signCoercion
       instance' = (<> line) . ppCode <$> _signInstance
       args' = hsep . fmap ppCode <$> nonEmpty _signArgs
       builtin' = (<> line) . ppCode <$> _signBuiltin

diff --git a/tests/negative/Internal/AmbiguousCoercions.juvix b/tests/negative/Internal/AmbiguousCoercions.juvix
@@ -17,12 +17,12 @@ unitT1 : T1 Unit := mkT1 (pp := λ{_ := unit});
 instance
 unitT2 : T2 Unit := mkT2 (pp := λ{_ := unit});
 
-coercion
+coercion instance
 fromT1toT {A} {{T1 A}} : T A := mkT@{
   pp := T1.pp
 };
 
-coercion
+coercion instance
 fromT2toT {A} {{T2 A}} : T A := mkT@{
   pp := T2.pp
 };

diff --git a/tests/negative/Internal/CoercionTargetNotATrait.juvix b/tests/negative/Internal/CoercionTargetNotATrait.juvix
@@ -5,5 +5,5 @@ type T A := mkT {a : A};
 
 type Maybe A := just A | nothing;
 
-coercion
+coercion instance
 inst {A} {{T A}} : Maybe A := nothing;
diff --git a/tests/negative/Internal/InvalidCoercionType.juvix b/tests/negative/Internal/InvalidCoercionType.juvix
@@ -3,7 +3,7 @@ module InvalidCoercionType;
 trait
 type T A := mkT {pp : A -> A};
 
-coercion
+coercion instance
 coe {A} : T A :=
   mkT@{
     pp (x : A) : A := x

diff --git a/tests/negative/Internal/LoopingCoercion.juvix b/tests/negative/Internal/LoopingCoercion.juvix
@@ -8,12 +8,12 @@ type T1 A := mkT1 {pp : A -> A};
 trait
 type T2 A := mkT2 {pp : A -> A};
 
-coercion
+coercion instance
 fromT1toT2 {A} {{T1 A}} : T2 A := mkT2@{
   pp := T1.pp
 };
 
-coercion
+coercion instance
 fromT2toT1 {A} {{T2 A}} : T1 A := mkT1@{
   pp := T2.pp
 };

diff --git a/tests/negative/Internal/WrongCoercionArgument.juvix b/tests/negative/Internal/WrongCoercionArgument.juvix
@@ -6,7 +6,7 @@ type T1 A := mkT1 {pp : A -> A};
 trait
 type T2 A := mkT2 {pp : A -> A};
 
-coercion
+coercion instance
 coe {A} {{T1 A}} {{T1 A}} : T2 A :=
   mkT2@{
     pp := T1.pp