Improvements to error messages

src/Cryptol/TypeCheck/Error.hs

@@ -338,14 +338,7 @@ instance PP (WithNames Error) where
              , "When checking" <+> pp src
              ]
 
-      UnsolvableGoals gs ->
-          addTVarsDescsAfter names err $
-          nested "Unsolvable constraints:" $
-          let unErr g = case tIsError (goal g) of
-                          Just p  -> g { goal = p }
-                          Nothing -> g
-          in
-          bullets (map (ppWithNames names) (map unErr gs))
+      UnsolvableGoals gs -> explainUnsolvable names gs
 
       UnsolvedGoals gs
         | noUni ->
@@ -451,6 +444,99 @@ instance PP (WithNames Error) where
 
 
 
+explainUnsolvable :: NameMap -> [Goal] -> Doc
+explainUnsolvable names gs =
+  addTVarsDescsAfter names gs (bullets (map explain gs))
+
+  where
+  bullets xs = vcat [ "•" <+> d | d <- xs ]
+
+
+
+  explain g =
+    let useCtr = "Unsolvable constraint:" $$
+                  nest 2 (ppWithNames names g)
+
+    in
+    case tNoUser (goal g) of
+      TCon (PC pc) ts ->
+        let tys = [ backticks (ppWithNames names t) | t <- ts ]
+            doc1 : _ = tys
+            custom msg = msg $$
+                         nest 2 (text "arising from" $$
+                                 pp (goalSource g)   $$
+                                 text "at" <+> pp (goalRange g))
+        in
+        case pc of
+          PEqual      -> useCtr
+          PNeq        -> useCtr
+          PGeq        -> useCtr
+          PFin        -> useCtr
+          PPrime      -> useCtr
+
+          PHas sel ->
+            custom ("Type" <+> doc1 <+> "does not have field" <+> f 
+                    <+> "of type" <+> (tys !! 1))
+            where f = case sel of
+                        P.TupleSel n _ -> int n
+                        P.RecordSel fl _ -> backticks (pp fl)
+                        P.ListSel n _ -> int n
+
+          PZero  ->
+            custom ("Type" <+> doc1 <+> "does not have `zero`")
+
+          PLogic ->
+            custom ("Type" <+> doc1 <+> "does not support logical operations.")
+
+          PRing ->
+            custom ("Type" <+> doc1 <+> "does not support ring operations.")
+
+          PIntegral ->
+            custom (doc1 <+> "is not an integral type.")
+
+          PField ->
+            custom ("Type" <+> doc1 <+> "does not support field operations.")
+
+          PRound ->
+            custom ("Type" <+> doc1 <+> "does not support rounding operations.")
+
+          PEq ->
+            custom ("Type" <+> doc1 <+> "does not support equality.")
+
+          PCmp        ->
+            custom ("Type" <+> doc1 <+> "does not support comparisons.")
+
+          PSignedCmp  ->
+            custom ("Type" <+> doc1 <+> "does not support signed comparisons.")
+
+          PLiteral ->
+            let doc2 = tys !! 1
+            in custom (doc1 <+> "is not a valid literal of type" <+> doc2)
+
+          PFLiteral ->
+            case ts of
+              ~[m,n,_r,_a] ->
+                 let frac = backticks (ppWithNamesPrec names 4 m <> "/" <>
+                                       ppWithNamesPrec names 4 n)
+                     ty   = tys !! 3
+                 in custom (frac <+> "is not a valid literal of type" <+> ty)
+
+          PValidFloat ->
+            case ts of
+              ~[e,p] ->
+                custom ("Unsupported floating point parameters:" $$
+                     nest 2 ("exponent =" <+> ppWithNames names e $$
+                             "precision =" <+> ppWithNames names p))
+
+
+          PAnd        -> useCtr
+          PTrue       -> useCtr
+
+      _ -> useCtr
+
+
+
+
 -- | This picks the names to use when showing errors and warnings.
 computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap
 computeFreeVarNames warns errs =

tests/issues/T146.icry.stdout

@@ -3,16 +3,16 @@ Loading module Cryptol
 Loading module Main
 
 [error] at T146.cry:1:18--6:10:
-  The type ?fv`786 is not sufficiently polymorphic.
+  The type ?a is not sufficiently polymorphic.
     It cannot depend on quantified variables: fv`770
     When checking type of field 'v0'
   where
