WellFoundedLT Prop is not found when importing too much

Stream: mathlib4

[Yaël Dillies]

As per the title,

import Mathlib

#synth WellFoundedLT Prop
#synth WellFoundedLT Bool

doesn't work even though the following does

import Mathlib.Data.Fintype.Card

#synth WellFoundedLT Prop
#synth WellFoundedLT Bool

[Eric Wieser]

import Mathlib

attribute [-instance]
  WellFounded.wellOrderExtension.isWellFounded_lt -- deprecated
  IsWellFounded.wellOrderExtension.isWellOrder_lt
  IsWellFounded.wellOrderExtension.isWellFounded_lt -- comment this one out to see a failure

set_option trace.Meta.synthInstance true
#synth WellFoundedLT Prop

fixes it

(docs#IsWellFounded.wellOrderExtension.isWellFounded_lt)

[Eric Wieser]

I don't understand what the :explosion: in set_option trace.Meta.synthInstance true is telling me

[Jannis Limperg]

This usually indicates that an exception was thrown.

[Yury G. Kudryashov]

Should we rewrite wellOrderExtension to a type synonym WellOrderExtension α r with LinearOrder etc instances on this type synonym?

[Yaël Dillies]

My personal solution to fixing the issue is adding a shortcut instance for WellFoundedLT Prop. Here is a first step: #19086

[Eric Wieser]

My initial impression is that mathlib is not to blame here

[Kim Morrison]

Minimising this would be helpful!

[Yury G. Kudryashov]

My guess is that Lean tries isDefEq on this instance (because it's about LT.lt), then something goes wrong. Should we remove more instances that make structural assumptions about instance arguments?

[Eric Wieser]

For a long time in mathlib we've assumed it's ok to write instances of the form

instance outerInstance : @SomeClass X instSomeNonCanonicalInstanceOnX

with the premise that outerInstance is about instSomeNonCanonicalInstanceOnX not X, and so it does not harm for it to be available globally

[Eric Wieser]

(this comes up, for instance, with "this non-canonical MulAction satisfies SMulCommClass with the canonical one")

[Yury G. Kudryashov]

But it means that Lean will try it every time and try to unify instSomeNonCanonicalInstanceOnX with the generated instance.

[Yury G. Kudryashov]

(BTW, did it change during Lean3->Lean4 migration?)

[Junyan Xu]

One example is IsScalarTower.of_algHom.

[Jovan Gerbscheid]

This reminds me of another type class failure. It turns out that turning off unification hints solves the problem. This is a bug where the discrimination tree used in unification hints can throw Meta.throwIsDefEqStuck. That is why you see the :explosion: in set_option trace.Meta.synthInstance true.

import Mathlib

open Lean Meta Elab Command
syntax (name := ha) "#mysynth" term : command
@[command_elab ha] def elabSynth : CommandElab := fun stx => do
  let term := stx[1]
  withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do
    withConfig ({· with unificationHints := false}) do -- turn off unification hints
    let inst ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing
    let inst ← instantiateMVars inst
    let val  ← synthInstance inst
    logInfo val
    pure ()

-- succeeds
#mysynth WellFoundedLT Prop
#mysynth WellFoundedLT Bool

[Jovan Gerbscheid]

This should be easy to fix by setting Config.isDefEqStuckEx to false when looking up in the discrimination tree when using unificationHints.

[Violeta Hernández]

Yury G. Kudryashov said:

Should we rewrite wellOrderExtension to a type synonym WellOrderExtension α r with LinearOrder etc instances on this type synonym?

Note docs#WellOrderExtension already exists

[Violeta Hernández]

And yes, I think a type synonym with an actual LinearOrder instance would be better here. Why use unbundled relations when we don't need to?

[Violeta Hernández]

Actually, docs#WellOrderExtension already has a linear order instance

[Yaël Dillies]

I also just found #18217, which introduces the following two looping instances:

instance (priority := 100) isWellOrder_lt [LinearOrder α] [WellFoundedLT α] :
    IsWellOrder α (· < ·) where

instance (priority := 100) isWellOrder_gt [LinearOrder α] [WellFoundedGT α] :
    IsWellOrder α (· > ·) where

[Yaël Dillies]

([IsWellOrder α (· < ·)] → WellFoundedLT α is an instance)

[Kevin Buzzard]

Loops are OK in some cases, right?

[Yaël Dillies]

Yes but here WellFoundedLT α and IsWellOrder α (· < ·) take or refer to a LT argument which is unlikely to be exactly the same between two rounds of the loop. Indeed, trying #synth WellFoundedLT Prop in Data.Fintype.Card I saw the loop do several rounds before stabilising

[Violeta Hernández]

That's unfortunate, as these instances have to be instantiated separately in a couple of places otherwise

[Violeta Hernández]

Wait, what two distinct LTs are there for Prop?

[Jovan Gerbscheid]

I have minimized the bug, and I was about to open an issue, but as of today, this minimized example does the expected behaviour on the nightly version of lean: it just so happens to have gotten fixed by lean#6053.

Here's the minimization:

class Inhabited' (α : Type) where
  default' : α

class A (α : Type) [Inhabited' α]


opaque opaqueProp : Prop

open Classical in
instance {α : Type} [Inhabited α] : Inhabited' α where
  default' := if opaqueProp then default else default

instance badInst (α : Type) [Inhabited α] : A α where


instance {α : Type} [Inhabited α] : Inhabited' α where
  default' := default

instance (priority := 1) goodInst (α : Type) [Inhabited α] : A α where

set_option trace.Meta.synthInstance true
#synth A Nat

[Yaël Dillies]

Thanks Jovan for the minimization, and Leo for always being a step ahead

[Violeta Hernández]

Glad to hear I didn't accidentally screw things up