Algebra.Module.Equiv mathlib4#1732

Stream: mathlib4

[Jakob von Raumer]

I have the issue that we can't infer FunLike (M ≃ₛₗ[σ] M₂) M (fun _ => M₂) anymore, which I think might either be because, as #lint says, there's something wrong with the instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M M₂ or, as the trace says, type class inference is running into some really weird dead end:

(Module.EndCat
          (Module.EndCat
            (Module.EndCat
              (Module.EndCat
                (Module.EndCat
                  (Module.EndCat
                    (Module.EndCat
                      (Module.EndCat
                        (Module.EndCat (Module.EndCat (Module.EndCat (Module.EndCat (Module.EndCat ℕ M₂) M₂) M₂) M₂) M₂)
                        M₂)
                      M₂)
                    M₂)
                  M₂)
                M₂)
              M₂)
            M₂)
          M₂)
````

[Jakob von Raumer]

Looks like @LinearMap.applyModule shouldn't be an instance, then?

[Anne Baanen]

I suppose most instances on Module.EndCat are going to give issues since it's merely an abbrev. So probably we'll have to make EndCat @[irreducible]?

[Eric Wieser]

docs4#LinearMap.applyModule doesn't need to be an instance on EndCat if that's causing problems'; the instance would have been fine in Lean 3 on M →ₗ[R] M too

[Eric Wieser]

also docs4#Module.EndCat is a porting error, and should be called Module.End to match docs4#Monoid.End (https://github.com/leanprover-community/mathlib4/pull/1778)

[Jakob von Raumer]

Eric Wieser said:

docs4#LinearMap.applyModule doesn't need to be an instance on EndCat if that's causing problems'; the instance would have been fine in Lean 3 on M →ₗ[R] M too

That's not it, changing it to M →ₗ[R] M gives the same chain

[Eric Wieser]

It's good to know that the abbrev isn't the cause. This instance wasn't a problem in Lean 3...

[Jakob von Raumer]

Maybe it's the other problem I described above and it only runs into the dead end because it does not find the correct instance before.

[Jakob von Raumer]

So why is instance : SemilinearEquivClass (M ≃ₛₗ[σ] M₂) σ M, according to #lint, causing

#check @SemilinearEquivClass.instSemilinearMapClass /- generates subgoals with metavariables: argument 6 inst✝⁷ : Semiring
  ?R, argument 7 inst✝⁶ : Semiring
  ?S, argument 8 inst✝⁵ : AddCommMonoid
  ?M, argument 9 inst✝⁴ : AddCommMonoid ?M₂, argument 14 inst✝¹ : RingHomInvPair ?σ ?σ' -/

[Jakob von Raumer]

Jakob von Raumer said:

Maybe it's the other problem I described above and it only runs into the dead end because it does not find the correct instance before.

Oh wait, that can't really be the case becaus it successfully infers EmbeddingLike (M ≃ₛₗ[σ] M₂) M M₂

[Jakob von Raumer]

I think I solved those issues by adding a FunLike instance which hopefully is not a doublet

[Eric Wieser]

What's the new instance?

[Jakob von Raumer]

instance : FunLike (M ≃ₛₗ[σ] M₂) M (fun _ => M₂) := ⟨(·.toFun),
  fun _ _ _ => by { apply toLinearMap_injective; apply FunLike.coe_injective; assumption } ⟩

[Eric Wieser]

That's a bad instance, because it unfolds to the wrong thing

[Eric Wieser]

instance : FunLike (M ≃ₛₗ[σ] M₂) M (fun _ => M₂) := ⟨FunLike.coe,
  fun _ _ _ => by { apply toLinearMap_injective; apply FunLike.coe_injective; assumption } ⟩

would be ok

[Jakob von Raumer]

Your suggestion only makes sense if there's already a FunLike instance.

[Jakob von Raumer]

There might or might not be one, but adding one definitely solves type inferernce running into the :end: :cat: problem

[Eric Wieser]

Jakob von Raumer said:

Your suggestion only makes sense if there's already a FunLike instance.

There is, via SemilinearEquivClass.instSemilinearMapClass

[Eric Wieser]

