Coercion to function dificulty

Stream: mathlib4

[Chris Hughes]

There seems to be a difficulty with coercions to functions not triggering in the port of Order.Hom.Basic . For example on line 177 it is neessary to write theorem map_lt_map_iff (f : F) {a b : α} : (f : α → β) a < (f : α → β) b ↔ a < b instead of theorem map_lt_map_iff (f : F) {a b : α} : f a < f b ↔ a < b. It is a major pain to have to write these types explicitly to get the coercions to trigger.

[Gabriel Ebner]

This was the fix:

-instance [LE α] [LE β] [OrderIsoClass F α β] : CoeTC F (α ≃o β) :=
+instance {_ : LE α} {_ : LE β} [OrderIsoClass F α β] : CoeTC F (α ≃o β) :=
   ⟨fun f => ⟨f, map_le_map_iff f⟩⟩

[Gabriel Ebner]

I should probably port/redo the typeclass linters for mathlib4 now!

[Gabriel Ebner]

(#lint also flags a lot of issues in the file btw)

[Kevin Buzzard]

But will this instance trigger if the order on some random type alpha is in the type class inference system? I have never properly understood this implicit typeclass trick.

[Gabriel Ebner]

Yes, the difference here is that [LE α] means "search for the type class by going through the registered instances", while {_ : LE α} means "hope that it will get filled in via unification".

[Gabriel Ebner]

In this case, it will get filled in via unification because the LE α argument appears in OrderIsoClass F α β.

[Chris Hughes]

There were still a few problems porting Order.Antisymmetrization. The coercions to function did not trigger on OrderIso.dualAntisymmetrization _ so I had to change the underscore to an α to get the coercion to work.

[Chris Hughes]

Gabriel Ebner said:

Yes, the difference here is that [LE α] means "search for the type class by going through the registered instances", while {_ : LE α} means "hope that it will get filled in via unification".

There are some other instances in Order.Hom.Bounded where instead of LE α you have PartialOrder α so this trick does not work because only LE α can be inferred via unification and not PartialOrder α

[Gabriel Ebner]

because only LE α can be inferred via unification and not PartialOrder α

This should still work (unification calls type-class synthesis in this case). Can you post examples / link to the branch?

[Chris Hughes]

Here is the PR

[Gabriel Ebner]

Pushed a fix to the branch:

 instance (α : Type _) [LE α] : LE αᵒᵈ :=
-  ⟨fun x y : α ↦ y ≤ x⟩
+  ⟨fun a b => @LE.le α _ b a⟩

The previous version of the LE instance unfolded @LE.le αᵒᵈ _ into fun (a : α) => ..., and then Lean failed to unify α and αᵒᵈ (with reducible transparency).

[Yaël Dillies]

The thing that jumps out as wrong with your snippet is that it doesn't mention of_dual.

[Eric Wieser]

Yael, Lean3 does the same questionable thing as Lean4 there

[Yaël Dillies]

Yes, my point is that it seems that the questionable thing is acceptable in Lean 3 but not in Lean 4. So the correct thing to do is to remove the questionable thing, rather than replacing it by another one.

[Yaël Dillies]

But I would like to know whether this is a wide-spread problem with type synonyms or a sporadic one.

[Eric Wieser]

I think it happens here because of some challenges straightening out the import heirarchy

[Eric Wieser]

Namely because we decided to make the type-cast functions bundled, and the bundling wasn't available early enough

[Chris Hughes]

Chris Hughes said:

Here is the PR

The issue is not fixed. I just merged master and the problem is still there

[Gabriel Ebner]

Is there a new issue? Mathlib.Order.Antisymmetrization compiles in the branch, and has dualAntisymmetrization _ (without the explicit α).

[Chris Hughes]

The problem is in Order.Hom.Bounded. Line 125 if I remember correctly, but I can't check easily right now

[Gabriel Ebner]

#lint flags a lot of issues that I think are relevant to the issue in that file.

[Chris Hughes]

The problem is that I cannot write the TopHomClass instance on line 102 in a way that satisfies the linter. The argument PartialOrder β cannot be inferred by unification or Type class inference.

[Anne Baanen]

Here's a minimized version of this issue:

class BoundedOrder (A : Type _) [LE A] where

class FunLike (F : Type _) (A B : outParam (Type _)) where toFun : F → A → B
instance [FunLike F A B] : CoeFun F fun _ => A → B where coe := FunLike.toFun
class LEHomClass (F) (A B : outParam _) [LE A] [LE B] extends FunLike F A B
class BoundedOrderHomClass (F) (A B : outParam _) [LE A] [LE B] [BoundedOrder A] [BoundedOrder B] extends LEHomClass F A B

section instanceParam

class OrderEquivClass₁ (F) (A B : outParam _) [LE A] [LE B] where toFun : F → A → B

instance OrderEquivClass₁.toBoundedOrderHomClass (F) (A B : outParam _)
    {_ : LE A} {_ : LE B} -- Implicit, because they depend on outParams and can be found through unification with the `OrderEquivClass` instance
    [BoundedOrder A] [BoundedOrder B] -- Can't be implicit, because they can't be find through unification.
    [OrderEquivClass₁ F A B] : BoundedOrderHomClass F A B where
  toFun := toFun

set_option trace.Meta.synthInstance true
example [LE A] [LE B] [BoundedOrder A] [BoundedOrder B] [OrderEquivClass₁ F A B] (f : F) (a : A) : f a = f a := rfl -- Error: function expected at `f`
-- Relevant part of the trace:
/-
[Meta.synthInstance] ❌ CoeFun F ?γ ▼
  [] new goal CoeFun F _tc.0 ▶
  [] ✅ apply @instCoeFunForAll to CoeFun F fun x => ?m.689 → ?m.690 ▶
  [] ✅ apply @LEHomClass.toFunLike to FunLike F ?m.707 ?m.708 ▶
  [] ✅ apply @BoundedOrderHomClass.toLEHomClass to LEHomClass F ?m.722 ?m.723 ▶
  [] ✅ apply OrderEquivClass₁.toBoundedOrderHomClass to BoundedOrderHomClass F ?m.745 ?m.746 ▼
    [tryResolve] ✅ BoundedOrderHomClass F ?m.745 ?m.746 ≟ BoundedOrderHomClass F ?m.745 ?m.746
    [] no instances for BoundedOrder _tc.1 ▶
-/

end instanceParam

section implicitParam

class OrderEquivClass₂ (F) (A B : outParam _) [LE A] [LE B] where toFun : F → A → B

instance OrderEquivClass₂.toBoundedOrderHomClass (F) (A B : outParam _)
    {_ : LE A} {_ : LE B} -- Implicit, because they depend on outParams and can be found through unification with the `OrderEquivClass` instance
    {_ : BoundedOrder A} {_ : BoundedOrder B} -- Can't be instance params, because they depend on outParam
    [OrderEquivClass₂ F A B] : BoundedOrderHomClass F A B where
  toFun := toFun

set_option trace.Meta.synthInstance true
example [LE A] [LE B] [BoundedOrder A] [BoundedOrder B] [OrderEquivClass₂ F A B] (f : F) (a : A) : f a = f a := rfl -- Error: function expected at `f`
-- Relevant part of the trace:
/-
▶ 47:66-47:69: information:
[Meta.synthInstance] ❌ CoeFun F ?γ ▼
  [] new goal CoeFun F _tc.0 ▶
  [] ✅ apply @instCoeFunForAll to CoeFun F fun x => ?m.1285 → ?m.1286 ▶
  [] ✅ apply @LEHomClass.toFunLike to FunLike F ?m.1303 ?m.1304 ▶
  [] ✅ apply @BoundedOrderHomClass.toLEHomClass to LEHomClass F ?m.1318 ?m.1319 ▶
  [] ✅ apply OrderEquivClass₂.toBoundedOrderHomClass to BoundedOrderHomClass F ?m.1344 ?m.1345 ▶
  [] ✅ apply inst✝ to OrderEquivClass₂ F A B ▶
  [resume] propagating OrderEquivClass₂ F A B to subgoal OrderEquivClass₂ F A B of BoundedOrderHomClass F A B ▶
  [resume] propagating (x_0 : BoundedOrder A) →
        (x_1 : BoundedOrder B) → BoundedOrderHomClass F A B to subgoal BoundedOrderHomClass F A B of LEHomClass F A B ▶
  [resume] propagating BoundedOrder A → BoundedOrder B → LEHomClass F A B to subgoal LEHomClass F A B of FunLike F A B ▶
  [resume] propagating BoundedOrder A → BoundedOrder B → FunLike F A B to subgoal FunLike F A B of CoeFun F fun x => A → B ▼
    [] size: 4
    [synthInstance] skip answer containing metavariables instCoeFunForAll
-/

end implicitParam

[Anne Baanen]

It looks like the instance OrderEquivClass₁.toBoundedOrderHomClass doesn't work because it has instance parameters depending on outParams, and the instance OrderEquivClass₂.toBoundedOrderHomClass doesn't work because it has implicit parameters that can't be figured out through unification.

[Anne Baanen]

(Edit: I went slightly overboard in minimizing, now I'm pretty sure the code is actually supposed to work!)

[Anne Baanen]

Update: in #888 I managed to work around this issue mostly, by turning all parameters implicit to placate the linter, and adding letI when such an intermediate instance can't be found through unification.

[Anne Baanen]

Another way to look at this issue is the linter, since #lint reports both instances in the example are dangerous:

#check OrderEquivClass₁.toBoundedOrderHomClass /- generates subgoals with metavariables: argument 6 inst✝² : BoundedOrder
  ?A, argument 7 inst✝¹ : BoundedOrder ?B -/
#check OrderEquivClass₂.toBoundedOrderHomClass /- unassigned metavariable in out-param: @BoundedOrderHomClass.{u_1, u_2, u_3} F A B x✝³ x✝² ?x✝ ?x✝¹ -/

(The latter error message isn't clear unless you set the option pp.all.)