Description
Prerequisites
Please put an X between the brackets as you perform the following steps:
- Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
Using the projection on an unsafeCast sometimes leads to an unhelpful and probably wrong "unknown free variable : _neutral" error.
def x : Type := Nat -- using some x of type Type, 1 = 1 or (Unit → Prop) will also fail, but not if x : Nat
/-- error: unknown free variable: _neutral -/
#guard_msgs in
unsafe example := (unsafeCast x : Unit × Unit).1In one case, I even get a segfault:
def x : Unit := .unit -- if we use sorry, we get no error whatsoever
unsafe example := (unsafeCast x : Unit × Unit).1Context
I don't know of any relevant additional context, the issue should be fairly self-contained. I ran into this issue while tinkering with efficient ways to use partial_fixpoint for monadic extrinsic termination proofs (I get the error in this file.)
Steps to Reproduce
Run the code from the description in Lean Web.
The segfault can also be reproduced in Lean Web.
Expected behavior:
No error: it should be perfectly fine to take the first projection of any tuple, including tuples obtained from unsafeCast.
Even if some unsafe expression leads to segfaults after compilation, it should not segfault at compile time.
Actual behavior:
Error: "unknown free variable: _neutral" / segfault.
Versions
Lean Web version used:
Lean 4.21.0-nightly-2025-05-19
Target: x86_64-unknown-linux-gnu
Additional Information
The error only appears for some types of x. The best pattern I can see is that we get this error whenever x has a type that would allow the compiler to erase x. For example, the error remains if x is of type Prop, Type or 1 = 1, all of which might be good candidates for erasure. However, if x is of type Nat, I don't get the error.
Unit is a peculiar case. With x : Unit := sorry, no error occurs, but with x : Unit := .unit we get a segfault. I suspect that the compiler tries to evaluate the expression in order to optimize it away, but that's a dangerous thing to do with unsafe code. I don't know where the segfault happens exactly but I suspect it's somewhere in the compiler.
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.