Placeholder type mismatch in monad

Stream: lean4

[Horațiu Cheval]

The output of the following snippet

def bar : ExceptT String (StateM Int) Bool := do
  Except.error _

is

type mismatch
  Except.error ?m.55
has type
  Except ?m.53 ?m.54 : Type ?u.52
but is expected to have type
  ExceptT String (StateM Int) Bool : Type

The code is though correct and the placeholder is of type String:

def bar : ExceptT String (StateM Int) Bool := do
  Except.error ""

This makes the strategy of putting _s in your code to fill gradually based on the expected types a bit less reliable,
because if, like me, you're not really accustomed to monads, it can trick you into thinking that your doing something wrong without understanding why, while you're actually on the right path.

Why does this happen here? I assume it's some kind of inherent limitation of the way monad lifting works (which in general is very nice)?. Is there a different way I could've written the code so that _ would have worked as I expected it to?

[Sebastian Ullrich]

I would argue you are still doing something wrong. The proper way to throw an exception in ExceptT is to use throw _, there is no such issue there

[Horațiu Cheval]

Ok, thanks, good to know then!