(kernel) function expected

Stream: lean4

[Enrico Borba]

Ran into (kernel) function expected trying to do some affine lambda calculus normalization. The logic of the substitution is clearly incorrect (doesn't recurse in the non-beta-reduction case), but I don't think that's relevant.

inductive Affine : (vs : Finset ℕ) → Type
| var (x : ℕ) : Affine {x}
| abs (x : ℕ) (e : Affine vs) : Affine (vs \ {x})
| app (e₁ : Affine vs₁) (e₂ : Affine vs₂) (h : vs₁ ∩ vs₂ = ∅) : Affine (vs₁ ∪ vs₂)

namespace Affine

/-- The free variables in an affine term. -/
abbrev free (_ : Affine vs) : Finset ℕ := vs

def subst (e : Affine vs₁) (x : ℕ) (hx : x ∈ vs₁) (e' : Affine vs₂) : Affine ((vs₁ \ {x}) ∪ vs₂) :=
  sorry

end Affine

/-- error: (kernel) function expected _x_48 (_ : HEq e₁✝ e₁✝) -/
def small_step (e : Affine vs) : (vs' : Finset ℕ) × (h : vs' ⊆ vs) ×' Affine vs' :=
  match e with
  | .app (.abs x e₁) e₂ h =>
    if hx₁ : x ∈ e₁.free then
      ⟨e₁.free \ {x} ∪ e₂.free, Finset.Subset.refl _, e₁.subst x hx₁ e₂⟩
    else
      have : e₁.free ⊆ e₁.free \ {x} ∪ e₂.free := by
        intro v hv
        have : v ∉ {x} := Finset.not_mem_singleton.mpr (fun heq : v = x => hx₁ (heq ▸ hv))
        exact Finset.mem_union_left _ (Finset.mem_sdiff.mpr ⟨hv, this⟩)

      ⟨e₁.free, this, e₁⟩

  | e => ⟨vs, Finset.Subset.refl _, e⟩

end Affine

It's not clear to me how to minimize this further. However, replacing that .app (.abs x e₁) e₂ h match arm with a sorry removes this error.

I saw that there were other posts about this, and that it's likely a compiler bug, but I wanted to confirm here before opening any issues.

[Enrico Borba]

Here's a bit smaller:

inductive Affine : (vs : Finset ℕ) → Type
| var (x : ℕ) : Affine {x}
| abs (x : ℕ) (e : Affine vs) : Affine (vs \ {x})
| app (e₁ : Affine vs₁) (e₂ : Affine vs₂) (h : vs₁ ∩ vs₂ = ∅) : Affine (vs₁ ∪ vs₂)

namespace Affine

/-- The free variables in an affine term. -/
abbrev free (_ : Affine vs) : Finset ℕ := vs

def subst (e : Affine vs₁) (x : ℕ) (hx : x ∈ vs₁) (e' : Affine vs₂) : Affine ((vs₁ \ {x}) ∪ vs₂) :=
  sorry

/-- error: (kernel) function expected _x_42 (_ : HEq e₁✝ e₁✝) -/
def small_step (e : Affine vs) : (vs' : Finset ℕ) × Affine vs' :=
  match e with
  | .app (.abs x e₁) e₂ h =>
    if hx₁ : x ∈ e₁.free then
      ⟨e₁.free \ {x} ∪ e₂.free, e₁.subst x hx₁ e₂⟩
    else
      ⟨e₁.free, e₁⟩

  | e => ⟨vs, e⟩

end Affine

[Enrico Borba]

This does not occur if I use a list instead of a Finset:

inductive Affine : (vs : List ℕ) → Type
| var (x : ℕ) : Affine {x}
| abs (x : ℕ) (e : Affine vs) : Affine (vs \ {x})
| app (e₁ : Affine vs₁) (e₂ : Affine vs₂) (h : vs₁ ∩ vs₂ = ∅) : Affine (vs₁ ∪ vs₂)

namespace Affine

/-- The free variables in an affine term. -/
abbrev free (_ : Affine vs) : List ℕ := vs

def subst (e : Affine vs₁) (x : ℕ) (hx : x ∈ vs₁) (e' : Affine vs₂) : Affine ((vs₁ \ {x}) ∪ vs₂) :=
  sorry

/- no error! -/
def small_step (e : Affine vs) : (vs' : List ℕ) × Affine vs' :=
  match e with
  | .app (.abs x e₁) e₂ h =>
    if hx₁ : x ∈ e₁.free then
      ⟨_, e₁.subst x hx₁ e₂⟩
    else
      ⟨_, e₁⟩

  | e => ⟨_, e⟩

end Affine

[Enrico Borba]

What are the proper steps to opening a bug, should I just file an issue in the lean4 repo?

[Mario Carneiro]

yes