Should Id be a structure?

Stream: lean4

[Eric Wieser]

It's very easy to forget Id.run and pure when working with the Id monad, resulting in defeq issues when silently casting between X and Id X. While core is now mostly free of these as of lean4#7352, it's still easy for them to end up reappearing in downstream projects, which lead users down dead ends like simp [Id.run, Pure.pure, Bind.bind], leaving them with a bad goal state.

Should Id be redefined as

structure Id (X : Type _) where
  /-- Not simp-normal, use Pure.pure instead. -/
  protected pure ::
  run : X

instance : Pure Id where pure := Id.pure

@[simp] theorem Id.pure_eq : Id.pure = Pure.pure := rfl

such that it is impossible to make this mistake?

[Niels Voss]

What's the difference between using a single element structure and removing @[expose] as a way to prevent defeqs?

[Yury G. Kudryashov]

With a 1-field structure, you still have .mk a.run = a as a defeq.

[Niels Voss]

Another difference is that for the 1-field structure, Id X = X (or equivalently, Id = id) becomes independent of Lean, which occasionally matters

[Eric Wieser]

Yury G. Kudryashov said:

With a 1-field structure, you still have .mk a.run = a as a defeq.

run (pure x) = x is the one we care about

[Tomas Skrivan]

YES please! When I was implementing automatic differentiation for monadic code the defeq abuse was a major pain point. At some point I just gave up an defined my own id monad.