From 01d0ca8cfe08fb3c04256528ef6e9fa08be01894 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Jul 2022 18:58:40 -0700
Subject: [PATCH] doc: `coeAtOutParam` todo's

---
 src/Lean/Elab/SyntheticMVars.lean | 3 +++
 src/Lean/Meta/SynthInstance.lean  | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index f00386d8e3..7d34da6163 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -172,6 +172,9 @@ where
       let (mvars, bis, _) ← forallMetaTelescopeReducing (← inferType candidate)
       let candidate := mkAppN candidate mvars
       trace[Elab.defaultInstance] "{toString (mkMVar mvarId)}, {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
+      /- The `coeAtOutParam` feature may mark output parameters of local instances as `syntheticOpaque`.
+         This kind of parameter is not assignable by default. We use `withAssignableSyntheticOpaque` to workaround this behavior
+         when processing default instances. TODO: try to avoid `withAssignableSyntheticOpaque`. -/
       if (← withAssignableSyntheticOpaque <| isDefEqGuarded (mkMVar mvarId) candidate) then
         -- Succeeded. Collect new TC problems
         trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}"
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index db426fece7..5b1ee1b2af 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -690,6 +690,9 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
           let (_, _, result) ← openAbstractMVarsResult result
           trace[Meta.synthInstance] "result {result}"
           let resultType ← inferType result
+          /- Output parameters of local instances may be marked as `syntheticOpaque` by the application-elaborator.
+             We use `withAssignableSyntheticOpaque` to make sure this kind of parameter can be assigned by the following `isDefEq`.
+             TODO: rewrite this check to avoid `withAssignableSyntheticOpaque`. -/
           if (← withDefault <| withAssignableSyntheticOpaque <| isDefEq type resultType) then
             let result ← instantiateMVars result
             /- We use `check` to propogate universe constraints implied by the `result`.