Add comments; simplify Aliases API a bit

Author: lukemaurer

middle_end/flambda/types/env/aliases.ml

@@ -807,21 +807,20 @@ let choose_canonical_element_to_be_demoted t ~canonical_element1
 type add_result = {
   t : t;
   canonical_element : Simple.t;
-  alias_of_demoted_element : Simple.t;
-  coercion_from_alias_of_demoted_to_canonical : Coercion.t;
+  demoted_alias : Simple.t;
 }
 
-let invariant_add_result ~original_t { canonical_element; alias_of_demoted_element; t; coercion_from_alias_of_demoted_to_canonical = _; } =
+let invariant_add_result ~original_t { canonical_element; demoted_alias; t; } =
   if !Clflags.flambda_invariant_checks then begin
     invariant t;
-    if not (Simple.equal canonical_element alias_of_demoted_element) then begin
+    if not (Simple.equal canonical_element demoted_alias) then begin
       if not (defined_earlier t canonical_element
-                ~than:alias_of_demoted_element) then begin
+                ~than:demoted_alias) then begin
         Misc.fatal_errorf "Canonical element %a should be defined earlier \
                            than %a after alias addition.@ Original alias tracker:@ %a@ \
                            Resulting alias tracker:@ %a"
           Simple.print canonical_element
-          Simple.print alias_of_demoted_element
+          Simple.print demoted_alias
           print original_t
           print t
       end
@@ -833,9 +832,9 @@ let add_alias t ~element1 ~coercion_from_element2_to_element1 ~element2 =
         ~coercion_from_element1_to_canonical_element1
         ~coercion_from_element2_to_canonical_element2
         ~coercion_from_canonical_element2_to_canonical_element1 =
-    let canonical_element, to_be_demoted, alias_of_demoted_element,
-        coercion_from_demoted_to_canonical,
-        coercion_from_alias_of_demoted_to_demoted = 
+    let canonical_element, demoted_canonical, demoted_alias,
+        coercion_from_demoted_canonical_to_canonical,
+        coercion_from_demoted_alias_to_demoted_canonical = 
       let which_element =
         choose_canonical_element_to_be_demoted t
           ~canonical_element1 ~canonical_element2
@@ -858,19 +857,22 @@ let add_alias t ~element1 ~coercion_from_element2_to_element1 ~element2 =
       add_alias_between_canonical_elements
         t
         ~canonical_element
-        ~coercion_to_canonical:coercion_from_demoted_to_canonical
-        ~to_be_demoted
+        ~coercion_to_canonical:coercion_from_demoted_canonical_to_canonical
+        ~to_be_demoted:demoted_canonical
     in
-    let coercion_from_alias_of_demoted_to_canonical =
+    let coercion_from_demoted_alias_to_canonical =
       Coercion.compose_exn
-        coercion_from_alias_of_demoted_to_demoted
-        ~then_:coercion_from_demoted_to_canonical
+        coercion_from_demoted_alias_to_demoted_canonical
+        ~then_:coercion_from_demoted_canonical_to_canonical
+    in
+    let demoted_alias =
+      Simple.with_coercion demoted_alias
+        coercion_from_demoted_alias_to_canonical
     in
     Or_bottom.map t ~f:(fun t ->
       { t;
         canonical_element;
-        alias_of_demoted_element;
-        coercion_from_alias_of_demoted_to_canonical;
+        demoted_alias;
       })
   in
   match canonical t element1, canonical t element2 with

middle_end/flambda/types/env/aliases.mli

@@ -14,7 +14,32 @@
 
 (** Union-find-like structure for keeping track of equivalence classes,
     used for alias resolution in the typing environment, with support for
-    associating orderings to aliases of canonical elements. *)
+    associating orderings to aliases of canonical elements.
+
+    The concept of "alias" needs to be broadened where coercions are involved.
+    A coercion is a sort of fudge factor---if [x] is equal to [(coerce y c)],
+    then [x] and [y] are {i essentially} equal, close enough that we want to
+    think of [y] as an alias of [x].
+
+    If the words "fudge factor" sound like we're being imprecise, happily we can
+    be precise about our imprecision. Let [x ~ y] mean [x] and [y] are _equal up
+    to coercion_, which is to say, there exists a coercion [c] such that [x =
+    (coerce y c)]. Coercions form a _groupoid_, meaning they have just the
+    right properties to let [~] be an equivalence relation:
+
+      + There is an identity coercion, so [x = (coerce x id)], meaning [x ~ x].
+      + Coercions can be inverted, so if [x ~ y], meaning [x = (coerce y c)],
+        then (writing [c^-1] for the inverse) we have [y = (coerce x c^-1)],
+        meaning [y ~ x].
+      + Coercions can be composed, so if [x ~ y] and [y ~ z], meaning
+        [x = (coerce y c_xy)] and [y = (coerce z c_yz)], then (using [>>] as
+        the composition operator) we have [x = (coerce z (c_xy >> c_yz))] and
+        [x ~ z].
+
+    Therefore we can safely redefine "alias" to mean [x ~ y] rather than [x =
+    y], and the coercions keep track of the precise sense in which [x] and [y]
+    are "equal enough." In particular, this module keeps track of aliases in
+    this looser sense. *)
 
 [@@@ocaml.warning "+a-4-30-40-41-42"]
 
@@ -28,11 +53,20 @@ val invariant : t -> unit
 
 val empty : t
 
+(** The result of calling [add] to state that two [Simple.t]s are now
+    aliases. *)
 type add_result = private {
   t : t;
-  canonical_element : Simple.t; (* has no coercion *)
-  alias_of_demoted_element : Simple.t; (* has no coercion *)
-  coercion_from_alias_of_demoted_to_canonical : Coercion.t;
+  (** The new state of the alias tracker. *)
+  canonical_element : Simple.t;
+  (** The canonical element of the combined equivalence class. In the type
+      environment, this will be the name (if it is a name) that is assigned a
+      concrete type. Does not carry a coercion. *)
+  demoted_alias: Simple.t;
+  (** Whichever argument to [add] had its equivalence class consumed and its
+      canonical element demoted to an alias. It is this name that needs its type
+      to change to record the new canonical element. Its coercion has been
+      adjusted so that it is properly an alias of [canonical_element]. *)
 }
 
 val add

middle_end/flambda/types/env/typing_env.rec.ml

@@ -1034,13 +1034,11 @@ and add_equation t name ty =
         let ty = Type_grammar.bottom_like ty in
         aliases, lhs, t, ty
       | Ok { canonical_element;
-             alias_of_demoted_element;
-             t = aliases;
-             coercion_from_alias_of_demoted_to_canonical; } ->
-        let lhs =
-          Simple.with_coercion alias_of_demoted_element
-            coercion_from_alias_of_demoted_to_canonical
-        in
+             demoted_alias;
+             t = aliases; } ->
+        (* We need to change the demoted alias's type to point to the new
+           canonical element. *)
+        let lhs = demoted_alias in
         let ty =
           Type_grammar.alias_type_of kind canonical_element
         in