9077, with options, downstream

src/Lean/Meta/ExprDefEq.lean

@@ -82,6 +82,90 @@ register_builtin_option backward.isDefEq.implicitBump : Bool := {
   not just instance-implicit ones"
 }
 
+/--
+Controls whether the transparency bump for implicit arguments is also applied in the first pass
+of `isDefEqArgs`, where an argument pair is unified eagerly because one side is an unassigned
+metavariable (the "easy cases" of `isDefEqArgsFirstPass`).
+
+Without the bump, such pairs are unified at the caller's transparency: inside type class
+resolution, the metavariable assignment — including the type check and the
+`backward.isDefEq.instanceTypes` fallbacks it triggers — then runs at `.instances`, even though
+the same argument pair would have been checked at `.implicit` had it been postponed to the
+second pass. Whether an argument gets the bump should not depend on which side happens to be an
+unassigned metavariable.
+
+Which arguments are bumped follows the same rules as the second pass: instance-implicit
+arguments always (when `backward.isDefEq.respectTransparency` is `true`), other implicit
+arguments only if `backward.isDefEq.implicitBump` is `true`. This option only has an effect when
+`backward.isDefEq.respectTransparency` is `true`.
+-/
+register_builtin_option backward.isDefEq.firstPassBump : Bool := {
+  defValue := true
+  descr    := "if true, apply the `.implicit` transparency bump for implicit arguments also in \
+  the eager (unassigned-metavariable) cases of the first pass of `isDefEqArgs`"
+}
+
+/--
+Controls how assignments to instance-typed metavariables (see
+`MetavarContext.instanceTypedMVars`) are restricted so that the final value of a
+metavariable created for an instance-implicit argument has the type the metavariable was
+created with, up to `TransparencyMode.instances`. This prevents unification from committing
+to an instance for a type that is different at instance-resolution time. See issue #9077.
+
+Valid values:
+- `"none"`: no restriction (the behavior before the fix for issue #9077).
+- `"mark"`: the value's type must match the metavariable's type at `.instances`
+  transparency, and the metavariables in type-determining (spine) positions of the value
+  inherit the restriction.
+- `"synth"`: the value must be free of metavariables and its type must match at `.instances`
+  transparency. Otherwise, the instance is synthesized directly and the value must be
+  definitionally equal to the synthesized instance; if synthesis fails, the assignment (and
+  with it the current unification attempt) fails.
+- `"markOrSynth"`: like `"synth"`, but a value whose spine metavariables are all themselves
+  instance-typed or not assignable by `isDefEq` is also accepted, provided its type matches
+  at `.instances` transparency.
+- `"synthOrStuck"`/`"markOrSynthOrStuck"`: like `"synth"`/`"markOrSynth"`, except that when
+  the fallback synthesis fails while the metavariable's type still contains metavariables,
+  the enclosing type class resolution is treated as stuck (postponed and retried by the
+  elaborator once more metavariables are solved) instead of failing definitively.
+-/
+register_builtin_option backward.isDefEq.instanceTypes : String := {
+  defValue := "mark"
+  descr    := "controls how assignments to instance metavariables are restricted to \
+  preserve the type up to `.instances` transparency; valid values: \"none\", \"mark\", \
+  \"synth\", \"markOrSynth\", \"synthOrStuck\", \"markOrSynthOrStuck\""
+}
+
+/-- Assignment policy for instance-typed metavariables. See `backward.isDefEq.instanceTypes`. -/
+inductive InstanceTypesMode where
+  /-- No restriction. -/
+  | none
+  /-- Check the value's type at `.instances` transparency and propagate the restriction to
+  the value's spine metavariables. -/
+  | mark
+  /-- Require an mvar-free value whose type matches at `.instances` transparency; otherwise
+  synthesize the instance and unify the value with it. -/
+  | synth
+  /-- Like `synth`, but also accept values whose spine metavariables are all instance-typed
+  or not assignable by `isDefEq` (see `spineMVarsAdmissible`). -/
+  | markOrSynth
+  /-- Like `synth`, but report the problem as stuck instead of failing when the fallback
+  synthesis fails while the metavariable's type is not fully determined. -/
+  | synthOrStuck
+  /-- Like `markOrSynth`, but report the problem as stuck instead of failing when the
+  fallback synthesis fails while the metavariable's type is not fully determined. -/
+  | markOrSynthOrStuck
+
+def getInstanceTypesMode : CoreM InstanceTypesMode := do
+  match backward.isDefEq.instanceTypes.get (← getOptions) with
+  | "none"               => return .none
+  | "mark"               => return .mark
+  | "synth"              => return .synth
+  | "markOrSynth"        => return .markOrSynth
+  | "synthOrStuck"       => return .synthOrStuck
+  | "markOrSynthOrStuck" => return .markOrSynthOrStuck
+  | val => throwError "invalid value `{val}` for option `backward.isDefEq.instanceTypes`, valid values are \"none\", \"mark\", \"synth\", \"markOrSynth\", \"synthOrStuck\", and \"markOrSynthOrStuck\""
+
 register_builtin_option trace.Meta.isDefEq.printTransparency : Bool := {
   defValue := false
   descr    := "if true, prefix `Meta.isDefEq` `=?=` trace messages with the current transparency level"
@@ -285,6 +369,23 @@ inductive DefEqArgsFirstPassResult where
   -/
   | ok (postponedImplicit : Array Nat) (postponedHO : Array Nat)
 
+/--
+Ensure `MetaM` configuration is strong enough for checking definitional equality of
+implicit and instance-implict arguments as well as assigned mvar types. Bumps transparency to at
+least `.implicit`, so both `[instance_reducible]` and `[implicit_reducible]` unfold.
+-/
+@[inline] def withImplicitConfig (x : MetaM α) : MetaM α := do
+  let old ← getTransparency
+  if old.lt .implicit then
+    trace[Meta.isDefEq.transparency]
+      "raising transparency {toString old} → implicit"
+  withAtLeastTransparency .implicit do
+    let cfg ← getConfig
+    if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
+      x
+    else
+      withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta }) x
+
 /--
   First pass for `isDefEqArgs`. We unify explicit arguments, *and* easy cases
   Here, we say a case is easy if it is of the form