Perhaps providing the SemilinearMapClass instance directly helps?

[Eric Wieser]

That doesn't have the problem of unfolding badly like your approach does

[Jakob von Raumer]

I still don't really get whether the EndCat dead end and the FunLike instance not being found are two separate issues or just one

[Jakob von Raumer]

Eric Wieser said:

Perhaps providing the SemilinearMapClass instance directly helps?

This works:

instance : FunLike (M ≃ₛₗ[σ] M₂) M (fun _ => M₂) := EmbeddingLike.toFunLike

[Eric Wieser]

That looks safe to me

[Jakob von Raumer]

Still bad that it's needed at all to not descent into the EndCat stuff

[Eric Wieser]

We had this type of shortcut instance in Lean3, implemented in the style you suggested earlier

[Eric Wieser]

For now we've just removed all those shortcuts because they mean the wrong thing with the new coe

[Eric Wieser]

But maybe we should instead be replacing them with shortcuts in the style of your most recent suggestion

[Johan Commelin]

@Jakob von Raumer Note that EndCat was an oopsie by mathport. It should just be called End. This has been fixed in master.

[Eric Wieser]

(docs4#Module.End)

[Jakob von Raumer]

But right now, in Lean 3 we don't require any short cut, or am I missing something?

[Jakob von Raumer]

@Johan Commelin Thanks, just using it as a catchy name for the issue described at the start of the thread here :grinning_face_with_smiling_eyes:

[Jakob von Raumer]

When trace.Meta.synthInstance says apply X to Y, then Y must have been a subgoal before, right? Because I don't know why it attempts to solve Module (Module.EndCat ?m.64808 M₂) M₂ in the first place, that is obviously a bad subgoal to have with that metavar.

[Jakob von Raumer]

Okay, the error is definitely not in Algebra.Module.Equiv itself: Inferring FunLike (R →+* S) R fun a => S runs into the same :cat: issue

[Eric Wieser]

Does the error message actually mention Cat? Can you give a mwe?

[Jakob von Raumer]

Took me a while to actually get the message to display, since it's too big to handle, but it does not mention the cat, instead it gets worked up in this:

 [] ✅ apply Nat.addMonoid to AddMonoid ℕ ▶
  [resume] propagating AddMonoid ℕ to subgoal AddMonoid ℕ of AddMonoid ℕᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈ to subgoal AddMonoid ℕᵒᵈ of AddMonoid ℕᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶
  [resume] propagating AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ to subgoal AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ of AddMonoid ℕᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈᵒᵈ ▶

[Jakob von Raumer]

Aha, all is good at the top of the file, but this instance seems to break it already:

[Jakob von Raumer]

instance (priority := 100) [RingHomInvPair σ σ'] [RingHomInvPair σ' σ]
    [s : SemilinearEquivClass F σ M M₂] : SemilinearMapClass F σ M M₂ :=
  { s with
    coe := (s.coe : F → M → M₂)
    coe_injective' := @FunLike.coe_injective F _ _ _ }

[Jakob von Raumer]

I thin I'm close to getting what's wrong

[Jakob von Raumer]

Nah I don't

[Jakob von Raumer]

But I guess it's just that the linter's warning that the instance is dangerious is on point...

[Jakob von Raumer]

-- σ' becomes a metavariable, but it's OK since it's an outparam the comment above it says

[Anne Baanen]

The Lean 4 dangerous instance linter now handles outParams correctly, so I don't think we should easily assume false positives anymore. In this case the comment is probably not applicable anymore. In particular the comment doesn't apply anymore: Lean 3 metavariables would block synthesis, so Lean would first search for a RingHomInvPair instance, find a value for σ' and be ready to start inferring the rest. Lean 4 often proceeds with synthesis even if there are still metavariables, so the presence of outParams doesn't help.

[Jakob von Raumer]

@Sebastian Ullrich has meanwhile pointed me to the existence of the attribute @[infer_tc_goals_rl] which does solve the issue for this particular instance. Not sure if it's a super stable workaround, though

[Jakob von Raumer]

Should be ready to review, with the @[infer_tc_goals_rl] trick at least