Compiler error with sizeOf

Stream: new members

[Josh Cohen]

I am experiencing some strange behavior with sizeOf. I can declare a type that takes in a parameter and write a sizeOf function, then instantiate with a concrete type:

inductive bar (A: Type) where
  | A1 (x : A) (y: bar A)
  | A2

def bar.sizeOf (b: bar A) : Nat :=
  match b with
  | A2 => 0
  | A1 x y => 1 + SizeOf.sizeOf x + y.sizeOf

inductive a where
  | foo (x: Nat)

def test : bar a := .A1 (.foo 1) .A2
#eval (test.sizeOf) -- Prints 1

But if I directly create the concrete type, I get an error:

inductive bar' where
  | A3 (x: a) (y: bar')
  | A4

def bar'.sizeOf (b: bar') : Nat :=
  match b with
  | A4 => 0
  | A3 x y => 1 + SizeOf.sizeOf x + y.sizeOf

failed to compile definition, compiler IR check failed at `sizeOf`. Error: depends on declaration 'a._sizeOf_inst', which has no executable code; consider marking definition as 'noncomputable'

Does anyone know why this is the case or how to fix it?

[Aaron Liu]

The compiler doesn't compile the SizeOf instances

[Josh Cohen]

I don't understand why the abstract version works and evaluates but the concrete version raises an error even when the end result should be the same in both cases.

[Aaron Liu]

hmm, not sure why the abstract version evaluates

[Aaron Liu]

maybe it's a bug

[Aaron Liu]

maybe it's because it was compiled again because of specialization

[Robin Arnez]

In the "abstract" version bar.sizeOf uses instSizeOfDefault i.e. SizeOf.sizeOf x = 0 (which is obviously computable) whereas bar'.sizeOf uses the actual SizeOf instance of a (which is not compiled and thus noncomputable)

[Robin Arnez]

A fair comparison would be bar'.sizeOf and

inductive bar (A: Type) where
  | A1 (x : A) (y: bar A)
  | A2

def bar.sizeOf [SizeOf A] (b: bar A) : Nat :=
  match b with
  | A2 => 0
  | A1 x y => 1 + SizeOf.sizeOf x + y.sizeOf

inductive a where
  | foo (x: Nat)

def test : bar a := .A1 (.foo 1) .A2
#eval (test.sizeOf) -- Fails
#reduce test.sizeOf -- 3

[Joachim Breitner]

Should we make instSizeOfDefault noncomputable for uniformity?
Let’s try: https://github.com/leanprover/lean4/pull/11505

[Joachim Breitner]

This breaks mathlib in uses of Mathlib.Util.CompileInductive. Not going to investigate for now.