From 4d44a0b0f8508cb7f58fd14057eab1060579390b Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Wed, 2 Dec 2020 18:01:39 +0100
Subject: [PATCH 1/7] Remove TypeReplacement exception in Subst

Use an explicit `'a or_replaced` type to better track where this need to
be handled.
---
 src/xref2/subst.ml | 129 +++++++++++++++++++++++++--------------------
 1 file changed, 71 insertions(+), 58 deletions(-)

diff --git a/src/xref2/subst.ml b/src/xref2/subst.ml
index dcf053654f..6f647a30df 100644
--- a/src/xref2/subst.ml
+++ b/src/xref2/subst.ml
@@ -1,8 +1,13 @@
-exception TypeReplacement of Component.TypeExpr.t
-
 exception Invalidated
+
 exception MTOInvalidated
 
+type 'a or_replaced = Not_replaced of 'a | Replaced of Component.TypeExpr.t
+
+let map_replaced f = function
+  | Not_replaced p -> Not_replaced (f p)
+  | Replaced _ as r -> r
+
 open Component
 open Substitution
 
@@ -201,43 +206,51 @@ and module_type_path : t -> Cpath.module_type -> Cpath.module_type =
   | `Dot (p, n) -> `Dot (module_path s p, n)
   | `ModuleType (p', str) -> `ModuleType (resolved_parent_path s p', str)
 
-and resolved_type_path : t -> Cpath.Resolved.type_ -> Cpath.Resolved.type_ =
+and resolved_type_path :
+    t -> Cpath.Resolved.type_ -> Cpath.Resolved.type_ or_replaced =
  fun s p ->
   match p with
   | `Local id -> (
       if PathTypeMap.mem id s.type_replacement then
-        raise (TypeReplacement (PathTypeMap.find id s.type_replacement));
-      match try Some (PathTypeMap.find id s.type_) with Not_found -> None with
-      | Some (`Prefixed (_p, rp)) -> rp
-      | Some (`Renamed x) -> `Local x
-      | None -> `Local id )
-  | `Identifier _ -> p
-  | `Substituted p -> `Substituted (resolved_type_path s p)
-  | `Type (p, n) -> `Type (resolved_parent_path s p, n)
-  | `ClassType (p, n) -> `ClassType (resolved_parent_path s p, n)
-  | `Class (p, n) -> `Class (resolved_parent_path s p, n)
-
-and type_path : t -> Cpath.type_ -> Cpath.type_ =
+        Replaced (PathTypeMap.find id s.type_replacement)
+      else
+        match
+          try Some (PathTypeMap.find id s.type_) with Not_found -> None
+        with
+        | Some (`Prefixed (_p, rp)) -> Not_replaced rp
+        | Some (`Renamed x) -> Not_replaced (`Local x)
+        | None -> Not_replaced (`Local id) )
+  | `Identifier _ -> Not_replaced p
+  | `Substituted p ->
+      resolved_type_path s p |> map_replaced (fun p -> `Substituted p)
+  | `Type (p, n) -> Not_replaced (`Type (resolved_parent_path s p, n))
+  | `ClassType (p, n) -> Not_replaced (`ClassType (resolved_parent_path s p, n))
+  | `Class (p, n) -> Not_replaced (`Class (resolved_parent_path s p, n))
+
+and type_path : t -> Cpath.type_ -> Cpath.type_ or_replaced =
  fun s p ->
   match p with
   | `Resolved r -> (
-      try `Resolved (resolved_type_path s r)
+      try resolved_type_path s r |> map_replaced (fun r -> `Resolved r)
       with Invalidated ->
         let path' = Cpath.unresolve_resolved_type_path r in
         type_path s (`Substituted path') )
-  | `Substituted p -> `Substituted (type_path s p)
+  | `Substituted p -> type_path s p |> map_replaced (fun r -> `Substituted r)
   | `Local (id, b) -> (
       if PathTypeMap.mem id s.type_replacement then
-        raise (TypeReplacement (PathTypeMap.find id s.type_replacement));
-      match try Some (PathTypeMap.find id s.type_) with Not_found -> None with
-      | Some (`Prefixed (p, _rp)) -> p
-      | Some (`Renamed x) -> `Local (x, b)
-      | None -> `Local (id, b) )
-  | `Identifier _ -> p
-  | `Dot (p, n) -> `Dot (module_path s p, n)
-  | `Type (p, n) -> `Type (resolved_parent_path s p, n)
-  | `Class (p, n) -> `Class (resolved_parent_path s p, n)
-  | `ClassType (p, n) -> `ClassType (resolved_parent_path s p, n)
+        Replaced (PathTypeMap.find id s.type_replacement)
+      else
+        match
+          try Some (PathTypeMap.find id s.type_) with Not_found -> None
+        with
+        | Some (`Prefixed (p, _rp)) -> Not_replaced p
+        | Some (`Renamed x) -> Not_replaced (`Local (x, b))
+        | None -> Not_replaced (`Local (id, b)) )
+  | `Identifier _ -> Not_replaced p
+  | `Dot (p, n) -> Not_replaced (`Dot (module_path s p, n))
+  | `Type (p, n) -> Not_replaced (`Type (resolved_parent_path s p, n))
+  | `Class (p, n) -> Not_replaced (`Class (resolved_parent_path s p, n))
+  | `ClassType (p, n) -> Not_replaced (`ClassType (resolved_parent_path s p, n))
 
 and resolved_class_type_path :
     t -> Cpath.Resolved.class_type -> Cpath.Resolved.class_type =
@@ -387,27 +400,31 @@ and type_package s p =
 
 and type_expr s t =
   let open Component.TypeExpr in
-  try
-    match t with
-    | Var s -> Var s
-    | Any -> Any
-    | Alias (t, str) -> Alias (type_expr s t, str)
-    | Arrow (lbl, t1, t2) -> Arrow (lbl, type_expr s t1, type_expr s t2)
-    | Tuple ts -> Tuple (List.map (type_expr s) ts)
-    | Constr (p, ts) -> Constr (type_path s p, List.map (type_expr s) ts)
-    | Polymorphic_variant v -> Polymorphic_variant (type_poly_var s v)
-    | Object o -> Object (type_object s o)
-    | Class (p, ts) -> Class (class_type_path s p, List.map (type_expr s) ts)
-    | Poly (strs, ts) -> Poly (strs, type_expr s ts)
-    | Package p -> Package (type_package s p)
-  with TypeReplacement y -> y
-
-and simple_expansion : t -> Component.ModuleType.simple_expansion -> Component.ModuleType.simple_expansion = fun s t ->
+  match t with
+  | Var s -> Var s
+  | Any -> Any
+  | Alias (t, str) -> Alias (type_expr s t, str)
+  | Arrow (lbl, t1, t2) -> Arrow (lbl, type_expr s t1, type_expr s t2)
+  | Tuple ts -> Tuple (List.map (type_expr s) ts)
+  | Constr (p, ts) -> (
+      match type_path s p with
+      | Replaced r -> r
+      | Not_replaced p -> Constr (p, List.map (type_expr s) ts) )
+  | Polymorphic_variant v -> Polymorphic_variant (type_poly_var s v)
+  | Object o -> Object (type_object s o)
+  | Class (p, ts) -> Class (class_type_path s p, List.map (type_expr s) ts)
+  | Poly (strs, ts) -> Poly (strs, type_expr s ts)
+  | Package p -> Package (type_package s p)
+
+and simple_expansion :
+    t ->
+    Component.ModuleType.simple_expansion ->
+    Component.ModuleType.simple_expansion =
+ fun s t ->
   let open Component.ModuleType in
   match t with
   | Signature sg -> Signature (signature s sg)
-  | Functor (arg, sg) ->
-      Functor (functor_parameter s arg, simple_expansion s sg)
+  | Functor (arg, sg) -> Functor (functor_parameter s arg, simple_expansion s sg)
 
 and module_type s t =
   let open Component.ModuleType in
@@ -571,11 +588,13 @@ and extension_constructor s c =
 
 and extension s e =
   let open Component.Extension in
-  {
-    e with
-    type_path = type_path s e.type_path;
-    constructors = List.map (extension_constructor s) e.constructors;
-  }
+  let type_path =
+    match type_path s e.type_path with
+    | Not_replaced p -> p
+    | Replaced (Constr (p, _)) -> p
+    | Replaced _ -> (* What else is possible ? *) assert false
+  and constructors = List.map (extension_constructor s) e.constructors in
+  { e with type_path; constructors }
 
 and external_ s e =
   let open Component.External in
@@ -724,11 +743,9 @@ and rename_bound_idents s sg =
   | Value (id, v) :: rest ->
       let id' = Ident.Rename.value id in
       rename_bound_idents s (Value (id', v) :: sg) rest
-  | External (id, e) :: rest -> (
-      try
+  | External (id, e) :: rest ->
         let id' = Ident.Rename.value id in
         rename_bound_idents s (External (id', e) :: sg) rest
-      with TypeReplacement _ -> rename_bound_idents s sg rest )
   | Class (id, r, c) :: rest ->
       let id' = new_class_id id in
       rename_bound_idents
@@ -818,11 +835,7 @@ and apply_sig_map s items removed =
     | Exception (id, e) :: rest ->
         inner rest (Exception (id, exception_ s e) :: acc)
     | TypExt e :: rest ->
-        inner rest
-          ( try
-              let e' = extension s e in
-              TypExt e' :: acc
-            with TypeReplacement _ -> acc )
+        inner rest ( TypExt (extension s e) :: acc)
     | Value (id, v) :: rest ->
         inner rest
           ( Value

From 5596b1778ea0c6b9da69acce1e5106325c52791f Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Thu, 3 Dec 2020 18:24:51 +0100
Subject: [PATCH 2/7] Add failing tests

---
 test/xref2/subst/test.md | 105 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 105 insertions(+)

diff --git a/test/xref2/subst/test.md b/test/xref2/subst/test.md
index fb998d49fb..5567523278 100644
--- a/test/xref2/subst/test.md
+++ b/test/xref2/subst/test.md
@@ -83,3 +83,108 @@ type vv/8 = resolved(local(SubTargets/1)).v
 
 - : unit = ()
 ```
+
+Now test by compiling signatures and printing the result:
+
+```ocaml
+(* Nicer output *)
+#install_printer Component.Fmt.signature;;
+
+let compile mli =
+  let open Component in
+  let id, docs, sg = Common.model_of_string mli in
+  Odoc_xref2.Compile.signature Env.empty (id :> Odoc_model.Paths.Identifier.Signature.t) sg
+  |> Of_Lang.signature Of_Lang.empty
+```
+
+```ocaml
+# compile {|
+  module type Monad = sig
+    type 'a t
+
+    val map : 'a t -> ('a -> 'b) -> 'b t
+
+    val join : 'a t t -> 'a t
+  end
+
+  (** Simplest case *)
+  module SomeMonad : sig
+    type 'a t
+
+    include Monad with type 'a t := 'a t
+  end
+
+  (** Substitute with a more complex type *)
+  module ComplexTypeExpr : sig
+    type ('a, 'b) t
+
+    include Monad with type 'a t := (int, 'a) t * ('a, int) t
+  end
+
+  (** No abstraction *)
+  module Erase : sig
+    include Monad with type 'a t := 'a
+  end
+  |}
+- : Component.Signature.t =
+module type Monad/30 = sig
+  type t/31
+  val map/32 : [a] resolved(t/31) -> a -> b -> [b] resolved(t/31)
+  val join/33 : [[a] resolved(t/31)] resolved(t/31) -> [a] resolved(t/31)
+   (removed=[])end
+module SomeMonad/29 : sig
+  type t/34
+  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = [a] resolved(t/34)] (sig =
+    val map/35 : [a] resolved(t/34) -> a -> b -> [a] resolved(t/34)
+    val join/36 : [a] resolved(t/34) -> [a] resolved(t/34)
+     (removed=[]))
+   (removed=[])end
+module ComplexTypeExpr/27 : sig
+  type t/37
+  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))] (sig =
+    val map/38 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> a -> b -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
+    val join/39 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
+     (removed=[]))
+   (removed=[])end
+module Erase/28 : sig
+  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = a] (sig =
+    val map/40 : a -> a -> b -> a
+    val join/41 : a -> a
+     (removed=[]))
+   (removed=[])end
+ (removed=[])
+```
+
+More tests with two type variables:
+
+```ocaml
+# compile {|
+  module type Monad_2 = sig
+    type ('a, 'err) t
+    val map : ('a, 'err) t -> f:('a -> 'b) -> ('b, 'err) t
+    val join : (('a, 'e) t, 'e) t -> ('a, 'e) t
+    val both : ('a, 'e) t -> ('b, 'e) t -> ('a * 'b, 'e) t
+  end
+
+  module SwappedVars : sig
+    type ('x, 'y) t
+    include Monad_2 with type ('a, 'b) t := ('b, 'a) t
+  end
+  |}
+- : Component.Signature.t =
+module type Monad_2/54 = sig
+  type t/55
+  val map/56 : [a * err] resolved(t/55) -> a -> b -> [b * err] resolved(t/55)
+  val join/57 : [[a * e] resolved(t/55) * e] resolved(t/55) -> [a * e] resolved(t/55)
+  val both/58 : [a * e] resolved(t/55) -> [b * e] resolved(t/55) -> [(a * b) * e] resolved(t/55)
+   (removed=[])end
+module SwappedVars/53 : sig
+  type t/59
+  include : resolved(Monad_2/54) with [resolved(root(Monad_2/54).t) = [b * a] resolved(t/59)] (sig =
+    val map/60 : [b * a] resolved(t/59) -> a -> b -> [b * a] resolved(t/59)
+    val join/61 : [b * a] resolved(t/59) -> [b * a] resolved(t/59)
+    val both/62 : [b * a] resolved(t/59) -> [b * a] resolved(t/59) -> [b * a] resolved(t/59)
+     (removed=[]))
+   (removed=[])end
+ (removed=[])
+```

From f944b5d2376fa157f50bbab70171728d9820d9ef Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Fri, 4 Dec 2020 13:23:20 +0100
Subject: [PATCH 3/7] Substitute type variables when substituting type
 constructors

---
 src/xref2/compile.ml     |  4 ++-
 src/xref2/component.ml   | 27 +++++++++++-------
 src/xref2/component.mli  |  6 ++--
 src/xref2/find.ml        |  6 ++--
 src/xref2/find.mli       |  2 +-
 src/xref2/link.ml        |  3 +-
 src/xref2/subst.ml       | 60 ++++++++++++++++++++++++++++++++++++----
 src/xref2/subst.mli      |  3 +-
 src/xref2/tools.ml       | 40 +++++++++++++--------------
 test/xref2/subst/test.md | 16 +++++------
 10 files changed, 112 insertions(+), 55 deletions(-)

diff --git a/src/xref2/compile.ml b/src/xref2/compile.ml
index e84fa96c33..6e269dfd9a 100644
--- a/src/xref2/compile.ml
+++ b/src/xref2/compile.ml
@@ -669,7 +669,9 @@ and type_expression : Env.t -> Id.Parent.t -> _ -> _ =
       | Ok (cp, (`FType _ | `FClass _ | `FClassType _)) ->
           let p = Cpath.resolved_type_path_of_cpath cp in
           Constr (`Resolved p, ts)
-      | Ok (_cp, `FType_removed (_, x)) -> Lang_of.(type_expr empty parent x)
+      | Ok (_cp, `FType_removed (_, x, _eq)) ->
+          (* Substitute type variables ? *)
+          Lang_of.(type_expr empty parent x)
       | Error _ -> Constr (Cpath.type_path_of_cpath cp, ts) )
   | Polymorphic_variant v ->
       Polymorphic_variant (type_expression_polyvar env parent v)
diff --git a/src/xref2/component.ml b/src/xref2/component.ml
index 9b8274bd0b..242d853044 100644
--- a/src/xref2/component.ml
+++ b/src/xref2/component.ml
@@ -304,7 +304,8 @@ and Signature : sig
        and the path they've been substituted with *)
   type removed_item =
     | RModule of Ident.module_ * Cpath.Resolved.module_
-    | RType of Ident.type_ * TypeExpr.t
+    | RType of Ident.type_ * TypeExpr.t * TypeDecl.Equation.t
+        (** [RType (_, texpr, eq)], [eq.manifest = Some texpr] *)
 
   type t = { items : item list; removed : removed_item list }
 end =
@@ -417,7 +418,7 @@ and Substitution : sig
     module_type : subst_module_type ModuleTypeMap.t;
     type_ : subst_type PathTypeMap.t;
     class_type : subst_class_type PathClassTypeMap.t;
-    type_replacement : TypeExpr.t PathTypeMap.t;
+    type_replacement : (TypeExpr.t * TypeDecl.Equation.t) PathTypeMap.t;
     path_invalidating_modules : Ident.path_module list;
     module_type_of_invalidating_modules : Ident.path_module list;
   }
@@ -579,8 +580,8 @@ module Fmt = struct
     | RModule (id, path) ->
         Format.fprintf ppf "module %a (%a)" Ident.fmt id resolved_module_path
           path
-    | RType (id, texpr) ->
-        Format.fprintf ppf "type %a (%a)" Ident.fmt id type_expr texpr
+    | RType (id, texpr, eq) ->
+        Format.fprintf ppf "type %a %a = (%a)" type_params eq.params Ident.fmt id type_expr texpr
 
   and removed_item_list ppf r =
     match r with
@@ -676,12 +677,18 @@ module Fmt = struct
     | Some x -> Format.fprintf ppf "= %a" type_expr x
     | None -> ()
 
-  and type_equation ppf t =
-    match t.TypeDecl.Equation.manifest with
-    | None -> ()
-    | Some m -> Format.fprintf ppf " = %a" type_expr m
+  and type_param ppf t =
+    let desc = match t.Odoc_model.Lang.TypeDecl.desc with Any -> "_" | Var n -> n
+    and variance =
+      match t.variance with Some Pos -> "+" | Some Neg -> "-" | None -> ""
+    and injectivity = if t.injectivity then "!" else "" in
+    Format.fprintf ppf "%s%s%s" variance injectivity desc
 
-  and type_equation2 ppf t =
+  and type_params ppf ts =
+    let pp_sep ppf () = Format.fprintf ppf ", " in
+    Format.fprintf ppf "(%a)" (Format.pp_print_list ~pp_sep type_param) ts
+
+  and type_equation ppf t =
     match t.TypeDecl.Equation.manifest with
     | None -> ()
     | Some m -> Format.fprintf ppf " = %a" type_expr m
@@ -700,7 +707,7 @@ module Fmt = struct
     | TypeEq (frag, decl) ->
         Format.fprintf ppf "%a%a" type_fragment frag type_equation decl
     | TypeSubst (frag, decl) ->
-        Format.fprintf ppf "%a%a" type_fragment frag type_equation2 decl
+        Format.fprintf ppf "%a%a" type_fragment frag type_equation decl
 
   and substitution_list ppf l =
     match l with
diff --git a/src/xref2/component.mli b/src/xref2/component.mli
index 2cf4ebda29..5f7f5ab32b 100644
--- a/src/xref2/component.mli
+++ b/src/xref2/component.mli
@@ -286,7 +286,7 @@ and Signature : sig
        and the path they've been substituted with *)
   type removed_item =
     | RModule of Ident.module_ * Cpath.Resolved.module_
-    | RType of Ident.type_ * TypeExpr.t
+    | RType of Ident.type_ * TypeExpr.t * TypeDecl.Equation.t
 
   type t = { items : item list; removed : removed_item list }
 end
@@ -391,7 +391,7 @@ and Substitution : sig
     module_type : subst_module_type ModuleTypeMap.t;
     type_ : subst_type PathTypeMap.t;
     class_type : subst_class_type PathClassTypeMap.t;
-    type_replacement : TypeExpr.t PathTypeMap.t;
+    type_replacement : (TypeExpr.t * TypeDecl.Equation.t) PathTypeMap.t;
     path_invalidating_modules : Ident.path_module list;
     module_type_of_invalidating_modules : Ident.path_module list;
   }
@@ -504,8 +504,6 @@ module Fmt : sig
 
   val type_equation : Format.formatter -> TypeDecl.Equation.t -> unit
 
-  val type_equation2 : Format.formatter -> TypeDecl.Equation.t -> unit
-
   val exception_ : Format.formatter -> Exception.t -> unit
 
   val extension : Format.formatter -> Extension.t -> unit
diff --git a/src/xref2/find.ml b/src/xref2/find.ml
index f360eec464..8cab1b2c03 100644
--- a/src/xref2/find.ml
+++ b/src/xref2/find.ml
@@ -103,7 +103,7 @@ let class_in_sig sg name =
         Some (`FClassType (N.class_type' id, c))
     | _ -> None)
 
-type removed_type = [ `FType_removed of TypeName.t * TypeExpr.t ]
+type removed_type = [ `FType_removed of TypeName.t * TypeExpr.t * TypeDecl.Equation.t ]
 
 type careful_module = [ module_ | `FModule_removed of Cpath.Resolved.module_ ]
 
@@ -123,8 +123,8 @@ let careful_module_in_sig sg name =
 
 let removed_type_in_sig sg name =
   let removed_type = function
-    | Signature.RType (id, p) when N.type_ id = name ->
-        Some (`FType_removed (N.type' id, p))
+    | Signature.RType (id, p, eq) when N.type_ id = name ->
+        Some (`FType_removed (N.type' id, p, eq))
     | _ -> None
   in
   find_map removed_type sg.Signature.removed
diff --git a/src/xref2/find.mli b/src/xref2/find.mli
index f2c4995cf3..5e6618281b 100644
--- a/src/xref2/find.mli
+++ b/src/xref2/find.mli
@@ -95,7 +95,7 @@ val any_in_class_signature : ClassSignature.t -> string -> any_in_class_sig list
 
 (** Lookup removed items *)
 
-type removed_type = [ `FType_removed of TypeName.t * TypeExpr.t ]
+type removed_type = [ `FType_removed of TypeName.t * TypeExpr.t * TypeDecl.Equation.t ]
 
 type careful_module = [ module_ | `FModule_removed of Cpath.Resolved.module_ ]
 
diff --git a/src/xref2/link.ml b/src/xref2/link.ml
index 0173d3578d..a9f19e1fa1 100644
--- a/src/xref2/link.ml
+++ b/src/xref2/link.ml
@@ -790,7 +790,8 @@ and type_expression : Env.t -> Id.Signature.t -> _ -> _ =
         | Ok (cp', (`FClass _ | `FClassType _)) ->
             let p = Cpath.resolved_type_path_of_cpath cp' in
             Constr (`Resolved p, ts)
-        | Ok (_cp, `FType_removed (_, x)) ->
+        | Ok (_cp, `FType_removed (_, x, _eq)) ->
+            (* Type variables ? *)
             Lang_of.(type_expr empty (parent :> Id.Parent.t) x)
         | Error _ -> Constr (Cpath.type_path_of_cpath cp, ts) )
   | Polymorphic_variant v ->
diff --git a/src/xref2/subst.ml b/src/xref2/subst.ml
index 6f647a30df..48c40b8eb5 100644
--- a/src/xref2/subst.ml
+++ b/src/xref2/subst.ml
@@ -1,8 +1,12 @@
+open Component
+
 exception Invalidated
 
 exception MTOInvalidated
 
-type 'a or_replaced = Not_replaced of 'a | Replaced of Component.TypeExpr.t
+type 'a or_replaced =
+  | Not_replaced of 'a
+  | Replaced of (TypeExpr.t * TypeDecl.Equation.t)
 
 let map_replaced f = function
   | Not_replaced p -> Not_replaced (f p)
@@ -81,9 +85,8 @@ let add_class_type :
         t.class_type;
   }
 
-let add_type_replacement : Ident.path_type -> Component.TypeExpr.t -> t -> t =
- fun id texp t ->
-  { t with type_replacement = PathTypeMap.add id texp t.type_replacement }
+let add_type_replacement id texp equation t =
+  { t with type_replacement = PathTypeMap.add id (texp, equation) t.type_replacement }
 
 let add_module_substitution : Ident.path_module -> t -> t =
  fun id t ->
@@ -113,6 +116,44 @@ let rename_class_type : Ident.path_class_type -> Ident.path_class_type -> t -> t
     class_type = PathClassTypeMap.add id (`Renamed id') t.class_type;
     type_ = PathTypeMap.add (id :> Ident.path_type) (`Renamed (id' :> Ident.path_type)) t.type_ }
 
+let rec substitute_vars vars t =
+  let open TypeExpr in
+  match t with
+  | Var s -> List.assoc s vars
+  | Any -> Any
+  | Alias (t, str) -> Alias (substitute_vars vars t, str)
+  | Arrow (lbl, t1, t2) -> Arrow (lbl, substitute_vars vars t1, substitute_vars vars t2)
+  | Tuple ts -> Tuple (List.map (substitute_vars vars) ts)
+  | Constr (p, ts) -> Constr (p, List.map (substitute_vars vars) ts)
+  | Polymorphic_variant v -> Polymorphic_variant (substitute_vars_poly_variant vars v)
+  | Object o -> Object (substitute_vars_type_object vars o)
+  | Class (p, ts) -> Class (p, List.map (substitute_vars vars) ts)
+  | Poly (strs, ts) -> Poly (strs, substitute_vars vars ts)
+  | Package p -> Package (substitute_vars_package vars p)
+
+and substitute_vars_package vars p =
+  let open TypeExpr.Package in
+  let subst_subst (p, t) = p, substitute_vars vars t in
+  { p with substitutions = List.map subst_subst p.substitutions }
+
+and substitute_vars_type_object vars o =
+  let open TypeExpr.Object in
+  let subst_field = function
+    | Method m -> Method { m with type_ = substitute_vars vars m.type_ }
+    | Inherit t -> Inherit (substitute_vars vars t)
+  in
+  { o with fields = List.map subst_field o.fields }
+
+and substitute_vars_poly_variant vars v =
+  let open TypeExpr.Polymorphic_variant in
+  let subst_element = function
+    | Type t -> Type (substitute_vars vars t)
+    | Constructor c ->
+      let arguments = List.map (substitute_vars vars) c.Constructor.arguments in
+      Constructor { c with arguments}
+  in
+  { v with elements = List.map subst_element v.elements }
+
 let rec resolved_module_path :
     t -> Cpath.Resolved.module_ -> Cpath.Resolved.module_ =
  fun s p ->
@@ -408,7 +449,14 @@ and type_expr s t =
   | Tuple ts -> Tuple (List.map (type_expr s) ts)
   | Constr (p, ts) -> (
       match type_path s p with
-      | Replaced r -> r
+      | Replaced (t, eq) ->
+          let mk_var acc pexpr param =
+            match param.Odoc_model.Lang.TypeDecl.desc with
+            | Any -> acc
+            | Var n -> (n, type_expr s pexpr) :: acc
+          in
+          let vars = List.fold_left2 mk_var [] ts eq.params in
+          substitute_vars vars t
       | Not_replaced p -> Constr (p, List.map (type_expr s) ts) )
   | Polymorphic_variant v -> Polymorphic_variant (type_poly_var s v)
   | Object o -> Object (type_object s o)
@@ -591,7 +639,7 @@ and extension s e =
   let type_path =
     match type_path s e.type_path with
     | Not_replaced p -> p
-    | Replaced (Constr (p, _)) -> p
+    | Replaced (TypeExpr.Constr (p, _), _) -> p
     | Replaced _ -> (* What else is possible ? *) assert false
   and constructors = List.map (extension_constructor s) e.constructors in
   { e with type_path; constructors }
diff --git a/src/xref2/subst.mli b/src/xref2/subst.mli
index 53b9803ac4..fa14d7ff2f 100644
--- a/src/xref2/subst.mli
+++ b/src/xref2/subst.mli
@@ -1,4 +1,5 @@
 (* Subst *)
+open Component
 
 type t = Component.Substitution.t
 
@@ -22,7 +23,7 @@ val add_class :
 val add_class_type :
   Ident.class_type -> Cpath.class_type -> Cpath.Resolved.class_type -> t -> t
 
-val add_type_replacement : Ident.path_type -> Component.TypeExpr.t -> t -> t
+val add_type_replacement : Ident.path_type -> TypeExpr.t -> TypeDecl.Equation.t -> t -> t
 
 val add_module_substitution : Ident.path_module -> t -> t
 
diff --git a/src/xref2/tools.ml b/src/xref2/tools.ml
index 81865eebbc..64cc529c24 100644
--- a/src/xref2/tools.ml
+++ b/src/xref2/tools.ml
@@ -93,7 +93,7 @@ let prefix_substitution path sg =
               (`Module (path, name))
               (`Module (path, name))
               map
-        | Component.Signature.RType (id, _) ->
+        | Component.Signature.RType (id, _, _) ->
             let name = Ident.Name.typed_type id in
             Subst.add_type id (`Type (path, name)) (`Type (path, name)) map)
       removed sub
@@ -421,14 +421,14 @@ and handle_type_lookup id p sg =
   | Some (`FClass (name, _) as t) -> Ok (`Class (p, name), t)
   | Some (`FClassType (name, _) as t) -> Ok (`ClassType (p, name), t)
   | Some (`FType (name, _) as t) -> Ok (`Type (p, name), t)
-  | Some (`FType_removed (name, _) as t) -> Ok (`Type (p, name), t)
+  | Some (`FType_removed (name, _, _) as t) -> Ok (`Type (p, name), t)
   | None -> Error `Find_failure
 
 and handle_class_type_lookup id p sg =
   match Find.careful_class_in_sig sg id with
   | Some (`FClass (name, _) as t) -> Ok (`Class (p, name), t)
   | Some (`FClassType (name, _) as t) -> Ok (`ClassType (p, name), t)
-  | Some (`FType_removed (_name, _) as _t) -> Error `Class_replaced
+  | Some (`FType_removed (_name, _, _) as _t) -> Error `Class_replaced
   | None -> Error `Find_failure
 
 and lookup_module :
@@ -549,8 +549,8 @@ and lookup_type :
       | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
       | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
       | `FType (name, t) -> `FType (name, Subst.type_ sub t)
-      | `FType_removed (name, texpr) ->
-          `FType_removed (name, Subst.type_expr sub texpr)
+      | `FType_removed (name, texpr, eq) ->
+          `FType_removed (name, Subst.type_expr sub texpr, eq)
     in
     Ok t
   in
@@ -594,8 +594,8 @@ and lookup_class_type :
       match t' with
       | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
       | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
-      | `FType_removed (name, texpr) ->
-          `FType_removed (name, Subst.type_expr sub texpr)
+      | `FType_removed (name, texpr, eq) ->
+          `FType_removed (name, Subst.type_expr sub texpr, eq)
     in
     Ok t
   in
@@ -752,8 +752,8 @@ and resolve_type : Env.t -> Cpath.type_ -> resolve_type_result =
         | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
         | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
         | `FType (name, t) -> `FType (name, Subst.type_ sub t)
-        | `FType_removed (name, texpr) ->
-            `FType_removed (name, Subst.type_expr sub texpr)
+        | `FType_removed (name, texpr, eq) ->
+            `FType_removed (name, Subst.type_expr sub texpr, eq)
       in
       (* let time3 = Unix.gettimeofday () in *)
       (* Format.fprintf Format.err_formatter "lookup: %f vs sig_of_mod: %f vs prefix_sub: %f vs rest: %f\n%!" (time1 -. start_time) (time1point5 -. time1) (time2 -. time1point5) (time3 -. time2); *)
@@ -792,8 +792,8 @@ and resolve_type : Env.t -> Cpath.type_ -> resolve_type_result =
         | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
         | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
         | `FType (name, t) -> `FType (name, Subst.type_ sub t)
-        | `FType_removed (name, texpr) ->
-            `FType_removed (name, Subst.type_expr sub texpr)
+        | `FType_removed (name, texpr, eq) ->
+            `FType_removed (name, Subst.type_expr sub texpr, eq)
       in
       Ok (p', t)
   | `Identifier (i, _) ->
@@ -824,8 +824,8 @@ and resolve_class_type : Env.t -> Cpath.class_type -> resolve_class_type_result
         match t' with
         | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
         | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
-        | `FType_removed (name, texpr) ->
-            `FType_removed (name, Subst.type_expr sub texpr)
+        | `FType_removed (name, texpr, eq) ->
+            `FType_removed (name, Subst.type_expr sub texpr, eq)
       in
       (* let time3 = Unix.gettimeofday () in *)
       (* Format.fprintf Format.err_formatter "lookup: %f vs sig_of_mod: %f vs prefix_sub: %f vs rest: %f\n%!" (time1 -. start_time) (time1point5 -. time1) (time2 -. time1point5) (time3 -. time2); *)
@@ -858,8 +858,8 @@ and resolve_class_type : Env.t -> Cpath.class_type -> resolve_class_type_result
         match t' with
         | `FClass (name, c) -> `FClass (name, Subst.class_ sub c)
         | `FClassType (name, ct) -> `FClassType (name, Subst.class_type sub ct)
-        | `FType_removed (name, texpr) ->
-            `FType_removed (name, Subst.type_expr sub texpr)
+        | `FType_removed (name, texpr, eq) ->
+            `FType_removed (name, Subst.type_expr sub texpr, eq)
       in
       Ok (p', t)
 
@@ -1143,12 +1143,12 @@ and fragmap :
                     true,
                     subbed_modules,
                     removed )
-            | Right y ->
+            | Right (texpr, eq) ->
                 Ok
                   ( items,
                     true,
                     subbed_modules,
-                    Component.Signature.RType (id, y) :: removed ) )
+                    Component.Signature.RType (id, texpr, eq) :: removed ) )
         | Component.Signature.Module (id, r, m), _, Some (id', fn)
           when Ident.Name.module_ id = id' -> (
             fn (Component.Delayed.get m) >>= function
@@ -1248,7 +1248,7 @@ and fragmap :
             let new_subst = Component.ModuleType.TypeSubst (frag', equation) in
             handle_intermediate name new_subst
         | name, None ->
-            let mapfn _t = Ok (Right x) in
+            let mapfn _t = Ok (Right (x, equation)) in
             map_signature (Some (name, mapfn)) None sg.items )
     | TypeSubst (_, { Component.TypeDecl.Equation.manifest = None; _ }) ->
         failwith "Unhandled condition: TypeSubst with no manifest"
@@ -1258,8 +1258,8 @@ and fragmap :
     match removed with
     | Component.Signature.RModule (id, p) ->
         Subst.add_module (id :> Ident.path_module) (`Resolved p) p sub
-    | Component.Signature.RType (id, replacement) ->
-        Subst.add_type_replacement (id :> Ident.path_type) replacement sub
+    | Component.Signature.RType (id, r_texpr, r_eq) ->
+        Subst.add_type_replacement (id :> Ident.path_type) r_texpr r_eq sub
   in
 
   let sub = List.fold_right sub_of_removed removed Subst.identity in
diff --git a/test/xref2/subst/test.md b/test/xref2/subst/test.md
index 5567523278..51c0f71964 100644
--- a/test/xref2/subst/test.md
+++ b/test/xref2/subst/test.md
@@ -135,20 +135,20 @@ module type Monad/30 = sig
 module SomeMonad/29 : sig
   type t/34
   include : resolved(Monad/30) with [resolved(root(Monad/30).t) = [a] resolved(t/34)] (sig =
-    val map/35 : [a] resolved(t/34) -> a -> b -> [a] resolved(t/34)
-    val join/36 : [a] resolved(t/34) -> [a] resolved(t/34)
+    val map/35 : [a] resolved(t/34) -> a -> b -> [b] resolved(t/34)
+    val join/36 : [[a] resolved(t/34)] resolved(t/34) -> [a] resolved(t/34)
      (removed=[]))
    (removed=[])end
 module ComplexTypeExpr/27 : sig
   type t/37
   include : resolved(Monad/30) with [resolved(root(Monad/30).t) = ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))] (sig =
-    val map/38 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> a -> b -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
-    val join/39 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
+    val map/38 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> a -> b -> ([resolved(identifier(int)) * b] resolved(t/37) * [b * resolved(identifier(int))] resolved(t/37))
+    val join/39 : ([resolved(identifier(int)) * ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))] resolved(t/37) * [([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) * resolved(identifier(int))] resolved(t/37)) -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
      (removed=[]))
    (removed=[])end
 module Erase/28 : sig
   include : resolved(Monad/30) with [resolved(root(Monad/30).t) = a] (sig =
-    val map/40 : a -> a -> b -> a
+    val map/40 : a -> a -> b -> b
     val join/41 : a -> a
      (removed=[]))
    (removed=[])end
@@ -181,9 +181,9 @@ module type Monad_2/54 = sig
 module SwappedVars/53 : sig
   type t/59
   include : resolved(Monad_2/54) with [resolved(root(Monad_2/54).t) = [b * a] resolved(t/59)] (sig =
-    val map/60 : [b * a] resolved(t/59) -> a -> b -> [b * a] resolved(t/59)
-    val join/61 : [b * a] resolved(t/59) -> [b * a] resolved(t/59)
-    val both/62 : [b * a] resolved(t/59) -> [b * a] resolved(t/59) -> [b * a] resolved(t/59)
+    val map/60 : [err * a] resolved(t/59) -> a -> b -> [err * b] resolved(t/59)
+    val join/61 : [e * [e * a] resolved(t/59)] resolved(t/59) -> [e * a] resolved(t/59)
+    val both/62 : [e * a] resolved(t/59) -> [e * b] resolved(t/59) -> [e * (a * b)] resolved(t/59)
      (removed=[]))
    (removed=[])end
  (removed=[])

From 3bac1cd3134bb16dc2b96a9387494d1ab04fb711 Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Mon, 7 Dec 2020 19:53:06 +0100
Subject: [PATCH 4/7] Improve Component.Fmt

Print type representation in declarations.
Print polymorphic variants.
Add missing parentheses around arrows arguments and shorten some paths.
---
 src/xref2/component.ml        | 119 ++++++++++++++++++++++------------
 test/xref2/strengthen/test.md |   2 +-
 test/xref2/subst/test.md      |  43 ++++++------
 3 files changed, 100 insertions(+), 64 deletions(-)

diff --git a/src/xref2/component.ml b/src/xref2/component.ml
index 242d853044..53032e3d50 100644
--- a/src/xref2/component.ml
+++ b/src/xref2/component.ml
@@ -492,6 +492,16 @@ end
 module Fmt = struct
   open Odoc_model.Names
 
+  let fpf = Format.fprintf
+
+  let fpp_opt fmt pp_a ppf = function Some t -> fpf ppf fmt pp_a t | None -> ()
+
+  let fpp_list fmt_sep fmt_outer pp_a ppf t =
+    let pp_sep ppf () = fpf ppf fmt_sep in
+    match t with
+    | [] -> ()
+    | t -> fpf ppf fmt_outer (Format.pp_print_list ~pp_sep pp_a) t
+
   let rec signature ppf sg =
     let open Signature in
     Format.fprintf ppf "@[<v>";
@@ -507,10 +517,10 @@ module Fmt = struct
             Format.fprintf ppf "@[<v 2>module type %a %a@]@," Ident.fmt id
               module_type (Delayed.get mt)
         | Type (id, _, t) ->
-            Format.fprintf ppf "@[<v 2>type %a %a@]@," Ident.fmt id type_decl
+            Format.fprintf ppf "@[<v 2>type %a%a@]@," Ident.fmt id type_decl
               (Delayed.get t)
         | TypeSubstitution (id, t) ->
-            Format.fprintf ppf "@[<v 2>type %a := %a@]@," Ident.fmt id type_decl
+            Format.fprintf ppf "@[<v 2>type %a :=%a@]@," Ident.fmt id type_decl
               t
         | Exception (id, e) ->
             Format.fprintf ppf "@[<v 2>exception %a %a@]@," Ident.fmt id
@@ -673,9 +683,42 @@ module Fmt = struct
       module_type_expr x.FunctorParameter.expr
 
   and type_decl ppf t =
-    match TypeDecl.(t.equation.Equation.manifest) with
-    | Some x -> Format.fprintf ppf "= %a" type_expr x
-    | None -> ()
+    let open TypeDecl in
+    match t.representation with
+    | Some repr ->
+        Format.fprintf ppf "%a = %a"
+          (fpp_opt " : %a" type_expr)
+          t.equation.Equation.manifest type_decl_repr repr
+    | None -> (fpp_opt " = %a" type_expr) ppf t.equation.Equation.manifest
+
+  and type_decl_repr ppf =
+    let open TypeDecl.Representation in
+    function
+    | Variant cs -> fpp_list " | " "%a" type_decl_constructor ppf cs
+    | Record fs -> type_decl_fields ppf fs
+    | Extensible -> Format.fprintf ppf ".."
+
+  and type_decl_constructor ppf t =
+    let open TypeDecl.Constructor in
+    match t.res with
+    | Some res ->
+        fpf ppf "%s : %a -> %a" t.name type_decl_constructor_arg t.args type_expr
+          res
+    | None -> fpf ppf "%s of %a" t.name type_decl_constructor_arg t.args
+
+  and type_decl_constructor_arg ppf =
+    let open TypeDecl.Constructor in
+    function
+    | Tuple ts -> type_tuple ppf ts | Record fs -> type_decl_fields ppf fs
+
+  and type_decl_field ppf t =
+    let open TypeDecl.Field in
+    let mutable_ = if t.mutable_ then "mutable " else "" in
+    fpf ppf "%s%s : %a" mutable_ t.name type_expr t.type_
+
+  and type_decl_fields ppf fs = fpp_list "; " "{ %a }" type_decl_field ppf fs
+
+  and type_tuple ppf ts = fpp_list " * " "%a" type_expr ppf ts
 
   and type_param ppf t =
     let desc = match t.Odoc_model.Lang.TypeDecl.desc with Any -> "_" | Var n -> n
@@ -736,28 +779,22 @@ module Fmt = struct
   and type_package ppf _p = Format.fprintf ppf "(package)"
 
   and type_expr_polymorphic_variant ppf p =
-    let kind ppf k =
-      let open Odoc_model.Lang.TypeExpr.Polymorphic_variant in
-      match k with
-      | Fixed -> Format.fprintf ppf "Fixed"
-      | Closed xs -> Format.fprintf ppf "Closed [%s]" (String.concat ";" xs)
-      | Open -> Format.fprintf ppf "Open"
-    in
     let open TypeExpr.Polymorphic_variant in
-    let constructor ppf c = Format.fprintf ppf "name=%s" c.Constructor.name in
-    let element ppf k =
-      match k with
-      | Type t -> Format.fprintf ppf "Type (%a)" type_expr t
-      | Constructor c -> Format.fprintf ppf "Constructor (%a)" constructor c
-    in
-    let rec elements ppf k =
-      match k with
-      | [] -> ()
-      | [ x ] -> Format.fprintf ppf "%a" element x
-      | x :: xs -> Format.fprintf ppf "%a; %a" element x elements xs
+    let pp_element ppf = function
+      | Type t -> type_expr ppf t
+      | Constructor c ->
+          fpf ppf "`%s%a" c.Constructor.name
+            (fpp_list " * " " of %a" type_expr)
+            c.arguments
     in
-    Format.fprintf ppf "{ kind=%a; elements=[%a] }" kind p.kind elements
-      p.elements
+    let pp_elements = fpp_list " | " "%a" pp_element in
+    match p.kind with
+    | Fixed -> fpf ppf "[ %a ]" pp_elements p.elements
+    | Closed xs ->
+        fpf ppf "[ %a > %a ]" pp_elements p.elements
+          (fpp_list " " "%a" Format.pp_print_string)
+          xs
+    | Open -> fpf ppf "[> %a ]" pp_elements p.elements
 
   and type_expr ppf e =
     let open TypeExpr in
@@ -765,8 +802,8 @@ module Fmt = struct
     | Var x -> Format.fprintf ppf "%s" x
     | Any -> Format.fprintf ppf "_"
     | Alias (x, y) -> Format.fprintf ppf "(alias %a %s)" type_expr x y
-    | Arrow (_l, t1, t2) ->
-        Format.fprintf ppf "%a -> %a" type_expr t1 type_expr t2
+    | Arrow (l, t1, t2) ->
+        Format.fprintf ppf "%a(%a) -> %a" type_expr_label l type_expr t1 type_expr t2
     | Tuple ts -> Format.fprintf ppf "(%a)" type_expr_list ts
     | Constr (p, args) -> (
         match args with
@@ -783,11 +820,11 @@ module Fmt = struct
       =
    fun ppf p ->
     match p with
-    | `Local ident -> Format.fprintf ppf "local(%a)" Ident.fmt ident
+    | `Local ident -> Format.fprintf ppf "%a" Ident.fmt ident
     | `Apply (p1, p2) ->
         Format.fprintf ppf "%a(%a)" resolved_module_path p1 resolved_module_path p2
     | `Identifier p ->
-        Format.fprintf ppf "identifier(%a)" model_identifier
+        Format.fprintf ppf "%a" model_identifier
           (p :> Odoc_model.Paths.Identifier.t)
     | `Substituted p ->
         Format.fprintf ppf "substituted(%a)" resolved_module_path p
@@ -813,7 +850,7 @@ module Fmt = struct
   and module_path : Format.formatter -> Cpath.module_ -> unit =
    fun ppf p ->
     match p with
-    | `Resolved p -> Format.fprintf ppf "resolved(%a)" resolved_module_path p
+    | `Resolved p -> Format.fprintf ppf "r(%a)" resolved_module_path p
     | `Dot (p, str) -> Format.fprintf ppf "%a.%s" module_path p str
     | `Module (p, n) ->
         Format.fprintf ppf "%a.%a" resolved_parent_path p ModuleName.fmt n
@@ -834,7 +871,7 @@ module Fmt = struct
     match p with
     | `Local id -> Format.fprintf ppf "%a" Ident.fmt id
     | `Identifier id ->
-        Format.fprintf ppf "identifier(%a)" model_identifier
+        Format.fprintf ppf "%a" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
     | `Substituted x ->
         Format.fprintf ppf "substituted(%a)" resolved_module_type_path x
@@ -851,7 +888,7 @@ module Fmt = struct
    fun ppf m ->
     match m with
     | `Resolved p ->
-        Format.fprintf ppf "resolved(%a)" resolved_module_type_path p
+        Format.fprintf ppf "r(%a)" resolved_module_type_path p
     | `Identifier (id, b) ->
         Format.fprintf ppf "identifier(%a, %b)" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
@@ -867,7 +904,7 @@ module Fmt = struct
     match p with
     | `Local id -> Format.fprintf ppf "%a" Ident.fmt id
     | `Identifier id ->
-        Format.fprintf ppf "identifier(%a)" model_identifier
+        Format.fprintf ppf "%a" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
     | `Substituted x ->
         Format.fprintf ppf "substituted(%a)" resolved_type_path x
@@ -891,7 +928,7 @@ module Fmt = struct
   and type_path : Format.formatter -> Cpath.type_ -> unit =
    fun ppf p ->
     match p with
-    | `Resolved r -> Format.fprintf ppf "resolved(%a)" resolved_type_path r
+    | `Resolved r -> Format.fprintf ppf "r(%a)" resolved_type_path r
     | `Identifier (id, b) ->
         Format.fprintf ppf "identifier(%a, %b)" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
@@ -947,7 +984,7 @@ module Fmt = struct
   and model_path : Format.formatter -> Odoc_model.Paths.Path.t -> unit =
    fun ppf (p : Odoc_model.Paths.Path.t) ->
     match p with
-    | `Resolved rp -> Format.fprintf ppf "resolved(%a)" model_resolved_path rp
+    | `Resolved rp -> Format.fprintf ppf "r(%a)" model_resolved_path rp
     | `Identifier (id, b) ->
         Format.fprintf ppf "identifier(%a, %b)" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
@@ -968,7 +1005,7 @@ module Fmt = struct
     let open Odoc_model.Paths.Path.Resolved in
     match p with
     | `Identifier id ->
-        Format.fprintf ppf "identifier(%a)" model_identifier
+        Format.fprintf ppf "%a" model_identifier
           (id :> Odoc_model.Paths.Identifier.t)
     | `Module (parent, name) ->
         Format.fprintf ppf "%a.%s" model_resolved_path
@@ -1179,25 +1216,25 @@ module Fmt = struct
   and signature_fragment ppf (f : Cfrag.signature) =
     match f with
     | `Resolved r ->
-        Format.fprintf ppf "resolved(%a)" resolved_signature_fragment r
+        Format.fprintf ppf "r(%a)" resolved_signature_fragment r
     | `Dot (s, n) -> Format.fprintf ppf "%a.%s" signature_fragment s n
     | `Root -> Format.fprintf ppf "root"
 
   and module_fragment ppf (f : Cfrag.module_) =
     match f with
     | `Resolved r ->
-        Format.fprintf ppf "resolved(%a)" resolved_module_fragment r
+        Format.fprintf ppf "r(%a)" resolved_module_fragment r
     | `Dot (s, n) -> Format.fprintf ppf "%a.%s" signature_fragment s n
 
   and type_fragment ppf (f : Cfrag.type_) =
     match f with
-    | `Resolved r -> Format.fprintf ppf "resolved(%a)" resolved_type_fragment r
+    | `Resolved r -> Format.fprintf ppf "r(%a)" resolved_type_fragment r
     | `Dot (s, n) -> Format.fprintf ppf "%a.%s" signature_fragment s n
 
   and model_resolved_reference ppf (r : Odoc_model.Paths.Reference.Resolved.t) =
     let open Odoc_model.Paths.Reference.Resolved in
     match r with
-    | `Identifier id -> Format.fprintf ppf "identifier(%a)" model_identifier id
+    | `Identifier id -> Format.fprintf ppf "%a" model_identifier id
     | `Hidden p ->
         Format.fprintf ppf "hidden(%a)" model_resolved_reference (p :> t)
     | `Module (parent, name) ->
@@ -1267,7 +1304,7 @@ module Fmt = struct
     let open Odoc_model.Paths.Reference in
     match r with
     | `Resolved r' ->
-        Format.fprintf ppf "resolved(%a)" model_resolved_reference r'
+        Format.fprintf ppf "r(%a)" model_resolved_reference r'
     | `Root (name, _) -> Format.fprintf ppf "unresolvedroot(%s)" name
     | `Dot (parent, str) ->
         Format.fprintf ppf "%a.%s" model_reference (parent :> t) str
diff --git a/test/xref2/strengthen/test.md b/test/xref2/strengthen/test.md
index b9e97f7e8b..7add8d6fcf 100644
--- a/test/xref2/strengthen/test.md
+++ b/test/xref2/strengthen/test.md
@@ -29,7 +29,7 @@ type u/1 = local(t/0,false)
  (removed=[])
 AFTER
 ======
-type t/2 = resolved(identifier((root Root))).t
+type t/2 = r((root Root)).t
 type u/3 = local(t/2,false)
  (removed=[])
 - : unit = ()
diff --git a/test/xref2/subst/test.md b/test/xref2/subst/test.md
index 51c0f71964..723790b73f 100644
--- a/test/xref2/subst/test.md
+++ b/test/xref2/subst/test.md
@@ -76,9 +76,9 @@ type vv/5 = local(SubstituteMe/2,false).v
 AFTER
 ======
 S: sig
-type tt/6 = resolved(local(SubTargets/1)).t
-type uu/7 = resolved(local(SubTargets/1)).u
-type vv/8 = resolved(local(SubTargets/1)).v
+type tt/6 = r(SubTargets/1).t
+type uu/7 = r(SubTargets/1).u
+type vv/8 = r(SubTargets/1).v
  (removed=[])end
 
 - : unit = ()
@@ -129,28 +129,27 @@ let compile mli =
 - : Component.Signature.t =
 module type Monad/30 = sig
   type t/31
-  val map/32 : [a] resolved(t/31) -> a -> b -> [b] resolved(t/31)
-  val join/33 : [[a] resolved(t/31)] resolved(t/31) -> [a] resolved(t/31)
+  val map/32 : ([a] r(t/31)) -> ((a) -> b) -> [b] r(t/31)
+  val join/33 : ([[a] r(t/31)] r(t/31)) -> [a] r(t/31)
    (removed=[])end
 module SomeMonad/29 : sig
   type t/34
-  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = [a] resolved(t/34)] (sig =
-    val map/35 : [a] resolved(t/34) -> a -> b -> [b] resolved(t/34)
-    val join/36 : [[a] resolved(t/34)] resolved(t/34) -> [a] resolved(t/34)
+  include : r(Monad/30) with [r(root(Monad/30).t) = [a] r(t/34)] (sig =
+    val map/35 : ([a] r(t/34)) -> ((a) -> b) -> [b] r(t/34)
+    val join/36 : ([[a] r(t/34)] r(t/34)) -> [a] r(t/34)
      (removed=[]))
    (removed=[])end
 module ComplexTypeExpr/27 : sig
   type t/37
-  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))] (sig =
-    val map/38 : ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) -> a -> b -> ([resolved(identifier(int)) * b] resolved(t/37) * [b * resolved(identifier(int))] resolved(t/37))
-    val join/39 : ([resolved(identifier(int)) * ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))] resolved(t/37) * [([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37)) * resolved(identifier(int))] resolved(t/37)) -> ([resolved(identifier(int)) * a] resolved(t/37) * [a * resolved(identifier(int))] resolved(t/37))
+  include : r(Monad/30) with [r(root(Monad/30).t) = ([r(int) * a] r(t/37) * [a * r(int)] r(t/37))] (sig =
+    val map/38 : (([r(int) * a] r(t/37) * [a * r(int)] r(t/37))) -> ((a) -> b) -> ([r(int) * b] r(t/37) * [b * r(int)] r(t/37))
+    val join/39 : (([r(int) * ([r(int) * a] r(t/37) * [a * r(int)] r(t/37))] r(t/37) * [([r(int) * a] r(t/37) * [a * r(int)] r(t/37)) * r(int)] r(t/37))) -> ([r(int) * a] r(t/37) * [a * r(int)] r(t/37))
      (removed=[]))
    (removed=[])end
 module Erase/28 : sig
-  include : resolved(Monad/30) with [resolved(root(Monad/30).t) = a] (sig =
-    val map/40 : a -> a -> b -> b
-    val join/41 : a -> a
-     (removed=[]))
+  include : r(Monad/30) with [r(root(Monad/30).t) = a] (sig = val map/40 : (a) -> ((a) -> b) -> b
+                                                              val join/41 : (a) -> a
+                                                               (removed=[]))
    (removed=[])end
  (removed=[])
 ```
@@ -174,16 +173,16 @@ More tests with two type variables:
 - : Component.Signature.t =
 module type Monad_2/54 = sig
   type t/55
-  val map/56 : [a * err] resolved(t/55) -> a -> b -> [b * err] resolved(t/55)
-  val join/57 : [[a * e] resolved(t/55) * e] resolved(t/55) -> [a * e] resolved(t/55)
-  val both/58 : [a * e] resolved(t/55) -> [b * e] resolved(t/55) -> [(a * b) * e] resolved(t/55)
+  val map/56 : ([a * err] r(t/55)) -> f:((a) -> b) -> [b * err] r(t/55)
+  val join/57 : ([[a * e] r(t/55) * e] r(t/55)) -> [a * e] r(t/55)
+  val both/58 : ([a * e] r(t/55)) -> ([b * e] r(t/55)) -> [(a * b) * e] r(t/55)
    (removed=[])end
 module SwappedVars/53 : sig
   type t/59
-  include : resolved(Monad_2/54) with [resolved(root(Monad_2/54).t) = [b * a] resolved(t/59)] (sig =
-    val map/60 : [err * a] resolved(t/59) -> a -> b -> [err * b] resolved(t/59)
-    val join/61 : [e * [e * a] resolved(t/59)] resolved(t/59) -> [e * a] resolved(t/59)
-    val both/62 : [e * a] resolved(t/59) -> [e * b] resolved(t/59) -> [e * (a * b)] resolved(t/59)
+  include : r(Monad_2/54) with [r(root(Monad_2/54).t) = [b * a] r(t/59)] (sig =
+    val map/60 : ([err * a] r(t/59)) -> f:((a) -> b) -> [err * b] r(t/59)
+    val join/61 : ([e * [e * a] r(t/59)] r(t/59)) -> [e * a] r(t/59)
+    val both/62 : ([e * a] r(t/59)) -> ([e * b] r(t/59)) -> [e * (a * b)] r(t/59)
      (removed=[]))
    (removed=[])end
  (removed=[])

From 3eb99ae7d714a3fea94c272eb4106e381435a6e5 Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Mon, 7 Dec 2020 19:21:02 +0100
Subject: [PATCH 5/7] Add a failing test

---
 test/xref2/subst/test.md | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/test/xref2/subst/test.md b/test/xref2/subst/test.md
index 723790b73f..40941f082f 100644
--- a/test/xref2/subst/test.md
+++ b/test/xref2/subst/test.md
@@ -187,3 +187,20 @@ module SwappedVars/53 : sig
    (removed=[])end
  (removed=[])
 ```
+
+Edge cases:
+
+```ocaml
+# compile {|
+  module type S = sig
+    type 'a t
+    val map : 'a t -> ('a -> 'b) -> 'b t
+  end
+
+  module M : sig
+    type 'a t
+    include S with type 'a t := ([ `A of 'a * 'b ] as 'b) t
+  end
+  |}
+Exception: Not_found.
+```

From e71da0da6fa1ec913e787726c4427dac6e3ffb7d Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Mon, 7 Dec 2020 19:27:26 +0100
Subject: [PATCH 6/7] Catch exception when unresolved var

---
 src/xref2/subst.ml       | 16 ++++++++++------
 test/xref2/subst/test.md | 13 ++++++++++++-
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/src/xref2/subst.ml b/src/xref2/subst.ml
index 48c40b8eb5..d50204e0c5 100644
--- a/src/xref2/subst.ml
+++ b/src/xref2/subst.ml
@@ -119,13 +119,15 @@ let rename_class_type : Ident.path_class_type -> Ident.path_class_type -> t -> t
 let rec substitute_vars vars t =
   let open TypeExpr in
   match t with
-  | Var s -> List.assoc s vars
+  | Var s -> ( try List.assoc s vars with Not_found -> t )
   | Any -> Any
   | Alias (t, str) -> Alias (substitute_vars vars t, str)
-  | Arrow (lbl, t1, t2) -> Arrow (lbl, substitute_vars vars t1, substitute_vars vars t2)
+  | Arrow (lbl, t1, t2) ->
+      Arrow (lbl, substitute_vars vars t1, substitute_vars vars t2)
   | Tuple ts -> Tuple (List.map (substitute_vars vars) ts)
   | Constr (p, ts) -> Constr (p, List.map (substitute_vars vars) ts)
-  | Polymorphic_variant v -> Polymorphic_variant (substitute_vars_poly_variant vars v)
+  | Polymorphic_variant v ->
+      Polymorphic_variant (substitute_vars_poly_variant vars v)
   | Object o -> Object (substitute_vars_type_object vars o)
   | Class (p, ts) -> Class (p, List.map (substitute_vars vars) ts)
   | Poly (strs, ts) -> Poly (strs, substitute_vars vars ts)
@@ -133,7 +135,7 @@ let rec substitute_vars vars t =
 
 and substitute_vars_package vars p =
   let open TypeExpr.Package in
-  let subst_subst (p, t) = p, substitute_vars vars t in
+  let subst_subst (p, t) = (p, substitute_vars vars t) in
   { p with substitutions = List.map subst_subst p.substitutions }
 
 and substitute_vars_type_object vars o =
@@ -149,8 +151,10 @@ and substitute_vars_poly_variant vars v =
   let subst_element = function
     | Type t -> Type (substitute_vars vars t)
     | Constructor c ->
-      let arguments = List.map (substitute_vars vars) c.Constructor.arguments in
-      Constructor { c with arguments}
+        let arguments =
+          List.map (substitute_vars vars) c.Constructor.arguments
+        in
+        Constructor { c with arguments }
   in
   { v with elements = List.map subst_element v.elements }
 
diff --git a/test/xref2/subst/test.md b/test/xref2/subst/test.md
index 40941f082f..16c0db7bd4 100644
--- a/test/xref2/subst/test.md
+++ b/test/xref2/subst/test.md
@@ -202,5 +202,16 @@ Edge cases:
     include S with type 'a t := ([ `A of 'a * 'b ] as 'b) t
   end
   |}
