contradiction tactic creates type-incorrect term

[kmill]

Description

The contradiction tactic uses absurd when discharging the goal using α → False, even if α is not a proposition, leading to a typechecking failure.

Context

Found on Zulip

Steps to Reproduce

theorem T0 (α : Type) (x : α) (H: α → False) : False := by
  contradiction

Expected behavior: Either this succeeds (without error) or reports "tactic 'contradiction' failed"

Actual behavior: The tactic succeeds without error, but there is an error at T0:

application type mismatch
  @absurd α
argument has type
  Type
but function has type
  ∀ {a b : Prop}, a → ¬a → b

Versions

4.11.0 commit from 7/25/2024

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.