Class params dependent on outParams

Stream: lean4

[James Gallicchio]

Looking at the definition of ForIn', the Membership parameter depends on the outParam of the declaration:

class ForIn' (m : Type u₁ → Type u₂) (ρ : Type u) (α : outParam (Type v)) (d : outParam $ Membership α ρ) where
  forIn' {β} [Monad m] (x : ρ) (b : β) (f : (a : α) → a ∈ x → β → m (ForInStep β)) : m β

is this member still filled via typeclass inference? if so, is it possible to make the notation more indicative of that behavior (maybe allow params of the form [outParam $ Membership α ρ] or something?)

[Henrik Böving]

In general all outParam's are filled via type class inference, at least that's my understanding.

If you mark a parameter of a certain type class as an outParam type class inference will start even without this parameter being inferred from the context already and then search for an instance which will in turn determine the value of the outParam. If that instance happens to figure out the Membership instance via type class inference itself it will be filled via that, if it figures it out statically it will be filled statically.

[James Gallicchio]

ah right, cuz it's set at the instance I guess