Error: Unknown Free Variable from kernel local_ctx.

[bollu]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Consider the MWE:

inductive ExTy
  | nat
  deriving DecidableEq, Repr

def ExTy.toType : ExTy → Type 
| .nat => Nat

/-- We need all four constructors for the error. -/
inductive ExOp :  Type
  | add : ExOp
  | beq : ExOp
  | cst : ExOp
  | runK  : ExOp
  deriving DecidableEq

/-- This needs to be a typeclass for the error. -/
class OpSignature (Op : Type) where
  sig : Op → List ExTy

instance : OpSignature ExOp where
  sig
  | .add => [.nat, .nat]
  | .beq => []
  | .cst => []
  | .runK => []

/-- An heterogeneous vector -/
inductive HVector {α : Type} (f : α → Type) : List α → Type _
  | nil : HVector f []
  | cons {a : α} : (f a) → HVector f as → HVector f (a :: as)

-- error: unknown free variable: _kernel_fresh.95
def denote' : (op : ExOp) → (args : HVector ExTy.toType (OpSignature.sig op)) → Nat
| .cst, _ => (0 : Nat)
| .add, .cons (a : Nat) (.cons (b : Nat) .nil) => a + b
| .beq, _ => (0 : Nat)
| .runK, _ => (0 : Nat)

This produces the error:

KernelFresh.lean:33:4: error: unknown free variable: _kernel_fresh.95

This error is generated from src/kernel/local_ctx.cpp:80 at local_ctx::get_local_decl.

Context

This occurred when developing intrinsically typed SSA encodings for MLIR at https://github.com/opencompl/lean-mlir/

Versions

Lean with instrumentation over commit 0d5f9122a1fc0cc1751a55eec8368a0d6592722a.

$ uname -a
Linux holonomic 5.15.90.1-microsoft-standard-WSL2 #1 SMP Fri Jan 27 02:56:13 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux

[Kha]

Triggered by the old compiler's erase_irrelevant_fn, marking the def noncomputable fixes the bug