type mismatch with identical types on named pattern match

Stream: lean4

[Andrés Goens]

I'm getting a strange behavior where Lean complains about a type mismatch, yet reports the expected and inferred types to be identical. This happens when trying to name a pattern-matched expression. Here is an attempt at an MWE:

inductive ListTree (α : Type) [BEq α] : List α → Type
 | leaf (val : List α) : ListTree α val
 | parentNil  (val : List α) : ListTree α val
 | parentCons (_ : ListTree α child) (_ : ListTree α sibling)
 (_ :  child.head? == sibling.head?) : ListTree α sibling

def ListTree.foo [BEq α] {l₁ l₂: List α} (h : l₁.head? == l₂.head?) : ListTree α l₁ → ListTree α l₂ → Option (ListTree α l₂)
  | t1@(leaf l₁), t₂@(parentNil l₂) => some $ parentCons t1 t2 h
  | _, _ => none

I get:

application type mismatch
  namedPattern t1 (leaf l₁)
argument
  leaf l₁
has type
  ListTree α l₁ : Type
but is expected to have type
  ListTree α l₁ : Type

Am I missing something here?

[Sébastien Michelland]

The latest nightly reveals the problem (notice the extra dagger):

application type mismatch
  namedPattern t1 (leaf l₁)
argument
  leaf l₁
has type
  ListTree α l₁ : Type
but is expected to have type
  ListTree α l₁✝ : Type

Pattern matching can destructure your inputs and name the subterms, but it can't implicitly check for equality. The pattern you wrote allows t₁ to be any leaf and then names that leaf's parameter l₁, shadowing the original name. By that time the strong information you had from the dependent type (that the parameter of leaf must be l₁) is lost.

The easy way around this problem is to simply let Lean infer with dependent matching.

def ListTree.foo [BEq α] {l₁ l₂: List α} (h : l₁.head? == l₂.head?) : ListTree α l₁ → ListTree α l₂ → Option (ListTree α l₂)
  | t₁@(leaf _), t₂@(parentNil _) => some $ parentCons t₁ t₂ h
  | _, _ => none

[Mauricio Collares]

(deleted, lost the race)

[Andrés Goens]

thanks for the explanation @Sébastien Michelland ! Does it mean I couldn't pattern match for the argument to be equal (without the @t name)? Can you pattern match to check for that equality? In my actual code I also care about that argument, just didn't need it for the MWE

[Andrés Goens]

btw, I thought I tried using the latest nightly, apparently changing it in the lean_toolchain file and restarting lean4 mode doesn't update the version :sweat_smile:

[Sébastien Michelland]

Barring more complicated features that I am not aware of, pattern matching is really only destructuring + binding new names. The thing is, checking for equality is not always possible; you either need the terms to be definitionally equal, or you need to have DecidableEq on the relevant type. Currently you only have BEq, which is simply any relation on the type, so you do not have the guarantees needed to compare List α. In addition to that, supporting equality would make it much harder to checking that patterns are exhaustive.

If you need to check for equality, then you would (1) want a strong enough structure on α: DecidableEq would definitely do, I believe there might also be something like LawfulBEq; and (2) check for equality explicitly.

[Sébastien Michelland]

As for changing the lean version, I personally run elan toolchain install leanprover/lean4:nightly-2022-07-01, then update the lean-toolchain file, and use the "Lean 4: Select Lean Toolchain" command of VSCode to make sure I switched to the new one.

[Sebastian Ullrich]

@Andrés Goens You likely want M-x lsp-workspace-restart in Emacs

[Andrés Goens]

ahh, right! just because someone says BEq corresponds to equality doesn't mean it actually does, that makes a lot of sense, thanks! Does that mean the delaborator checks for a DecidableEq instance in the pattern match and change its behavior accordingly? :open_mouth:

[Sébastien Michelland]

The pattern match remains the same and will shadow existing variables even if decidable equality is available. If you do want equality, you need to check after =>:

def follow_each_other (n m: Int): Bool :=
  match m with
--| .S n => true -- INCORRECT
  | .S n' => n' = n
  | _ => false

[Andrés Goens]

Yep, I've used that pattern too, it makes sense. Thanks for the explanation.

[Andrés Goens]

Sebastian Ullrich said:

Andrés Goens You likely want M-x lsp-workspace-restart in Emacs

Hm, that's curious, I actually don't get the dagger in emacs (I opened up vs code to check and it shows in vs code)

[Andrés Goens]

which is strange, I imagine that should come directly from the LSP, right?