From 9fdf11fa541a5876036478dcda5574437fcc78ee Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 17 May 2017 11:15:54 +0200
Subject: [PATCH] fix(frontends/lean/pp): shadowing shortened const

Fixes #1584
---
 src/frontends/lean/pp.cpp                      | 18 ++++++++++++------
 tests/lean/pp_shadowed_const.lean              |  5 +++++
 tests/lean/pp_shadowed_const.lean.expected.out | 12 ++++++++++++
 3 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 59a23466b1..5f019f2793 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -686,10 +686,11 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
     // Remark: if num_ref_univ_params is "some", then it contains the number of
     // universe levels that are fixed in a section. That is, \c e corresponds to
     // a constant in a section which has fixed levels.
+    auto short_n = n;
     if (!m_full_names) {
         if (auto it = is_aliased(n)) {
             if (!m_private_names || !hidden_to_user_name(m_env, n))
-                n = *it;
+                short_n = *it;
         } else {
             for (name const & ns : get_namespaces(m_env)) {
                 if (!ns.is_anonymous()) {
@@ -697,7 +698,7 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
                     if (new_n != n &&
                         !new_n.is_anonymous() &&
                         (!new_n.is_atomic() || !is_protected(m_env, n))) {
-                        n = new_n;
+                        short_n = new_n;
                         break;
                     }
                 }
@@ -705,11 +706,16 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
         }
     }
     if (!m_private_names) {
-        if (auto n1 = hidden_to_user_name(m_env, n))
-            n = *n1;
+        if (auto n1 = hidden_to_user_name(m_env, short_n))
+            short_n = *n1;
+    }
+    if (m_ctx.has_local_pp_name(short_n.get_root())) {
+        if (m_ctx.has_local_pp_name(n.get_root())) {
+            n = get_root_tk() + n;
+        }
+    } else {
+        n = short_n;
     }
-    if (m_ctx.has_local_pp_name(n.get_root()))
-        n = get_root_tk() + n;
     if (m_universes && !empty(const_levels(e))) {
         unsigned first_idx = 0;
         buffer<level> ls;
diff --git a/tests/lean/pp_shadowed_const.lean b/tests/lean/pp_shadowed_const.lean
index 2acd96fe6a..c15b5a9b61 100644
--- a/tests/lean/pp_shadowed_const.lean
+++ b/tests/lean/pp_shadowed_const.lean
@@ -2,3 +2,8 @@ def f : Π (x : nat) (b : bool), bool = bool := λ bool, _
 
 def g (heq : 1 == 1) := heq.symm
 #print g
+
+open nat
+def h1 : Π n : nat, pred n = n := λ n, _
+def h2 : Π n : nat, pred n = n := λ pred, _
+def h3 : Π n m : nat, pred n = m := λ pred nat, _
diff --git a/tests/lean/pp_shadowed_const.lean.expected.out b/tests/lean/pp_shadowed_const.lean.expected.out
index 75d6472427..20014117bd 100644
--- a/tests/lean/pp_shadowed_const.lean.expected.out
+++ b/tests/lean/pp_shadowed_const.lean.expected.out
@@ -4,3 +4,15 @@ bool : ℕ
 ⊢ _root_.bool → _root_.bool = _root_.bool
 def g : 1 == 1 → 1 == 1 :=
 λ (heq_1 : 1 == 1), heq.symm heq_1
+pp_shadowed_const.lean:7:39: error: don't know how to synthesize placeholder
+context:
+n : ℕ
+⊢ pred n = n
+pp_shadowed_const.lean:8:42: error: don't know how to synthesize placeholder
+context:
+pred : ℕ
+⊢ nat.pred pred = pred
+pp_shadowed_const.lean:9:48: error: don't know how to synthesize placeholder
+context:
+pred nat : ℕ
+⊢ _root_.nat.pred pred = nat