structure not picking up unnecessary typeclass

Stream: lean4

[Kevin Buzzard]

So I think I understand what's going on here but just want to run it past the experts to check I'm understanding correctly.

I think I just learnt a change between Lean 3 and Lean 4, and I think I know the fix. Here's the change:

-- Lean 3
universes u v w

variables (F : Type u → Type v) [applicative F] [is_lawful_applicative F]
variables (G : Type u → Type w) [applicative G] [is_lawful_applicative G]

structure applicative_transformation : Type (max (u+1) v w) :=
(app : Π α : Type u, F α → G α)
(preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x)
(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y)

--- #print applicative_transformation
/-
structure applicative_transformation : Π (F : Type u → Type v) [_inst_1 : applicative F]
  [_inst_2 : is_lawful_applicative F] (G : Type u → Type w) [_inst_3 : applicative G]
  [_inst_4 : is_lawful_applicative G], Type (max (u+1) v w)
fields: ...
-/

vs

-- Lean 4
universe u v w

variable (F : Type u → Type v) [Applicative F] [LawfulApplicative F]
variable (G : Type u → Type w) [Applicative G] [LawfulApplicative G]

structure applicative_transformation : Type (max (u+1) v w) :=
(app : ∀ α : Type u, F α → G α)
(preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x)
(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y)

#print applicative_transformation
/-
inductive applicative_transformation.{u, v, w} : (F : Type u → Type v) →
  [inst : Applicative F] → (G : Type u → Type w) → [inst : Applicative G] → Type (max (u + 1) v w)
number of parameters: 4
...
-/

Forgive all the functor nonsense. The point I'm trying to make is that when defining the structure in Lean 3, I think what's going on is that Lean 3 says "OK so F's are mentioned so let's throw in the variable F and oh look it has some typeclasses associated to it so let's throw them in too". As a result, the definition of applicative_transformation F G demands both [applicative F] and [is_lawful_applicative F]. However in the Lean 4 version, Lean is smart enough to observe that in the actual definition of the declaration we do need F and we also need Applicative F but we don't actually need LawfulApplicative F (which is just a bunch of Props), so the declaration only asks that F be Applicative.

As a result, the unused arguments linter is complaining to me that I am occasionally asking for LawfulApplicative when I don't need to. If my understanding of the above is correct, then as far as I can see the correct fix is to observe that it's absolutely right and I should just delete the unused arguments (the Lean 3 unused arguments linter is not highlighting these because they are needed in Lean 3 because the structure declaraction has dragged them in).

Does this sound right or have I misunderstood what's going on?

[Floris van Doorn]

Sounds right to me.