Collect #

Preliminaries #

We use the term "instance transformers" (or simply "transformers") to refer to instances which map one or more instances to another instance. For example, CommGroup.toGroup is an instance transformer. An "instance transformation" (or simply "transformation"), meanwhile, will refer to an application of an instance transformer, e.g. @CommGroup.toGroup G inst. Note that both instance transformers and instance transformations are themselves instances; the former are declared as such, while the latter are instance-valued expressions. To disambiguate, we will refer to instances that aren't instance transformers or instance transformations as "root instances".

Oftentimes, transformations may be nested:

Weak.toWeakest α (Strong.toWeak α (Strongest.toStrong α ⟨inst of Strongest on α⟩))
                                                        └──────── root ────────┘

These nested transformations often involve "junctions": transformations that have ≥2 class-typed args. Sometimes, these junctions are bona-fide confluences, as is the case for e.g. Prod.instMonoid {M : Type u} {N : Type v} [Monoid M] [Monoid N] : Monoid (M × N), where the conclusion isn't just a "projection" of one of the class-typed args. In many other cases, the junctions are such projections, however (if not technically then at least in spirit). We call junctions of this second kind tributary junctions, borrowing from hydrology again, and distinguish two sub-categories:

Unconditional tributary junctions (UTJ) (projections): When one (and only one) of the class-typed args contains all other args in its type, then that single class-typed arg "pins" (or "fixes") the values of all other arguments (no matter their annotation) through unification, i.e., it's the sole degree of freedom. As such, when we have, for example, an instance of IsStrictOrderedRing R — or, written more explicitly, an instance inst₃ : @IsStrictOrderedRing.{u} R inst₁ inst₂, where inst₁ : Semiring.{u} R and inst₂ : PartialOrder.{u} R — then that instance alone, through its type, pins all the other arguments (including universe levels) of, for example, the transformation IsStrictOrderedRing.toIsOrderedRing:
```
instance IsStrictOrderedRing.toIsOrderedRing.{u} {R : Type u}
  [Semiring R]               -- [inst₁ : Semiring.{u} R]
  [PartialOrder R]           -- [inst₂ : PartialOrder.{u} R]
  [IsStrictOrderedRing R] :  -- [inst₃ : @IsStrictOrderedRing.{u} R inst₁ inst₂],
  IsOrderedRing R            -- @IsOrderedRing.{u} R inst₁ inst₂
```
Hence, we treat IsStrictOrderedRing.toIsOrderedRing as a mere projection of IsStrictOrderedRing R: hand someone inst₃, and they can take IsStrictOrderedRing.toIsOrderedRing, fill out all other argument slots, and give you an instance of IsOrderedRing R.
We call inst₃ the "source" of the transformation (it's what the projection is "forgetting from"). We call class-typed arguments other than the source "tributaries".
- NB: In auto-generated projections (IsStrictOrderedRing.toIsOrderedRing is not one), inst₃ would be called self. See e.g. IsStrictOrderedRing.toPosMulStrictMono.
Conditional tributary junctions (CTJ): When we add one or more Prop mixins to what would otherwise have been an unconditional tributary junction, we get a conditional tributary junction. Here, we have that, under the assumption that the mixins are satisfied, this junction is also essentially a projection in spirit. Nonetheless, CTJ's are out of scope for now.
- CTJs would need tie-breakers. For example:
```
IsNoetherianRing.wfDvdMonoid.{u} : forall {R : Type.{u}}
  [inst₁ : @CommSemiring.{u} R]
  [inst₂ : @IsDomain.{u} R (@CommSemiring.toSemiring.{u} R inst₁)]
  [h : @IsNoetherianRing.{u} R (@CommSemiring.toSemiring.{u} R inst₁)],
  @WfDvdMonoid.{u} R (@CommSemiring.toCommMonoidWithZero.{u} R inst₁)
```
  here, if we removed either the IsDomain R or IsNoetherianRing R mixins, we'd have a UTJ (as well as an impossible-to-prove signature, but that's beside the point) with h or inst₂ as sources, respectively. However, the signature per se doesn't tell us whether we should treat IsDomain R as the mixin or IsNoetherianRing R. One sensible heuristic would be to check the class names of the types against the namespace of the transformation, which in this case would pick h as the source and designate inst₂ as the mixin.
- CTJs can be tricky to detect reliably. Take the following non-example:
```
LeftCancelMonoid.groupOfFinite.{u} : forall {G : Type.{u}}
  [inst₁ : @LeftCancelMonoid.{u} G]
  [inst₂ : @Finite.{succ u} G],
  @Group.{u} G
```
  Here, if we adopted the namespace tie-breaker we suggested before, inst₁ would be chosen as the source, and inst₂ would be chosen as the mixin. But to call LeftCancelMonoid.groupOfFinite a projection from LeftCancelMonoid G to Group G conditioned on Finite G would flow in the opposite direction of strength, as Group G is strictly stronger than LeftCancelMonoid G (if inst : Group G, then @CancelMonoid.toLeftCancelMonoid G (@Group.toCancelMonoid G inst) yields an instance of LeftCancelMonoid G).
  Whether this would inherently be a problem further down the road is hard to say, but it contradicts our intent and hence motivates us to shelf this feature for now.

This module #

