From bfad11ba8676d36817f2f97aabb7d423ca578c38 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Nov 2020 13:29:57 -0800 Subject: [PATCH] Improvements to error messages --- src/Cryptol/TypeCheck/Error.hs | 102 ++++- tests/issues/T146.icry.stdout | 8 +- tests/issues/T820.icry.stdout | 20 +- tests/issues/issue101.icry.stdout | 5 +- tests/issues/issue582.icry.stdout | 30 +- tests/issues/issue835.icry.stdout | 10 +- tests/issues/issue845.icry.stdout | 50 +-- tests/issues/issue910.icry.stdout | 40 +- tests/issues/issue913.icry.stdout | 5 +- tests/mono-binds/test04.icry.stdout | 10 +- tests/regression/float.icry.stdout | 20 +- tests/regression/instance.icry.stdout | 551 +++++++++++-------------- tests/regression/primes.icry.stdout | 10 +- tests/regression/tc-errors.icry.stdout | 21 +- 14 files changed, 421 insertions(+), 461 deletions(-) diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index abe79178e..3ce356135 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/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 = diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 99be75750..7e58a3521 100644 --- a/tests/issues/T146.icry.stdout +++ b/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 diff --git a/tests/issues/T820.icry.stdout b/tests/issues/T820.icry.stdout index 54e3594a6..b63b6350c 100644 --- a/tests/issues/T820.icry.stdout +++ b/tests/issues/T820.icry.stdout @@ -4,15 +4,13 @@ Showing a specific instance of polymorphic result: (ratio 1 2) [error] at :1:1--1:8: - Unsolvable constraints: - • Integral ?a`776 - arising from - use of expression (/) - at :1:1--1:8 - • FLiteral 1 1 0 ?a`776 - arising from - use of fractional literal - at :1:1--1:8 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (/) + at :1:1--1:8 + • `1/1` is not a valid literal of type `?a` + arising from + use of fractional literal + at :1:1--1:8 where - ?a`776 is type argument 'a' of 'fraction' at :1:1--1:8 + ?a is type argument 'a' of 'fraction' at :1:1--1:8 diff --git a/tests/issues/issue101.icry.stdout b/tests/issues/issue101.icry.stdout index 42f87d8fa..f6c0dd270 100644 --- a/tests/issues/issue101.icry.stdout +++ b/tests/issues/issue101.icry.stdout @@ -1,9 +1,8 @@ Loading module Cryptol [error] at :1:1--1:11: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (-) at :1:1--1:11 - • Reason: It is not the case that 0 >= 1 diff --git a/tests/issues/issue582.icry.stdout b/tests/issues/issue582.icry.stdout index 1bb4e3e2b..cf51aa924 100644 --- a/tests/issues/issue582.icry.stdout +++ b/tests/issues/issue582.icry.stdout @@ -1,52 +1,46 @@ Loading module Cryptol [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (/^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (/^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:16: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (/^) at :1:1--1:16 - • Reason: It is not the case that 0 >= 1 [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (%^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (%^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:16: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (%^) at :1:1--1:16 - • Reason: It is not the case that 0 >= 1 Loading module Cryptol Loading module Main diff --git a/tests/issues/issue835.icry.stdout b/tests/issues/issue835.icry.stdout index 6e6137910..13187f61b 100644 --- a/tests/issues/issue835.icry.stdout +++ b/tests/issues/issue835.icry.stdout @@ -3,9 +3,7 @@ Loading module Cryptol Loading module Float [error] at :1:1--1:28: - Unsolvable constraints: - • SignedCmp (Float 5 11) - arising from - use of expression (<$) - at :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 :1:1--1:28 diff --git a/tests/issues/issue845.icry.stdout b/tests/issues/issue845.icry.stdout index 35e922401..1a48ca0db 100644 --- a/tests/issues/issue845.icry.stdout +++ b/tests/issues/issue845.icry.stdout @@ -27,45 +27,35 @@ Loading module Main (ratio 1 2) [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 0 0 Rational - arising from - use of fractional literal - at :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 :1:1--1:9 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral inf 2 0 Rational - arising from - use of fractional literal - at :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 :1:1--1:9 Loading module Cryptol Loading module Float 0x0.8 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 0 0 Float64 - arising from - use of fractional literal - at :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 :1:1--1:9 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral inf 2 0 Float64 - arising from - use of fractional literal - at :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 :1:1--1:9 0x0.2 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 10 1 (Float 3 2) - arising from - use of fractional literal - at :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 :1:1--1:9 diff --git a/tests/issues/issue910.icry.stdout b/tests/issues/issue910.icry.stdout index 231673c25..6341a306c 100644 --- a/tests/issues/issue910.icry.stdout +++ b/tests/issues/issue910.icry.stdout @@ -1,29 +1,25 @@ Loading module Cryptol [error] at :1:1--1:21: - Unsolvable constraints: - • Integral ?a`778 - arising from - use of expression (@) - at :1:8--1:21 - • Field ?a`778 - arising from - use of expression (/.) - at :1:14--1:20 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (@) + at :1:8--1:21 + • Type `?a` does not support field operations. + arising from + use of expression (/.) + at :1:14--1:20 where - ?a`778 is type argument 'a' of '(/.)' at :1:14--1:20 + ?a is type argument 'a' of '(/.)' at :1:14--1:20 [error] at :1:1--1:16: - Unsolvable constraints: - • Integral ?a`776 - arising from - use of expression (@) - at :1:8--1:16 - • FLiteral 6 5 0 ?a`776 - arising from - use of fractional literal - at :1:13--1:16 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (@) + at :1:8--1:16 + • `6/5` is not a valid literal of type `?a` + arising from + use of fractional literal + at :1:13--1:16 where - ?a`776 is type argument 'a' of 'fraction' at :1:13--1:16 + ?a is type argument 'a' of 'fraction' at :1:13--1:16 diff --git a/tests/issues/issue913.icry.stdout b/tests/issues/issue913.icry.stdout index 7472047c0..a3ab7aca3 100644 --- a/tests/issues/issue913.icry.stdout +++ b/tests/issues/issue913.icry.stdout @@ -5,9 +5,8 @@ False number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:2: - Unsolvable constraints: - • 1 >= 2 + • Unsolvable constraint: + 1 >= 2 arising from use of literal or demoted expression at :1:1--1:2 - • Reason: It is not the case that 1 >= 2 diff --git a/tests/mono-binds/test04.icry.stdout b/tests/mono-binds/test04.icry.stdout index 377b32b69..f7b58b6d4 100644 --- a/tests/mono-binds/test04.icry.stdout +++ b/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 diff --git a/tests/regression/float.icry.stdout b/tests/regression/float.icry.stdout index 7524004a0..de525a4e8 100644 --- a/tests/regression/float.icry.stdout +++ b/tests/regression/float.icry.stdout @@ -71,24 +71,20 @@ IEEE-754 floating point numbers. 0x4.0p0 [error] at :1:1--1:20: - Unsolvable constraints: - • FLiteral 5 1 1 Small - arising from - use of fractional literal - at :1:1--1:6 - • Reason: 5/1 cannot be represented in Float 3 2 + • `5/1` is not a valid literal of type `Small` + arising from + use of fractional literal + at :1:1--1:6 0x1.3p0 0x2.0p-4 0x2.0p-4 0x8.0p0 [error] at :1:1--1:2: - Unsolvable constraints: - • Literal 7 Small - arising from - use of literal or demoted expression - at :1:1--1:2 - • Reason: 7 cannot be represented in Float 3 2 + • `7` is not a valid literal of type `Small` + arising from + use of literal or demoted expression + at :1:1--1:2 "-- NaN------------------------------------------------------------------------" fpNaN : {e, p} (ValidFloat e p) => Float e p diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index bce056f4c..2818b2a18 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -16,30 +16,24 @@ zero`{Float _ _} : {n, m} (ValidFloat n m) => Float n m complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: - Unsolvable constraints: - • Logic Integer - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Integer' does not support logical operations. + • Type `Integer` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 [error] at :1:1--1:11: - Unsolvable constraints: - • Logic Rational - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Rational' does not support logical operations. + • Type `Rational` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 [error] at :1:1--1:11: - Unsolvable constraints: - • Logic (Z ?n`1011) - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Z' does not support logical operations. + • Type `Z ?m` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 where - ?n`1011 is type wildcard (_) at :1:15--1:16 + ?m is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -49,23 +43,19 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => {x : a, y : b} -> {x : a, y : b} [error] at :1:1--1:11: - Unsolvable constraints: - • Logic (Float ?n`1025 ?n`1026) - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Float' does not support logical operations. + • Type `Float ?m ?n` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 where - ?n`1025 is type wildcard (_) at :1:19--1:20 - ?n`1026 is type wildcard (_) at :1:21--1:22 + ?m is type wildcard (_) at :1:19--1:20 + ?n is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: - Unsolvable constraints: - • Ring Bit - arising from - use of expression negate - at :1:1--1:7 - • Reason: Type 'Bit' does not support ring operations. + • Type `Bit` does not support ring operations. + arising from + use of expression negate + at :1:1--1:7 negate`{Integer} : Integer -> Integer negate`{Rational} : Rational -> Rational negate`{Z _} : {n} (n >= 1, fin n) => Z n -> Z n @@ -81,259 +71,207 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m [error] at :1:1--1:4: - Unsolvable constraints: - • Integral Bit - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Bit' is not an integral type. + • `Bit` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 (%)`{Integer} : Integer -> Integer -> Integer [error] at :1:1--1:4: - Unsolvable constraints: - • Integral Rational - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Rational' is not an integral type. + • `Rational` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (Z ?n`1049) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Z ?n`1049' is not an integral type. + • `Z ?m` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?n`1049 is type wildcard (_) at :1:8--1:9 + ?m is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (?a`1052 -> ?a`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '?a`1052 -> ?a`1053' is not an integral type. + • `?a -> ?b` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:7--1:8 - ?a`1053 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral () - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '()' is not an integral type. + • `()` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (?a`1052, ?a`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '(?a`1052, ?a`1053)' is not an integral type. + • `(?a, ?b)` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:7--1:8 - ?a`1053 is type wildcard (_) at :1:10--1:11 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral {} - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '{}' is not an integral type. + • `{}` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral {x : ?a`1052, y : ?a`1053} - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '{x : ?a`1052, y : ?a`1053}' is not an integral type. + • `{x : ?a, y : ?b}` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:11--1:12 - ?a`1053 is type wildcard (_) at :1:18--1:19 + ?a is type wildcard (_) at :1:11--1:12 + ?b is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (Float ?n`1052 ?n`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Float ?n`1052 ?n`1053' is not an integral type. + • `Float ?m ?n` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?n`1052 is type wildcard (_) at :1:12--1:13 - ?n`1053 is type wildcard (_) at :1:14--1:15 + ?m is type wildcard (_) at :1:12--1:13 + ?n is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Field Bit - arising from - use of expression recip - at :1:1--1:6 - • Reason: Type 'Bit' does not support field operations. + • Type `Bit` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field Integer - arising from - use of expression recip - at :1:1--1:6 - • Reason: Type 'Integer' does not support field operations. + • Type `Integer` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 recip`{Rational} : Rational -> Rational recip`{Z _} : {n} (prime n, n >= 1) => Z n -> Z n [error] at :1:1--1:6: - Unsolvable constraints: - • Field ([?n`1055]?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Sequence types do not support field operations. + • Type `[?m]?a` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?n`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:11--1:12 + ?m is type wildcard (_) at :1:9--1:10 + ?a is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: - Unsolvable constraints: - • Field (?a`1055 -> ?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Function types do not support field operations. + • Type `?a -> ?b` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:14--1:15 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Field () - arising from - use of expression recip - at :1:1--1:6 - • Reason: Tuple types do not support field operations. + • Type `()` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field (?a`1055, ?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Tuple types do not support field operations. + • Type `(?a, ?b)` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: - Unsolvable constraints: - • Field {} - arising from - use of expression recip - at :1:1--1:6 - • Reason: Record types do not support field operations. + • Type `{}` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field {x : ?a`1055, y : ?a`1056} - arising from - use of expression recip - at :1:1--1:6 - • Reason: Record types do not support field operations. + • Type `{x : ?a, y : ?b}` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:13--1:14 - ?a`1056 is type wildcard (_) at :1:20--1:21 + ?a is type wildcard (_) at :1:13--1:14 + ?b is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m [error] at :1:1--1:6: - Unsolvable constraints: - • Round Bit - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Bit' does not support rounding operations. + • Type `Bit` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round Integer - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Integer' does not support rounding operations. + • Type `Integer` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: - Unsolvable constraints: - • Round (Z ?n`1059) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Z' does not support rounding operations. + • Type `Z ?m` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?n`1059 is type wildcard (_) at :1:10--1:11 + ?m is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: - Unsolvable constraints: - • Round ([?n`1059]?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Sequence types do not support rounding operations. + • Type `[?m]?a` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?n`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:11--1:12 + ?m is type wildcard (_) at :1:9--1:10 + ?a is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: - Unsolvable constraints: - • Round (?a`1059 -> ?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Function types do not support rounding operations. + • Type `?a -> ?b` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:14--1:15 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Round () - arising from - use of expression floor - at :1:1--1:6 - • Reason: Tuple types do not support rounding operations. + • Type `()` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round (?a`1059, ?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Tuple types do not support rounding operations. + • Type `(?a, ?b)` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: - Unsolvable constraints: - • Round {} - arising from - use of expression floor - at :1:1--1:6 - • Reason: Record types do not support rounding operations. + • Type `{}` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round {x : ?a`1059, y : ?a`1060} - arising from - use of expression floor - at :1:1--1:6 - • Reason: Record types do not support rounding operations. + • Type `{x : ?a, y : ?b}` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:13--1:14 - ?a`1060 is type wildcard (_) at :1:20--1:21 + ?a is type wildcard (_) at :1:13--1:14 + ?b is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -342,15 +280,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{[_]_} : {n, a} (Eq a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • Eq (?a`1070 -> ?a`1071) - arising from - use of expression (==) - at :1:1--1:5 - • Reason: Function types do not support comparisons. + • Type `?a -> ?b` does not support equality. + arising from + use of expression (==) + at :1:1--1:5 where - ?a`1070 is type wildcard (_) at :1:8--1:9 - ?a`1071 is type wildcard (_) at :1:13--1:14 + ?a is type wildcard (_) at :1:8--1:9 + ?b is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -363,26 +299,22 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (<)`{Rational} : Rational -> Rational -> Bit [error] at :1:1--1:4: - Unsolvable constraints: - • Cmp (Z ?n`1084) - arising from - use of expression (<) - at :1:1--1:4 - • Reason: Type 'Z' does not support order comparisons. + • Type `Z ?m` does not support comparisons. + arising from + use of expression (<) + at :1:1--1:4 where - ?n`1084 is type wildcard (_) at :1:8--1:9 + ?m is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: - Unsolvable constraints: - • Cmp (?a`1087 -> ?a`1088) - arising from - use of expression (<) - at :1:1--1:4 - • Reason: Function types do not support order comparisons. + • Type `?a -> ?b` does not support comparisons. + arising from + use of expression (<) + at :1:1--1:4 where - ?a`1087 is type wildcard (_) at :1:7--1:8 - ?a`1088 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -392,50 +324,40 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer Float n m -> Float n m -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Bit - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Bit' does not support signed comparisons. + • Type `Bit` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Integer - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Integer' does not support signed comparisons. + • Type `Integer` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Rational - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Rational' does not support signed comparisons. + • Type `Rational` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (Z ?n`1098) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Z' does not support signed comparisons. + • Type `Z ?m` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?n`1098 is type wildcard (_) at :1:9--1:10 + ?m is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (?a`1101 -> ?a`1102) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Function types do not support signed comparisons. + • Type `?a -> ?b` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?a`1101 is type wildcard (_) at :1:8--1:9 - ?a`1102 is type wildcard (_) at :1:13--1:14 + ?a is type wildcard (_) at :1:8--1:9 + ?b is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -444,15 +366,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer {x : a, y : b} -> {x : a, y : b} -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (Float ?n`1109 ?n`1110) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Float' does not support signed comparisons. + • Type `Float ?m ?n` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?n`1109 is type wildcard (_) at :1:13--1:14 - ?n`1110 is type wildcard (_) at :1:15--1:16 + ?m is type wildcard (_) at :1:13--1:14 + ?n is type wildcard (_) at :1:15--1:16 number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:7: @@ -465,61 +385,50 @@ number`{rep = Z _} : {n, m} (m >= 1 + n, m >= 1, fin m, fin n) => number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 (?a`1119 -> ?a`1120) - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '?a`1119 -> ?a`1120' does not support integer literals. + • `?m` is not a valid literal of type `?a -> ?b` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:15--1:16 - ?a`1120 is type wildcard (_) at :1:20--1:21 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:15--1:16 + ?b is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 () - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '()' does not support integer literals. + • `?m` is not a valid literal of type `()` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 + ?m is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 (?a`1119, ?a`1120) - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '(?a`1119, ?a`1120)' does not support integer literals. + • `?m` is not a valid literal of type `(?a, ?b)` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:16--1:17 - ?a`1120 is type wildcard (_) at :1:19--1:20 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:16--1:17 + ?b is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 {} - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '{}' does not support integer literals. + • `?m` is not a valid literal of type `{}` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 + ?m is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 {x : ?a`1119, y : ?a`1120} - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '{x : ?a`1119, - y : ?a`1120}' does not support integer literals. + • `?m` is not a valid literal of type `{x : ?a, y : ?b}` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:20--1:21 - ?a`1120 is type wildcard (_) at :1:27--1:28 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:20--1:21 + ?b is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i diff --git a/tests/regression/primes.icry.stdout b/tests/regression/primes.icry.stdout index 9a2ed204a..2233014d9 100644 --- a/tests/regression/primes.icry.stdout +++ b/tests/regression/primes.icry.stdout @@ -49,20 +49,18 @@ Expected test coverage: 0.00% (100 of 2^^1042 values) 1 [error] at :1:1--1:8: - Unsolvable constraints: - • prime 8 + • Unsolvable constraint: + prime 8 arising from use of expression z1prime at :1:1--1:8 - • Reason: 8 is not a prime number [error] at :1:1--1:8: - Unsolvable constraints: - • prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 + • Unsolvable constraint: + prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 arising from use of expression z1prime at :1:1--1:8 - • Reason: 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 is not a prime number Q.E.D. Q.E.D. Q.E.D. diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout index 127121d75..a2bde3033 100644 --- a/tests/regression/tc-errors.icry.stdout +++ b/tests/regression/tc-errors.icry.stdout @@ -16,20 +16,19 @@ Loading module Cryptol [error] at :1:9--1:10: Matching would result in an infinite type. - The type: ?arg`771 - occurs in: ?arg`771 -> ?res + The type: ?b + occurs in: ?b -> ?a When checking type of function argument where - ?res is type of function result at :1:1--1:10 - ?arg`771 is type of function argument at :1:7--1:10 + ?a is type of function result at :1:1--1:10 + ?b is type of function argument at :1:7--1:10 [error] at :1:1--1:5: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of expression take at :1:1--1:5 - • Reason: Expected a finite type, but found `inf`. Parse error at :1:8, unexpected: , @@ -85,18 +84,18 @@ Loading module Main [error] at tc-errors-5.cry:2:5--2:7: Inferred type is not sufficiently polymorphic. Quantified variable: a`767 - cannot match type: [0]?a`769 + cannot match type: [0]?a When checking the type of 'Main::f' where - ?a`769 is type of sequence member at tc-errors-5.cry:2:5--2:7 + ?a is type of sequence member at tc-errors-5.cry:2:5--2:7 a`767 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 Loading module Cryptol Loading module Main [error] at tc-errors-6.cry:4:7--4:8: - The type ?x`770 is not sufficiently polymorphic. + The type ?a is not sufficiently polymorphic. It cannot depend on quantified variables: b`771 When checking the type of 'Main::g' where - ?x`770 is the type of 'x' at tc-errors-6.cry:1:3--1:4 + ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4 b`771 is signature variable 'b' at tc-errors-6.cry:3:8--3:9