'unreachable' code was reached

Stream: general

[Eric Wieser]

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]

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]

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]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Alyssa Renata]

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]

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

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

This is just a guess

[Yuyang Zhao]

I get this error in refl_zero.

#mwe

universes u v

namespace list

inductive dependent {α : Type u} (β : α → Sort v) : list α → Type (max u v)
| nil : dependent []
| cons {a : α} (b : β a) {l : list α} : dependent l → dependent (a :: l)

infixr ` ᵈ:: `:67 := list.dependent.cons
notation `ᵈ[` l:(foldr `, ` (h t, list.dependent.cons h t) list.dependent.nil `]`) := l

end list

def function_type : list (Sort u) → Sort u → Sort u
| []        β := β
| (α :: tl) β := α → function_type tl β

def function_type.equiv : Π {args : list (Sort u)} (ss : args.dependent setoid) (β : Sort u),
  function_type args β → function_type args β → Prop
| []      ᵈ[]      β f₁ f₂ := f₁ = f₂
| (α::tl) (sᵈ::ss) β f₁ f₂ := ∀ a b : α, s.r a b → function_type.equiv ss β (f₁ a) (f₂ b)

@[simp] lemma refl_zero {β} (b : β) : function_type.equiv list.dependent.nil β b b := rfl

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

[Kyle Miller]

@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]

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

[Kyle Miller]

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.