Consider the following program:
f : {n} (n < 1) => [n]
f = []
This uses the (<) constraint, which is defined as a type synonym:
|
/** |
|
* Assert that the first numeric type is less than the second. |
|
*/ |
|
type constraint i < j = j >= i + 1 |
If you compile the program with Cryptol 3.5.0 and print the typechecked code using :set debug=on, it will preserve the (<) type synonym:
$ ~/Software/cryptol-3.5.0/bin/cryptol -c ":set debug=on" -c ":l Bug.cry"
Loading module Cryptol
Loading module Cryptol
Loading module Main
module Main
/* Not recursive */
Main::f : {n} (n < 1) => [n]
Main::f = \{n} (n < 1) -> [] : Bit
If you do the same thing with a nightly Cryptol (at commit c4da478), on the other hand, the type synonym will not be preserved:
$ cabal -v0 run exe:cryptol -- -c ":set debug=on" -c ":l Bug.cry"
Loading module Cryptol
Loading module Cryptol
Loading module Main
module Main
/* Not recursive */
Main::f : {n} (1 >= 1 + n) => [n]
Main::f = \{n} (1 >= 1 + n) -> [] : Bit
This is not wrong necessarily, but it is somewhat unfortunate, as the user-written type synonym is not preserved through to the typechecked AST. This can cause issues for downstream projects that search for type synonyms when determining how to post-process typechecked Cryptol code.
Consider the following program:
This uses the
(<)constraint, which is defined as a type synonym:cryptol/lib/Cryptol.cry
Lines 159 to 162 in c4da478
If you compile the program with Cryptol 3.5.0 and print the typechecked code using
:set debug=on, it will preserve the(<)type synonym:If you do the same thing with a nightly Cryptol (at commit c4da478), on the other hand, the type synonym will not be preserved:
This is not wrong necessarily, but it is somewhat unfortunate, as the user-written type synonym is not preserved through to the typechecked AST. This can cause issues for downstream projects that search for type synonyms when determining how to post-process typechecked Cryptol code.