Help understanding type errors

Stream: lean4

[Francisco Giordano]

In this file I see 2 type errors that I cannot understand. Would appreciate any help

live.lean-lang.org

[Markus Schmaus]

The error message is:

invalid match-expression, pattern contains metavariables
none

Lean uses metavariables for types it could not (yet) infer, so in this error message indicates, that Lean wasn't able to figure out the type of all your variables. You can fix this by specifying the type of q:

class Queue (α : outParam (Type)) (γ : Type) where
  empty : γ
  enqueue: γ → α → γ
  dequeue : γ → Option (γ × α)

  dequeue_empty : dequeue empty = none
  dequeue_none : dequeue q = none → q = empty

  dequeue_enqueue :
    dequeue (enqueue q x) = some (match dequeue q with
                                   | none => (empty, x)
                                   | some (q', y) => (enqueue q' x, y))

namespace ListQueue

abbrev empty : List α := []

def enqueue (q : List α) (x : α) : List α := List.cons x q

def dequeue : List α → Option (List α × α)
  | [] => none
  | x :: q =>
    match dequeue q with
    | none => some ([], x)
    | some (q', y) => some (x :: q', y)

theorem dequeue_empty : @dequeue α empty = none := by rfl

theorem dequeue_none : dequeue q = none → q = empty := by
    cases q <;> simp [dequeue] <;> (try split) <;> simp

-- This is what I would write but doesn't compile:
theorem dequeue_enqueue' {q : List α} :
    dequeue (enqueue q x) = some (match dequeue q with
                                   | none => (empty, x)
                                   | some (q', y) => (enqueue q' x, y)) := sorry

[Markus Schmaus]

You can also use variable to specify the type of q for the whole section

namespace ListQueue

variable {α : Type u} {q : List α}

abbrev empty : List α := []

def enqueue (q : List α) (x : α) : List α := List.cons x q

def dequeue : List α → Option (List α × α)
  | [] => none
  | x :: q =>
    match dequeue q with
    | none => some ([], x)
    | some (q', y) => some (x :: q', y)

theorem dequeue_empty : @dequeue α empty = none := by rfl

theorem dequeue_none : dequeue q = none → q = empty := by
    cases q <;> simp [dequeue] <;> (try split) <;> simp

-- This is what I would write but doesn't compile:
theorem dequeue_enqueue' :
    dequeue (enqueue q x) = some (match dequeue q with
                                   | none => (empty, x)
                                   | some (q', y) => (enqueue q' x, y)) := sorry

[Francisco Giordano]

I see. So I understand why in the none branch it is not able to infer a type for q, because there is nothing constraining it, but I'd expect the inference be completed by the some branch.

The other thing that is confusing to me is that the same expression seems to be inferred correctly in the class method declaration

[Markus Schmaus]

If you hover over the terms you can see which types Lean is able to figure out and which not. In the class, lean is able to figure out that q is γ and all is well. In the theorem, Lean is able to figure out that q is a List, but it cannot figure out of what that list may contain, so it is stuck with List ?m.2019with the meta variable ?m.2019. The error is then caused by match which doesn't want to deal with a type with unresolved meta variables.

[Francisco Giordano]

Oh this makes total sense to me now. Thanks!