WriterT type variation on port

Stream: mathlib4

[Arien Malec]

In control.monad.writer, writer_t is a structure. As ported, it looks like

structure WriterT (ω : Type u) (m : Type u → Type v) (α : Type u) : Type max u v where
  run : m (α × ω)

In the stub ported Control.Writer, WriterT is a def:

def WriterT (ω : Type u) (M : Type u → Type v) (α : Type u) : Type v :=
  M (α × ω)

Except for universes, the types are identical.

This difference isn't possible to #align away, for callers that rely, e.g., on naked constructors, or use proofs that rely on constructors.

I think all such callers are within Control.Writer.WriterT (grepping across the mathlib codebase, it seems so), but it might be better just to follow the structure based definition of the existing code (which would also resolve the difference is universes).

[Mario Carneiro]

removing a structure is something we can #align

[Mario Carneiro]

adding a structure is not

[Mario Carneiro]

(well, we can align it regardless, it will just break sometimes)

[Mario Carneiro]

Lean 4 generally prefers structures for this kind of thing though; I would follow the examples in core here

[Arien Malec]

What I mean here is I can construct a WriterT with the original syntax as ⟨pure (a, 1)⟩ which fails for the def because there's no constructor, and I can destructure via tactics, which fails for the def.

But no issue since I'll go with structure here...

[Richard Osborn]

When I looked at this earlier, the lean4 version of ReaderT switched to using def instead of structure.