`simp`, `omega` in `module` cause type mismatch in kernel

[datokrat]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
• [x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
• [x] 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

A call to simp followed by omega in a module leads to an "application type mismatch" error in the kernel. The problem seems to be related to Int8.reduceToInt.

Steps to Reproduce

Run this:

module

-- import all Init.Data.SInt.Basic -- solves the problem

/--
error: (kernel) application type mismatch
  Eq.trans
    (congrArg (fun x => (Int8.ofInt x).toInt)
      (congr (congrArg (fun x => HAdd.hAdd ↑x) (UInt8.toNat_add x 1)) (Int8.toInt_neg 128)))
    Int8.toInt_ofInt
argument has type
  (Int8.ofInt (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8))).toInt =
    (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size
but function has type
  (Int8.ofInt (↑((x.toNat + UInt8.toNat 1) % 2 ^ 8) + (-Int8.toInt 128).bmod (2 ^ 8))).toInt =
      (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size →
    (Int8.ofInt (↑(x + 1).toNat + (-128).toInt)).toInt =
      (↑(x.toNat + 1) % ↑(2 ^ 8) + (- -128).bmod (2 ^ 8)).bmod Int8.size
-/
#guard_msgs in
example {x : UInt8}
    (h : (Int8.ofInt (↑(x + 1).toNat + Int8.minValue.toInt)).toInt = Int8.minValue.toInt) :
    256 ∣ ↑x.toNat + 1 := by
  -- squashed form of: simp [Int.natCast_emod, Int.bmod_eq_iff] at h ⊢
  -- reducing `Int8.reduceToInt` solves the problem
  simp only [UInt8.toNat_add, UInt8.reduceToNat, Int.natCast_emod, Int.cast_ofNat_Int, Int8.toInt_neg,
    Int8.reduceToInt, Int8.toInt_ofInt, Nat.zero_lt_succ, Int.bmod_eq_iff] at h ⊢
  omega

Expected behavior:

Either omega or simp themselves fail, or they succeed and generate a proof term the kernel is happy with.

Actual behavior:

simp and omega together create a proof term that does not type check in the kernel.

(Note that omega does not see anything related to Int8, so that omega itself does not really seem to be the problem. However, the error also goes away if omega is replaced with sorry.)

Versions

Lean 4.25.0-nightly-2025-09-24
Target: x86_64-unknown-linux-gnu

Impact

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

[nomeata]

Int.reducetoInt is a simproc using Int8.toInt. Have you tried adding @[expose] to def Int8.toInt (i : Int8) : Int := i.toBitVec.toInt?

[datokrat]

That indeed solves the MWE, but it turns out that in the actual situation I had, I need to expose lots of defs.

not so minimal working example

module

prelude
public import Init.Data.SInt
import Init.Data.Range.Polymorphic.UInt

open Std Std.PRange

private def UInt8.toInt8Mono (a : UInt8) : Int8 :=
  Int8.ofInt (↑a.toNat + Int8.minValue.toInt)

instance : UpwardEnumerable Int8 where
  succ? i := if i + 1 = Int8.minValue then none else some (i + 1)
  succMany? n i :=
    have := i.minValue_le_toInt
    if h : i.toInt + n ≤ Int8.maxValue.toInt then some (.ofIntLE _ (by omega) h) else none

/--
warning: declaration uses 'sorry'
---
error: (kernel) application type mismatch
  Eq.trans (Int8.toInt_neg 128) (congrArg (fun x => x.bmod 256) (Int.neg_neg 128))
argument has type
  (fun x => x.bmod 256) (- -128) = (fun x => x.bmod 256) 128
but function has type
  (-Int8.toInt 128).bmod (2 ^ 8) = Int.bmod 128 256 → (-128).toInt = Int.bmod 128 256
-/
#guard_msgs in
private theorem succ?_toInt8Mono {x : UInt8} :
    UpwardEnumerable.succ? x.toInt8Mono = UInt8.toInt8Mono <$> UpwardEnumerable.succ? x := by
  simp [succ?]
  split <;> rename_i h
  · rw [if_pos]
    · simp [-Int8.reduceToInt]
    · simp [UInt8.toInt8Mono, ← UInt8.toNat_inj, ← Int8.toInt_inj, ← Int.ofNat_inj,
        Int.natCast_emod, Int.emod_eq_iff, Int.bmod_eq_iff] at h ⊢
      omega
  · sorry

In this longer example, I also need to expose Int8.neg, Int8.toInt, Int8.ofInt, Int8.toBitVec and (for dependency reasons) Int8.ofUInt8.