Indent goals to be shown a bit further, to line up with assumptions.

src/Cryptol/TypeCheck/InferTypes.hs

@@ -300,8 +300,11 @@ instance PP (WithNames Goal) where
 instance PP (WithNames DelayedCt) where
   ppPrec _ (WithNames d names) =
     sig $$ "we need to show that" $$
-    nest 2 (vcat ( [ vars, asmps, "the following constraints hold:"] ++
-                   bullets (map (ppWithNames ns1) (dctGoals d)) ))
+    nest 2 (vcat [ vars, asmps, "the following constraints hold:"
+                 , nest 2 $ vcat
+                          $ bullets
+                          $ map (ppWithNames ns1)
+                          $ dctGoals d ])
     where
     bullets xs = [ "•" <+> x | x <- xs ]
 

tests/issues/issue058.icry.stdout

@@ -8,10 +8,10 @@ Loading module Main
     we need to show that
       for any type n
       the following constraints hold:
-      • fin n
-          arising from
-          use of literal or demoted expression
-          at ./issue058.cry:4:15--4:16
+        • fin n
+            arising from
+            use of literal or demoted expression
+            at ./issue058.cry:4:15--4:16
 [error] at ./issue058.cry:7:1--7:17:
   Failed to validate user-specified signature.
     in the definition of 'Main::last', at ./issue058.cry:7:1--7:5,
@@ -20,17 +20,17 @@ Loading module Main
       assuming
         • n >= 1
       the following constraints hold:
-      • fin n
-          arising from
-          use of expression (!)
-          at ./issue058.cry:7:11--7:17
+        • fin n
+            arising from
+            use of expression (!)
+            at ./issue058.cry:7:11--7:17
 [error] at ./issue058.cry:10:1--10:17:
   Failed to validate user-specified signature.
     in the definition of 'Main::pad', at ./issue058.cry:10:1--10:4,
     we need to show that
       for any type n
       the following constraints hold:
-      • fin n
-          arising from
-          use of expression (#)
-          at ./issue058.cry:10:9--10:17
+        • fin n
+            arising from
+            use of expression (#)
+            at ./issue058.cry:10:9--10:17

tests/issues/issue323.icry.stdout

@@ -10,7 +10,7 @@ Loading module Main
     we need to show that
       for any type a
       the following constraints hold:
-      • fin a
-          arising from
-          use of expression take
-          at ./issue323.cry:2:43--2:47
+        • fin a
+            arising from
+            use of expression take
+            at ./issue323.cry:2:43--2:47

tests/issues/issue416.icry.stdout

@@ -11,10 +11,10 @@ Loading module Main
         • fin n
         • 3 >= width n
       the following constraints hold:
-      • 1 != n
-          arising from
-          use of partial type function lengthFromThenTo
-          at ./issue416.cry:1:5--1:61
+        • 1 != n
+            arising from
+            use of partial type function lengthFromThenTo
+            at ./issue416.cry:1:5--1:61
 [error] at ./issue416.cry:5:1--5:16:
   Failed to validate user-specified signature.
     in the definition of 'Main::g', at ./issue416.cry:5:1--5:2,
@@ -24,7 +24,7 @@ Loading module Main
         • fin n
         • 3 >= width n
       the following constraints hold:
-      • 1 != n
-          arising from
-          use of finite enumeration
-          at ./issue416.cry:5:5--5:16
+        • 1 != n
+            arising from
+            use of finite enumeration
+            at ./issue416.cry:5:5--5:16