Improve destructuring existential types

Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:

val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}

function test (() : unit) -> unit = {
  let matrix as vector('width, _, 'height) = mk_square ();
  _prove(constraint('width = 'height));
  ()
}

where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax

let vector as 'length  = ...
or even
let 'vector = ...

still works under this new scheme in a uniform way, so this is backwards compatible

The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.

3 files changed, 19 insertions, 2 deletions

diff --git a/test/typecheck/pass/bind_typ_var.sail b/test/typecheck/pass/bind_typ_var.sail
new file mode 100644
index 00000000..c442d6a8
--- /dev/null
+++ b/test/typecheck/pass/bind_typ_var.sail
@@ -0,0 +1,17 @@
+
+val mk_vector : unit -> {'n, 'n in {32, 64}. vector('n, dec, bit)}
+
+val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
+
+val test : unit -> unit
+
+function test () = {
+  let v as vector('len, _, _) = mk_vector ();
+  // could still be
+  let v2 as 'len2 = mk_vector ();
+  let matrix as vector('width, _, 'height) = mk_square ();
+  _prove(constraint('width = 'height));
+  _prove(constraint('len = 32 | 'len = 64));
+  _prove(constraint('len2 = 32 | 'len2 = 64));
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 67355f59..62788484 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -3,4 +3,4 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23,
 let _ = test(32)
 
 Tried performing type coercion on 32
-Failed because atom<32> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
+Failed because atom<32> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index fb31fbed..1b9bb23d 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -3,4 +3,4 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23,
 let _ = test(64)
 
 Tried performing type coercion on 64
-Failed because atom<64> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
+Failed because atom<64> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64)