type mismatch (Nat vs Float) 数値式が Nat だが Float が要求されている

Error message

type mismatch
  n
has type
  Nat : Type
but is expected to have type
  Float : Type

This surfaces whenever a term of type Nat is used where Float is required. Numeric literals are polymorphic in Lean 4 via OfNat, so (3 : Float) works. The mismatch happens for terms — variables, arithmetic expressions, function results — where the elaborator has committed to Nat.

Minimal reproduction

-- File: Example.lean
def anchor (n : Nat) : Float := n
Example.lean:1:32: error: type mismatch
  n
has type
  Nat : Type
but is expected to have type
  Float : Type

Both types are in Lean 4 core — Float lives in Init.Data.Float — so this error appears without any Mathlib import.

Why it happens

There is no automatic coercion from Nat to Float in Lean 4 core. This is deliberate: floating-point conversion is lossy and non-associative, so the language forces the author to spell out where the boundary is.

Fix

Insert an explicit conversion:

-- Option A: dot notation
def anchor (n : Nat) : Float := n.toFloat

-- Option B: qualified call
def anchor' (n : Nat) : Float := Float.ofNat n

In LeanDFumt, this pattern shows up when writing numeric anchors for the eight-valued logic — for example the toFloat map on DFUMT8 that Papers 75 / 76 use for the QuTiP bridge. The fix is the same: convert at the boundary. 

-- Analogous DFUMT8 case: DFUMT8 → Float
example : (DFUMT8.TRUE.toTernary : Int).toNat.toFloat > 0.0 := by native_decide

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): Lean rejects elaboration, so no VERDICT line is emitted on stdout. verify() returns UNDECIDED / UNSUPPORTED_SYNTAX with the first type mismatch diagnostic carried in detail. A concentration of UNSUPPORTED_SYNTAX under stats().reason_breakdown whose detail lines lead with type mismatch is the direct v0 signal that this error class is active in the workload — and per spec §7 it becomes the next sprint.

Post-v0 Layer 2 (planned — spec §13): locate_first_error(kind = "type_mismatch") returns the position and pair (actual_type, expected_type) of the first elaboration failure whose Lean-emitted category is type mismatch. Useful for downstream tooling that suggests the corresponding .toX or X.ofY coercion. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also