GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-29 10:53:31 +03:00
Code Issues Projects Releases Wiki Activity

Generalize the type of generate.

Browse Source 
This allows the indexing type to be arbitraty `Integral` types,
provided the type is large enough to index the sequence.

Fixes #848
This commit is contained in:
Rob Dockins 2020-08-22 15:23:38 -07:00
parent 7cb9dc2ce3
commit 82187952e7
8 changed files with 115 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Cryptol.cry
View File

@ -874,7 +874,7 @@ updatesEnd xs0 idxs vals = xss!0
* Declarations of the form 'x @ i = e' are syntactic sugar for
* 'x = generate (\i -> e)'.
*/
generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]

16
tests/issues/T146.icry.stdout
View File

@ -3,14 +3,14 @@ Loading module Cryptol
Loading module Main
[error] at T146.cry:1:18--6:10:
The type ?fv`958 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`942
The type ?fv`959 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`943
where
?fv`958 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
fv`942 is signature variable 'fv' at T146.cry:11:10--11:12
?fv`959 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
fv`943 is signature variable 'fv' at T146.cry:11:10--11:12
[error] at T146.cry:5:19--5:24:
The type ?fv`960 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`942
The type ?fv`961 is not sufficiently polymorphic.
It cannot depend on quantified variables: fv`943
where
?fv`960 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
fv`942 is signature variable 'fv' at T146.cry:11:10--11:12
?fv`961 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
fv`943 is signature variable 'fv' at T146.cry:11:10--11:12

4
tests/issues/issue226.icry.stdout
View File

