From 8598dde6e66f84c2fe9d3cd6f89a46763580b005 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Nov 2020 20:51:28 -0800
Subject: [PATCH] fix: if-then-else elaboration issue

@Kha I hate this kind of hack, but the behavior looked unacceptabled
to me. I added a big comment describing the issue and the hack.
---
 src/Lean/Elab/App.lean              | 49 +++++++++++++++++++++--------
 src/Lean/Expr.lean                  |  4 +++
 tests/lean/run/ifThenElseIssue.lean | 32 +++++++++++++++++++
 3 files changed, 72 insertions(+), 13 deletions(-)
 create mode 100644 tests/lean/run/ifThenElseIssue.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 457040d41d..ab1403fc0b 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -264,19 +264,42 @@ private def propagateExpectedType : M Unit := do
     match s.expectedType? with
     | none              => pure ()
     | some expectedType =>
-      let numRemainingArgs := s.args.length
-      trace[Elab.app.propagateExpectedType]! "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
-      match getForallBody numRemainingArgs s.namedArgs s.fType with
-      | none           => pure ()
-      | some fTypeBody =>
-        unless fTypeBody.hasLooseBVars do
-          let hasTypeMVar     := (fTypeBody.findMVar? fun mvarId => s.typeMVars.contains mvarId).isSome
-          let hasOnlyTypeMVar := (fTypeBody.findMVar? fun mvarId => !s.typeMVars.contains mvarId).isNone
-          if hasTypeMVar && hasOnlyTypeMVar then
-            unless (← hasOptAutoParams fTypeBody) do
-              trace[Elab.app.propagateExpectedType]! "{expectedType} =?= {fTypeBody}"
-              isDefEq expectedType fTypeBody
-              pure ()
+      /- We don't propagate `Prop` because we often use `Prop` as a more general "Bool" (e.g., `if-then-else`).
+         If we propagate `expectedType == Prop` in the following examples, the elaborator would fail
+         ```
+         def f1 (s : Nat × Bool) : Bool := if s.2 then false else true
+
+         def f2 (s : List Bool) : Bool := if s.head! then false else true
+
+         def f3 (s : List Bool) : Bool := if List.head! (s.map not) then false else true
+         ```
+         They would all fail for the same reason. So, let's focus on the first one.
+         We would elaborate `s.2` with `expectedType == Prop`.
+         Before we elaborate `s`, this method would be invoked, and `s.fType` is `?α × ?β → ?β` and after
+         propagation we would have `?α × Prop → Prop`. Then, when we would try to elaborate `s`, and
+         get a type error because `?α × Prop` cannot be unified with `Nat × Bool`
+         Most users would have a hard time trying to understand why these examples failed.
+
+         Here is a possible alternative workarounds. We give up the idea of using `Prop` at `if-then-else`.
+         Drawback: users use `if-then-else` with conditions that are not Decidable.
+         So, users would have to embrace `propDecidable` and `choice`.
+         This may not be that bad since the developers and users don't seem to care about constructivism.
+
+         We currently use a different workaround, we just don't propagate the expected type when it is `Prop`. -/
+      unless expectedType.isProp do
+        let numRemainingArgs := s.args.length
+        trace[Elab.app.propagateExpectedType]! "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}"
+        match getForallBody numRemainingArgs s.namedArgs s.fType with
+        | none           => pure ()
+        | some fTypeBody =>
+          unless fTypeBody.hasLooseBVars do
+            let hasTypeMVar     := (fTypeBody.findMVar? fun mvarId => s.typeMVars.contains mvarId).isSome
+            let hasOnlyTypeMVar := (fTypeBody.findMVar? fun mvarId => !s.typeMVars.contains mvarId).isNone
+            if hasTypeMVar && hasOnlyTypeMVar then
+              unless (← hasOptAutoParams fTypeBody) do
+                trace[Elab.app.propagateExpectedType]! "{expectedType} =?= {fTypeBody}"
+                isDefEq expectedType fTypeBody
+                pure ()
 
 /-
   Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 33fa2e721e..c572b21870 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -390,6 +390,10 @@ def isSort : Expr → Bool
   | sort _ _ => true
   | _        => false
 
+def isProp : Expr → Bool
+  | sort (Level.zero ..) _ => true
+  | _ => false
+
 def isBVar : Expr → Bool
   | bvar _ _ => true
   | _        => false
diff --git a/tests/lean/run/ifThenElseIssue.lean b/tests/lean/run/ifThenElseIssue.lean
new file mode 100644
index 0000000000..92394fb82d
--- /dev/null
+++ b/tests/lean/run/ifThenElseIssue.lean
@@ -0,0 +1,32 @@
+-- set_option trace.Meta.isDefEq true
+-- set_option trace.Elab true
+
+def f1 (s : Nat × Bool) : Bool :=
+  if s.2 then false else true
+
+def f2 (s : Nat × Bool) : Bool :=
+  if @Prod.snd _ _ s then false else true
+
+def f3 (s : Nat × Bool) : Bool :=
+  if Prod.snd s then false else true
+
+def f4 (s : Nat × String × Bool) : Bool :=
+  if s.2.2 then false else true
+
+def sec (s : α × β) : β :=
+  s.2
+
+def f5 (s : Nat × Bool) : Bool :=
+  if sec s then false else true
+
+def f6 (s : Nat × (Bool → Bool)) : Bool :=
+  if sec s true then false else true
+
+def f7 (s : List Bool) : Bool :=
+  if s.head! then false else true
+
+def f8 (s : List Bool) : Bool :=
+  if (s.map not).head! then false else true
+
+def f9 (s : List Bool) : Bool :=
+  if List.head! (s.map not) then false else true