unassigned metavariable 暗黙引数を推論できない（メタ変数が確定していない）

Error message

don't know how to synthesize implicit argument
  @DFUMT8.toBool ?a
context:
⊢ DFUMT8

Sometimes surfaces instead as:

unassigned metavariable
  ?m.42 : DFUMT8

Both messages come from the same underlying condition: after elaboration the term still contains a metavariable Lean could not resolve. The compiler cannot invent the missing value on its own.

Minimal reproduction

-- File: Meta.lean
import LeanDFumt
open LeanDFumt

example : DFUMT8.toBool _ = true := by decide
Meta.lean:4:26: error: don't know how to synthesize implicit argument
  @DFUMT8.toBool ?a
context:
⊢ DFUMT8

The underscore _ asks Lean to fill in a value of type DFUMT8. Nothing in the surrounding expression constrains which of the eight values it should be, so elaboration gives up.

Why it happens

Lean's elaborator solves metavariables by unification. It walks the expression, records constraints, and tries to satisfy all of them. When a metavariable has no constraint that fixes its value — no equality, no type-class instance, no unique inhabitant — the elaborator has no basis for a choice and reports failure rather than guess.

Fix

Supply the value explicitly. In the LeanDFumt case, pick which of the eight truth values you actually meant:

example : DFUMT8.toBool .TRUE  = true  := by decide
example : DFUMT8.toBool .BOTH  = true  := by decide  -- BOTH collapses to true
example : DFUMT8.toBool .FALSE = false := by decide

For quantified statements, bind the value first with intro:

example : ∀ a : DFUMT8, DFUMT8.toBool a = DFUMT8.toBool a := by
  intro a
  rfl

For implicit type arguments elsewhere, use the (t := …) named-argument syntax:

-- Instead of List.length _
example : List.length (α := DFUMT8) [] = 0 := rfl

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): Lean fails elaboration without producing a VERDICT line; verify() returns UNDECIDED / UNSUPPORTED_SYNTAX with the first don't know how to synthesize or unassigned metavariable line preserved in detail. Distinguishable from type mismatch by grouping stats().reason_breakdown.UNSUPPORTED_SYNTAX on the leading substring of detail.

Post-v0 Layer 2 (planned — spec §13): locate_first_error(kind = "metavariable") returns the position and expected type of the first unresolved metavariable reported by the elaborator. When paired with Lean.MessageData parsing, this can be surfaced as a concrete list of candidate values (e.g. all eight DFUMT8 constructors) to speed up interactive fixes. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also