RFC: ForIn keys on the value rather than the type

Proposal

Currently, ForIn has the following type:

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

Note in particular that the class depends on ρ (the collection type) but not (x : ρ) (the particular collection being iterated over). This means that it is impossible to implement an iterator where the yielded element type depends on the value:

for x in (g : MyGraph) do
  -- x : VertexOf g

The current workaround for this is to define a wrapper type structure ElementOf (g : MyGraph) but this requires some boilerplate to set up, complicates usage code, and is also not very discoverable.

The way this situation can be improved is to move the (x : ρ) argument to a parameter, so that it can participate in typeclass inference such that α can depend on x:

class ForIn (m : Type u₁ → Type u₂) {ρ : Sort u} (x : ρ) (α : outParam (Sort v)) where
  forIn {β} [Monad m] (b : β) (f : α → β → m (ForInStep β)) : m β

(Note, I've also changed Type to Sort in two places here. I believe the use of Type in this position is not necessary, but this can be considered separately if desired.)

This impacts mainly users of the ForIn typeclass, namely libraries for programming such as Batteries, as well as users that have set up their own iterable collection types.

Community Feedback

This was recently discussed on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start with the ForIn class declaration shown in the issue, then inspect its downstream users, especially Batteries and custom iterable collection types. Evaluate how moving the collection value into the class parameters affects typeclass inference and dependent yielded types, and consider the proposed Sort changes separately. Done means a reviewed design or implementation that supports the MyGraph/VertexOf g example without the ElementOf wrapper and accounts for affected users.