-  ?fv`786 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
+  ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
   fv`770 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:5:19--5:24:
-  The type ?fv`788 is not sufficiently polymorphic.
+  The type ?b is not sufficiently polymorphic.
     It cannot depend on quantified variables: fv`770
     When checking signature variable 'fv'
   where
-  ?fv`788 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
+  ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
   fv`770 is signature variable 'fv' at T146.cry:11:10--11:12

tests/issues/T820.icry.stdout

@@ -4,15 +4,13 @@ Showing a specific instance of polymorphic result:
 (ratio 1 2)
 
 [error] at <interactive>:1:1--1:8:
-  Unsolvable constraints:
-    • Integral ?a`776
-        arising from
-        use of expression (/)
-        at <interactive>:1:1--1:8
-    • FLiteral 1 1 0 ?a`776
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:8
-    • Reason: Mutually exclusive goals
+  • `?a` is not an integral type.
+      arising from
+      use of expression (/)
+      at <interactive>:1:1--1:8
+  • `1/1` is not a valid literal of type `?a`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:8
   where
-  ?a`776 is type argument 'a' of 'fraction' at <interactive>:1:1--1:8
+  ?a is type argument 'a' of 'fraction' at <interactive>:1:1--1:8

tests/issues/issue101.icry.stdout

@@ -1,9 +1,8 @@
 Loading module Cryptol
 
 [error] at <interactive>:1:1--1:11:
-  Unsolvable constraints:
-    • 0 >= 1
+  • Unsolvable constraint:
+      0 >= 1
         arising from
         use of partial type function (-)
         at <interactive>:1:1--1:11
-    • Reason: It is not the case that 0 >= 1

tests/issues/issue582.icry.stdout

@@ -1,52 +1,46 @@
 Loading module Cryptol
 
 [error] at <interactive>:1:1--1:18:
-  Unsolvable constraints:
-    • fin inf
+  • Unsolvable constraint:
+      fin inf
         arising from
         use of partial type function (/^)
         at <interactive>:1:1--1:18
-    • Reason: Expected a finite type, but found `inf`.
 
 [error] at <interactive>:1:1--1:18:
-  Unsolvable constraints:
-    • fin inf
+  • Unsolvable constraint:
+      fin inf
         arising from
         use of partial type function (/^)
         at <interactive>:1:1--1:18
-    • Reason: Expected a finite type, but found `inf`.
 
 [error] at <interactive>:1:1--1:16:
-  Unsolvable constraints:
-    • 0 >= 1
+  • Unsolvable constraint:
+      0 >= 1
         arising from
         use of partial type function (/^)
         at <interactive>:1:1--1:16
-    • Reason: It is not the case that 0 >= 1
 
 [error] at <interactive>:1:1--1:18:
-  Unsolvable constraints:
-    • fin inf
+  • Unsolvable constraint:
+      fin inf
         arising from
         use of partial type function (%^)
         at <interactive>:1:1--1:18
-    • Reason: Expected a finite type, but found `inf`.
 
 [error] at <interactive>:1:1--1:18:
-  Unsolvable constraints:
-    • fin inf
+  • Unsolvable constraint:
+      fin inf
         arising from
         use of partial type function (%^)
         at <interactive>:1:1--1:18
-    • Reason: Expected a finite type, but found `inf`.
 
 [error] at <interactive>:1:1--1:16:
-  Unsolvable constraints:
-    • 0 >= 1
+  • Unsolvable constraint:
+      0 >= 1
         arising from
         use of partial type function (%^)
         at <interactive>:1:1--1:16
-    • Reason: It is not the case that 0 >= 1
 Loading module Cryptol
 Loading module Main
 

tests/issues/issue835.icry.stdout

@@ -3,9 +3,7 @@ Loading module Cryptol
 Loading module Float
 
 [error] at <interactive>:1:1--1:28:
-  Unsolvable constraints:
-    • SignedCmp (Float 5 11)
-        arising from
-        use of expression (<$)
-        at <interactive>:1:1--1:28
-    • Reason: Type 'Float' does not support signed comparisons.
+  • Type `Float 5 11` does not support signed comparisons.
+      arising from
+      use of expression (<$)
+      at <interactive>:1:1--1:28

tests/issues/issue845.icry.stdout

@@ -27,45 +27,35 @@ Loading module Main
 (ratio 1 2)
 
 [error] at <interactive>:1:1--1:9:
-  Unsolvable constraints:
-    • FLiteral 1 0 0 Rational
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:9
-    • Reason: Fractions may not have 0 as the denominator.
+  • `1/0` is not a valid literal of type `Rational`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:9
 
 [error] at <interactive>:1:1--1:9:
-  Unsolvable constraints:
-    • FLiteral inf 2 0 Rational
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:9
-    • Reason: Fractions may not use `inf`
+  • `inf/2` is not a valid literal of type `Rational`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:9
 Loading module Cryptol
 Loading module Float
 0x0.8
 
 [error] at <interactive>:1:1--1:9:
-  Unsolvable constraints:
-    • FLiteral 1 0 0 Float64
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:9
-    • Reason: Fractions may not have 0 as the denominator.
+  • `1/0` is not a valid literal of type `Float64`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:9
 
 [error] at <interactive>:1:1--1:9:
-  Unsolvable constraints:
-    • FLiteral inf 2 0 Float64
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:9
-    • Reason: Fractions may not use `inf`
+  • `inf/2` is not a valid literal of type `Float64`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:9
 0x0.2
 
 [error] at <interactive>:1:1--1:9:
-  Unsolvable constraints:
-    • FLiteral 1 10 1 (Float 3 2)
-        arising from
-        use of fractional literal
-        at <interactive>:1:1--1:9
-    • Reason: 1/10 cannot be represented in Float 3 2
+  • `1/10` is not a valid literal of type `Float 3 2`
+      arising from
+      use of fractional literal
+      at <interactive>:1:1--1:9

tests/issues/issue910.icry.stdout

@@ -1,29 +1,25 @@
 Loading module Cryptol
 
 [error] at <interactive>:1:1--1:21:
-  Unsolvable constraints:
-    • Integral ?a`778
-        arising from
-        use of expression (@)
-        at <interactive>:1:8--1:21
-    • Field ?a`778
-        arising from
-        use of expression (/.)
-        at <interactive>:1:14--1:20
-    • Reason: Mutually exclusive goals
+  • `?a` is not an integral type.
+      arising from
+      use of expression (@)
+      at <interactive>:1:8--1:21
+  • Type `?a` does not support field operations.
+      arising from
+      use of expression (/.)
+      at <interactive>:1:14--1:20
   where
-  ?a`778 is type argument 'a' of '(/.)' at <interactive>:1:14--1:20
+  ?a is type argument 'a' of '(/.)' at <interactive>:1:14--1:20
 
 [error] at <interactive>:1:1--1:16:
