Module substitution is very costly

[ppedrot]

Description of the problem

Manipulating big modules is linear in the size of the data due to substitutions. Reported by @Zdancewic.

Small Rocq / Coq file to reproduce the bug

(* Build a lage module signature that is noticeably slow to work with.

   Using [Program Fixpoint] in this way is an artificial way to create 
   a huge signature.  The actual development *doesn't* do that, it just has
   large signatures.
 *)
Module Type SLOW.

  (* Some types with lots of constructors *)
  Inductive T :=
  | C1 | C2 | C3 | C4  | C5 | C6 | C7 | C8 | C9 | C10
  | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19 | C20. 

  Inductive S :=
  | D1 (t : T)
  | D2 (s : S) (s : S).

  (* Some tactics to solve case-analysis goals generated by Program Fixpoint. *)
  Ltac solve_H :=
     repeat match goal with
       | [ |- S ] => exact (D1 C1)
       | [ |- ?E /\ ?F ] => split; intros
       | [ |- ~ ?X ] => intro CONTRA
       | [ H : ?E /\ ?F |- _ ] => destruct H
       | [ H := ?E : D1 _ |- _ ] => unfold H in *; clear H                                       
       | [ H := D1 _ : S |- _ ] => unfold H in *; clear H
       | [ H := D2 _ _: S |- _ ] => unfold H in *; clear H
       end.

  Ltac solve_X :=
     repeat match goal with 
       | [ H : D1 _ = D1 _ |- _ ] => inversion H; clear H 
       | [ H : D2 _ _ = D1 _ |- _ ] => inversion H; clear H
       | [ H : D2 _ _ = D2 _ _ |- _ ] => inversion H; clear H
       | [ H : D1 _ = D2 _ _ |- _ ] => inversion H; clear H
       end.
  
  Ltac solve_it := intros; solve_H; solve_X.

  Set Transparent Obligations.
  Obligation Tactic :=  solve_it.
  (* Generate many hidden obligations. *)
  Program Fixpoint foo (s1 s2 s3 : S) : S :=
    match s1, s2, s3 with
    | D1 C1, D1 C1, D1 C20 => D1 C1
    | D1 _, D1 C20, D1 C0 => D1 C20
    | D2 (D1 C1) x2, D2 y1 y2, D1 _ => D1 C20
    | D2 (D1 C20) _, _, D2 _ (D1 C20) => D1 C1
    | _, D1 C20, _ => D1 C20
    | D1 C19, D1 C19, _ => D1 C20
    | D1 _, D1 C19, D2 _ _ => D1 C20
    | _, _, _ => D1 C20
    end.
  (* Discharges 1318 obligations *)

End SLOW.


Time Module UseSlow1x (X : SLOW).
(* 0.37 to 0.5 seconds *)
End UseSlow1x.

(* Checking that SLOW is well-formed repeatedly: time seems linear in the number of occurrences of SLOW. *)
Time Module UseSlow3x (X : SLOW) (Y : SLOW) (Z : SLOW).
(* 1.2 - 2.5 seconds *)
End UseSlow3x.

Time Module UseSlow6x (X : SLOW) (Y : SLOW) (Z : SLOW) (W : SLOW) (U : SLOW) (V : SLOW).
(* ~2.5 - g seconds *)
End UseSlow6x.

Time Module Type INC (S : SLOW) <: SLOW.
  (* 1-2 seconds: two well-formedness + subsumption check? *) 
  Time Include S. (* ~0.6 - 0.8 seconds *)
  Time Module F := UseSlow3x S S S. (* ~2.2 seconds *)
End INC.

(* When constructing large module structures, we often end up with "telescoping" definitions. *)
Time Module Type TELESCOPE (S : SLOW) (B : INC S) (C : INC B).
(* ~4.7 to 5 seconds *)
Time Module X : SLOW := S. (* ~2.7 to 3 seconds *)
Time Module Y : SLOW := B. (* ~2.7 seconds *)
Time Module Z : SLOW := C. (* ~3 seconds *)
End TELESCOPE.

Module SlowInstance : SLOW.
  Include SLOW.
End SlowInstance.

Module IncInstance : INC SlowInstance.
  Include SlowInstance.
  Module F := UseSlow3x SlowInstance SlowInstance SlowInstance.
End IncInstance.  

Module IncIncInstance : INC IncInstance.
  Include IncInstance.
End IncIncInstance.

Time Module TelescopeInstance : TELESCOPE SlowInstance IncInstance IncIncInstance.  (* ~3.7 seconds *)
  Time Module X : SLOW := SlowInstance. (* ~2.5 seconds *)
  Time Module Y : SLOW := IncInstance. (* ~2.5 seconds *)
  Time Module Z : SLOW := IncIncInstance. (* ~2.7 seconds *)
Time End TelescopeInstance.  (* 4.45 seconds *)

Version of Rocq / Coq where this bug occurs

9.2

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response