Skip to content

shake incorrectly removes imports providing typeclass instances used by inferInstanceAsΒ #13417

@bryangingechen

Description

@bryangingechen

Prerequisites

  • 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, (tested against both v4.30.0-rc1 and nightly-2026-04-15`)

Description

Imports providing a typeclass instance are incorrectly removed by shake when the instance is resolved via
inferInstanceAs rather than by direct name reference. Minimal example provided in https://github.com/bryangingechen/shake-bug-inferInstanceAs .

Context

Found while running lake shake against mathlib4. Zulip thread.

Steps to Reproduce

  1. git clone https://github.com/bryangingechen/shake-bug-inferInstanceAs && cd shake-bug-inferInstanceAs
  2. lake build: succeeds
  3. lake shake --fix
  4. lake build: now fails

Expected behavior: Such imports should not be removed.

Actual behavior: Imports are removed, breaking the build.

Versions

v4.30.0-rc1

Impact

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions