'unreachable' code was reached

Stream: new members

[Patrick Johnson]

Lean version 3.35.1

inductive P : Prop
| mk : id P → P

Error: 'unreachable' code was reached. What does it mean?

[Reid Barton]

in this case, it indicates a bug in Lean

[Reid Barton]

Do you have a real example?

[Reid Barton]

It's hard to guess what feature(s) of id might be relevant

[Patrick Johnson]

In Lean 4 it gives a much better error: only trivial inductive applications supported in premises

[Huỳnh Trần Khanh]

Reid Barton said:

Do you have a real example?

hmm what do you mean by "real example"? I ran exactly that code on TIO and it produced the exact same error, so this is pretty much a #mwe

[Reid Barton]

An example which achieves something useful

[Mario Carneiro]

You can actually get a whole bunch of distinct errors for various combinations of whether it is a def or abbreviation, and whether it is constructing a simple kernel inductive or a nested inductive in the end:

def foo (X : Type) := X × X
set_option trace.inductive_compiler.nested.simp.failure true
inductive P : Type | mk : foo P → P
-- simplifier failed to prove goal; trace 'inductive_compiler.nested.simp.failure' for more information

-- [inductive_compiler.nested.simp.failure]
-- -------------------

def foo2 (X : Type) := X
inductive P2 : Type | mk : foo2 P2 → P2
-- type mismatch at definition 'P2.mk.sizeof_spec', has type
--   ∀ (ᾰ : foo2 P2), P2.sizeof (P2.mk ᾰ) = P2.sizeof (P2.mk ᾰ)
-- but is expected to have type
--   ∀ (ᾰ : foo2 P2), P2.sizeof (P2.mk ᾰ) = 1

abbreviation foo3 (X : Type) := X × X
inductive P3 : Type | mk : foo3 P3 → P3 -- ok

#check @P3.mk -- P3.mk : foo3 P3 → P3
#check @P3.rec -- P3.rec : Π (C : P3 → Sort u_1), (Π (ᾰ : P3 × P3), C (P3.mk ᾰ)) → Π (x : P3), C x

abbreviation foo4 (X : Type) := X
inductive P4 : Type | mk : foo4 P4 → P4 -- ok

#check @P4.mk -- P4.mk : foo4 P4 → P4
#check @P4.rec -- P4.rec : Π {motive : P4 → Sort u_1},
               --   (Π (ᾰ : foo4 P4), motive ᾰ → motive (P4.mk ᾰ)) → Π (n : P4), motive n

abbreviation foo5 (X : Prop) := X ∧ X
inductive P5 : Prop | mk : foo5 P5 → P5
-- invalid nested occurrence 'and P5 P5', either both must eliminate to Type or both must eliminate only to Prop

abbreviation foo6 (X : Prop) := X
inductive P6 : Prop | mk : foo6 P6 → P6 -- ok

#check @P6.mk -- P6.mk : foo6 P6 → P6
#check @P6.rec -- P6.rec : Π {motive : Sort u_1}, (foo6 P6 → motive → motive) → P6 → motive
#check @P6.drec -- P6.drec : Π {motive : P6 → Sort u_1}, (Π (ᾰ : foo6 P6), motive ᾰ → motive _) → Π (n : P6), motive n

def foo8 (X : Prop) := X
inductive P8 : Prop | mk : foo8 P8 → P8
-- LEAN ASSERTION VIOLATION
-- File: /home/mario/Documents/lean/lean/src/library/constructions/drec.cpp
-- Line: 132
-- Task: /home/mario/Documents/lean/lean/library/test.lean: parsing at line 41
-- j - num_fields < recursive_params.size()

[Mario Carneiro]

Part of the problem is that I'm not sure what the answer is even supposed to be. The error occurs during the construction of the type of the T.drec recursor for the inductive type, and you can see that different combinations here result in different types. Notice, for example, that the minor premise of P3.rec unfolds the definition in (ᾰ : P3 × P3), while P4.rec and P6.drec don't: (ᾰ : foo4 P4)

[Patrick Johnson]

Should I worry about the consistency of the kernel? The 'unreachable' code was reached indicates that someone didn't expect such use case, which means that there may be something like:

inductive Not : Prop → Prop
| mk : Π p, ¬p → Not p

inductive P : Prop
| mk : Not P → P

that would allow us to prove P ↔ ¬P and then 0 = 1

[Mario Carneiro]

This code is not part of the kernel

[Mario Carneiro]

The issue is not with the kernel spec, but rather what the front end is allowed to desugar to the kernel spec. The kernel spec says nothing about definitions, and would reject all these examples, but the front end thinks it would be fine as long as the generated types are defeq to the kernel types

[Mario Carneiro]

and then there is additional complication when it is a nested inductive, in which case even after unfolding definitions you get something that is not a valid kernel inductive and the front end does a more complicated simulation of the nested inductive (which is known to have bugs and be generally unreliable)