From 7bad9fe554129f8903b7c4119e823f7b09cc1b5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Jun 2015 14:46:51 -0700
Subject: [PATCH] feat(library/error_handling/error_handling): set 'pp.beta' to
 false when displaying errors

see issue #669
---
 src/library/error_handling/error_handling.cpp |  8 +++++++-
 tests/lean/669.lean                           |  1 +
 tests/lean/669.lean.expected.out              | 15 +++++++++++++++
 3 files changed, 23 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/669.lean
 create mode 100644 tests/lean/669.lean.expected.out

diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp
index 19c86fa41..903ee2930 100644
--- a/src/library/error_handling/error_handling.cpp
+++ b/src/library/error_handling/error_handling.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/parser_nested_exception.h"
 #include "library/generic_exception.h"
 #include "library/flycheck.h"
+#include "library/pp_options.h"
 #include "library/error_handling/error_handling.h"
 
 namespace lean {
@@ -144,7 +145,12 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
     }
 }
 
-void display_error(io_state_stream const & ios, pos_info_provider const * p, throwable const & ex) {
+void display_error(io_state_stream const & _ios, pos_info_provider const * p, throwable const & ex) {
+    options opts = _ios.get_options();
+    // Disable pp.beta to avoid cryptic error messages.
+    // See issue https://github.com/leanprover/lean/issues/669
+    opts         = opts.update_if_undef(get_pp_beta_name(), false);
+    io_state_stream ios = _ios.update_options(opts);
     flycheck_error err(ios);
     if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
         display_error(ios, p, *k_ex);
diff --git a/tests/lean/669.lean b/tests/lean/669.lean
new file mode 100644
index 000000000..dae81746a
--- /dev/null
+++ b/tests/lean/669.lean
@@ -0,0 +1 @@
+check (λ {T : Prop} (t : T), t) bool.tt
diff --git a/tests/lean/669.lean.expected.out b/tests/lean/669.lean.expected.out
new file mode 100644
index 000000000..fdc9a651e
--- /dev/null
+++ b/tests/lean/669.lean.expected.out
@@ -0,0 +1,15 @@
+669.lean:1:9: error: type error in placeholder assigned to
+  bool
+placeholder has type
+  Type₁
+but is expected to have type
+  Prop
+the assignment was attempted when trying to solve
+    type mismatch at application
+      (λ {T : Prop} (t : T), t) bool.tt
+    term
+      bool.tt
+    has type
+      bool
+    but is expected to have type
+      bool