FunLike issues

Stream: mathlib4

[Frédéric Dupuis]

I've just hit what looks like a very scary issue when trying to port Algebra.Order.Hom.Monoid in mathlib4#944. If you look at the instance [OrderMonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) in that PR, you'll see that when proving map_one, (1) the type class system is struggling to get the OneHomClass instance it needs, and (2) when it is supplied manually, we run into the issue that @FunLike.coe F α (fun a ↦ β) MulHomClass.toFunLike f 1 is apparently not defeq with @FunLike.coe F α (fun a ↦ β) OneHomClass.toFunLike f 1. This looks eerily reminiscent of issues that we had in mathlib3 when not using old_structure_cmd to define these objects. Does anyone have any insights about how to fix this?

[Jireh Loreaux]

I think we don't want CoeTC here, but I'm not sure if changing it will fix the problem.

[Eric Wieser]

I find it very hard to believe those are not defeq. Is this just another synthesized/unified clash again? How did you test if they were defeq?

[Kevin Buzzard]

      map_one' := by
        letI : MonoidHomClass F α β := MonoidWithZeroHomClass.toMonoidHomClass
        exact map_one f

You had haveI instead of letI, so the data was being forgotten.

[Kevin Buzzard]

That resolves the second issue, but the first one is still confusing to me:

attribute [instance] MonoidWithZeroHomClass.toMonoidHomClass -- presumably it's an instance,
-- even though this is not possible to easily check in Lean 4

