Instance diamonds depending on `outParam`s

Stream: general

[Anne Baanen]

Here's an interesting edge case in the typeclass system I came across in #16919 involving outParams. Suppose we have a chain of instances Top α β → Middle α β → Bot α β, where β is an outParam, and both take an instance on β as a parameter. If the classes on β arise from diamond inheritance, Lean 3 can't find the desired instance automatically:

set_option old_structure_cmd true

class Root (α : Type) : Type :=
(blah : α)
class Left (α : Type) extends Root α
class Right (α : Type) extends Root α
class Leaf (α : Type) extends Left α, Right α

class Bottom (_ : Type) (β : out_param Type) [Root β]
class Middle (α : Type) (β : out_param Type) [Root β]
class Top (α : Type) (β : out_param Type) [Root β]

instance Top.toMiddle {α β} [Left β] [Top α β] : Middle α β := {}
instance Middle.toBottom {α β} [Right β] [Middle α β] : Bottom α β := {}

set_option trace.class_instances true
set_option trace.type_context.is_def_eq_detail true

instance Top.toBottom {α β} [Leaf β] [Top α β] : Bottom α β :=
by apply_instance -- Fails

The reason for this issue is as follows. After we apply Middle.toBottom we want to apply Top.toMiddle, so we need to unify @Middle ?x_3 ?x_4 (@Right.to_Root ?x_4 ?x_5) arising from Middle.toBottom with @Middle ?x_7 ?x_8 (@Left.to_Root ?x_8 ?x_9) arising from Top.toMiddle. To unify (@Right.to_Root ?x_4 ?x_5) =?= (@Left.to_Root ?x_8 ?x_9) we need to fill in a value for the metavariables (which will be β). But the value of this metavariable is only available through unification with Top.toMiddle, so we are stuck in a dependency cycle.

[Anne Baanen]

On the other hand, Lean 4 can successfully find this instance:

import Std.Tactic.Lint

class Root (α : Type) : Type where
(blah : α)
class Left (α : Type) extends Root α
class Right (α : Type) extends Root α
class Leaf (α : Type) extends Left α, Right α

class Bottom (_ : Type) (β : outParam Type) [Root β]
class Middle (α : Type) (β : outParam Type) [Root β]
class Top (α : Type) (β : outParam Type) [Root β]

instance Top.toMiddle [Left β] [Top α β] : Middle α β where
instance Middle.toBottom [Right β] [Middle α β] : Bottom α β where

set_option trace.Meta.synthInstance true

instance Top.toBottom [Leaf β] [Top α β] : Bottom α β :=
inferInstance -- Succeeds

However, the dangerous instance linter is not satisfied:

/- The `dangerousInstance` linter reports:
SOME INSTANCES ARE DANGEROUS
During type-class search, they produce subgoals like `Group ?M`.
Try marking the dangerous arguments as implicit instead. -/
#check @Top.toMiddle /- generates subgoals with metavariables: argument 3 inst✝¹ : Left ?β -/
#check @Middle.toBottom /- generates subgoals with metavariables: argument 3 inst✝¹ : Right ?β -/

[Anne Baanen]

This seems to be caused by Lean 4 going ahead and solving the Leaf ?β instance with backtracking. For example, if I try to confuse matters by adding in more Leaf instances, we see the backtracking:

