Inductive type compilation error

Stream: general

[Jesse Michael Han]

What's up with the following error? The presence of the complete_boolean_algebra instance in the following code

universe u

inductive B_name (β : Type u) [complete_boolean_algebra β] : Type (u+1) -- complains only if complete_boolean_algebra instance is there
| mk (α : Type u) (A : α → (B_name × β)) : B_name

results in the following error message:

23:1: nested inductive type compiled to invalid inductive type
nested exception message:
type mismatch at definition '_nest_1_1.prod.B_name.mk.sizeof_spec', has type
  ∀ (β : Type u) [_inst_1 : complete_boolean_algebra β] [β_inst_inst : has_sizeof β]
  (fst : _nest_1_1.B_name β _inst_1) (snd : β),
    _nest_1_1.prod.B_name.sizeof β _inst_1 β_inst_inst (_nest_1_1.prod.B_name.mk β _inst_1 fst snd) =
      _nest_1_1.prod.B_name.sizeof β _inst_1 β_inst_inst (_nest_1_1.prod.B_name.mk β _inst_1 fst snd)
but is expected to have type
  ∀ (β : Type u) [_inst_1 : complete_boolean_algebra β] [β_inst_inst : has_sizeof β]
  (fst : _nest_1_1.B_name β _inst_1) (snd : β),
    _nest_1_1.prod.B_name.sizeof β _inst_1 β_inst_inst (_nest_1_1.prod.B_name.mk β _inst_1 fst snd) = 1 + sizeof snd

[Mario Carneiro]

That's a nested inductive type

[Mario Carneiro]

these aren't compiled very well

[Jesse Michael Han]

Does the presence of the complete_boolean_algebra instance make it nested, or is it nested because of the type of the constructor mk?

[Mario Carneiro]

an isomorphic regular inductive is

inductive B_name (β : Type u) [complete_boolean_algebra β] : Type (u+1) -- complains only if complete_boolean_algebra instance is there
| mk (α : Type u) (A : α → B_name) (B : α → β) : B_name

[Mario Carneiro]

it's the fact that you used a product of some type that hasn't been constructed yet

[Jesse Michael Han]

I see... I guess it's "simpler" to just specify two simultaneous values instead of specifying a pair as a value

[Jesse Michael Han]

Thanks for clarifying!

[Mario Carneiro]

Well, it's mostly the fact that inductives have a strict specification on what is allowed in the constructors, and other inductive types aren't in that specification. Lean has a trick for compiling them anyway, but it's complicated and not completely correct in some edge cases