Remove unused equality check and change comments.

client/FTypeChecker.ml

@@ -204,86 +204,13 @@ let rec as_forall ty =
 
 (* -------------------------------------------------------------------------- *)
 
-(* [equal1] groups the easy cases of the type equality test. It does not
-   accept arguments of the form [TyMu]. It expects a self parameter [equal]
-   that is used to compare the children of the two root nodes. *)
-
-let pointwise equal tys1 tys2 =
-  try
-    List.for_all2 equal tys1 tys2
-  with Invalid_argument _ ->
-    (* Catching [Invalid_argument] is bad style, but saves a couple calls
-       to [List.length]. A cleaner approach would be to use arrays instead
-       of lists. *)
-    false
-
-let equal1 equal ty1 ty2 =
-  match ty1, ty2 with
-  | TyMu _, _
-  | _, TyMu _ ->
-      assert false
-  | TyVar x1, TyVar x2 ->
-      Int.equal x1 x2
-  | TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b)
-  | TyEq (ty1a, ty1b), TyEq (ty2a, ty2b) ->
-      equal ty1a ty2a && equal ty1b ty2b
-  | TyForall ((), ty1), TyForall ((), ty2) ->
-      equal ty1 ty2
-  | TyProduct tys1, TyProduct tys2 ->
-      pointwise equal tys1 tys2
-  | TyConstr (Datatype.Type tyconstr1, tys1),
-    TyConstr (Datatype.Type tyconstr2, tys2) ->
-      String.equal tyconstr1 tyconstr2 &&
-      pointwise equal tys1 tys2
-  | (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _ | TyEq _),
-    _ ->
-      false
-
-(* -------------------------------------------------------------------------- *)
-
-(* An unsound approximation of the equality test. (Now unused.) *)
-
-(* Comparing two [TyMu] types simply by comparing their bodies would be
-   correct, but incomplete: some types that are equal would be considered
-   different. *)
-
-(* Naively unfolding every [TyMu] type is sound and complete, but leads to
-   potential non-termination. The following code avoids non-termination by
-   imposing a budget limit. This makes this equality test unsound: two types
-   may be considered equal when they are in fact different. *)
-
-let rec equal budget ty1 ty2 =
-  match ty1, ty2 with
-  | (TyMu _ as ty1), ty2
-  | ty2, (TyMu _ as ty1) ->
-      budget = 0 || equal (budget - 1) (unfold ty1) ty2
-  | _, _ ->
-      equal1 (equal budget) ty1 ty2
-
-let budget =
-  4
-
-let _unsound_equal ty1 ty2 =
-  equal budget ty1 ty2
-
-(* -------------------------------------------------------------------------- *)
-
 (* A sound approximation of the equality test. *)
 
 (* The System F types produced by an ML type inference algorithm cannot
    contain [TyForall] under [TyMu]. In this restricted setting, deciding
-   type equality is relatively easy. We proceed in two layers, as follows:
-
-   - Initially, we perform a normal (structural) equality test, going
-     down under [TyForall] constructors if necessary. As soon as we
-     hit a [TyMu] constructor on either side, we switch to the lower
-     layer:
-
-   - In the lower layer, we know that we cannot hit a [TyForall]
-     constructor (if we do, we report that the types differ). We
-     map each type (separately) to a graph of unification variables
-     (where every variable has rigid structure), then we check that
-     the two graphs can be unified. *)
+   type equality is relatively easy. We map each type to a graph of
+   unification variables (where every variable has rigid structure),
+   then we check that the two graphs can be unified. *)
 
 exception Clash =
   Structure.Iter2