Make Sail more flexible with existentials in union types

Issues came up with Christophers translation of hand-written ARM into
Sail2 where we were being overly pedantic about the exact position of
existential quantifiers in constructors with multiple arguments. This
commit generalises unify_typ and type_coercion_unify to be more
flexible and support this. Should think at some point if unify_typ can
be generalised further.

This fix should fix the decode side of things, but may be some issues
with the executes that still need looking into when existentials and
multiple argument constructors are mixed.

7 files changed, 228 insertions, 0 deletions

diff --git a/test/typecheck/pass/existential_ast.sail b/test/typecheck/pass/existential_ast.sail
new file mode 100644
index 00000000..37cf2378
--- /dev/null
+++ b/test/typecheck/pass/existential_ast.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v1.expect b/test/typecheck/pass/existential_ast/v1.expect
new file mode 100644
index 00000000..f743abb6
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v1.sail]:46:7-21
+46 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v1.sail b/test/typecheck/pass/existential_ast/v1.sail
new file mode 100644
index 00000000..935313f7
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v1.sail
@@ -0,0 +1,47 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b01);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v2.expect b/test/typecheck/pass/existential_ast/v2.expect
new file mode 100644
index 00000000..20738cd8
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.expect
@@ -0,0 +1,6 @@
+Type error:
+[existential_ast/v2.sail]:39:7-21
+39 |  Some(Ctor2(y, x, c))
+   |       ^------------^
+   | No valid casts resulted in unification
+   | 
diff --git a/test/typecheck/pass/existential_ast/v2.sail b/test/typecheck/pass/existential_ast/v2.sail
new file mode 100644
index 00000000..fd272dbb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v2.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 30)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
new file mode 100644
index 00000000..1b6239bb
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -0,0 +1,7 @@
+Type error:
+[existential_ast/v3.sail]:26:7-21
+26 |  Some(Ctor1(a, x, c))
+   |       ^------------^
+   | Could not resolve quantifiers for Ctor1
+   | * datasize('ex59#)
+   | 
diff --git a/test/typecheck/pass/existential_ast/v3.sail b/test/typecheck/pass/existential_ast/v3.sail
new file mode 100644
index 00000000..1bacbf80
--- /dev/null
+++ b/test/typecheck/pass/existential_ast/v3.sail
@@ -0,0 +1,54 @@
+default Order dec
+
+$include <prelude.sail>
+
+type datasize('n: Int) -> Bool = 'n in {32, 64}
+
+type regno = range(0, 31)
+
+union ast = {
+  Ctor1 : {'d, datasize('d). (bits(4), int('d), bits(4))},
+  Ctor2 : {'d, datasize('d). (regno, int('d), bits(4))}
+}
+
+val decode : bits(16) -> option(ast)
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000110) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+  y : {'d, datasize('d). (bits(4), int('d), bits(4))} = (a, x, c);
+
+  Some(Ctor1(y))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  x : {|16, 32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000101) = {
+  let x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor1(a, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  let y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a @ 0b0);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
+
+function clause decode(a : bits(4) @ b : bits(1) @ c : bits(4) @ 0b0000111) = {
+  y = unsigned(a);
+  x : {|32, 64|} = if b == 0b0 then 32 else 64;
+
+  Some(Ctor2(y, x, c))
+}
\ No newline at end of file