instance [OrderMonoidWithZeroHomClass F α β] : CoeTC F (α →*₀o β) :=
  ⟨fun f =>
    -- comment out the next line and the proof breaks
    -- `:= inferInstance` also fails here (deterministic timeout)
    letI : MonoidHomClass F α β := MonoidWithZeroHomClass.toMonoidHomClass;
    { toFun := f,
      map_one' := map_one f
      map_zero' := map_zero f,
      map_mul' := map_mul f
      monotone' := OrderMonoidWithZeroHomClass.Monotone f }⟩

[Kevin Buzzard]

The fact that it's a deterministic timeout rather than just an "i give up" makes me wonder if typeclass inference is getting into some kind of loop. Can someone remind me how to look at instance traces in Lean 4? I don't think I've done this before. I tried set_option trace.Meta.synthInstance true but all I got was

[Meta.synthInstance] 💥 MonoidHomClass F α β ▶

which is certainly funny, but also not helpful enough

[Kevin Buzzard]

trace.png
The various options I've found all have defeq docstrings :-(

[Kevin Buzzard]

set_option trace.Meta.synthInstance.tryResolve true

generates so much output that it crashes VS Code :-(

[Kevin Buzzard]

(in the same file in the same PR):

-- this is in the file already
-- See note [lower instance priority]
instance (priority := 100) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
    [OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
  { ‹OrderMonoidWithZeroHomClass F α β› with }

-- this is where the experiment starts
variable [OrderMonoidWithZeroHomClass F α β] in
#synth OrderMonoidHomClass F α β -- fails

Am I doing something wrong? It doesn't work if you change the priority to 100000000000000 either.

[Kevin Buzzard]

OK so here is a not particularly MWE of the borkage:

import Mathlib.Algebra.Hom.Group

variable [MulZeroOneClass α] [MulZeroOneClass β] [MonoidWithZeroHomClass F α β] in
#synth MonoidHomClass F α β -- works

This file works as it stands on master. On branch dupuisf/algebra/order/hom/monoid (which has a half-finished Algebra.Order.Hom.Monoid) if you replace lines 177ff of Algebra.Order.Hom.Monoid with

-- See note [lower instance priority]
instance (priority := 100) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
    [OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
  { ‹OrderMonoidWithZeroHomClass F α β› with }
#align
  order_monoid_with_zero_hom_class.to_order_monoid_hom_class OrderMonoidWithZeroHomClass.toOrderMonoidHomClass

end MonoidWithZero

variable [MulZeroOneClass α] [MulZeroOneClass β] [MonoidWithZeroHomClass F α β] in
#synth MonoidHomClass F α β -- now fails

#exit

then it doesn't work any more. Instead, the #synth fails with a timeout. So this instance OrderMonoidWithZeroHomClass.toOrderMonoidHomClass seems to me to be introducing a loop. I am eager to learn how to diagnose this further, but cannot figure out how to look at the traces myself. This failure is very strange to me because the failing #synth has nothing to do with the Order heirarchy.

[Kevin Buzzard]

Here's a version which demonstrates the issue on mathlib4 master:

import Mathlib.Algebra.Hom.Group
import Mathlib.Order.Hom.Basic

variable {F α β : Type _}

class OrderMonoidHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
  [MulOneClass α] [MulOneClass β] extends MonoidHomClass F α β where
  Monotone (f : F) : Monotone f

class OrderMonoidWithZeroHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
  [MulZeroOneClass α] [MulZeroOneClass β] extends MonoidWithZeroHomClass F α β where
  Monotone (f : F) : Monotone f

-- deleting this instance makes the below #synth work
instance (priority := 100) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
    [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β]
    [OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β :=
  { ‹OrderMonoidWithZeroHomClass F α β› with }

variable [MulZeroOneClass α] [MulZeroOneClass β] [MonoidWithZeroHomClass F α β] in
#synth MonoidHomClass F α β -- fails

Removing mathlib is harder: I tried here but couldn't reproduce as yet, #synth succeeds. If I could figure out how to see the traces I'd know which instances are missing in my mathlib-free failed MWE attempt. I think I'm going to have to leave this now; any help with figuring out how to see which instances Lean is getting confused by is welcome! Let me stress again that something very weird is going on here -- this MWE adds two new order-releated classes and an instance relating them; this then makes a type class inference search whch has nothing to do with orders fail.

[Mario Carneiro]

Kevin Buzzard said:

The fact that it's a deterministic timeout rather than just an "i give up" makes me wonder if typeclass inference is getting into some kind of loop. Can someone remind me how to look at instance traces in Lean 4? I don't think I've done this before. I tried set_option trace.Meta.synthInstance true but all I got was

[Meta.synthInstance] 💥 MonoidHomClass F α β ▶

which is certainly funny, but also not helpful enough

That line is a link

[Kevin Buzzard]

oh cool! Indeed, it's a link which crashes VS Code. Edit: set_option synthInstance.maxHeartbeats 400 saves me. Thanks a lot!

[Kevin Buzzard]

[] ✅ apply OrderDual.instPreorderOrderDual to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) →
            (i_3 : ?m.1278 i i_1 i_2) →
              (i_4 : ?m.1458 i i_1 i_2 i_3) →
                (i_5 : ?m.1674 i i_1 i_2 i_3 i_4) →
                  (i_6 : ?m.1926 i i_1 i_2 i_3 i_4 i_5) →
                    (i_7 : ?m.2214 i i_1 i_2 i_3 i_4 i_5 i_6) →
                      (i_8 : ?m.2538 i i_1 i_2 i_3 i_4 i_5 i_6 i_7) →
                        Preorder (?m.2753 i i_1 i_2 i_3 i_4 i_5 i_6 i_7 i_8)ᵒᵈ

Is this bad?

[Yaël Dillies]

An auto-implicit issue?

[Kevin Buzzard]

definitely not.

[Mario Carneiro]

searching for a preorder on a metavar means we applied a dangerous instance. Goals should not be metavars or it will enumerate all preorders

[Mario Carneiro]

you should look for who introduced that

[Kevin Buzzard]

[Meta.synthInstance] 💥 MonoidHomClass F α β ▼
  [] new goal MonoidHomClass F _tc.0 _tc.1 ▶
  [] ✅ apply @OrderMonoidHomClass.toMonoidHomClass to MonoidHomClass F ?m.848 ?m.849 ▶
  [] ✅ apply @OrderMonoidWithZeroHomClass.toOrderMonoidHomClass to OrderMonoidHomClass F ?m.869 ?m.870 ▶
  [] ✅ apply @WithTop.preorder to Preorder (WithTop ?m.911) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to Preorder (?m.914 →o ?m.915) ▶
  [] ✅ apply @WithTop.preorder to Preorder (WithTop ?m.930) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to Preorder (?m.934 →o ?m.935) ▶
  [] ✅ apply Prod.instPreorderProd to Preorder (?m.939 × ?m.940) ▶
  [] ✅ apply OrderDual.instPreorderOrderDual to Preorder ?m.944ᵒᵈ ▶
  [] ✅ apply @Subtype.instPreorderSubtype to Preorder (Subtype ?m.949) ▶
  [] ✅ apply @WithBot.preorder to Preorder (WithBot ?m.951) ▶
  [] ✅ apply @instPreorderForAll to Preorder ((i : ?m.954) → ?m.955 i) ▶
  [] ✅ apply @WithTop.preorder to (i : ?m.954) → Preorder (WithTop (?m.972 i)) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to (i : ?m.954) → Preorder (?m.981 i →o ?m.982 i) ▶
  [] ✅ apply Prod.instPreorderProd to (i : ?m.954) → Preorder (?m.991 i × ?m.992 i) ▶
  [] ✅ apply OrderDual.instPreorderOrderDual to (i : ?m.954) → Preorder (?m.1001 i)ᵒᵈ ▶
  [] ✅ apply @Subtype.instPreorderSubtype to (i : ?m.954) → Preorder (Subtype (?m.1011 i)) ▶
  [] ✅ apply @WithBot.preorder to (i : ?m.954) → Preorder (WithBot (?m.1018 i)) ▶
  [] ✅ apply @instPreorderForAll to (i : ?m.954) → Preorder ((i_1 : ?m.1026 i) → ?m.1027 i i_1) ▶
  [] ✅ apply @WithTop.preorder to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (WithTop (?m.1050 i i_1)) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (?m.1064 i i_1 →o ?m.1065 i i_1) ▶
  [] ✅ apply Prod.instPreorderProd to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (?m.1079 i i_1 × ?m.1080 i i_1) ▶
  [] ✅ apply OrderDual.instPreorderOrderDual to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (?m.1094 i i_1)ᵒᵈ ▶
  [] ✅ apply @Subtype.instPreorderSubtype to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (Subtype (?m.1109 i i_1)) ▶
  [] ✅ apply @WithBot.preorder to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder (WithBot (?m.1121 i i_1)) ▶
  [] ✅ apply @instPreorderForAll to (i : ?m.954) → (i_1 : ?m.1026 i) → Preorder ((i_2 : ?m.1134 i i_1) → ?m.1135 i i_1 i_2) ▶
  [] ✅ apply @WithTop.preorder to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (WithTop (?m.1164 i i_1 i_2)) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (?m.1183 i i_1 i_2 →o ?m.1184 i i_1 i_2) ▶
  [] ✅ apply Prod.instPreorderProd to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (?m.1203 i i_1 i_2 × ?m.1204 i i_1 i_2) ▶
  [] ✅ apply OrderDual.instPreorderOrderDual to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (?m.1223 i i_1 i_2)ᵒᵈ ▶
  [] ✅ apply @Subtype.instPreorderSubtype to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (Subtype (?m.1243 i i_1 i_2)) ▶
  [] ✅ apply @WithBot.preorder to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder (WithBot (?m.1260 i i_1 i_2)) ▶
  [] ✅ apply @instPreorderForAll to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → Preorder ((i_3 : ?m.1278 i i_1 i_2) → ?m.1279 i i_1 i_2 i_3) ▶
  [] ✅ apply @WithTop.preorder to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (WithTop (?m.1314 i i_1 i_2 i_3)) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (?m.1338 i i_1 i_2 i_3 →o ?m.1339 i i_1 i_2 i_3) ▶
  [] ✅ apply Prod.instPreorderProd to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (?m.1363 i i_1 i_2 i_3 × ?m.1364 i i_1 i_2 i_3) ▶
  [] ✅ apply OrderDual.instPreorderOrderDual to (i : ?m.954) →
        (i_1 : ?m.1026 i) → (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (?m.1388 i i_1 i_2 i_3)ᵒᵈ ▶
  [] ✅ apply @Subtype.instPreorderSubtype to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (Subtype (?m.1413 i i_1 i_2 i_3)) ▶
  [] ✅ apply @WithBot.preorder to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) → (i_3 : ?m.1278 i i_1 i_2) → Preorder (WithBot (?m.1435 i i_1 i_2 i_3)) ▶
  [] ✅ apply @instPreorderForAll to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) →
            (i_3 : ?m.1278 i i_1 i_2) → Preorder ((i_4 : ?m.1458 i i_1 i_2 i_3) → ?m.1459 i i_1 i_2 i_3 i_4) ▶
  [] ✅ apply @WithTop.preorder to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) →
            (i_3 : ?m.1278 i i_1 i_2) → (i_4 : ?m.1458 i i_1 i_2 i_3) → Preorder (WithTop (?m.1500 i i_1 i_2 i_3 i_4)) ▶
  [] ✅ apply @OrderHom.instPreorderOrderHom to (i : ?m.954) →
        (i_1 : ?m.1026 i) →
          (i_2 : ?m.1134 i i_1) →
            (i_3 : ?m.1278 i i_1 i_2) →
              (i_4 : ?m.1458 i i_1 i_2 i_3) → Preorder (?m.1529 i i_1 i_2 i_3 i_4 →o ?m.1530 i i_1 i_2 i_3 i_4) ▶

At what point did it go wrong? I've never seen one of these outputs before.

[Mario Carneiro]

  [] ✅ apply @OrderMonoidWithZeroHomClass.toOrderMonoidHomClass to OrderMonoidHomClass F ?m.869 ?m.870 ▶
  [] ✅ apply @WithTop.preorder to Preorder (WithTop ?m.911) ▶

[Mario Carneiro]

second line is definitely bad, first line is ok iff the two metavariables are out params

[Mario Carneiro]

so OrderMonoidWithZeroHomClass.toOrderMonoidHomClass looks like the suspect

[Kevin Buzzard]

And what's wrong with this instance, which has lived in mathlib3 for a while now?

[Mario Carneiro]

what's the signature?

[Kevin Buzzard]

See the MWE above.

[Ruben Van de Velde]

(docs#order_monoid_with_zero_hom_class.to_order_monoid_hom_class)

[Mario Carneiro]

is it true that the last two params in MonoidHomClass are outparams?

[Mario Carneiro]

You may need to mark [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] as outparams. I thought this was fixed so that they were automatically marked as outparams? cc: @Gabriel Ebner

[Kevin Buzzard]

/-- `MonoidHomClass F M N` states that `F` is a type of `Monoid`-preserving homomorphisms.
You should also extend this typeclass when you extend `MonoidHom`. -/
@[to_additive]
class MonoidHomClass (F : Type _) (M N : outParam (Type _)) [MulOneClass M] [MulOneClass N]
  extends MulHomClass F M N, OneHomClass F M N
#align monoid_hom_class MonoidHomClass

[Mario Carneiro]

That seems like it might be worth posting as an issue

[Mario Carneiro]

that is, it is surprising to me that OrderMonoidWithZeroHomClass.toOrderMonoidHomClass is being applied in this situation

[Mario Carneiro]

what happens if you mark alpha and beta as outparams in the instance?

[Kevin Buzzard]

these links are super-cool BTW

[Kevin Buzzard]

Mario Carneiro said:

what happens if you mark alpha and beta as outparams in the instance?

Doesn't fix it :-(

[Mario Carneiro]

Can you make an MWE just for this instance to be applied in a TC search? It shouldn't depend on anything other than the types of the classes and instances used

[Kevin Buzzard]

It's this instance which causes the chaos:

instance {ι : Type u} {α : ι → Type v} [∀ i, Preorder (α i)] : Preorder (∀ i, α i) where
  __ := inferInstanceAs (LE (∀ i, α i))
  le_refl := fun a i ↦ le_refl (a i)
  le_trans := fun a b c h₁ h₂ i ↦ le_trans (h₁ i) (h₂ i)

[Kevin Buzzard]

Mathlib-free MWE on the way

[Kevin Buzzard]

(unless someone tells me that something should be an outparam in the above instance)

[Kevin Buzzard]

@Mario Carneiro is this OK as a MWE?

class Preorder (α : Type _) where

class Zero.{u} (α : Type u) 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
  coe : F → ∀ a : α, β a

instance (priority := 100) {F α β} [FunLike F α β] : CoeFun F fun _ => ∀ a : α, β a where
  coe := FunLike.coe

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 #synth below succeed
instance (priority := 1000) OrderMonoidWithZeroHomClass.toOrderMonoidHomClass
    {α β 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

[Kevin Buzzard]

https://github.com/leanprover/lean4/issues/1940

[Frédéric Dupuis]

@Kevin Buzzard Thanks a lot for distilling this down to an MWE!

[Kevin Buzzard]

I quite like this kind of detective work. It teaches me more about the system. I've learnt several new things just from this conversation.

[Gabriel Ebner]

You may need to mark [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] as outparams. I thought this was fixed so that they were automatically marked as outparams?

You're mixing things up, this has only incidentally to do with outparams. The issue is that TC search shouldn't create a subgoal for the [Preorder α] argument (because that will almost certainly be the very very bad subgoal Preorder ?m).

For automatically created instances, like the parent projection, we now mark these arguments as implicit instead of instance-implicit. (This was the quick fix to lean4#1901) We might need to do (something like) this also for manually declared instances if writing {_ : Preorder α} proves too cumbersome.

[Kevin Buzzard]

Thanks a lot Gabriel! I've learnt a ton today.

[Kevin Buzzard]

@Frédéric Dupuis I've pushed Gabriel's fix to your branch.

[Mario Carneiro]

@Gabriel Ebner I was thinking about that, but it seemed not to be the right solution in a lot of instances like this because we do want to use instance search once we know what alpha and beta are, because we won't be able to find those arguments by unification esp. if it's a stronger class than is expected by whatever is producing the outparam values (e.g if the instance only applies when the preorder on alpha is actually a linear order)

[Gabriel Ebner]

That is wishful thinking and not at all what the square brackets mean today.

[Gabriel Ebner]

Marking those arguments as instance implicit right now won't magically make TC search do the right thing. It will just time out.

[Gabriel Ebner]

If you mark then as implicit it should work with the current set up. The LinearOrder instance should be synthesized during unification as a nested TC problem.

[Kevin Buzzard]

Well, it works for now and I know what to look for later; we'll see if any problems show up later and if so we can revisit.

[Gabriel Ebner]

I kind of agree that this is an inadequate solution. We shouldn't need to tweak the braces everywhere (because it's awkward and inconsistent with other definitions). TC search should probably also fill in the LinearOrder as a separate subgoal, but that's a much larger refactoring.

[Mario Carneiro]

Gabriel Ebner said:

That is wishful thinking and not at all what the square brackets mean today.

I understand that, but {} brackets are also not the right solution, which is why I recommended to make an issue for it. It's possible that we can delay fixing the problem by using {} brackets instead, but this will fail if you actually need to use instance search on these arguments, which seems like a fairly common situation for typeclass instances.

[Mario Carneiro]

Gabriel Ebner said:

If you mark then as implicit it should work with the current set up. The LinearOrder instance should be synthesized during unification as a nested TC problem.

If you use implicits, why would it be solved as a nested TC problem at all? It would just be an implicit arg that can't be inferred.

[Gabriel Ebner]

"Nested" TC problem means a TC problem that is created during unification. E.g. you unify inferInstanceAs (Add Nat) =?= @AddMonoid.toAdd Nat ?m, then Lean will try to synthesize an AddMonoid Nat (the type of ?m) instance to unstuck the unification.

[Gabriel Ebner]

(This solves the same issue as the unification hints in canonical structures, btw.)

[Winston Yin]

Is this failure to synthesise a Preorder instance an example of the issue in this thread?

[Winston Yin]

mathlib4#927 also has problems synthesising LE instance, preventing any progress on the file. Happy to start a new thread if this isn't the same problem

[Kevin Buzzard]

Winston Yin said:

Is this failure to synthesise a Preorder instance an example of the issue in this thread?

I don't think it is. Hovering over the ↑ in failed to synthesize instance Preorder ↑s indicates that it's type_of_Set, so it seems to me that the issue is that the instance Subtype.instPreorderSubtype isn't firing because it's looking for Preorder (Subtype p). If you add the missing instance, e.g.

instance [Preorder α] (s : Set α) : Preorder (↑s) := Subtype.instPreorderSubtype s

(although probably the construction should be filled in properly rather than relying on defeq abuse) then

theorem monotoneOn_iff_monotone : MonotoneOn f s ↔
  (Monotone fun a : s => f a) := by
...

works (the proof breaks, but that's another issue)

[Kevin Buzzard]

Winston Yin said:

mathlib4#927 also has problems synthesising LE instance, preventing any progress on the file. Happy to start a new thread if this isn't the same problem

Can you show me where the error is? I'm not even sure which file you're talking about in that PR. The first error in Data.Nat.Order.Lemmas is not related to LE.

[Scott Morrison]

Coming late to this thread, but just in case not everyone has seen this: Gabriel recently gave #lint a power-up for detecting instances which will create bad typeclass searches (e.g. Preorder ?α). Your first step upon encountering a typeclass search blow-up should always be a #lint immediately before it, and then go solve any problems it finds before even beginning to think about the blow-up.

[Gabriel Ebner]

The lean4#2174 PR addresses the issue and after that instance [Preorder α] [Preorder β] [MulZeroOneClass α] [MulZeroOneClass β] [OrderMonoidWithZeroHomClass F α β] : OrderMonoidHomClass F α β will work out of the box. When adding the instance, the new code figures out the order the arguments should be synthesized in (here, we'd start with the OrderMonoidWithZeroHomClass and then do the rest from left-to-right).

[Gabriel Ebner]

To figure out the order, it adds a new semiOutParam tag to some classes like Coe because otherwise we can't figure out the order for those classes. (For those who know the dangerous instances linter in std4, it's got a hardcoded list to encode that information.)

[Gabriel Ebner]

outParam means two things: 1) instances should provide a value for that parameter (e.g. an instance : FunLike Nat Nat fun _ => β := ... is not kosher because it doesn't determine the β), and 2) this value must be unique (you shouldn't have both FunLike Nat Nat fun _ => Nat and FunLike Nat Nat fun _ => Int)

[Gabriel Ebner]

semiOutParam is just like outParam except that it only means (1) and not (2).

[Gabriel Ebner]

Does that make any sense to you?

[Gabriel Ebner]

Here's how mathlib would look like after the change: https://github.com/leanprover-community/mathlib4/pull/3139/files

[Gabriel Ebner]

I have prepared a bump PR for tomorrow, only the lean-toolchain file needs to be updated: !4#3139

[Matthew Ballard]

(Sadly no squee emoji)

[Nikolas Kuhn]

There's different naming conventions for FunLike instances: I've found both funLike and FunLike_instance. Do we have a preferred one, or is there some principle distinguishing their usage?
Edit: As Moritz Doll points out, there is also instFunLike.

[Moritz Doll]

shouldn't it be instFunLike?

[Nikolas Kuhn]

Following a suggestion of @Scott Morrison in https://github.com/leanprover-community/mathlib4/pull/4047, I tried to add a FunLike instance to the homomorphism type of SemiNormedGroupCat. Previously, I had added a CoeFun instance.

Now, this seems to break some proof step where I need to show ↑f 0 = 0 further down in the file. Trying to rw [map_zero] gives a complaint that there is no instance of ZeroHomClass is missing. Is the solution here to add that instance ?

[Nikolas Kuhn]

Concretely, I've been replacing

instance {X Y : SemiNormedGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
  coe (f : X ⟶ Y) := NormedAddGroupHom.toFun f

by

instance FunLike_instance (X Y : SemiNormedGroupCat) : FunLike (X ⟶ Y) X (fun _ => Y) :=
show FunLike (NormedAddGroupHom X Y) X (fun _ => Y) from inferInstance

in the current version of the PR.

[Yury G. Kudryashov]

(deleted)

[Nikolas Kuhn]

I added a ZeroHomClass, and everything seems to work.