Help: A weird type instance bug

Stream: general

[J. Simon Richard]

I'm working on creating a superficial model for some Rust APIs, which includes trying to create a type class for Rust's PartialOrd trait. While I was working on this, I ran into a weird behavior that I think might be a bug in Lean... but I could be wrong, and I don't really know what I'm looking at.

Here's a minimal example:

This compiles:

class PartialOrd2 (α: Type) where
  compare (a b : α) : Option Ordering
  beq: α → α → Bool := λ a b => compare a b = some Ordering.eq
  compare_eq : beq a b ↔ compare a b = some Ordering.eq --:= by intros; rfl

  eq_symm' {a b : α} : beq a b → beq b a

instance : PartialOrd α where
  compare (a b: α) := none
  compare_eq := by
    intro a b
    simp

  eq_symm' := sorry

But this instance doesn't compile:

instance : PartialOrd2 α where
  compare (a b: α) := none
  compare_eq := by
    intro a b
    simp

  eq_symm' := Eq.symm

Of course, Eq.symm isn't the right type for eq_symm', so it shouldn't compile. But that's not where the error is thrown. Instead, I get this (which is on the compare_eq line):

PartialOrd.lean:10:16
unsolved goals
α : Type
a b : α
⊢ False

And when I hover over the compare_eq field to see it's type, this is what lean reports (in VS Code): compare_eq : ∀ {a b : α}, true = true ↔ none = some Ordering.eq.

Any idea what's going on? Why is the compare_eq type changing when I edit a (seemingly) unrelated line?

[Jovan Gerbscheid]

You are telling Lean to unify the expected type self.beq a b = true → self.beq b a = true with the term Eq.symm : ?a = ?b → ?b = ?a. So instead of using the default value for beq, it infers that beq needs to be fun a b => true. This is then reflected in the goal generated by by.

So this is Lean being maybe a bit too smart :)

[Jovan Gerbscheid]

You can avoid this surprising behaviour by using by for all your proofs:

def bld : PartialOrd α where
  compare (a b: α) := none
  compare_eq := by
    sorry

  eq_symm' := by exact Eq.symm -- error message is here

[J. Simon Richard]

Huh... okay, I guess that makes sense. Thanks!