typeclass instance that fails linting

Stream: mathlib4

[Arien Malec]

In Algebra.PUnitInstances I ported an instance for CanonicallyOrderedAddMonoid that I changed from mathport only by adding an manual instance name and marking parameters as implicits.

It somehow, and uniquely for all the instances in this file, require an argument (of unit) to use, and it fails the impossibleInstance lint

The definition in mathlib4#1319 is:

instance canonicallyOrderedAddMonoid: CanonicallyOrderedAddMonoid PUnit := by
  refine'
        { PUnit.commRing, PUnit.partialOrder with
          exists_add_of_le := fun {_ _} _ => ⟨PUnit.unit, Subsingleton.elim _ _⟩.. } <;>
      intros <;>
    trivial

As mathport had it:

instance : CanonicallyOrderedAddMonoid PUnit := by
  refine'
        { PUnit.commRing, PUnit.completeBooleanAlgebra with
          exists_add_of_le := fun _ _ _ => ⟨star, Subsingleton.elim _ _⟩.. } <;>
      intros <;>
    trivial

Any ideas?

[Arien Malec]

I fixed this, but not clear on why/how.

[Reid Barton]

It somehow, and uniquely for all the instances in this file, require an argument (of unit) to use, and it fails the impossibleInstance lint

What does this mean?

[Yaël Dillies]

Have you tried set_option autoImplicit false?

[Arien Malec]

Reid Barton said:

It somehow, and uniquely for all the instances in this file, require an argument (of unit) to use, and it fails the impossibleInstance lint

What does this mean?

I have no idea what the impossibleInstances lint is or does...

[Arien Malec]

but it exists.

[Arien Malec]

https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Lint/TypeClass.html#Std.Tactic.Lint.impossibleInstance

[Arien Malec]

If you pull down mathlib4##1319 and change

instance canonicallyOrderedAddMonoid: CanonicallyOrderedAddMonoid PUnit := by
  refine'
        { PUnit.commRing,  PUnit.completeBooleanAlgebra with
          exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩.. } <;>
      intros <;>
    trivial

to

instance partialOrdered: PartialOrder PUnit where
  le_antisymm := by intros; rfl

instance canonicallyOrderedAddMonoid: CanonicallyOrderedAddMonoid PUnit := by
  refine'
        { PUnit.commRing,  PUnit.partialOrdered with
          exists_add_of_le := fun {_ _} _ => ⟨unit, Subsingleton.elim _ _⟩.. } <;>
      intros <;>
    trivial

you then get a syntax error later on that requires adding a unit that then triggers the lint.

[Arien Malec]

The errors are expected structure
and then the super confusing:

type mismatch
  LinearOrderedCancelAddCommMonoid.le_total
has type
  ∀ (a b : PUnit), a ≤ b ∨ b ≤ a : Prop
but is expected to have type
  ∀ (a b : PUnit), a ≤ b ∨ b ≤ a : Prop

[Kevin Buzzard]

I bet if you put pp.all on then the two <= s will look super-different but will be defeq.

[Arien Malec]

Can try this. But the major weirdness is why the transformation above leads to a type error that’s solve by inserting a ()

[Gabriel Ebner]

The culprit here is variable (y : PUnit) combined with by trivial. My suggestion would be to remove the variable (and universe) commands in the file.

[Arien Malec]

Will eliminate in next push.