@@ -318,6 +419,10 @@ inductive DefEqArgsFirstPassResult where
 -/
 private def isDefEqArgsFirstPass
     (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do
+  let opts ← getOptions
+  let firstPassBump := backward.isDefEq.respectTransparency.get opts
+    && backward.isDefEq.firstPassBump.get opts
+  let implicitBump := backward.isDefEq.implicitBump.get opts
   let mut postponedImplicit := #[]
   let mut postponedHO := #[]
   for h : i in *...paramInfo.size do
@@ -338,8 +443,17 @@ private def isDefEqArgsFirstPass
       unless (← Meta.isExprDefEqAux a₁ a₂) do
         return .failed
     else if (← isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂) then
-      unless (← Meta.isExprDefEqAux a₁ a₂) do
-        return .failed
+      /- Easy cases are still argument unifications at an implicit position, so they get the same
+         transparency bump as the second pass: whether an argument is checked at `.implicit`
+         should not depend on which side happens to be an unassigned metavariable. In particular,
+         the assignment triggered here — including the type check and `instanceTypes` fallbacks
+         run by `checkTypesAndAssign` — sees the bumped ambient transparency. -/
+      if firstPassBump && (info.binderInfo.isInstImplicit || implicitBump) then
+        unless (← withImplicitConfig <| Meta.isExprDefEqAux a₁ a₂) do
+          return .failed
+      else
+        unless (← Meta.isExprDefEqAux a₁ a₂) do
+          return .failed
     else
       if info.isProp then
         unless ← isAbstractedUnassignedMVar a₁ <||> isAbstractedUnassignedMVar a₂ do
@@ -352,16 +466,12 @@ private def isDefEqArgsFirstPass
   return .ok postponedImplicit postponedHO
 
 /--
-Ensure `MetaM` configuration is strong enough for checking definitional equality of
-implicit and instance-implict arguments as well as assigned mvar types. Bumps transparency to at
-least `.implicit`, so both `[instance_reducible]` and `[implicit_reducible]` unfold.
+Like `withImplicitConfig`, but sets transparency to exactly `.instances`: instance-typed
+metavariable assignments must preserve the type at `.instances` even when the ambient
+transparency is higher.
 -/
-@[inline] def withImplicitConfig (x : MetaM α) : MetaM α := do
-  let old ← getTransparency
-  if old.lt .implicit then
-    trace[Meta.isDefEq.transparency]
-      "raising transparency {toString old} → implicit"
-  withAtLeastTransparency .implicit do
+@[inline] def withInstancesConfig (x : MetaM α) : MetaM α := do
+  withTransparency .instances do
     let cfg ← getConfig
     if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaHave && cfg.zetaDelta && cfg.proj == .yesWithDelta then
       x
@@ -489,12 +599,167 @@ abbrev respectTransparencyAtTypes : CoreM Bool := do
   let opts ← getOptions
   return backward.isDefEq.respectTransparency.types.get opts && backward.isDefEq.respectTransparency.get opts
 
+/--
+Mark the metavariables in type-determining (spine) positions of `e` as instance-typed
+(see `MetavarContext.instanceTypedMVars`).
+
+Only spine metavariables need the marking to preserve the instance-typed invariant:
+`inferType` consults the type of a subterm only in spine positions (the head of an
+application, the body of a lambda or `let`, the structure of a projection). A metavariable
+in argument position enters the inferred type only by substitution, so instantiating it
+changes the value's type and its occurrences in the already-checked expected type in the
+same way.
+-/
+partial def markInstanceTypedSpineMVars (e : Expr) : MetaM Unit := go e
+where
+  go (e : Expr) : MetaM Unit := do
+    unless e.hasExprMVar do return ()
+    match e with
+    | .mvar mvarId =>
+      mvarId.markInstanceTyped
+      -- The value of a delayed-assigned metavariable is determined by its pending metavariable.
+      if let some d ← getDelayedMVarAssignment? mvarId then
+        go (mkMVar d.mvarIdPending)
+    | .app f _ => go f
+    | .lam _ _ b _ => go b
+    | .letE _ _ v b _ => go v; go b
+    | .proj _ _ s => go s
+    | .mdata _ b => go b
+    | _ => return ()
+
+/--
+Return `true` if all metavariables in type-determining (spine) positions of `e` are
+admissible in a value assigned to an instance-typed metavariable in `markOrSynth` mode (see
+`markInstanceTypedSpineMVars` for why only spine positions matter). Admissible are:
+- instance-typed metavariables: their own assignments are subject to the same restriction;
+- metavariables `isDefEq` cannot assign (from an outer `MetavarContext` depth, or synthetic
+  opaque): the current instance search cannot commit them to a wrong-typed value, and their
+  eventual assignment is governed by whoever created them (e.g. the elaborator's pending
+  instance metavariables, which are synthesized against their recorded type).
+
+A delayed-assigned spine metavariable need not be admissible itself — it will never be
+assigned directly — but the spine of its pending metavariable is checked instead.
+-/
+partial def spineMVarsAdmissible (e : Expr) : MetaM Bool := go e
+where
+  go (e : Expr) : MetaM Bool := do
+    unless e.hasExprMVar do return true
+    match e with
+    | .mvar mvarId =>
+      if let some d ← getDelayedMVarAssignment? mvarId then
+        go (mkMVar d.mvarIdPending)
+      else
+        mvarId.isInstanceTyped <||> mvarId.isReadOnlyOrSyntheticOpaque
+    | .app f _ => go f
+    | .lam _ _ b _ => go b
+    | .letE _ _ v b _ => go v <&&> go b
+    | .proj _ _ s => go s
+    | .mdata _ b => go b
+    | _ => return true
+
+/--
+Type check for assignments to instance-typed metavariables: the value's type must agree with
+the metavariable's type at `.instances` transparency.
+
+The check is *eta-tolerant*: when the types are function types whose binder domains agree
+only above `.instances` (e.g. across a semireducible synonym like Mathlib's `OrderDual`), we
+accept the value as long as the codomain — where instance selection actually happens —
+agrees at `.instances` for the metavariable type's own binders. Without this, acceptance
+would depend on which eta-representative of the value the unifier happened to build
+(`tryResolve` eta-reduces answers, so `fun i : Dual ι => inst i` becomes the bare `inst`,
+whose inferred type has the `ι` binder). The full types must still agree at the ordinary
+transparency, ensuring the assignment remains type-correct.
+-/
+private def checkInstanceTypedTypes (mvarType vType v : Expr) : MetaM Bool := do
+  if (← withInstancesConfig <| Meta.isExprDefEqAux mvarType vType) then
+    return true
+  unless mvarType.isForall do return false
+  let oldOk ← if (← respectTransparencyAtTypes) then
+    withImplicitConfig <| Meta.isExprDefEqAux mvarType vType
+  else
+    withInferTypeConfig <| Meta.isExprDefEqAux mvarType vType
+  unless oldOk do return false
+  forallTelescope mvarType fun xs body => do
+    withInstancesConfig <| Meta.isExprDefEqAux body (← inferType (mkAppN v xs))
+
+/--
+Fallback for assignments to instance-typed metavariables in the `synth` and `markOrSynth`
+modes of `backward.isDefEq.instanceTypes` when the candidate value `v` is not directly
+acceptable: synthesize the instance for the metavariable's type, assign it, and require `v`
+to be definitionally equal to the synthesized instance. This mirrors the elaboration order
+in which instance arguments were synthesized first and only then unified. Fails without
+modifying the state if synthesis fails or if `v` does not match the synthesized instance.
+
+With `stuckOnUndeterminedType := true` (the `synthOrStuck`/`markOrSynthOrStuck` modes), when
+synthesis fails while the metavariable's type still contains metavariables, the goal may
+simply not be determined enough yet (e.g. `BEq ?α` for a still-unknown `?α`), so under
+`isDefEqStuckEx` we throw the `isDefEqStuck` exception instead of failing: the enclosing
+type class resolution then reports "undecidable for now" and is postponed and retried by the
+elaborator once more metavariables are solved. This mirrors what `isDefEqQuick` does for a
+unification of two nonassignable metavariables.
+-/
+private def synthInstanceTypedMVarAndUnify (mvar v : Expr) (stuckOnUndeterminedType : Bool) : MetaM Bool := do
+  checkpointDefEq do
+    unless (← Meta.synthPending mvar.mvarId!) do
+      if stuckOnUndeterminedType && (← getConfig).isDefEqStuckEx
+          && (← instantiateMVars (← inferType mvar)).hasExprMVar then
+        Meta.throwIsDefEqStuck
+      if (← isDiagnosticsEnabled) then
+        trace[diagnostics] "failure when assigning instance metavariable with type{indentExpr (← inferType mvar)}\nthe candidate value{indentExpr v}\nwas rejected and the instance could not be synthesized directly.\nWorkaround: `set_option backward.isDefEq.instanceTypes \"none\"`"
+      return false
+    let inst ← instantiateMVars mvar
+    if (← Meta.isExprDefEqAux v inst) then
+      return true
+    else
+      if (← isDiagnosticsEnabled) then
+        trace[diagnostics] "failure when assigning instance metavariable with type{indentExpr (← inferType mvar)}\nthe rejected candidate value{indentExpr v}\nis not definitionally equal to the synthesized instance{indentExpr inst}\nWorkaround: `set_option backward.isDefEq.instanceTypes \"none\"`"
+      return false
+
 private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
   withTraceNodeBefore `Meta.isDefEq.assign.checkTypes (fun _ => return m!"({mvar} : {← inferType mvar}) := ({v} : {← inferType v})") do
     if !mvar.isMVar then
       trace[Meta.isDefEq.assign.checkTypes] "metavariable expected"
       return false
-    else
+    let mode ← if (← mvar.mvarId!.isInstanceTyped) then getInstanceTypesMode else pure InstanceTypesMode.none
+    match mode with
+    | .mark =>
+      /- The final value of an instance metavariable must have a type that agrees with the
+         metavariable's type at `.instances` transparency (issue #9077). We instantiate `v` first
+         so that the check sees the types of values assigned to metavariables in `v` (their own
+         assignments may have been checked at a weaker transparency, before they were marked),
+         and we propagate the marking to the metavariables remaining in `v` so that their future
+         assignments are checked as well. -/
+      let v ← instantiateMVars v
+      let mvarType ← inferType mvar
+      let vType ← inferType v
+      if (← checkInstanceTypedTypes mvarType vType v) then
+        mvar.mvarId!.assign v
+        markInstanceTypedSpineMVars v
+        return true
+      else
+        if (← isDiagnosticsEnabled) then withInferTypeConfig do
+          if (← Meta.isExprDefEqAux mvarType vType) then
+            trace[diagnostics] "failure when assigning instance metavariable with type{indentExpr mvarType}\nwhich is not definitionally equal to{indentExpr vType}\nwhen using `.instances` transparency, but it is with `.default`.\nWorkaround: `set_option backward.isDefEq.instanceTypes \"none\"`"
+        return false
+    | .synth | .markOrSynth | .synthOrStuck | .markOrSynthOrStuck =>
+      /- The value of an instance metavariable must be determined by instance synthesis, up
+         to defeq at `.instances` transparency: either the candidate value already is such a
+         value — mvar-free (`synth*`) resp. with only admissible metavariables in its spine
+         (`markOrSynth*`) — and has the right type, or we synthesize the instance now and
+         require the candidate to be defeq to the result. -/
+      let v ← instantiateMVars v
+      let directOk ← match mode with
+        | .synth | .synthOrStuck => pure !v.hasExprMVar
+        | _                      => spineMVarsAdmissible v
+      if directOk then
+        let mvarType ← inferType mvar
+        let vType ← inferType v
+        if (← checkInstanceTypedTypes mvarType vType v) then
+          mvar.mvarId!.assign v
+          return true
+      synthInstanceTypedMVarAndUnify mvar v
+        (stuckOnUndeterminedType := mode matches .synthOrStuck | .markOrSynthOrStuck)
+    | .none =>
       -- must check whether types are definitionally equal or not, before assigning and returning true
       let mvarType ← inferType mvar
       let vType ← inferType v

src/Lean/Meta/SynthInstance.lean

@@ -352,6 +352,10 @@ def tryResolve (mvar : Expr) (inst : Instance) : MetaM (Option (MetavarContext 
   let localInsts ← getLocalInstances
   forallTelescopeReducing mvarType fun xs mvarTypeBody => do
     let { subgoals, instVal, instTypeBody } ← getSubgoals lctx localInsts xs inst
+    -- Mark the instance-argument metavariables before unifying with the goal type, so that a
+    -- would-be assignment by unification must preserve the type at `.instances` transparency.
+    -- See `MetavarContext.instanceTypedMVars` and issue #9077.
+    subgoals.forM fun subgoal => subgoal.mvarId!.markInstanceTyped
     withTraceNode `Meta.synthInstance.tryResolve (fun _ => do withMCtx (← getMCtx) do
         return m!"{← instantiateMVars mvarTypeBody} ≟ {← instantiateMVars instTypeBody}") do
     if (← isDefEq mvarTypeBody instTypeBody) then