Add tests for pattern-matching.

client/test/TestF.ml

@@ -83,7 +83,7 @@ let let_prod =
     (app (var p) (tuple []))
     (app (var f) (var x))
 
-(* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *)
+(* Λαβ. λx:{α*β}. match x with (_, y) -> y end *)
 let match_with_prod =
   let alpha, beta = 1, 0 in
     tyabs alpha @@
@@ -93,6 +93,15 @@ let match_with_prod =
         (ptuple [ pwildcard ; pvar "y" ]) , var"y"
       ]
 
+(* Λα. λx:{α*α}. match x with (y, y) -> y end *)
+let match_variable_bound_twice =
+  let alpha = 0 in
+    tyabs alpha @@
+    abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar alpha ]) @@
+    match_ (F.TyVar alpha) (var "x") [
+        (ptuple [ pvar "y" ; pvar "y" ]) , var"y"
+      ]
+
 (* option *)
 let option_env =
   let option_typedecl =
@@ -157,6 +166,25 @@ let match_none =
     (some_pattern , unit);
   ]
 
+(* Λα. λx:α.
+   match (x,Some x) with
+   | (y, None)  -> y
+   | (y,Some y) -> y
+   end
+ *)
+let match_variable_bound_twice_under_tuple =
+  let alpha = 0 in
+  let none_label = Datatype.Label "None" in
+  let some_label = Datatype.Label "Some" in
+  let datatype = Datatype.Type "option", [ F.TyVar alpha ] in
+  tyabs alpha @@
+  abs "x" (F.TyVar alpha) @@
+  match_ (F.TyVar alpha)
+    (tuple [var "x"; variant some_label datatype (var "x")]) [
+      (ptuple [ pvar "y" ; pvariant none_label datatype unit_pattern ]) , var"y" ;
+      (ptuple [ pvar "y" ; pvariant some_label datatype (pvar "y") ]) , var"y"
+      ]
+
 (* ( refl_{} : Eq(∀α.{} , {}) ) *)
 let type_eq =
   let alpha = 0 in
@@ -645,12 +673,17 @@ let test_suite =
     "test F ast",
     [ test_ok_from_ast "let prod" Datatype.Env.empty let_prod;
       test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
+      test_type_error "match variable bound twice" Datatype.Env.empty
+        match_variable_bound_twice;
       test_ok_from_ast "unit" option_env unit;
       test_ok_from_ast "none" option_env none;
       test_ok_from_ast "some" option_env some;
       test_ok_from_ast "match none" option_env match_none;
+      test_type_error "match deep variable bound twice" option_env
+        match_variable_bound_twice_under_tuple;
       test_type_error "type equality" Datatype.Env.empty type_eq;
-      test_ok_from_ast "introduce type equality" Datatype.Env.empty introduce_type_eq;
+      test_ok_from_ast "introduce type equality" Datatype.Env.empty
+        introduce_type_eq;
       test_ok_from_ast "symmetry" Datatype.Env.empty sym;
       test_ok_from_ast "transitivity" Datatype.Env.empty trans;
       test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall;