has_seq vs Seq

Stream: mathlib4

[Jireh Loreaux]

Note that in Lean 3:

has_seq.seq : Π {α β : Type u}, f (α → β) → f α → f β

whereas in Lean 4:

Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

What are we supposed to do about this? For example, in control.functor there is functor.comp.seq which then gets made into a has_seq instance for functor.comp. On the Lean 4 side should I change the type of Functor.Comp.seq so that it will match the Seq instance? If I do that do I need to #align it with an ₓ? I'm not sure what the protocol is here.

[Mario Carneiro]

On the Lean 4 side should I change the type of Functor.Comp.seq so that it will match the Seq instance?

Yes. The reason for the signature change is that the second argument to seq should be lazily evaluated, and function arguments are eagerly evaluated so anything that wraps a seq instance also needs to have the Unit -> unless f is already known to be a function.

If I do that do I need to #align it with an ₓ? I'm not sure what the protocol is here.

Yes, that seems like the least breaking way to do this. You will still get errors at all uses of the constant but I think the breakage will be more localized.