-  Unsolvable constraints:
-    • Integral ?a`776
-        arising from
-        use of expression (@)
-        at <interactive>:1:8--1:16
-    • FLiteral 6 5 0 ?a`776
-        arising from
-        use of fractional literal
-        at <interactive>:1:13--1:16
-    • Reason: Mutually exclusive goals
+  • `?a` is not an integral type.
+      arising from
+      use of expression (@)
+      at <interactive>:1:8--1:16
+  • `6/5` is not a valid literal of type `?a`
+      arising from
+      use of fractional literal
+      at <interactive>:1:13--1:16
   where
-  ?a`776 is type argument 'a' of 'fraction' at <interactive>:1:13--1:16
+  ?a is type argument 'a' of 'fraction' at <interactive>:1:13--1:16

tests/issues/issue913.icry.stdout

@@ -5,9 +5,8 @@ False
 number`{rep = Bit} : {n} (1 >= n) => Bit
 
 [error] at <interactive>:1:1--1:2:
-  Unsolvable constraints:
-    • 1 >= 2
+  • Unsolvable constraint:
+      1 >= 2
         arising from
         use of literal or demoted expression
         at <interactive>:1:1--1:2
-    • Reason: It is not the case that 1 >= 2

tests/mono-binds/test04.icry.stdout

@@ -18,9 +18,7 @@ Loading module Cryptol
 Loading module test04
 
 [error] at test04.cry:1:1--5:14:
-  Unsolvable constraints:
-    • Literal 10 ()
-        arising from
-        use of literal or demoted expression
-        at test04.cry:3:19--3:21
-    • Reason: Type '()' does not support integer literals.
+  • `10` is not a valid literal of type `()`
+      arising from
+      use of literal or demoted expression
+      at test04.cry:3:19--3:21