Type mismatch related to an instance argument (very flaky)

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

In the presence of non-unique instances where either instance would produce a well-typed expression, Lean produces a "type mismatch" error that does not help.

Context

This issue occurred while I was trying yet another approach to avoid universe issues in the iterator library. The basic problem is that iterators have their state in some type α : Type u, but its monadic effects are happening in some (intuitively larger) universe Type w. For technical reasons, we need to be able to have a ULift-like equivalence from α into Type w. The idea is to introduce a ComputableUnivLE typeclass that works like UnivLE except that it provides a computable equivalence and, in particular, does not live in Prop. Therefore, there are many definitionally unequal instances of ComputableUnivLE.{u, v} (that are all equally good for my purposes).

While working with these instances, I need to be careful that I don't get type errors because a different instance is expected than used. However, the bug happens in a setting in which I think that the result should be valid no matter how the instances are resolved.

As far as I can tell, there's an easy fix for me (explicitly passing the desired instance to Iter), so I am not blocked by this bug.

Steps to Reproduce

Run this in Lean Web (I have worked a lot on minimizing it but can't get it any smaller; the comments indicate multiple places that play into the bug):

class ComputableUnivLE.{u, v} where
  Lift : Type u → Type v

instance ComputableUnivLE.self : ComputableUnivLE.{0, 0} where
  Lift α := sorry

instance ComputableUnivLE.ofMax [i : ComputableUnivLE.{v, v}] : ComputableUnivLE.{0, v} where
  Lift α := sorry

-- adding the zero instance _after `ofMax`_ resolves the errors
-- instance ComputableUnivLE.zero : ComputableUnivLE.{0, u} := sorry

class ComputableSmall.{v} (α : Type 0) where
  Lift : Type v

instance [ComputableUnivLE.{0, v}] {α} : ComputableSmall.{v} α where
  Lift := ComputableUnivLE.Lift α -- replacing this with sorry resolves the errors

structure Iter {α : Type 0} (m : Type w → Type 0) (β : Type 0) [ComputableSmall.{w} α] where

inductive T where
inductive W
inductive X
inductive Y
| y : Y

def Y.iter (l : Y) : Iter (α := X) Id W := sorry

-- replacing w with 0 resolves the errors
-- replacing m altogether with Id, too
@[inline]
def Iter.take {α : Type 0} {m : Type w → Type 0}
    -- exchanging ComputableUnivLE and n resolves the errors
    [ComputableUnivLE.{0, w}]
    (n : Nat) {_ : ComputableSmall.{w} α} (it : Iter (α := α) m W) : Iter (α := T) m W :=
  sorry

def flatMap {β : Type 0} {_ : ComputableSmall.{0} T} (f : β → Iter (α := T) Id W) (it : β) :
    W := sorry

/--
error: type mismatch
  Iter.take 1 x.iter
has type
  @Iter T Id W instComputableSmallOfComputableUnivLE : Type
but is expected to have type
  @Iter T Id W (?m.686 x✝) : Type
-/
#guard_msgs in
def fails :=
  flatMap (fun x => x.iter |>.take 1) Y.y
where
  x := 0

def succeeds :=
  flatMap (fun x => Y.iter x |>.take 1) Y.y
where
  x := 0

Expected behavior: [Clear and concise description of what you expect to happen]

Lean should accept the above snippet without errors. (If the snippet is actually invalid, which I don't think, I would like to get a helpful error message.)

Actual behavior: [Clear and concise description of what actually happens]

I get the error seen in the #guard_msgs comment above.

It does not really explain the problem: The only "mismatch" I can see is that the expected type has a metavariable the the actual type has a instComputableSmallOfComputableUnivLE instance. The types of both match perfectly, including the universe levels. I can't think of any reason why this should be a problem.

As described in the (Lean, not GitHub) comments, various seemingly unimportant changes cause the error to disappear.

Update: I also tried making the instance argument in the type of Iter into an explicit parameter. If I then pass inferInstance everywhere, the error disappears, too.

Versions

Lean 4.20.0-nightly-2025-04-16
Target: x86_64-unknown-linux-gnu

Impact

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

Start by running the minimal reproducer in the issue against the specified Lean nightly version, then compare the failing fails definition with the succeeding succeeds definition. The payload names no repository files or tests; done means accepting the snippet or producing a diagnostic that explains the instance mismatch.