typeclass search being derailed despite out_params #1940
Description
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Reduced the issue to a self-contained, reproducible test case.
Description
The below classes are all in mathlib3, and a typeclass search which was succeeding in lean3 is failing in lean4.
class Preorder (α : Type _) where
class Zero (α : Type _) where
class One (α : Type _) where
-- this instance (in mathlib) is just here in this example to ensure that
-- typeclass search for `Preorder ?m_1` causes chaos;
instance {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] : Preorder (∀ i, α i) where
class MulZeroClass (M₀ : Type _) extends Mul M₀, Zero M₀ where
class MulOneClass (M : Type _) extends One M, Mul M where
class MulZeroOneClass (M₀ : Type _) extends MulOneClass M₀, MulZeroClass M₀
class FunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
class MulHomClass (F : Type _) (M N : outParam (Type _)) [Mul M] [Mul N]
extends FunLike F M fun _ => N where
class OneHomClass (F : Type _) (M N : outParam (Type _)) [One M] [One N]
extends FunLike F M fun _ => N where
class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N]
extends FunLike F M fun _ => N where
class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
extends MulHomClass F M N, OneHomClass F M N
class MonoidWithZeroHomClass (F : Type _) (M N : outParam (Type _)) [MulZeroOneClass M]
[MulZeroOneClass N] extends MonoidHomClass F M N, ZeroHomClass F M N
class OrderMonoidHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
[MulOneClass α] [MulOneClass β] extends MonoidHomClass F α β where
class OrderMonoidWithZeroHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
[MulZeroOneClass α] [MulZeroOneClass β] extends MonoidWithZeroHomClass F α β where
-- removing this instance makes the first `#synth` below succeed
instance (priority := 100) foo
{α β F : Type _} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β]
[OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
{ ‹OrderMonoidWithZeroHomClass F α β› with }
set_option synthInstance.maxHeartbeats 400 -- make trace manageable
set_option trace.Meta.synthInstance true
variable {α β F : Type _} [MulZeroOneClass α] [MulZeroOneClass β] [MonoidWithZeroHomClass F α β] in
#synth MonoidHomClass F α β -- fails
variable {α β F : Type _} [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β]
[OrderMonoidWithZeroHomClass F α β] in
#synth OrderMonoidHomClass F α β -- fails even though we just defined exactly this instanceIn Lean 3 typeclass inference gives up on the idea of Order having anything to do with the first problem, very quickly. But Lean 4 gets sucked into an infinite loop. Making alpha and beta outParams in the instance OrderMonoidWithZeroHomClass.toOrderMonoidHomClass doesn't seem to help.