-Exception: Not_found.
+- : Component.Signature.t =
+module type S/69 = sig
+  type t/70
+  val map/71 : ([a] r(t/70)) -> ((a) -> b) -> [b] r(t/70)
+   (removed=[])end
+module M/68 : sig
+  type t/72
+  include : r(S/69) with [r(root(S/69).t) = [(alias (poly_var [ `A of (a * b) ]) b)] r(t/72)] (sig =
+    val map/73 : ([(alias (poly_var [ `A of (a * b) ]) b)] r(t/72)) -> ((a) -> b) -> [(alias (poly_var [ `A of (b * b) ]) b)] r(t/72)
+     (removed=[]))
+   (removed=[])end
+ (removed=[])
 ```

From 9219cadbd3618b7d4cc162bce5f43d9469bfdf13 Mon Sep 17 00:00:00 2001
From: Jules Aguillon <juloo.dsi@gmail.com>
Date: Mon, 7 Dec 2020 19:43:12 +0100
Subject: [PATCH 7/7] Restrict subst tests to OCaml >= 4.06

---
 test/xref2/subst/dune | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/xref2/subst/dune b/test/xref2/subst/dune
index 4321daba9e..50686ac771 100644
--- a/test/xref2/subst/dune
+++ b/test/xref2/subst/dune
@@ -8,5 +8,6 @@
 
 (rule
  (alias runtest)
+ (enabled_if (>= %{ocaml_version} 4.06))
  (action
   (diff test.md test.output)))