From 4cb8fb20fe0fd6b1eebcff7a3eb65bb5ccd59145 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Aug 2014 10:58:20 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): bug when mixing string and
 non-strict implict arguments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp |  4 ++-
 tests/lean/run/congr_imp_bug.lean | 47 +++++++++++++++++++++++++++++++
 tests/lean/run/implicit.lean      | 10 +++++++
 3 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/congr_imp_bug.lean
 create mode 100644 tests/lean/run/implicit.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index dc558553a3..926fa3c35b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -814,13 +814,15 @@ public:
         expr f_type = f_t.second;
         lean_assert(is_pi(f_type));
         if (!expl) {
-            while (binding_info(f_type).is_strict_implicit()) {
+            bool first = true;
+            while (binding_info(f_type).is_strict_implicit() || (!first && binding_info(f_type).is_implicit())) {
                 tag g        = f.get_tag();
                 expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(f_type)), g);
                 f            = mk_app(f, imp_arg, g);
                 auto f_t     = ensure_fun(f);
                 f            = f_t.first;
                 f_type       = f_t.second;
+                first        = false;
             }
         }
         expr d_type = binding_domain(f_type);
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
new file mode 100644
index 0000000000..dece99882a
--- /dev/null
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -0,0 +1,47 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+import logic.connectives.basic logic.connectives.function
+using function
+
+namespace congr
+
+inductive struc {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → T2 → Prop)
+    (f : T1 → T2) : Prop :=
+| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → struc R1 R2 f
+
+abbreviation app {T1 : Type} {T2 : Type} {R1 : T1 → T1 → Prop} {R2 : T2 → T2 → Prop}
+    {f : T1 → T2} (C : struc R1 R2 f) {x y : T1} : R1 x y → R2 (f x) (f y) :=
+struc_rec id C x y
+
+inductive struc2 {T1 : Type} {T2 : Type} {T3 : Type} (R1 : T1 → T1 → Prop)
+    (R2 : T2 → T2 → Prop) (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
+| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
+    struc2 R1 R2 R3 f
+
+abbreviation app2 {T1 : Type} {T2 : Type} {T3 : Type} {R1 : T1 → T1 → Prop}
+    {R2 : T2 → T2 → Prop} {R3 : T3 → T3 → Prop} {f : T1 → T2 → T3}
+    (C : struc2 R1 R2 R3 f) {x1 y1 : T1} {x2 y2 : T2}
+  : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
+struc2_rec id C x1 y1 x2 y2
+
+theorem compose21
+    {T2 : Type} {R2 : T2 → T2 → Prop}
+    {T3 : Type} {R3 : T3 → T3 → Prop}
+    {T4 : Type} {R4 : T4 → T4 → Prop}
+    {g : T2 → T3 → T4} (C3 : congr.struc2 R2 R3 R4 g)
+    ⦃T1 : Type⦄  -- nice!
+    {R1 : T1 → T1 → Prop}
+    {f1 : T1 → T2} (C1 : congr.struc R1 R2 f1)
+    {f2 : T1 → T3} (C2 : congr.struc R1 R3 f2) :
+  congr.struc R1 R4 (λx, g (f1 x) (f2 x)) := mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H))
+
+theorem congr_and : congr.struc2 iff iff iff and := sorry
+
+theorem congr_and_comp [instance] {T : Type} {R : T → T → Prop} {f1 f2 : T → Prop}
+     (C1 : struc R iff f1) (C2 : struc R iff f2) :
+   congr.struc R iff (λx, f1 x ∧ f2 x) := congr.compose21 congr_and C1 C2
+
+end
\ No newline at end of file
diff --git a/tests/lean/run/implicit.lean b/tests/lean/run/implicit.lean
new file mode 100644
index 0000000000..1c642fb37e
--- /dev/null
+++ b/tests/lean/run/implicit.lean
@@ -0,0 +1,10 @@
+import standard
+
+definition f {A : Type} {B : Type} (f : A → B → Prop) ⦃C : Type⦄ {R : C → C → Prop} {c : C} (H : R c c) : R c c
+:= H
+
+variable g : Prop → Prop → Prop
+variable H : true ∧ true
+
+check f g H
+