diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 925153be05..693d7985ce 100644
--- 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
index fd05039672..3eb03893f7 100644
--- 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
index ee2b5d563e..fd8bd0c760 100644
--- 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
index 8e20ee0c3f..ef2c889b2a 100644
--- 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
index d5b41f105e..48decf4a46 100644
--- 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
index efba5e399b..5a831e4002 100644
--- 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