TC: Simplify synonym expansion

This commit removes checking constraints from synonym expansion, so the type:
```
type foo('n), 'n >= 32 = bar('n)
```
when appearing as `foo(N)` will just expand directly to `bar(N)` without checking
`N >= 32`.

This is possible because the well-formedness check already checks this, i.e.
`foo(N)` is well-formed only if `N >= 32` holds, so we don't need to check
again when we do the expansion.

This fixes a bug where synonym expansion wasn't handling existentials correctly.

src/lib/type_env.ml

@@ -753,48 +753,32 @@ module Well_formedness = struct
 end
 
 let mk_synonym typq typ_arg =
-  let kopts, ncs = quant_split typq in
+  let kopts, _ = quant_split typq in
   let kopts = List.map (fun kopt -> (kopt, fresh_existential (kopt_loc kopt) (unaux_kind (kopt_kind kopt)))) kopts in
-  let ncs =
-    List.map
-      (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts)
-      ncs
-  in
   let typ_arg =
     List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts
   in
   let kopts = List.map snd kopts in
   let rec subst_args env l kopts args =
     match (kopts, args) with
     | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        ( typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
-          List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
-        )
+        let typ_arg = subst_args env l kopts args in
+        typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg
     | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        (typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs)
+        let typ_arg = subst_args env l kopts args in
+        typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg
     | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
-        let typ_arg, ncs = subst_args env l kopts args in
-        (typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs)
-    | [], [] -> (typ_arg, ncs)
+        let typ_arg = subst_args env l kopts args in
+        typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg
+    | [], [] -> typ_arg
     | kopts, args ->
         typ_error l
           ("Synonym applied to bad arguments "
           ^ Util.string_of_list ", " string_of_kinded_id kopts
           ^ Util.string_of_list ", " string_of_typ_arg args
           )
   in
-  fun l env args ->
-    let typ_arg, ncs = subst_args env l kopts args in
-    if match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false then typ_arg
-    else
-      typ_error l
-        ("Could not prove constraints "
-        ^ string_of_list ", " string_of_n_constraint ncs
-        ^ " in type synonym " ^ string_of_typ_arg typ_arg ^ " with "
-        ^ Util.string_of_list ", " string_of_n_constraint (get_constraints env)
-        )
+  fun l env args -> subst_args env l kopts args
 
 let get_typ_synonym id env =
   match Option.map (get_item (id_loc id) env) (Bindings.find_opt id env.global.synonyms) with

test/lem/run_tests.py

@@ -28,7 +28,6 @@
     'float_prelude',
     # No possible configuration
     'config_mismatch',
-    'config_bits_types',
 }
 skip_tests_mwords = {
     'phantom_option',
@@ -66,7 +65,6 @@
     'float_prelude',
     # No possible configuration
     'config_mismatch',
-    'config_bits_types',
 }
 
 print('Sail is {}'.format(sail))

test/typecheck/fail/negative_bits_union.expect

@@ -1,5 +1,17 @@
 Type error:
-fail/negative_bits_union.sail:6.10-22:
-6 |    Bar : bits('n - 2),
-  |          ^----------^
-  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with 
+fail/negative_bits_union.sail:5.0-7.1:
+5 |union Foo('n: Int) = {
+  |^---------------------
+7 |}
+  |^
+  | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+  | 
+  | Caused by fail/negative_bits_union.sail:6.10-22:
+  | 6 |    Bar : bits('n - 2),
+  |   |          ^----------^
+  |   | Well-formedness check failed for type
+  |   | 
+  |   | Caused by fail/negative_bits_union.sail:6.10-14:
+  |   | 6 |    Bar : bits('n - 2),
+  |   |   |          ^--^
+  |   |   | Could not prove ('n - 2) >= 0 for type constructor bits

test/typecheck/fail/negative_bits_union2.expect

@@ -1,5 +1,17 @@
 Type error:
-fail/negative_bits_union2.sail:8.10-22:
-8 |    Bar : bits('n - 2),
-  |          ^----------^
-  | Could not prove constraints ('n - 2) >= 0 in type synonym bitvector(('n - 2)) with 
+fail/negative_bits_union2.sail:7.0-10.1:
+7  |union Foo('n: Int) = {
+   |^---------------------
+10 |}
+   |^
+   | Types are not well-formed within this type definition. Note that recursive types are forbidden.
+   | 
+   | Caused by fail/negative_bits_union2.sail:8.10-22:
+   | 8 |    Bar : bits('n - 2),
+   |   |          ^----------^
+   |   | Well-formedness check failed for type
+   |   | 
+   |   | Caused by fail/negative_bits_union2.sail:8.10-14:
+   |   | 8 |    Bar : bits('n - 2),
+   |   |   |          ^--^
+   |   |   | Could not prove ('n - 2) >= 0 for type constructor bits