Unexpected Error

Stream: lean4

[Sofia Rodrigues]

inductive Danger
  | high
  | low

inductive Class : Danger -> Type
  | golden : Class Danger.high
  | silver : Class Danger.low

structure Adventurer (x: Danger) where
  name : String
  classif : Class x

def highDanger? (x: Adventurer x) : Bool :=
  match x.classif with
  | Class.golden => true
  | Class.silver => false

I can't use this code because of this error:

compiler IR check failed at 'highDanger?._rarg', error: unexpected type 'obj', scalar expected

Why I'm having this error and how to fix it?

[Eric Wieser]

You can work around it for now by adding noncomputable to tell the compiler not to compile it at all

[Eric Wieser]

But this looks like a bug

[Eric Wieser]

Another workaround would be

def highDanger {d} (a : Adventurer d) : Bool :=
  match d with
  | Danger.high => true
  | Danger.low => false

[Mac Malone]

The underlying bug here is that the compiler IR is mistyping the x.classif sproj as an Lean object (obj) rather than the primitive scalar u8:

/-
[init]
def highDanger?._rarg (x_1 : obj) : u8 :=
  let x_2 : obj := sproj[1, 0] x_1;
  case x_2 : obj of
  Class.golden →
    let x_3 : u8 := 1;
    ret x_3
  Class.silver →
    let x_4 : u8 := 0;
    ret x_4
def highDanger? (x_1 : u8) : obj :=
  let x_2 : obj := pap highDanger?._rarg;
  ret x_2
-/
set_option trace.compiler.ir true in
def highDanger? (x: Adventurer d) : Bool :=
  match x.classif with
  | Class.golden => true
  | Class.silver => false

[Mac Malone]

@Henrik Böving may have some clue why this occurs due to his familiarity with the compiler.

[Henrik Böving]

It seems it already fucked up in the init phase of the Lean part so this is a bug in the C++ part of the compiler which I don't know much about as we want to get rid off it anyways...I guess you can open an issue about it and it will be put onto the "new code generator" pile