instance Top.toBottom [correctInst : Leaf β] [badInst1 : Leaf Nat] [badInst2 : Right Int] [Top α β] : Bottom α β :=
inferInstance -- succeeds
/--
  [] new goal Bottom α _tc.0 ▶
  [] ✅ apply @Middle.toBottom to Bottom α ?m.332 ▼
    [tryResolve] ✅ Bottom α ?m.332 ≟ Bottom α ?m.332 ▼
      [synthInstance] 💥 Right ?m.332 ▶
      [synthInstance] 💥 Right ?m.332 ▼
        [] new goal Right ?m.332 ▼
          [instances] #[@Leaf.toRight, badInst2]
        [] 💥 apply badInst2 to Right ?m.332 ▼
          [tryResolve] 💥 Right ?m.332 ≟ Right Int
    [] new goal Right _tc.0 ▼
      [instances] #[@Leaf.toRight, badInst2]
  [] ✅ apply badInst2 to Right Int ▶
  [resume] propagating Right Int to subgoal Right Int of Bottom α Int ▶
  [] ❌ apply @Top.toMiddle to Middle α Int ▶
  [] ✅ apply @Leaf.toRight to Right ?m.356 ▼
    [tryResolve] ✅ Right ?m.356 ≟ Right ?m.356
    [] new goal Leaf _tc.0 ▶
  [] ✅ apply badInst1 to Leaf Nat ▼
    [tryResolve] ✅ Leaf Nat ≟ Leaf Nat
  [resume] propagating Leaf Nat to subgoal Leaf Nat of Right Nat ▶
  [resume] propagating Right Nat to subgoal Right Nat of Bottom α Nat ▶
  [] ✅ apply @Top.toMiddle to Middle α Nat ▶
  [] ✅ apply @Leaf.toLeft to Left Nat
  [resume] propagating Left Nat to subgoal Left Nat of Middle α Nat ▶
  [] ❌ apply inst✝ to Top α Nat ▶
  [] ✅ apply correctInst to Leaf β ▶
  [resume] propagating Leaf β to subgoal Leaf β of Right β ▶
  [resume] propagating Right β to subgoal Right β of Bottom α β ▶
  [] ✅ apply @Top.toMiddle to Middle α β ▶
  [] ✅ apply @Leaf.toLeft to Left β
  [resume] propagating Left β to subgoal Left β of Middle α β ▶
  [] ✅ apply inst✝ to Top α β ▶
  [resume] propagating Top α β to subgoal Top α β of Middle α β ▶
  [resume] propagating Middle α β to subgoal Middle α β of Bottom α β ▶
  [] result Middle.toBottom
-/

[Anne Baanen]

Finally, if we follow the dangerousInstance linter and turn the instance parameters into implicits, the example breaks in Lean 4 for the same reason as in Lean 3:

import Std.Tactic.Lint

class Root (α : Type) : Type where
(blah : α)
class Left (α : Type) extends Root α
class Right (α : Type) extends Root α
class Leaf (α : Type) extends Left α, Right α

class Bottom (_ : Type) (β : outParam Type) [Root β]
class Middle (α : Type) (β : outParam Type) [Root β]
class Top (α : Type) (β : outParam Type) [Root β]

instance Top.toMiddle {_ : Left β} [Top α β] : Middle α β where
instance Middle.toBottom {_ : Right β} [Middle α β] : Bottom α β where

set_option trace.Meta.synthInstance true

instance Top.toBottom [Leaf β] [Top α β] : Bottom α β :=
inferInstance -- Failed
/-
[Meta.synthInstance] ❌ Bottom α β ▼
  [] new goal Bottom α _tc.0 ▶
  [] ✅ apply @Middle.toBottom to Bottom α ?m.322 ▶
  [] ❌ apply @Top.toMiddle to Middle α ?m.322 ▼
    [tryResolve] ❌ Middle α ?m.322 ≟ Middle ?m.340 ?m.339 ▼
      [synthInstance] 💥 Right ?m.339 ▼
        [] new goal Right ?m.339 ▶
        [] ✅ apply @Leaf.toRight to Right ?m.339 ▶
        [] 💥 apply inst✝¹ to Leaf ?m.339 ▼
          [tryResolve] 💥 Leaf ?m.339 ≟ Leaf β
      [synthInstance] 💥 Left ?m.339 ▶
      [synthInstance] 💥 Right ?m.339 ▶
      [synthInstance] 💥 Left ?m.339 ▶
-/

[Anne Baanen]

I'm not entirely sure what the conclusion is supposed to be. We can see it is possible to make this construction work, and it certainly does arise naturally in mathlib (since I came across it in #16919), so I'd love for this to just work unconditionally. But the elaboration order to make this work without backtracking is highly nontrivial.

[Anne Baanen]

Perhaps the conclusion is that we shouldn't have instances that take instance parameters depending on outParams only, and instead only do constructions like this:

class Root (α : Type) : Type where
(blah : α)
class Left (α : Type) extends Root α
class Right (α : Type) extends Root α
class Leaf (α : Type) extends Left α, Right α

class ParamProvider (α : Type) (β : outParam Type)

class Bottom (α : Type) (β : Type) [ParamProvider α β] [Root β]
class Middle (α : Type) (β : Type) [ParamProvider α β] [Root β]
class Top (α : Type) (β : Type) [ParamProvider α β] [Root β]

instance Top.toMiddle [ParamProvider α β] [Left β] [Top α β] : Middle α β where
instance Middle.toBottom [ParamProvider α β] [Right β] [Middle α β] : Bottom α β where

instance Top.toBottom [ParamProvider α β] [Leaf β] [Top α β] : Bottom α β :=
inferInstance

That is, unbundled inheritance from FunLike and SetLike.