invalid projection from Meta.reduce

[marcusrossel]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The following code snippet (thanks @kmill) unexpectedly produces the error invalid projection s.1:

import Lean
open Lean Meta Elab Term

elab "#reduce'" t:term : command => Elab.Command.runTermElabM fun _ => do
  let e ← withSynthesize <| elabTerm t none
  let e ← Meta.reduce e
  logInfo m!"{← inferType e}"

structure S where
  x : Nat

def S' := S
def S'.x (s : S') : Nat := S.x s

attribute [irreducible] S'

variable (s : S')
#reduce' s.x -- invalid projection s.1

Context

This issue has been discussed on Zulip. The problem originally arose in the following code snippet:

import Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
import Lean
open Lean Meta

elab "#fails" : term => do
  let info ← getConstInfo ``SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty
  forallTelescopeReducing info.type fun _ body => do
    match body.eq? with
    | none => return mkNatLit 0
    | some (_, lhs, _) => 
      let _ ← Meta.reduceAll lhs
      return mkNatLit 0

#eval #fails -- invalid projection g.1

The intent was to get the type of SimplicialObject.Splitting.πSummand_comp_ιSummand_comp_PInfty_eq_PInfty, extract its underlying equality, and reduce the type of each side of the equality. This produces an error that is hard to understand as it references a term g whose origin isn't immediately clear.

Steps to Reproduce

Run the code snippet shown in the description using Lean version 4.3.0-rc2.

Expected behavior: The command #reduce' s.x prints the type Nat.

Actual behavior: The command #reduce' s.x fails with the error invalid projection s.1.

Versions

#eval Lean.versionString -- "4.3.0-rc2"

$ sw_vers
ProductName:		macOS
ProductVersion:		14.0
BuildVersion:		23A344

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[leodemoura]

The failure occurs at inferProjType. Meta.reduce reduces S'.x s to s.1, but then inferProjType fails because S' is [irreducible].

[nomeata]

I just ran into something similar. It’s not quite the same, but while debugging I think we can fix this issue by setting the transparency to .all not only while reducing, but also in the subsequent

        withTransparency .all <|  logInfoAt tk e

In the example above, it is the call

  logInfo m!"{← inferType e}"

that one should wrap in withTransparency .all.

However, that didn't quite work, due to #5562. The fix for that, in #5563, can also be considered a fix for this issue, and includes it as a test case.