New mode solver supporting multiple axes with morphisms (#1760)

* new solver

* better printing

* remove solver_mono from mode_intf

* document solver_polarized

* address some comments

* address more comments

* rename "constrain" to "zap"

* rename constrain_legacy

* make depend

* make fmt

* remove _intf.ml

* use comonadic in env

* Add Allow_Disallow, restricting types of Obj.magic

* Fix type errors discovered in previous commit

* Use Allow_disallow in more places

* show soundness of allow_disallow

* Prevent chance of forgetting the "sound" version

* minor changes

* Remove the Solver_polarized.morph type (#1)

* adjust comments

* remove address_of

* more comments

* make [log] non-optional

* better comments

* More fixes

* bind temp results

* add C.eq_morph

* set_append_changes

* compare Value with Alloc

* more comments

* warn about infinite lattices

* Small simplification to set_obj

* example of variable cycle

* say "uniqueness_op" because monotonicity

* rename set to lift

* exhaustive match

* inline unusual helper functions

* fix rebase issues

* Small simplification

* some renaming and comments

* more comment

* remove un-needed assertions.

* fix chamelon

* make fmt

* add file header comments

* exhausive match

* use ref for morph counting

* Reorder in maybe_compose

* switch from lift to map

* avoid caml_curry

* dedup in join and meet

* better error message

* fix tests

* comments

* inlining newvar_above/blow, and more uncurrying

* remove ?logging

* make sure arity is correct and avoid closure allocation

* remove morphism counting

* force inline to avoid caml_applyX

* address comments

* rename and phy eq in eq_morphvar

* Small improvement to [eq_morphvar]

* better comments about lattices

* don't hint to use exclave when useless

* fix type_argument

* comments about inner_alloc_mode

* magic for eq_obj and eq_morph

* allow/disallow for Value.List

* Add comment about actual vs expected

* comment mode_argument

* eq_morph doesn't take dst

* Magic_equal

* better comment about adjunction

* abstraction in ctype

* comment close_over and partial_apply

* fix eta expansion bug

* Alloc.Const.t is record, not tuple

* Simplify interface to [close_over]

* Generalize the type of close_over

* fixed definition of partial adjoint

* better comment about partial adjoint

* even better comments

* make fmt

* bootstrap

---------

Co-authored-by: Richard Eisenberg <reisenberg@janestreet.com>
Co-authored-by: Richard Eisenberg <rae@richarde.dev>

Author: riaqn

chamelon/compat.jst.ml

@@ -3,7 +3,7 @@ open Types
 open Mode
 
 let dummy_jkind = Jkind.value ~why:(Unknown "dummy_layout")
-let dummy_value_mode = Value.legacy
+let dummy_value_mode = Value.disallow_right Value.legacy
 let mkTvar name = Tvar { name; jkind = dummy_jkind }
 
 let mkTarrow (label, t1, t2, comm) =
@@ -16,30 +16,33 @@ let mkTexp_ident ?id:(ident_kind, uu = (Id_value, shared_many_use))
   Texp_ident (path, longident, vd, ident_kind, uu)
 
 type nonrec apply_arg = apply_arg
-type texp_apply_identifier = apply_position * Locality.t
+type texp_apply_identifier = apply_position * Locality.l
 
-let mkTexp_apply ?id:(pos, mode = (Default, Locality.legacy)) (exp, args) =
+let mkTexp_apply
+    ?id:(pos, mode = (Default, Locality.disallow_right Locality.legacy))
+    (exp, args) =
   Texp_apply (exp, args, pos, mode)
 
-type texp_tuple_identifier = string option list * Alloc.t
+type texp_tuple_identifier = string option list * Alloc.r
 
 let mkTexp_tuple ?id exps =
   let labels, alloc =
     match id with
-    | None -> (List.map (fun _ -> None) exps, Alloc.legacy)
+    | None -> (List.map (fun _ -> None) exps, Alloc.disallow_left Alloc.legacy)
     | Some id -> id
   in
   let exps = List.combine labels exps in
   Texp_tuple (exps, alloc)
 
-type texp_construct_identifier = Alloc.t option
+type texp_construct_identifier = Alloc.r option
 
-let mkTexp_construct ?id:(mode = Some Alloc.legacy) (name, desc, args) =
+let mkTexp_construct ?id:(mode = Some (Alloc.disallow_left Alloc.legacy))
+    (name, desc, args) =
   Texp_construct (name, desc, args, mode)
 
 type texp_function_param_identifier = {
   param_sort : Jkind.Sort.t;
-  param_mode : Alloc.t;
+  param_mode : Alloc.l;
   param_curry : function_curry;
   param_newtypes : (string Location.loc * Jkind.annotation option) list;
 }
@@ -54,7 +57,7 @@ type texp_function_param = {
 }
 
 type texp_function_cases_identifier = {
-  last_arg_mode : Alloc.t;
+  last_arg_mode : Alloc.l;
   last_arg_sort : Jkind.Sort.t;
   last_arg_exp_extra : exp_extra option;
   last_arg_attributes : attributes;
@@ -75,15 +78,15 @@ type texp_function = {
 }
 
 type texp_function_identifier = {
-  alloc_mode : Alloc.t;
+  alloc_mode : Alloc.r;
   ret_sort : Jkind.sort;
   region : bool;
-  ret_mode : Alloc.t;
+  ret_mode : Alloc.l;
 }
 
 let texp_function_cases_identifier_defaults =
   {
-    last_arg_mode = Alloc.legacy;
+    last_arg_mode = Alloc.disallow_right Alloc.legacy;
     last_arg_sort = Jkind.Sort.value;
     last_arg_exp_extra = None;
     last_arg_attributes = [];
@@ -92,16 +95,16 @@ let texp_function_cases_identifier_defaults =
 let texp_function_param_identifier_defaults =
   {
     param_sort = Jkind.Sort.value;
-    param_mode = Alloc.legacy;
-    param_curry = More_args { partial_mode = Alloc.legacy };
+    param_mode = Alloc.disallow_right Alloc.legacy;
+    param_curry = More_args { partial_mode = Alloc.disallow_right Alloc.legacy };
     param_newtypes = [];
   }
 
 let texp_function_defaults =
   {
-    alloc_mode = Alloc.legacy;
+    alloc_mode = Alloc.disallow_left Alloc.legacy;
     ret_sort = Jkind.Sort.value;
-    ret_mode = Alloc.legacy;
+    ret_mode = Alloc.disallow_right Alloc.legacy;
     region = false;
   }
 
@@ -249,12 +252,12 @@ let view_texp (e : expression_desc) =
   | Texp_match (e, sort, cases, partial) -> Texp_match (e, cases, partial, sort)
   | _ -> O e
 
-type tpat_var_identifier = Value.t
+type tpat_var_identifier = Value.l
 
 let mkTpat_var ?id:(mode = dummy_value_mode) (ident, name) =
   Tpat_var (ident, name, Uid.internal_not_actually_unique, mode)
 
-type tpat_alias_identifier = Value.t
+type tpat_alias_identifier = Value.l
 
 let mkTpat_alias ?id:(mode = dummy_value_mode) (p, ident, name) =
   Tpat_alias (p, ident, name, Uid.internal_not_actually_unique, mode)

native_toplevel/opttoploop.ml

@@ -348,7 +348,7 @@ let name_expression ~loc ~attrs sort exp =
   in
   let sg = [Sig_value(id, vd, Exported)] in
   let pat =
-    { pat_desc = Tpat_var(id, mknoloc name, vd.val_uid, Mode.Value.legacy);
+    { pat_desc = Tpat_var(id, mknoloc name, vd.val_uid, Mode.Value.disallow_right Mode.Value.legacy);
       pat_loc = loc;
       pat_extra = [];
       pat_type = exp.exp_type;

ocaml/.depend

@@ -1114,12 +1114,22 @@ typing/jkind.cmi : \
     parsing/jane_asttypes.cmi \
     typing/ident.cmi
 typing/mode.cmo : \
+    typing/solver_intf.cmi \
+    typing/solver.cmi \
+    typing/mode_intf.cmi \
     utils/misc.cmi \
     typing/mode.cmi
 typing/mode.cmx : \
+    typing/solver_intf.cmi \
+    typing/solver.cmx \
+    typing/mode_intf.cmi \
     utils/misc.cmx \
     typing/mode.cmi
-typing/mode.cmi :
+typing/mode.cmi : \
+    typing/mode_intf.cmi
+typing/mode_intf.cmi : \
+    typing/solver_intf.cmi \
+    typing/solver.cmi
 typing/mtype.cmo : \
     typing/types.cmi \
     typing/subst.cmi \
@@ -1507,6 +1517,16 @@ typing/signature_group.cmx : \
     typing/signature_group.cmi
 typing/signature_group.cmi : \
     typing/types.cmi
+typing/solver.cmo : \
+    typing/solver_intf.cmi \
+    typing/solver.cmi
+typing/solver.cmx : \
+    typing/solver_intf.cmi \
+    typing/solver.cmi
+typing/solver.cmi : \
+    typing/solver_intf.cmi
+typing/solver_intf.cmi : \
+    utils/misc.cmi
 typing/stypes.cmo : \
     typing/typedtree.cmi \
     typing/printtyp.cmi \

ocaml/boot/ocamlc

@@ -82,6 +82,7 @@ PARSING_CMI = \
   parsing/parsetree.cmi
 
 TYPING = \
+  typing/solver.cmo \
   typing/path.cmo \
   typing/jkind.cmo \
   typing/primitive.cmo \

ocaml/compilerlibs/Makefile.compilerlibs

@@ -68,7 +68,7 @@
        parser)))
  (library_flags -linkall)
  (modules_without_implementation
-   annot asttypes cmo_format outcometree parsetree debug_event)
+   annot asttypes cmo_format outcometree parsetree debug_event solver_intf mode_intf)
  (modules
    ;; UTILS
    config build_path_prefix_map misc identifiable numbers arg_helper clflags
@@ -91,7 +91,7 @@
    tast_iterator tast_mapper signature_group cmt_format cms_format untypeast
    includemod includemod_errorprinter
    typetexp patterns printpat parmatch stypes typedecl typeopt rec_check
-   typecore mode uniqueness_analysis
+   typecore solver_intf solver mode_intf mode uniqueness_analysis
    typeclass typemod typedecl_variance typedecl_properties
    typedecl_separability cmt2annot
    ; manual update: mli only files
@@ -317,6 +317,7 @@
     (typeopt.mli as compiler-libs/typeopt.mli)
     (rec_check.mli as compiler-libs/rec_check.mli)
     (typecore.mli as compiler-libs/typecore.mli)
+    (solver.mli as compiler-libs/solver.mli)
     (mode.mli as compiler-libs/mode.mli)
     (uniqueness_analysis.mli as compiler-libs/uniqueness_analysis.mli)
     (typeclass.mli as compiler-libs/typeclass.mli)