Add well-formedness check for type schemes in valspecs.

Fixes #47.
Also adjust the nexp substitution so that the error message points to a
useful location, and replace the empty environment with the initial
environment in a few functions that do type checking to ensure that the
prover is set up (which may be needed for the wf check).

10 files changed, 42 insertions, 15 deletions

diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index acadd4e2..89ab2910 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex172# : Int), true. vector(('M * 'ex172#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 7bb8a4ab..56b89364 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex196#)
+   | * datasize('ex248#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 4b9bd7cc..346b7b75 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(33), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex205# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex206# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex210# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 52eb2f13..7f18c94e 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
+   | (int(31), int('ex210#)) is not a subtype of (int('ex205#), int('ex206#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex205# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex154# bound here
+   |    | 'ex206# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex158# bound here
+   |    | 'ex210# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 0e43cd52..585cf2c6 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex249# & ('ex249# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 011ecbdf..50bd530d 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 3)
+   |    * (0 <= 'ex166# & ('ex166# + 1) <= 3)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 3)
+   |    * (0 <= 'ex169# & ('ex169# + 1) <= 3)
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 9a34f688..27b05208 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex115# & ('ex115# + 1) <= 4)
+   |    * (0 <= 'ex166# & ('ex166# + 1) <= 4)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex118# & ('ex118# + 1) <= 4)
+   |    * (0 <= 'ex169# & ('ex169# + 1) <= 4)
    | 
diff --git a/test/typecheck/pass/wf_specs.sail b/test/typecheck/pass/wf_specs.sail
new file mode 100644
index 00000000..2bacf7e0
--- /dev/null
+++ b/test/typecheck/pass/wf_specs.sail
@@ -0,0 +1,11 @@
+/* Example from https://github.com/rems-project/sail/issues/47 where a variable
+   name is mistakenly used at the type level, which wasn't caught before due to
+   the lack of a well-formedness check on specs.  This is the corrected version.
+   */
+
+default Order dec
+$include <prelude.sail>
+
+let 'THIRTY_TWO : atom(32) = 32
+
+val f : bits(32) -> bits('THIRTY_TWO)
diff --git a/test/typecheck/pass/wf_specs/wf_specs.expect b/test/typecheck/pass/wf_specs/wf_specs.expect
new file mode 100644
index 00000000..88844e18
--- /dev/null
+++ b/test/typecheck/pass/wf_specs/wf_specs.expect
@@ -0,0 +1,6 @@
+Type error:
+[wf_specs/wf_specs.sail]:10:25-35
+10 |val f : bits(32) -> bits(THIRTY_TWO)
+   |                         ^--------^
+   | Undefined synonym THIRTY_TWO
+   | 
diff --git a/test/typecheck/pass/wf_specs/wf_specs.sail b/test/typecheck/pass/wf_specs/wf_specs.sail
new file mode 100644
index 00000000..bb108ee3
--- /dev/null
+++ b/test/typecheck/pass/wf_specs/wf_specs.sail
@@ -0,0 +1,10 @@
+/* Example from https://github.com/rems-project/sail/issues/47 where a variable
+   name is mistakenly used at the type level, which wasn't caught before due to
+   the lack of a well-formedness check on specs. */
+
+default Order dec
+$include <prelude.sail>
+
+let THIRTY_TWO : atom(32) = 32
+
+val f : bits(32) -> bits(THIRTY_TWO)