This module concerns itself with finding out what classes a declaration actually uses each of its targeted binders as (which we'll use to set the requirements that any weakening of that binder must still satisfy).

We use the following artificial declaration and proof as a guiding example:
theorem thm {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (r : R) (m : M) :
    r • (m + m) = r • m + r • m := smul_add r m m
Now, let sig be the Expr corresponding to {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (r : R) (m : M) : r • (m + m) = r • m + r • m, and let proof be the Expr corresponding to smul_add r m m.

For a given pair sig proof : Expr, where proof is the proof of sig, we begin by calling getTargetedBinders sig, which will assign each targeted (class) binder of sig an fvar, which we'll treat as the targeted binder's "canonical" fvar. To encode this "canonicity", we create the wrapper type BinderId around FVarId. These fvars are returned within an array of TargetedBinders, each containing a BinderId. The array obeys the order in which the targeted binders appear in sig. Call that array tbinders.

In our example, tbinders = #[inst₁, inst₂, inst₃], where inst₁ is the "canonical" fvar of the Ring R instance, inst₂ that of the AddCommGroup M instance, and inst₃ that of the Module R M instance.

Next, we call getMIChains tbinders sig proof. Now, getMIChains will telescope sig once more, generating fresh fvars for all binders. However, given that it's the same sig as was passed to getTargetedBinders, we can define a bijection between the targeted binder fvars from getTargetedBinders and the corresponding fvars generated by the telescope in getMIChains by using the fvars' positional indices within sig. We store this bijection as binderIdOf.

In our example, say that getMIChains's forallTelescope sig produces the binder fvars R' M' inst₁' inst₂' inst₃' r' m'. Then binderIdOf is the bijection {inst₁' ↦ inst₁, inst₂' ↦ inst₂, inst₃' ↦ inst₃} from getMIChains's targeted binder fvars inst₁' inst₂' inst₃' to their matching BinderIds.

After this bijection is established, getMIChains then walks

every binder's type,
the sig's conclusion, and
the proof term "syntactically applied" to getMIChains's telescope and β-reduced (the β-reduction is what transforms the syntactic application @proof R' M' inst₁' inst₂' inst₃' r' m' into an Expr of proof where all its binder bvars are replaced with the corresponding fvars from getMIChains's telescope).

Note: A targeted binder only appearing within another targeted binder's type, and nowhere else, does not mean that it is superfluous.

In our example, the things getMIChains will walk look like this:
"every binder's type": Type*, Type*, Ring R', AddCommGroup M', @_root_.Module R' M' (@Ring.toSemiring R' inst₁') (@AddCommGroup.toAddCommMonoid M' inst₂'), R', and M'.
"the sig's conclusion": @Eq M' (...) (...) (very long, with plenty of instance chains).
"the proof term applied to getMIChains's telescope and β-reduced":
@smul_add R' M'
(@AddMonoid.toAddZeroClass M'
  (@SubNegMonoid.toAddMonoid M' (@AddGroup.toSubNegMonoid M' (@AddCommGroup.toAddGroup M' inst₂'))))
(@DistribMulAction.toDistribSMul R' M' (@Semiring.toMonoid R' (@Ring.toSemiring R' inst₁'))
  (@SubNegMonoid.toAddMonoid M' (@AddGroup.toSubNegMonoid M' (@AddCommGroup.toAddGroup M' inst₂')))
  (@Module.toDistribMulAction R' M' (@Ring.toSemiring R' inst₁') (@AddCommGroup.toAddCommMonoid M' inst₂') inst₃'))
r' m' m'

walk is defined inductively over every possible Expr constructor. Its job is to find any spot where the elaborator put an instance transformation or root instance. It recurses through function applications, projections, lets, and fun and ∀ abstractions. In the case of fun and ∀ abstractions, it walks the domain type first, and then the body, with the abstracted bvar within it instantiated to a fresh fvar of the right type, since walk can't query the type of anything that contains a loose bvar.

As it recurses, there are exactly two spots at which walk will pass a subterm to route:

The subterm is an argument in an application.
The subterm is the base of a projection (.proj).

Once walk passes a subterm e to route, route decides what to do next based on the type of the subterm. If it's class-typed, it runs collect e none, starting a new chain. If it's not class-typed, route hands e back to walk to keep recursing on.

Assuming that the subterm is an instance chain, collect will record what class the chain is an instance of (i.e., the head of the subterm's outermost class application) and carry it with it as chainHead? as it descends the chain. At every instance transformation (e.g. Module.toDistribMulAction ...), collect will call walk on all non-class-typed arguments to ensure any instances that might have been involved in the construction of the non-class-typed argument are still taken into account. collect then asks whether this application is a tributary junction (i.e., whether one class-typed argument pins all the others) by consulting sourceArg?:

sourceArg? returns some src: collect continues the current chain by descending into src, carrying the head returned by propagatedHead? (which may be none, in which case the chain is dropped), and routes every other argument, starting a new chain at each class-typed one. This happens when the application is an unconditional tributary junction.
sourceArg? returns none: collect drops the current chain and routes every argument, starting a new chain at each class-typed one. This happens when the application is a confluence, currently also when it is a conditional tributary junction, and whenever the head has no source slot at all (a lone class-typed argument is not automatically the source; for example, in PProd.isEmpty_right {α : Sort u} {β : Sort v} [IsEmpty β] : IsEmpty (α ×' β), the only class-typed argument is IsEmpty β, which doesn't pin α and hence couldn't be the source).

Once the MIChains have been collected, getMIChains returns them. We then pass the chains to getReqs, which associates each chain to the corresponding TargetedBinder. It then converts each chain to a Requirement, and returns the requirements as an array.

In our example, the collected MIChains are
{ head := Monoid R', root := inst₁ } (4 times)
{ head := Semiring R', root := inst₁ } (5 times)
{ head := Add M', root := inst₂ } (2 times)
{ head := AddCommMonoid M', root := inst₂ } (5 times)
{ head := AddMonoid M', root := inst₂ } (4 times)
{ head := AddZeroClass M', root := inst₂ } (4 times)
{ head := Zero M', root := inst₂ } (3 times)
{ head := DistribSMul R' M', root := inst₃ } (1 time)
{ head := SMul R' M', root := inst₃ } (3 times)