doc: coeAtOutParam todo's

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}"

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`.