@ -142,7 +142,9 @@ Symbols
Literal last a) =>
[1 + (last - first)]a
fromZ : {n} (fin n, n >= 1) => Z n -> Integer
generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
generate :
{n, a, ix} (fin n, n >= 1, Integral ix, Literal (n - 1) ix) =>
(ix -> a) -> [n]a
groupBy :
{each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
head : {n, a} [1 + n]a -> a

4
tests/issues/issue290v2.icry.stdout
View File

@ -4,9 +4,9 @@ Loading module Main
[error] at issue290v2.cry:2:1--2:19:
Unsolved constraints:
• n`939 == 1
• n`940 == 1
arising from
checking a pattern: type of 1st argument of Main::minMax
at issue290v2.cry:2:8--2:11
where
n`939 is signature variable 'n' at issue290v2.cry:1:11--1:12
n`940 is signature variable 'n' at issue290v2.cry:1:11--1:12

4
tests/issues/issue723.icry.stdout
View File

@ -10,9 +10,9 @@ Loading module Main
assuming
• fin k
the following constraints hold:
• k == n`939
• k == n`940
arising from
matching types
at issue723.cry:7:17--7:19
where
n`939 is signature variable 'n' at issue723.cry:1:6--1:7
n`940 is signature variable 'n' at issue723.cry:1:6--1:7

3
tests/issues/issue848.icry Normal file
View File

@ -0,0 +1,3 @@
let a@i = i + 10
:t a
a : [10][32]

6
tests/issues/issue848.icry.stdout Normal file
View File

@ -0,0 +1,6 @@
Loading module Cryptol
a : {n, a} (Integral a, n >= 1, Literal (max 10 (n - 1)) a,
fin n) =>
[n]a
[0x0000000a, 0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e,
0x0000000f, 0x00000010, 0x00000011, 0x00000012, 0x00000013]

180
tests/regression/instance.icry.stdout
View File

@ -33,13 +33,13 @@ complement`{Bit} : Bit -> Bit
[error] at <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic (Z ?n`1179)
• Logic (Z ?n`1180)
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Z' does not support logical operations.
where
?n`1179 is type wildcard (_) at <interactive>:1:15--1:16
?n`1180 is type wildcard (_) at <interactive>: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 <interactive>:1:1--1:11:
Unsolvable constraints:
• Logic (Float ?n`1193 ?n`1194)
• Logic (Float ?n`1194 ?n`1195)
arising from
use of expression complement
at <interactive>:1:1--1:11
• Reason: Type 'Float' does not support logical operations.
where
?n`1193 is type wildcard (_) at <interactive>:1:19--1:20
?n`1194 is type wildcard (_) at <interactive>:1:21--1:22
?n`1194 is type wildcard (_) at <interactive>:1:19--1:20
?n`1195 is type wildcard (_) at <interactive>:1:21--1:22
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
@ -99,25 +99,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) =>
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (Z ?n`1217)
• Integral (Z ?n`1218)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Z ?n`1217' is not an integral type.
• Reason: Type 'Z ?n`1218' is not an integral type.
where
?n`1217 is type wildcard (_) at <interactive>:1:8--1:9
?n`1218 is type wildcard (_) at <interactive>:1:8--1:9
(%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (?a`1220 -> ?a`1221)
• Integral (?a`1221 -> ?a`1222)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '?a`1220 -> ?a`1221' is not an integral type.
• Reason: Type '?a`1221 -> ?a`1222' is not an integral type.
where
?a`1220 is type wildcard (_) at <interactive>:1:7--1:8
?a`1221 is type wildcard (_) at <interactive>:1:12--1:13
?a`1221 is type wildcard (_) at <interactive>:1:7--1:8
?a`1222 is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
@ -129,14 +129,14 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) =>
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (?a`1220, ?a`1221)
• Integral (?a`1221, ?a`1222)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '(?a`1220, ?a`1221)' is not an integral type.
• Reason: Type '(?a`1221, ?a`1222)' is not an integral type.
where
?a`1220 is type wildcard (_) at <interactive>:1:7--1:8
?a`1221 is type wildcard (_) at <interactive>:1:10--1:11
?a`1221 is type wildcard (_) at <interactive>:1:7--1:8
?a`1222 is type wildcard (_) at <interactive>:1:10--1:11
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
@ -148,25 +148,25 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) =>
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral {x : ?a`1220, y : ?a`1221}
• Integral {x : ?a`1221, y : ?a`1222}
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type '{x : ?a`1220, y : ?a`1221}' is not an integral type.
• Reason: Type '{x : ?a`1221, y : ?a`1222}' is not an integral type.
where
?a`1220 is type wildcard (_) at <interactive>:1:11--1:12
?a`1221 is type wildcard (_) at <interactive>:1:18--1:19
?a`1221 is type wildcard (_) at <interactive>:1:11--1:12
?a`1222 is type wildcard (_) at <interactive>:1:18--1:19
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Integral (Float ?n`1220 ?n`1221)
• Integral (Float ?n`1221 ?n`1222)
arising from
use of expression (%)
at <interactive>:1:1--1:4
• Reason: Type 'Float ?n`1220 ?n`1221' is not an integral type.
• Reason: Type 'Float ?n`1221 ?n`1222' is not an integral type.
where
?n`1220 is type wildcard (_) at <interactive>:1:12--1:13
?n`1221 is type wildcard (_) at <interactive>:1:14--1:15
?n`1221 is type wildcard (_) at <interactive>:1:12--1:13
?n`1222 is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
@ -187,35 +187,35 @@ recip`{Rational} : Rational -> Rational
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field (Z ?n`1221)
• Field (Z ?n`1222)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Type 'Z' does not support field operations.
where
?n`1221 is type wildcard (_) at <interactive>:1:10--1:11
?n`1222 is type wildcard (_) at <interactive>:1:10--1:11
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field ([?n`1221]?a`1222)
• Field ([?n`1222]?a`1223)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Sequence types do not support field operations.
where
?n`1221 is type wildcard (_) at <interactive>:1:9--1:10
?a`1222 is type wildcard (_) at <interactive>:1:11--1:12
?n`1222 is type wildcard (_) at <interactive>:1:9--1:10
?a`1223 is type wildcard (_) at <interactive>:1:11--1:12
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field (?a`1221 -> ?a`1222)
• Field (?a`1222 -> ?a`1223)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Function types do not support field operations.
where
?a`1221 is type wildcard (_) at <interactive>:1:9--1:10
?a`1222 is type wildcard (_) at <interactive>:1:14--1:15
?a`1222 is type wildcard (_) at <interactive>:1:9--1:10
?a`1223 is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
@ -227,14 +227,14 @@ recip`{Rational} : Rational -> Rational
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field (?a`1221, ?a`1222)
• Field (?a`1222, ?a`1223)
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Tuple types do not support field operations.
where
?a`1221 is type wildcard (_) at <interactive>:1:9--1:10
?a`1222 is type wildcard (_) at <interactive>:1:12--1:13
?a`1222 is type wildcard (_) at <interactive>:1:9--1:10
?a`1223 is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
@ -246,14 +246,14 @@ recip`{Rational} : Rational -> Rational
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Field {x : ?a`1221, y : ?a`1222}
• Field {x : ?a`1222, y : ?a`1223}
arising from
use of expression recip
at <interactive>:1:1--1:6
• Reason: Record types do not support field operations.
where
?a`1221 is type wildcard (_) at <interactive>:1:13--1:14
?a`1222 is type wildcard (_) at <interactive>:1:20--1:21
?a`1222 is type wildcard (_) at <interactive>:1:13--1:14
?a`1223 is type wildcard (_) at <interactive>:1:20--1:21
recip`{Float _ _} : {n, m} (ValidFloat n m) =>
Float n m -> Float n m
@ -276,35 +276,35 @@ floor`{Rational} : Rational -> Integer
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (Z ?n`1225)
• Round (Z ?n`1226)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Type 'Z' does not support rounding operations.
where
?n`1225 is type wildcard (_) at <interactive>:1:10--1:11
?n`1226 is type wildcard (_) at <interactive>:1:10--1:11
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round ([?n`1225]?a`1226)
• Round ([?n`1226]?a`1227)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Sequence types do not support rounding operations.
where
?n`1225 is type wildcard (_) at <interactive>:1:9--1:10
?a`1226 is type wildcard (_) at <interactive>:1:11--1:12
?n`1226 is type wildcard (_) at <interactive>:1:9--1:10
?a`1227 is type wildcard (_) at <interactive>:1:11--1:12
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (?a`1225 -> ?a`1226)
• Round (?a`1226 -> ?a`1227)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Function types do not support rounding operations.
where
?a`1225 is type wildcard (_) at <interactive>:1:9--1:10
?a`1226 is type wildcard (_) at <interactive>:1:14--1:15
?a`1226 is type wildcard (_) at <interactive>:1:9--1:10
?a`1227 is type wildcard (_) at <interactive>:1:14--1:15
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
@ -316,14 +316,14 @@ floor`{Rational} : Rational -> Integer
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round (?a`1225, ?a`1226)
• Round (?a`1226, ?a`1227)
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Tuple types do not support rounding operations.
where
?a`1225 is type wildcard (_) at <interactive>:1:9--1:10
?a`1226 is type wildcard (_) at <interactive>:1:12--1:13
?a`1226 is type wildcard (_) at <interactive>:1:9--1:10
?a`1227 is type wildcard (_) at <interactive>:1:12--1:13
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
@ -335,14 +335,14 @@ floor`{Rational} : Rational -> Integer
[error] at <interactive>:1:1--1:6:
Unsolvable constraints:
• Round {x : ?a`1225, y : ?a`1226}
• Round {x : ?a`1226, y : ?a`1227}
arising from
use of expression floor
at <interactive>:1:1--1:6
• Reason: Record types do not support rounding operations.
where
?a`1225 is type wildcard (_) at <interactive>:1:13--1:14
?a`1226 is type wildcard (_) at <interactive>:1:20--1:21
?a`1226 is type wildcard (_) at <interactive>:1:13--1:14
?a`1227 is type wildcard (_) at <interactive>: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 +352,14 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• Eq (?a`1236 -> ?a`1237)
• Eq (?a`1237 -> ?a`1238)
arising from
use of expression (==)
at <interactive>:1:1--1:5
• Reason: Function types do not support comparisons.
where
?a`1236 is type wildcard (_) at <interactive>:1:8--1:9
?a`1237 is type wildcard (_) at <interactive>:1:13--1:14
?a`1237 is type wildcard (_) at <interactive>:1:8--1:9
?a`1238 is type wildcard (_) at <interactive>:1:13--1:14
(==)`{()} : () -> () -> Bit
(==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit
(==)`{{}} : {} -> {} -> Bit
@ -373,25 +373,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Cmp (Z ?n`1250)
• Cmp (Z ?n`1251)
arising from
use of expression (<)
at <interactive>:1:1--1:4
• Reason: Type 'Z' does not support order comparisons.
where
?n`1250 is type wildcard (_) at <interactive>:1:8--1:9
?n`1251 is type wildcard (_) at <interactive>:1:8--1:9
(<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit
[error] at <interactive>:1:1--1:4:
Unsolvable constraints:
• Cmp (?a`1253 -> ?a`1254)
• Cmp (?a`1254 -> ?a`1255)
arising from
use of expression (<)
at <interactive>:1:1--1:4
• Reason: Function types do not support order comparisons.
where
?a`1253 is type wildcard (_) at <interactive>:1:7--1:8
?a`1254 is type wildcard (_) at <interactive>:1:12--1:13
?a`1254 is type wildcard (_) at <interactive>:1:7--1:8
?a`1255 is type wildcard (_) at <interactive>:1:12--1:13
(<)`{()} : () -> () -> Bit
(<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit
(<)`{{}} : {} -> {} -> Bit
@ -426,25 +426,25 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (Z ?n`1264)
• SignedCmp (Z ?n`1265)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Z' does not support signed comparisons.
where
?n`1264 is type wildcard (_) at <interactive>:1:9--1:10
?n`1265 is type wildcard (_) at <interactive>:1:9--1:10
(<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (?a`1267 -> ?a`1268)
• SignedCmp (?a`1268 -> ?a`1269)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Function types do not support signed comparisons.
where
?a`1267 is type wildcard (_) at <interactive>:1:8--1:9
?a`1268 is type wildcard (_) at <interactive>:1:13--1:14
?a`1268 is type wildcard (_) at <interactive>:1:8--1:9
?a`1269 is type wildcard (_) at <interactive>:1:13--1:14
(<$)`{()} : () -> () -> Bit
(<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) =>
(a, b) -> (a, b) -> Bit
@ -454,24 +454,24 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer
[error] at <interactive>:1:1--1:5:
Unsolvable constraints:
• SignedCmp (Float ?n`1275 ?n`1276)
• SignedCmp (Float ?n`1276 ?n`1277)
arising from
use of expression (<$)
at <interactive>:1:1--1:5
• Reason: Type 'Float' does not support signed comparisons.
where
?n`1275 is type wildcard (_) at <interactive>:1:13--1:14
?n`1276 is type wildcard (_) at <interactive>:1:15--1:16
?n`1276 is type wildcard (_) at <interactive>:1:13--1:14
?n`1277 is type wildcard (_) at <interactive>:1:15--1:16
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1275 Bit
• Literal ?val`1276 Bit
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type 'Bit' does not support integer literals.
where
?val`1275 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?val`1276 is type argument 'val' of 'number' at <interactive>:1:1--1:7
[error] at <interactive>:1:1--1:7:
Ambiguous numeric type: type argument 'val' of 'number'
@ -484,60 +484,60 @@ number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m]
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1282 (?a`1283 -> ?a`1284)
• Literal ?val`1283 (?a`1284 -> ?a`1285)
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '?a`1283 -> ?a`1284' does not support integer literals.
• Reason: Type '?a`1284 -> ?a`1285' does not support integer literals.
where
?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1283 is type wildcard (_) at <interactive>:1:15--1:16
?a`1284 is type wildcard (_) at <interactive>:1:20--1:21
?val`1283 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1284 is type wildcard (_) at <interactive>:1:15--1:16
?a`1285 is type wildcard (_) at <interactive>:1:20--1:21
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1282 ()
• Literal ?val`1283 ()
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '()' does not support integer literals.
where
?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?val`1283 is type argument 'val' of 'number' at <interactive>:1:1--1:7
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1282 (?a`1283, ?a`1284)
• Literal ?val`1283 (?a`1284, ?a`1285)
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '(?a`1283, ?a`1284)' does not support integer literals.
• Reason: Type '(?a`1284, ?a`1285)' does not support integer literals.
where
?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1283 is type wildcard (_) at <interactive>:1:16--1:17
?a`1284 is type wildcard (_) at <interactive>:1:19--1:20
?val`1283 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1284 is type wildcard (_) at <interactive>:1:16--1:17
?a`1285 is type wildcard (_) at <interactive>:1:19--1:20
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1282 {}
• Literal ?val`1283 {}
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '{}' does not support integer literals.
where
?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?val`1283 is type argument 'val' of 'number' at <interactive>:1:1--1:7
[error] at <interactive>:1:1--1:7:
Unsolvable constraints:
• Literal ?val`1282 {x : ?a`1283, y : ?a`1284}
• Literal ?val`1283 {x : ?a`1284, y : ?a`1285}
arising from
use of literal or demoted expression
at <interactive>:1:1--1:7
• Reason: Type '{x : ?a`1283,
y : ?a`1284}' does not support integer literals.
• Reason: Type '{x : ?a`1284,
y : ?a`1285}' does not support integer literals.
where
?val`1282 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1283 is type wildcard (_) at <interactive>:1:20--1:21
?a`1284 is type wildcard (_) at <interactive>:1:27--1:28
?val`1283 is type argument 'val' of 'number' at <interactive>:1:1--1:7
?a`1284 is type wildcard (_) at <interactive>:1:20--1:21
?a`1285 is type wildcard (_) at <interactive>:1:27--1:28
number`{rep = Float _ _} : {n, m, i} (ValidFloat m i,
Literal n (Float m i)) =>
Float m i