Utterly confusing error message

Stream: general

[Patrick Massot]

example {P Q : Prop} : P → Q :=
begin
  by_contra H, -- tactic by_contradiction failed, target is not a proposition
  sorry
end

Is there something we can do?

[Patrick Massot]

Of course the error message goes away in math mode.

[Patrick Massot]

But still, people can forget to enter math mode.

[Eric Wieser]

"math mode" is "open_locale classical"?

[Patrick Massot]

Don't forget to also write noncomputable theory

[Gabriel Ebner]

This is indeed a bug. Under the hood the following happens:

example {P Q : Prop} : P → Q :=
by apply classical.by_contradiction
/-
invalid apply tactic, failed to unify
  P → Q
with
  (¬?m_1 → false) → ?m_1
-/

[Johan Commelin]

Should by_contra always use refine?

[Gabriel Ebner]

This is what by_contradiction does:

  (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip) <|>
  applyc ``classical.by_contradiction <|>

I guess the easiest fix is to do same mk_mapp incantation for classical.by_contradiction as well.

[Mario Carneiro]

maybe we should just look for and remove all uses of applyc and apply in tactics. They are pretty much all bugs waiting to happen

[Mario Carneiro]

it would be even better if we could come up with a replacement that is equally convenient, although I'm not sure if there is a better general purpose heuristic than what apply already uses