Instances in !4#2138

Stream: mathlib4

[Yury G. Kudryashov]

In !4#2138, mathport generated (modulo minor fixes):

class ContinuousOrderHomClass (F : Type _) (α β : outParam <| Type _) [Preorder α] [Preorder β]
    [TopologicalSpace α] [TopologicalSpace β] extends
    RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop) where
  map_continuous (f : F) : Continuous f

instance (priority := 100) ContinuousOrderHomClass.toContinuousMapClass [Preorder α] [Preorder β]
    [TopologicalSpace α] [TopologicalSpace β] [ContinuousOrderHomClass F α β] :
    ContinuousMapClass F α β :=
  { ‹ContinuousOrderHomClass F α β› with }

instance : ContinuousOrderHomClass (α →Co β) α β where
  coe f := f.toFun
  coe_injective' f g h := by
    obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr
  map_rel f _ _ h := f.monotone' h
  map_continuous f := f.continuous_toFun

With these instances, Lean often fails to find a coercion of f : ContinuousOrderHom α β to function (but sometimes it succeeds).

[Yury G. Kudryashov]

I suspect that this is related to some outParams.

[Yury G. Kudryashov]

It seems that the issue is in docs4#OrderHomClass

[Yury G. Kudryashov]

It unfolds to docs4#RelHomClass which uses relations as outParams

[Yury G. Kudryashov]

IMHO, relations should not be outParams because the same map can be RelHomClass for le and for lt.

[Eric Wieser]

Can you add a shortcut coefun instance? (Defined as FunLike.coe)

[Anne Baanen]

I left a comment on the PR, because I suspect ContinuousOrderHomClass.toContinuousMapClass is a dangerous instance.

[Gabriel Ebner]

Yes, this is a bug. https://github.com/leanprover/std4/pull/102

[Yury G. Kudryashov]

If I add a shortcut CoeFun instance, then Lean will unfold coercions to toFun

[Yury G. Kudryashov]

@Eric Wieser :up:

[Eric Wieser]

Defined as FunLike.coe

not as toFun

[Yury G. Kudryashov]

I should read more carefully. Anyway, it compiles now.

[Yury G. Kudryashov]

@Anne Baanen Do you think TC search fails in !4#2163 for a similar reason? If yes, how can we fix it?

[Anne Baanen]

From trace.Meta.synthInstance and trace.Meta.isDefEq we get a suggestion of the error:

  [] ❌ apply @InfₛHomClass.toInfTopHomClass to InfTopHomClass (InfₛHom α β) ?m.17624 ?m.17625 ▼
    [tryResolve] ❌ InfTopHomClass (InfₛHom α β) ?m.17624 ?m.17625 ≟ InfTopHomClass ?m.17844 ?m.17845 ?m.17846 ▼
      [isDefEq] ❌ InfTopHomClass (InfₛHom α β) ?m.17624 ?m.17625 =?= InfTopHomClass ?m.17844 ?m.17845 ?m.17846 ▼
        [] ✅ InfₛHom α β =?= ?m.17844 ▶
        [] ✅ ?m.17624 =?= ?m.17845 ▶
        [] ✅ ?m.17625 =?= ?m.17846 ▶
        [] ✅ ?m.17628 =?= CompleteLattice.toTop ▶
        [] ✅ ?m.17629 =?= CompleteLattice.toTop ▶
        [synthInstance] 💥 SemilatticeInf ?m.17845 ▶
        [synthInstance] 💥 CompleteLattice ?m.17845 ▶
        [] ❌ SemilatticeInf.toHasInf =?= Lattice.toHasInf ▶
        [onFailure] ❌ InfTopHomClass (InfₛHom α β) ?m.17624 ?m.17625 =?= InfTopHomClass ?m.17844 ?m.17845 ?m.17846
        [onFailure] ❌ InfTopHomClass (InfₛHom α β) ?m.17624 ?m.17625 =?= InfTopHomClass ?m.17844 ?m.17845 ?m.17846

What's happening here is that InfₛHomClass.toInfTopHomClass needs stronger assumptions (CompleteLattice) than can be found either in InfₛHomClass (InfSet) or in InfTopHomClass (Inf + Top). So to apply this instance, unification needs to find a CompleteLattice record that projects into the right InfSet, Inf and Top instances. This can't really be done automatically, so instead we can "unstuck" the problem through instance synthesis: find a CompleteLattice instance and check it satisfies the conditions. But we haven't yet reached the end of the inheritance chain that will tell us what the domain and codomain for the morphisms are, so we are left with a CompleteLattice ?m.17845 instance search which fails.

This is a limitation in Lean 4, although I am not sure that this counts as a bug: Lean 3 actually has trouble with similar cases, where we have diamond inheritance in instance parameters depending on outParams.

If we expect this limitation to be fixed at some point, I would advise to try to fix the issue here: for that, we need some way to inform Lean about either the CompleteLattice structure, or at least the type on which to find this structure. If we do not expect it to be fixed, we should instead add a shortcut instance giving OrderHom on InfₛHomClass without needing to go through diamond inheritance of CompleteLattice.