diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout index 497e0c6df..b1d3ce75d 100644 --- a/tests/issues/issue226.icry.stdout +++ b/tests/issues/issue226.icry.stdout @@ -55,6 +55,7 @@ Primitive Types lengthFromThenTo : # -> # -> # -> # max : # -> # -> # min : # -> # -> # + prime : # -> Prop Rational : * Ring : * -> Prop Round : * -> Prop diff --git a/tests/regression/instance.cry b/tests/regression/instance.cry index 331f3634d..96e2f4754 100644 --- a/tests/regression/instance.cry +++ b/tests/regression/instance.cry @@ -198,6 +198,10 @@ fieldRational = recip fieldFloat : {e, p} (ValidFloat e p) => Float e p -> Float e p fieldFloat = recip +/** instance (prime p) => Field (Z p) */ +fieldZ : {p} prime p => Z p -> Z p +fieldZ = recip + //////////////////////////////////////////////////////////////////////////////// // Round diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index bba099f86..8dc6690e4 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Z ?n`1203) + • Logic (Z ?n`1205) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Z' does not support logical operations. where - ?n`1203 is type wildcard (_) at :1:15--1:16 + ?n`1205 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`{()} : () -> () @@ -50,14 +50,14 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => [error] at :1:1--1:11: Unsolvable constraints: - • Logic (Float ?n`1217 ?n`1218) + • Logic (Float ?n`1219 ?n`1220) arising from use of expression complement at :1:1--1:11 • Reason: Type 'Float' does not support logical operations. where - ?n`1217 is type wildcard (_) at :1:19--1:20 - ?n`1218 is type wildcard (_) at :1:21--1:22 + ?n`1219 is type wildcard (_) at :1:19--1:20 + ?n`1220 is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: Unsolvable constraints: @@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Z ?n`1241) + • Integral (Z ?n`1243) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Z ?n`1241' is not an integral type. + • Reason: Type 'Z ?n`1243' is not an integral type. where - ?n`1241 is type wildcard (_) at :1:8--1:9 + ?n`1243 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`1244 -> ?a`1245) + • Integral (?a`1246 -> ?a`1247) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '?a`1244 -> ?a`1245' is not an integral type. + • Reason: Type '?a`1246 -> ?a`1247' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:7--1:8 - ?a`1245 is type wildcard (_) at :1:12--1:13 + ?a`1246 is type wildcard (_) at :1:7--1:8 + ?a`1247 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: Unsolvable constraints: @@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral (?a`1244, ?a`1245) + • Integral (?a`1246, ?a`1247) arising from use of expression (%) at :1:1--1:4 - • Reason: Type '(?a`1244, ?a`1245)' is not an integral type. + • Reason: Type '(?a`1246, ?a`1247)' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:7--1:8 - ?a`1245 is type wildcard (_) at :1:10--1:11 + ?a`1246 is type wildcard (_) at :1:7--1:8 + ?a`1247 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: Unsolvable constraints: @@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => [error] at :1:1--1:4: Unsolvable constraints: - • Integral {x : ?a`1244, y : ?a`1245} + • Integral {x : ?a`1246, y : ?a`1247} arising from use of expression (%) at :1:1--1:4 - • Reason: Type '{x : ?a`1244, y : ?a`1245}' is not an integral type. + • Reason: Type '{x : ?a`1246, y : ?a`1247}' is not an integral type. where - ?a`1244 is type wildcard (_) at :1:11--1:12 - ?a`1245 is type wildcard (_) at :1:18--1:19 + ?a`1246 is type wildcard (_) at :1:11--1:12 + ?a`1247 is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: Unsolvable constraints: - • Integral (Float ?n`1244 ?n`1245) + • Integral (Float ?n`1246 ?n`1247) arising from use of expression (%) at :1:1--1:4 - • Reason: Type 'Float ?n`1244 ?n`1245' is not an integral type. + • Reason: Type 'Float ?n`1246 ?n`1247' is not an integral type. where - ?n`1244 is type wildcard (_) at :1:12--1:13 - ?n`1245 is type wildcard (_) at :1:14--1:15 + ?n`1246 is type wildcard (_) at :1:12--1:13 + ?n`1247 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -184,38 +184,29 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => at :1:1--1:6 • Reason: Type 'Integer' does not support field operations. recip`{Rational} : Rational -> Rational +recip`{Z _} : {n} (prime n, n >= 1) => Z n -> Z n [error] at :1:1--1:6: Unsolvable constraints: - • Field (Z ?n`1245) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Type 'Z' does not support field operations. - where - ?n`1245 is type wildcard (_) at :1:10--1:11 - -[error] at :1:1--1:6: - Unsolvable constraints: - • Field ([?n`1245]?a`1246) + • Field ([?n`1249]?a`1250) arising from use of expression recip at :1:1--1:6 • Reason: Sequence types do not support field operations. where - ?n`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:11--1:12 + ?n`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1245 -> ?a`1246) + • Field (?a`1249 -> ?a`1250) arising from use of expression recip at :1:1--1:6 • Reason: Function types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:14--1:15 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -227,14 +218,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field (?a`1245, ?a`1246) + • Field (?a`1249, ?a`1250) arising from use of expression recip at :1:1--1:6 • Reason: Tuple types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:9--1:10 - ?a`1246 is type wildcard (_) at :1:12--1:13 + ?a`1249 is type wildcard (_) at :1:9--1:10 + ?a`1250 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -246,14 +237,14 @@ recip`{Rational} : Rational -> Rational [error] at :1:1--1:6: Unsolvable constraints: - • Field {x : ?a`1245, y : ?a`1246} + • Field {x : ?a`1249, y : ?a`1250} arising from use of expression recip at :1:1--1:6 • Reason: Record types do not support field operations. where - ?a`1245 is type wildcard (_) at :1:13--1:14 - ?a`1246 is type wildcard (_) at :1:20--1:21 + ?a`1249 is type wildcard (_) at :1:13--1:14 + ?a`1250 is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m @@ -276,35 +267,35 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (Z ?n`1249) + • Round (Z ?n`1253) arising from use of expression floor at :1:1--1:6 • Reason: Type 'Z' does not support rounding operations. where - ?n`1249 is type wildcard (_) at :1:10--1:11 + ?n`1253 is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: Unsolvable constraints: - • Round ([?n`1249]?a`1250) + • Round ([?n`1253]?a`1254) arising from use of expression floor at :1:1--1:6 • Reason: Sequence types do not support rounding operations. where - ?n`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:11--1:12 + ?n`1253 is type wildcard (_) at :1:9--1:10 + ?a`1254 is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1249 -> ?a`1250) + • Round (?a`1253 -> ?a`1254) arising from use of expression floor at :1:1--1:6 • Reason: Function types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:14--1:15 + ?a`1253 is type wildcard (_) at :1:9--1:10 + ?a`1254 is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: Unsolvable constraints: @@ -316,14 +307,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round (?a`1249, ?a`1250) + • Round (?a`1253, ?a`1254) arising from use of expression floor at :1:1--1:6 • Reason: Tuple types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:9--1:10 - ?a`1250 is type wildcard (_) at :1:12--1:13 + ?a`1253 is type wildcard (_) at :1:9--1:10 + ?a`1254 is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: Unsolvable constraints: @@ -335,14 +326,14 @@ floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: Unsolvable constraints: - • Round {x : ?a`1249, y : ?a`1250} + • Round {x : ?a`1253, y : ?a`1254} arising from use of expression floor at :1:1--1:6 • Reason: Record types do not support rounding operations. where - ?a`1249 is type wildcard (_) at :1:13--1:14 - ?a`1250 is type wildcard (_) at :1:20--1:21 + ?a`1253 is type wildcard (_) at :1:13--1:14 + ?a`1254 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 @@ -352,14 +343,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • Eq (?a`1260 -> ?a`1261) + • Eq (?a`1264 -> ?a`1265) arising from use of expression (==) at :1:1--1:5 • Reason: Function types do not support comparisons. where - ?a`1260 is type wildcard (_) at :1:8--1:9 - ?a`1261 is type wildcard (_) at :1:13--1:14 + ?a`1264 is type wildcard (_) at :1:8--1:9 + ?a`1265 is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -373,25 +364,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:4: Unsolvable constraints: - • Cmp (Z ?n`1274) + • Cmp (Z ?n`1278) arising from use of expression (<) at :1:1--1:4 • Reason: Type 'Z' does not support order comparisons. where - ?n`1274 is type wildcard (_) at :1:8--1:9 + ?n`1278 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`1277 -> ?a`1278) + • Cmp (?a`1281 -> ?a`1282) arising from use of expression (<) at :1:1--1:4 • Reason: Function types do not support order comparisons. where - ?a`1277 is type wildcard (_) at :1:7--1:8 - ?a`1278 is type wildcard (_) at :1:12--1:13 + ?a`1281 is type wildcard (_) at :1:7--1:8 + ?a`1282 is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -426,25 +417,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Z ?n`1288) + • SignedCmp (Z ?n`1292) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Z' does not support signed comparisons. where - ?n`1288 is type wildcard (_) at :1:9--1:10 + ?n`1292 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`1291 -> ?a`1292) + • SignedCmp (?a`1295 -> ?a`1296) arising from use of expression (<$) at :1:1--1:5 • Reason: Function types do not support signed comparisons. where - ?a`1291 is type wildcard (_) at :1:8--1:9 - ?a`1292 is type wildcard (_) at :1:13--1:14 + ?a`1295 is type wildcard (_) at :1:8--1:9 + ?a`1296 is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -454,14 +445,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer [error] at :1:1--1:5: Unsolvable constraints: - • SignedCmp (Float ?n`1299 ?n`1300) + • SignedCmp (Float ?n`1303 ?n`1304) arising from use of expression (<$) at :1:1--1:5 • Reason: Type 'Float' does not support signed comparisons. where - ?n`1299 is type wildcard (_) at :1:13--1:14 - ?n`1300 is type wildcard (_) at :1:15--1:16 + ?n`1303 is type wildcard (_) at :1:13--1:14 + ?n`1304 is type wildcard (_) at :1:15--1:16 number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:7: @@ -475,60 +466,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1308 (?a`1309 -> ?a`1310) + • Literal ?val`1312 (?a`1313 -> ?a`1314) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '?a`1309 -> ?a`1310' does not support integer literals. + • Reason: Type '?a`1313 -> ?a`1314' does not support integer literals. where - ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1309 is type wildcard (_) at :1:15--1:16 - ?a`1310 is type wildcard (_) at :1:20--1:21 + ?val`1312 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1313 is type wildcard (_) at :1:15--1:16 + ?a`1314 is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1308 () + • Literal ?val`1312 () arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '()' does not support integer literals. where - ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1312 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1308 (?a`1309, ?a`1310) + • Literal ?val`1312 (?a`1313, ?a`1314) arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '(?a`1309, ?a`1310)' does not support integer literals. + • Reason: Type '(?a`1313, ?a`1314)' does not support integer literals. where - ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1309 is type wildcard (_) at :1:16--1:17 - ?a`1310 is type wildcard (_) at :1:19--1:20 + ?val`1312 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1313 is type wildcard (_) at :1:16--1:17 + ?a`1314 is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1308 {} + • Literal ?val`1312 {} arising from use of literal or demoted expression at :1:1--1:7 • Reason: Type '{}' does not support integer literals. where - ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 + ?val`1312 is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: Unsolvable constraints: - • Literal ?val`1308 {x : ?a`1309, y : ?a`1310} + • Literal ?val`1312 {x : ?a`1313, y : ?a`1314} arising from use of literal or demoted expression at :1:1--1:7 - • Reason: Type '{x : ?a`1309, - y : ?a`1310}' does not support integer literals. + • Reason: Type '{x : ?a`1313, + y : ?a`1314}' does not support integer literals. where - ?val`1308 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1309 is type wildcard (_) at :1:20--1:21 - ?a`1310 is type wildcard (_) at :1:27--1:28 + ?val`1312 is type argument 'val' of 'number' at :1:1--1:7 + ?a`1313 is type wildcard (_) at :1:20--1:21 + ?a`1314 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