From 19be535fb33a0602bf427edfde871f48d86ef8e6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Sep 2020 19:29:54 -0700
Subject: [PATCH] chore: add TODO

---
 src/Lean/Elab/Match.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 8e33cbcff7..229a0226ff 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -546,6 +546,7 @@ withPatternVars patternVars fun patternVarDecls => do
     let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr;
     rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambdaFVars xs rhs;
     trace `Elab.match fun _ => "rhs: " ++ rhs;
+    -- TODO: we should promote `.(?m ...)` to pattern variables too. This can happen when users misuse `{}` in constructors
     -- TODO: check whether altLHS still has metavariables
     pure (altLHS, rhs)