Zulip Chat Archive

Stream: general

Topic: 'unreachable' code was reached


Eric Wieser (Apr 26 2021 at 11:45):

This produces an error message I've never seen before on the {:

import algebra.group.defs

variables {X : Type*}

structure is_unital (m : X  X  X) (e : X) extends is_left_id _ m e, is_right_id _ m e.

lemma mul_one_class.is_unital [G : mul_one_class X] : is_unital (*) (1 : X) :=
{ left_id := one_mul, right_id := mul_one }

'unreachable' code was reached

Kevin Buzzard (Apr 26 2021 at 11:48):

Oh classy! That one used to show up all the time, until Gabriel hacked core Lean to make it go away. I've not seen it for years!

Eric Wieser (Apr 26 2021 at 11:49):

There are still about 100 lean_unreachable() calls in lean core, so it's not entirely clear which one is being hit here

Eric Wieser (Apr 26 2021 at 11:50):

It looks like if you have a debug build of lean it actually shows file/line numbers

Kevin Buzzard (Apr 26 2021 at 12:23):

File: /home/runner/work/lean/lean/src/frontends/lean/elaborator.cpp
Line: 3025

Eric Wieser (Apr 26 2021 at 12:37):

https://github.com/leanprover-community/lean/blob/af06b6aab669edfee7e310c5eab4c948bba173bb/src/frontends/lean/elaborator.cpp#L3025

Alyssa Renata (Jan 27 2022 at 19:05):

I have this issue where having an encodable instance causes the 'unreachable' code was reached error. Here's the MWE:

import tactic

inductive Form (vars : Type) : Type
| Bottom : Form
| Var : vars  Form

variables {vars : Type} [encodable vars]

instance : has_bot (Form vars) := Form.Bottom

def eval (v : vars  bool) : Form vars  bool
|  := false
| (Form.Var x) := v x

However if I reorder it as below, the error disappears:

import tactic

inductive Form (vars : Type) : Type
| Bottom : Form
| Var : vars  Form

variables {vars : Type}
instance : has_bot (Form vars) := Form.Bottom
variable [encodable vars]

def eval (v : vars  bool) : Form vars  bool
|  := false
| (Form.Var x) := v x

Kevin Buzzard (Jan 27 2022 at 19:07):

Alyssa is on my course and this is her first coursework :-/

Kevin Buzzard (Jan 27 2022 at 19:27):

Mathlib-free:

inductive Form (vars : Type) : Type
| Bottom : Form
| Var : vars  Form

variables {vars : Type} [nonempty vars]

class has_bot (α : Type) := (bot : α)

notation `⊥` := has_bot.bot

attribute [pattern] has_bot.bot

instance : has_bot (Form vars) := Form.Bottom

def eval (v : vars  bool) : Form vars  bool -- 'unreachable' code was reached
|  := false
| (Form.Var x) := v x

Yury G. Kudryashov (Jan 31 2022 at 00:56):

If you use a type in a definition or a lemma, then lean pulls all instances from variables for this type

Yury G. Kudryashov (Jan 31 2022 at 00:58):

Probably unused args cause the trouble later because lean can't unify them

Yury G. Kudryashov (Jan 31 2022 at 00:58):

This is just a guess

Yuyang Zhao (Jan 17 2023 at 03:07):

I get this error in refl_zero.

I have to write by { dsimp [function_type.equiv], refl } to get rid of this error.

Kyle Miller (Jan 17 2023 at 09:27):

@Yuyang Zhao A simpler workaround is by exact rfl.

This "unreachable code was reached" error comes from a small bug that likely won't be fixed since this workaround exists. Here's the line that raises the alarm. I haven't done an in-depth analysis, but here is what I believe is going on: First, there is a feature in Lean called a "rfl lemma." These are lemmas that dsimp is allowed to use, since any equality that is provable by rfl is a definitional equality. The way Lean determines what is a rfl lemma is by looking at the literal proof and seeing if it's rfl or iff.rfl (so your lemma is a rfl lemma due to this check). Then this part of the code is checking whether this rfl lemma is an iff or an equality, since both of these are handled a little differently, and once processed they're added to the list of rfl lemmas. However, your lemma produces a function_type.equiv, which is neither, so this supposedly unreachable code on line 887 is reached.

By using by exact rfl instead, the proof isn't literally rfl, so then Lean doesn't think it's a rfl lemma, and so it doesn't try processing it as one.

Eric Wieser (Jan 17 2023 at 11:41):

Is this possible to reproduce with something like 1 ∈ [1] := rfl?

Kyle Miller (Jan 17 2023 at 15:01):

Yeah, it's easy to come up with something that reproduces it:

def blah := 37 = 37

@[simp] lemma foo : blah := rfl

Note that it also reports "not a rfl-lemma, even though marked as rfl" in addition to "'unreachable' code was reached". Removing the @[simp] causes it to report just the "not a rfl-lemma" error.


Last updated: Dec 20 2023 at 11:08 UTC