From dce62fc190ab9b05445d7c04f3e104f3094fc6f0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 16 Jan 2019 10:45:26 +0100
Subject: [PATCH] fix(library/init/lean/expander): structural substitution
 instead of abstraction-application when applying notations

---
 library/init/lean/expander.lean | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 0e8ea4f55f..ee76faa429 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -134,10 +134,15 @@ def mk_notation_transformer (nota : notation_macro) : transformer :=
       | none := pure ()
       | _ := error stx "mk_notation_transformer: unimplemented"),
     st ← get,
-    let substs := st.substs.reverse,
-    -- apply substitutions [(x1, e1), ...] via `(λ x1 ..., nota.nota.term) e1 ...`
-    let lam := review lambda {binders := st.substs.map prod.fst, body := nota.nota.term},
-    pure $ some $ st.substs.foldl (λ fn subst, review app {fn := fn, arg := subst.2}) lam
+    -- apply substitutions
+    -- HACK: this substitution completely disregards binders on the notation's RHS.
+    -- We have discussed switching to a more explicit antiquotation syntax like %%_
+    -- that cannot be abstracted over.
+    let substs := st.substs.map (λ ⟨id, t⟩, (id.val, t)),
+    let t := nota.nota.term.replace $ λ stx, match try_view ident_univs stx with
+      | some {id := id, univs := none} := pure $ substs.assoc id.val
+      | _                              := pure none,
+    pure $ some $ t
 
 def mixfix_to_notation_spec (k : mixfix.kind.view) (sym : notation_symbol.view) : transform_m notation_spec.view :=
 let prec := match sym with