Monad instances and operations for `Except ε` and `ExceptT ε Id` are not definitionally equal

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following test case fails because instance : Monad (Except ε) is entirely different to instance : Monad (ExceptT ε Id), similarly for other specialised operations:

example ε : ExceptT.instMonad (ε:=ε) (m:=Id) = Except.instMonad (ε:=ε) := rfl -- fails
example ε α : @ExceptT.pure ε Id _ α = @Except.pure ε α := rfl -- OK
example ε α β : @ExceptT.map ε Id _ α β = @Except.map ε α β := rfl -- fails
example ε α β : @ExceptT.adapt ε Id _ α β = @Except.mapError ε α β := rfl -- OK
example ε α β : @ExceptT.bind ε Id _ α β = @Except.bind ε α β := rfl -- fails
example ε α β : @ExceptT.tryCatch ε Id _ α β = @Except.tryCatch ε α β := rfl -- OK

Expected behavior: All equalities should hold definitionally.

Actual behavior: Some hold, some don't.

Solution

The resolution, at least for the monad instance, is simple:

@[always_inline]
instance (ε) : Monad (Except ε) := inferInstanceAs (Monad (ExceptT ε Id))

For fixing the other equalities, it would be preferable to define the Except operations after and in terms of the ExceptT ones. There might affect the order of rendered documentation. Do we care? Can we prevent this?

Versions

Lean 4.19.0 dev commit

Impact

This makes it hard to reuse instances of ExceptT for Except in the monadic program logic work.
ExceptT is already very tiresome to handle because of all the splitting involved; having to redo all the work for Except makes this doubly annoying.

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the Except and ExceptT definitions and the Monad, map, adapt, bind, and tryCatch operations shown in the reproducer; compare how the specialised operations are defined. Run the minimal standalone examples against Lean nightly, with completion indicated when all listed equalities reduce definitionally with rfl.