Merge pull request formal-land#203 from foobar-land/allow-to-remove-m…

…onad-type-family

Code cleaning phantom types

src/adtConstructors.ml

@@ -88,8 +88,8 @@ type item = {
   constructor_name : Name.t;
   param_typs : Type.t list;  (** The parameters of the constructor. *)
   res_typ_params : ret_typ;
-  is_tagged : bool;
       (** The type parameters of the result type of the constructor. *)
+  is_tagged : bool;
   typ_vars : VarEnv.t;  (** The polymorphic type variables. *)
 }
 (** The constructors of an inductive type, either in a GADT or non-GADT form.

src/adtParameters.ml

@@ -47,15 +47,11 @@ let get_set_varenv (typs : t) : VarEnv.t =
 let of_ocaml : Types.type_expr list -> t Monad.t =
   Monad.List.map AdtVariable.of_ocaml
 
-let filter_params (typs : Types.type_expr list) : t Monad.t =
-  of_ocaml typs >>= fun typs ->
-  typs
-  |> Monad.List.filter (function
-       | AdtVariable.Parameter _ -> return true
-       | _ -> return false)
-
 let typ_params_ghost_marked (typs : Types.type_expr list) : t Monad.t =
-  typs |> filter_params
+  let* typs = of_ocaml typs in
+  return
+    (typs
+    |> List.filter (function AdtVariable.Parameter _ -> true | _ -> false))
 
 let equal (param1 : AdtVariable.t) (param2 : AdtVariable.t) : bool =
   match (param1, param2) with

src/pathName.ml

@@ -292,10 +292,9 @@ let is_record (path : Path.t) : bool Monad.t =
 let is_tagged_variant (path : Path.t) : bool Monad.t =
   let* env = get_env in
   match Env.find_type path env with
-  | { type_kind = Type_variant _; type_attributes; _ } ->
+  | { type_kind = Type_variant _ | Type_record _; type_attributes; _ } ->
       let* type_attributes = Attribute.of_attributes type_attributes in
       return @@ Attribute.has_tag_gadt type_attributes
-  | { type_kind = Type_record _; _ } -> return true
   | _ | (exception _) -> return false
 
 let is_native_type (path : Path.t) : bool =