From 17907a78290e0df5e2c5b2e5bcb0317031df70cc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 22 Mar 2021 20:35:07 -0700
Subject: [PATCH] fix: perform topological sort on pattern variables

---
 src/Lean/Elab/Match.lean          |  4 ++-
 src/Lean/Meta.lean                |  1 +
 src/Lean/Meta/SortLocalDecls.lean | 50 +++++++++++++++++++++++++++++++
 3 files changed, 54 insertions(+), 1 deletion(-)
 create mode 100644 src/Lean/Meta/SortLocalDecls.lean

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index f8ac9634a1..9a25a70e43 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Match.MatchPatternAttr
 import Lean.Meta.Match.Match
+import Lean.Meta.SortLocalDecls
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.App
 import Lean.Parser.Term
@@ -563,7 +564,8 @@ def finalizePatternDecls (patternVarDecls : Array PatternVarDecl) : TermElabM (A
          let decl ← instantiateLocalDeclMVars decl
          decls := decls.push decl
        | _ => pure ()
-  return decls
+  /- We perform a topological sort (dependecies) on `decls` because the pattern elaboration process may produce a sequence where a declaration d₁ may occur after d₂ when d₂ depends on d₁. -/
+  sortLocalDecls decls
 
 open Meta.Match (Pattern Pattern.var Pattern.inaccessible Pattern.ctor Pattern.as Pattern.val Pattern.arrayLit AltLHS MatcherResult)
 
diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean
index 75be9686fb..7b2d3475c7 100644
--- a/src/Lean/Meta.lean
+++ b/src/Lean/Meta.lean
@@ -30,3 +30,4 @@ import Lean.Meta.UnificationHint
 import Lean.Meta.Inductive
 import Lean.Meta.SizeOf
 import Lean.Meta.Coe
+import Lean.Meta.SortLocalDecls
diff --git a/src/Lean/Meta/SortLocalDecls.lean b/src/Lean/Meta/SortLocalDecls.lean
new file mode 100644
index 0000000000..df39bf5ede
--- /dev/null
+++ b/src/Lean/Meta/SortLocalDecls.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Basic
+
+namespace Lean.Meta
+
+namespace SortLocalDecls
+
+structure Context where
+  localDecls : NameMap LocalDecl := {}
+
+structure State where
+  visited : NameSet := {}
+  result  : Array LocalDecl := #[]
+
+abbrev M := ReaderT Context $ StateRefT State MetaM
+
+mutual
+  partial def visitExpr (e : Expr) : M Unit := do
+    match e with
+    | Expr.proj _ _ e _    => visitExpr e
+    | Expr.forallE _ d b _ => visitExpr d; visitExpr b
+    | Expr.lam _ d b _     => visitExpr d; visitExpr b
+    | Expr.letE _ t v b _  => visitExpr t; visitExpr v; visitExpr b
+    | Expr.app f a _       => visitExpr f; visitExpr a
+    | Expr.mdata _ b _     => visitExpr b
+    | Expr.mvar _ _        => let v ← instantiateMVars e; unless v.isMVar do visitExpr v
+    | Expr.fvar fvarId _   => if let some localDecl := (← read).localDecls.find? fvarId then visitLocalDecl localDecl
+    | _                    => return ()
+
+  partial def visitLocalDecl (localDecl : LocalDecl) : M Unit := do
+    unless (← get).visited.contains localDecl.fvarId do
+      modify fun s => { s with visited := s.visited.insert localDecl.fvarId }
+      visitExpr localDecl.type
+      if let some val := localDecl.value? then
+        visitExpr val
+      modify fun s => { s with result := s.result.push localDecl }
+end
+
+end SortLocalDecls
+
+open SortLocalDecls in
+def sortLocalDecls (localDecls : Array LocalDecl) : MetaM (Array LocalDecl) :=
+  let aux : M (Array LocalDecl) := do localDecls.forM visitLocalDecl; return (← get).result
+  aux.run { localDecls := localDecls.foldl (init := {}) fun s d => s.insert d.fvarId d } |>.run' {}
+
+end Lean.Meta
\ No newline at end of file