Apply 1 suggestion(s) to 1 file(s)

These comments should appear in F.mli too, but I'm waiting for feedbacks before I copy-paste them.

-   we must be able to display them as part of a type error message. *)
+   we must be able to display them as part of a type error message.
+   We use a restricted version of this system where a recursive cycle cannot
+   go through a universal quantifier. *)

+
+   [Use] is a construct that "opens" a type equality. That is, it allows to
+   reason in a context a context where two types are assumed to be equals.
+   It is supposed to be used with a [Refl] as a left-hand side :

       str "The variable %s is unbound." x
+  | UnboundTypeVariable x ->
+      str "Scope error." ++
+      str "The variable %d is unbound." x

+   [store] and [tyvars] *)
+type consistency =
+  | Consistent of store * tyvars
+  | Inconsistent

 
-(* This function assumes that no occurence of forall quantification
-   appear under a mu-type. *)
+(* This function assumes no universal quantification inside a μ-type.

+   - decompose an equality assumption
+   - perform an equality check
+   Since these two operations can be break down into similar parts, we
+   factorize the code, by passing a [mode] argument to the functions. *)

-let (--) ty1 ty2 env : unit =
-  if not (equal Check env ty1 ty2) then
+(* Re-package the type equality test as a type equality check. *)
+let equal env ty1 ty2 : unit =

+                typeof { env with uf_state = Inconsistent } u
+           | ty ->
+              raise (TypeError (NotAnEqual ty))
+         end

+let check
+      (env : F.nominal_datatype_env) (t : F.nominal_term)
+      (on_error : FTypeChecker.type_error -> unit)
+      (on_ok : unit -> unit)

+
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+   equality checking, we do not permit recursive cycles through universal
+   quantifiers, that is, we don't allow ∀ under μ.

+           ... (* here ty1 and ty2 are assumed to be equal *)
+
+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce

+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce
+   a construct [Absurd], that can be used as a placeholder in pieces of code
+   where it happens and that are thus unreachable. *)

       str "Type error." ++
-      str "The context is not absurd"
+      str "The typing context was expected to be inconsistent but is not." ++
+      str "This means that two types were assumed to be different but are not."

-  (* Is set to false when an inconsistent equation is introduced in the
-     environment. It is useful while typechecking pattern-matching. *)
-  consistent: bool;
+  (* We keep trace of wheter or not the typing equations is consistent *)

-  store = UF.new_store();
-  tyvars = [];
-  consistent = true;
+  equations_env = Equations { store = UF.new_store() ; tyvars = [] };

+(* This function assumes no universal quantification inside a μ-type, because
+   it would be difficult to check type equality otherwise. That is why we need
+   a boolean [inside_mu] during the traversal of the type to remember wether
+   or not we are under a μ-quantification *)

+   - decompose an equality assumption
+   - perform an equality check
+   Since these two operations can be break down into similar parts, we
+   factorize the code, by passing a [mode] argument to the functions. *)

-(* Re-package the type equality test as a type equality check. *)
+(* Re-package the type equality assumption as a type consistency check. *)
+let consistent env ty1 ty2 : bool =
+  unify_types Input env ty1 ty2

+       | Equations { store ; tyvars } ->
+          let store_copy = UF.copy store in
+          let equations_env = Equations { store = store_copy; tyvars } in
+          let env = { env with equations_env } in