Stack overflow during elaboration

[kmill]

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

From this example, it there seems there could be an invalid level metavariable assignment during elaboration, one that forms a loop.

Context

Reported on Zulip

Steps to Reproduce

namespace CategoryTheory
universe v v₁ v₂ v₃ u u₁ u₂ u₃ w₀ w₁

class Quiver (V : Type u) where Hom : V → V → Sort v
structure Functor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
class Cat (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
structure Iso {C : Type u} [Cat.{v} C] (X Y : C) where

def Functor.id (C : Type u₁) [Cat.{v₁} C] : Functor C C where

instance pi' {I : Type v₁} (C : I → Type u₁) [∀ i, Cat.{v₁} (C i)] :
    Cat (∀ i, C i) := sorry

variable {C : Type u₁} [Cat.{v₁} C] {D : Type u₂} [Cat.{v₂} D]
  (F : Functor C C)

instance Functor.category :
    Cat.{max u₁ v₂} (Functor C D) := sorry

#check Iso Functor.id F

Expected behavior: This raises a normal error.

Actual behavior: At #check there is a stack overflow.

Versions

Lean 4.15.0-nightly-2024-11-26
Target: x86_64-unknown-linux-gnuLean 4

Additional Information

I tested this locally too on macOS. There are tens of thousands of stack frames for libleanshared.dylib`lean::instantiate_lmvars_fn::visit(lean::level const&). This is what leads me to guess that there is an invalid universe level assignment somewhere.

Impact

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