Is this a bug in the pattern compiler?

Stream: lean4

[David Thrane Christiansen]

I figured I'd try to do a bit of gratuitously dependently typed representation of a little lambda calculus (hey, I'm on vacation this week!) and I ran into an error message that is not so excellent that I think may be a bug. This code is reduced from a larger example:

def Scope := { xs : List String // True }

def Scope.empty : Scope := ⟨[], True.intro⟩

def Scope.extend? (xs : Scope) (x : String) : Option Scope :=
  if h : ¬ x ∈ xs.val then some ⟨x::xs.val, True.intro⟩ else none

class IsSome (e : Option α) (v : α) where
  isSome : e = some v

instance : IsSome (some x) x where
  isSome := rfl

inductive Context : Scope → Type u where
  | empty : Context .empty
  | extend : Context sc → (x : String) → [IsSome (sc.extend? x) sc'] → Bool → Context sc'

def Var (sc : Scope) := {x : String // x ∈ sc.val}

def Context.lookup {sc : Scope} (Γ : Context sc) (x : Var sc) : Bool :=
  match sc, Γ with
  | ⟨[], _⟩, Context.empty => nomatch x.property
  | ⟨_ :: xs, _⟩, Context.extend Γ' y t =>
    true

In the real version, scopes have unique contents, and the types are an inductive type rather than Bool.

The error I get is:

(kernel) function expected
   _x_28 (_ : HEq Γ✝ Γ✝)

This occurred after the pattern-match compiler didn't seem to be doing the dependent pattern matching that I expected, but those intermediate states of the code didn't survive.

Any pointers? I think that at least the error message is a bug. I'm running Lean 4.1.0.

[David Thrane Christiansen]

Same thing happens in 4.2.0-rc1

[Mario Carneiro]

(kernel) errors are almost always bugs

[Mario Carneiro]

my guess is that the dependent pattern matcher generated a bad term, although it's also possible that the input is bad (which is still no excuse for producing a bad term)

[Mario Carneiro]

oh, I found an unrelated bug while minimizing:

def Scope := { xs : List String // True }

def Context.lookup {sc : Scope} : Bool :=
  match sc with
  | ⟨_ :: xs, _⟩ => true
  | ⟨[], ⟨⟩⟩ => false
-- unsupported `True.casesOn` application during code generation

[David Thrane Christiansen]

All right, I'll open an issue once I get the kid out the door - thanks

[David Thrane Christiansen]

(and this definitely looks like unification leaving behind some evidence that wasn't expected elsewhere)

[Mario Carneiro]

minimized:

inductive Context : { _x : Bool // False } → Type where
  | empty (_ : False) : Context ⟨false, x⟩
  | extend : Context sc

def Context.lookup {sc : { _x : Bool // False }} (Γ : Context sc) : Unit :=
  match sc, Γ with
  | ⟨_, _⟩, Context.extend => ()
-- (kernel) function expected
--   _x_6 (_ : HEq Γ✝ Γ✝)

there are a bunch of weird things that have to come together to cause the issue

[David Thrane Christiansen]

Thanks!

[David Thrane Christiansen]

https://github.com/leanprover/lean4/issues/2588