kernel invalid projection

Stream: lean4

[David Richter]

Hi, here are two functions ERR and OK, ERR does not compile because of a 'kernel invalid projection' and OK compiles. But I think the two functions ERR and OK should be equivalent?

The problem appears, when I perform a boolean equality over the projection of a term whose type has been rewritten to be a tuple. I'm not sure how to minimize the problem further.

inductive Ty where
  | bool : Ty
  | prod : Ty → Ty → Ty
open Ty

abbrev Ty.de : Ty → Type
  | bool => Bool
  | prod a b => a.de × b.de

instance {t: Ty} : BEq (t.de) where
  beq := let rec go : (t : Ty) → t.de → t.de → Bool
  | .bool => λ a b => a == b
  | .prod α β => λ a b => go α a.1 b.1 ∧ go β a.2 b.2
  go t

def FST (ab: (prod a b).de): a.de := ab.1

def ERR (h: t=prod a b) (a: a.de) (e: t.de): Bool := a == (h ▸ e).1 -- (kernel) invalid projection
def OK  (h: t=prod a b) (a: a.de) (e: t.de): Bool := a == FST (h ▸ e) -- ok

#eval OK (a:=bool) (b:=bool) rfl true (true, true) -- OK is computable
#eval OK (a:=bool) (b:=bool) rfl false (true, true) -- OK is computable

EDIT: In particular the error message is

(kernel) invalid projection
  e.1

So it seems, lean thinks that the code contained e.1 directly, which is of course type incorrect, although the code clearly says (h ▸ e).1. Maybe that's related to how this error happens? Or are rewrites just not printed in the error message there?

[Kevin Buzzard]

Higher order unification is undecidable so you can't expect everything to work with no clues. I'm guessing that it will work if you write (h \t e : <write the type here>).1 .

[David Richter]

Hi, I suppose the ▸ looks so innocent that I forgot that it has to perform higher order unification in the background. Nevertheless, I'm not convinced that's the issue here:

I think lean is able to correctly guess the expected rewriting, otherwise I would expect (h ▸ c).1 to be a type error not a kernel invalid projection.

If I write def ERR₂ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool := let tmp := h ▸ c; a == tmp.1 then I can hover over tmp with the mouse and see that the type (prod α β).de is correctly deduced.

Indeed, writing the type explicitly like def ERR₁ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool := let tmp := (h ▸ c : (prod α β).de); a == tmp.1 doesnt change anything, the kernel invalid projection error still appears.

See:

inductive Ty where
  | bool : Ty
  | prod : Ty → Ty → Ty
open Ty

abbrev Ty.de : Ty → Type
  | bool => Bool
  | prod a b => a.de × b.de

instance {t: Ty} : BEq (t.de) where
  beq := let rec go : (t : Ty) → t.de → t.de → Bool
  | .bool => λ a b => a == b
  | .prod α β => λ a b => go α a.1 b.1 ∧ go β a.2 b.2
  go t

def FST (c: (prod α β).de): α.de := c.1

def OK  (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  a == FST (h ▸ c) -- ok
def ERR₁ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  let tmp := (h ▸ c : (prod α β).de); a == tmp.1 -- (kernel) invalid projection
def ERR₂ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  let tmp := h ▸ c; a == tmp.1 -- (kernel) invalid projection
def ERR₃ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  a == (h ▸ c).1 -- (kernel) invalid projection

-- EDIT: here is a very verbose variant
def ERR₄ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool := -- (kernel) invalid projection
  let tmp: α.de × β.de := (h ▸ c : (prod α β).de)
  let tmp1: α.de := tmp.1
  a == tmp1

#eval OK (α := bool) (β := bool) rfl true  (true, true) -- OK is computable
#eval OK (α := bool) (β := bool) rfl false (true, true) -- OK is computable

[Mario Carneiro]

Note that your type ascriptions are doing nothing for the kernel, they are only seen by the elaborator. Here are some variants that work:

def OK₄ (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  let tmp: α.de × β.de := (show (prod α β).de from h ▸ c)
  let tmp1: α.de := tmp.1
  a == tmp1

def hc (h: γ = prod α β) (c: γ.de) : (prod α β).de := (h ▸ c)
def OK  (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  a == (hc h c).1

[Mario Carneiro]

The use of show and hc in these examples is forcing an intermediate term whose type is (prod α β).de. My guess is that without this, the term h ▸ c gets the type acquired from its underlying term @Eq.rec Ty γ (fun x h ↦ de x) c (prod α β) h, which is (fun x h ↦ de x) (prod α β) h, but ascribing this type explicitly also seems to work...

[Mario Carneiro]

Also, my guess is that the c.1 you see in the error message is not actually the (h ▸ c).1 term you wrote itself, but rather a subterm generated during the typechecking of this term: the type of a projection can refer to other projections, and after whnf it can be a bit difficult to say exactly what terms it decided to synthesize here. I'll see if I can reproduce with lean4lean

[Mario Carneiro]

oh, extra weird:

theorem OK  {γ α β} (h: γ = prod α β) (a: α.de) (c: γ.de): Bool := a == (h ▸ c).1 -- ok
def     ERR {γ α β} (h: γ = prod α β) (a: α.de) (c: γ.de): Bool := a == (h ▸ c).1 -- invalid projection

so somehow being a definition is relevant here; perhaps the error is actually occurring in the equation lemma?

[Mario Carneiro]

Using #whatsnew in on the def reveals

#whatsnew in
def OK {γ α β} (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  a == (@id _ <| h ▸ c).1

unsafe def OK._rarg._cstage2 : _obj → _obj → _neutral → _obj → _obj → _obj :=
fun α β h a c ↦
  let _x_1 := c.1;
  instBEqDe.go α a _x_1

unsafe def OK._cstage2 : _obj → _obj :=
fun γ ↦ OK._rarg

def OK : {γ α β : Ty} → γ = prod α β → de α → de γ → Bool :=
fun {γ α β} h a c ↦ a == (id (h ▸ c)).fst

unsafe def OK._cstage1 : {γ α β : Ty} → γ = prod α β → de α → de γ → Bool :=
fun {γ α β} h a c ↦
  let _x_3 := c.1;
  instBEqDe.go α a _x_3

where in the last definition we indeed have a c.1 subterm for which hovering it says "invalid projection"

[Mario Carneiro]

So it seems like this is actually an ill-formed definition OK._cstage1 being produced by the compiler. (unsafe def turns off some checks in the kernel, but not this one)

[Mario Carneiro]

this does make some sense, because the compiler erases Eq.rec terms, which can produce ill formed expressions, and this has been the source of several compiler bugs. I think you should report this. The new compiler uses a custom typechecker instead of reusing lean's typechecker in order to better handle these kind of weakly typed terms

[Mario Carneiro]

As added evidence that this is the issue,

noncomputable def OK {γ α β} (h: γ = prod α β) (a: α.de) (c: γ.de): Bool :=
  a == (h ▸ c).1

compiles fine (using noncomputable to tell the compiler not to try to produce the bad auxiliary defs)

[David Richter]

I think you should report this

Like this https://github.com/leanprover/lean4/issues/3761 ?