Zulip Chat Archive

Stream: general

Topic: Inductive type compilation error


view this post on Zulip Jesse Michael Han (Feb 02 2019 at 05:12):

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

view this post on Zulip Mario Carneiro (Feb 02 2019 at 05:17):

That's a nested inductive type

view this post on Zulip Mario Carneiro (Feb 02 2019 at 05:17):

these aren't compiled very well

view this post on Zulip Jesse Michael Han (Feb 02 2019 at 05:18):

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

view this post on Zulip Mario Carneiro (Feb 02 2019 at 05:19):

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

view this post on Zulip Mario Carneiro (Feb 02 2019 at 05:20):

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

view this post on Zulip Jesse Michael Han (Feb 02 2019 at 05:21):

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

view this post on Zulip Jesse Michael Han (Feb 02 2019 at 05:21):

Thanks for clarifying!

view this post on Zulip Mario Carneiro (Feb 02 2019 at 05:24):

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


Last updated: May 08 2021 at 19:11 UTC