From d4340ea781b11d60f7bf8d244d60ecab572dc822 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 29 Aug 2023 18:36:40 +0200
Subject: [PATCH] add negative test

---
 src/Juvix/Compiler/Concrete/Print/Base.hs                   | 2 +-
 .../FromInternal/Analysis/TypeChecking/Error/Types.hs       | 2 +-
 test/Termination/Negative.hs                                | 6 ++++++
 tests/negative/Termination/Axiom.juvix                      | 5 +++++
 tests/negative/Termination/Ord.juvix                        | 1 -
 5 files changed, 13 insertions(+), 3 deletions(-)
 create mode 100644 tests/negative/Termination/Axiom.juvix

diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 2945c2b115..36e51f5a28 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -752,7 +752,7 @@ instance (SingI s) => PrettyPrint (AxiomDef s) where
       ?<> ppCode _axiomKw
       <+> axiomName'
       <+> ppCode _axiomColonKw
-      <+> ppExpressionType _axiomType
+      <+> nest (ppExpressionType _axiomType)
 
 instance PrettyPrint BuiltinInductive where
   ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
index 37031edd5b..5324c87d46 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -335,7 +335,7 @@ instance ToGenericError UnsupportedTypeFunction where
             <+> ppCode opts (_unsupportedTypeFunction ^. funDefName)
               <> "."
               <> line
-              <> "Only functions with a single clause and no pattern matching are supported."
+              <> "Only terminating functions with a single clause and no pattern matching are supported."
     return
       GenericError
         { _genericErrorLoc = i,
diff --git a/test/Termination/Negative.hs b/test/Termination/Negative.hs
index 088c883940..139c262dfe 100644
--- a/test/Termination/Negative.hs
+++ b/test/Termination/Negative.hs
@@ -73,6 +73,12 @@ tests =
       "Quicksort is not terminating"
       $(mkRelDir ".")
       $(mkRelFile "Data/QuickSort.juvix")
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Loop in axiom type"
+      $(mkRelDir ".")
+      $(mkRelFile "Axiom.juvix")
       $ \case
         ErrNoLexOrder {} -> Nothing
   ]
diff --git a/tests/negative/Termination/Axiom.juvix b/tests/negative/Termination/Axiom.juvix
new file mode 100644
index 0000000000..3c849a06c8
--- /dev/null
+++ b/tests/negative/Termination/Axiom.juvix
@@ -0,0 +1,5 @@
+module Axiom;
+
+axiom A : let
+    x : Type := x;
+  in x;
diff --git a/tests/negative/Termination/Ord.juvix b/tests/negative/Termination/Ord.juvix
index 8bf362f7ce..2c94f4c593 100644
--- a/tests/negative/Termination/Ord.juvix
+++ b/tests/negative/Termination/Ord.juvix
@@ -17,4 +17,3 @@ addord : Ord -> Ord -> Ord
 aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
   
   | f y z := addord (f z) y;
-