unable to replace a value of type `False=True` with `impossible`

[rgrover]

Steps to Reproduce

I'm trying to prove that for any x that satisfies Eq, x == x should return True. Maybe my assumption is incorrect, and this property is unprovable in general. Nevertheless, my proof reaches a point where I get a hole with the type False = True, which is obviously uninhabited, but I fail to make progress.

module Equality

equalityReflexive : Eq a => (x : a) -> (x == x) = True
equalityReflexive x with (x == x)
  equalityReflexive x | True = Refl
  equalityReflexive x | False = ?contradiction

Expected Behavior

In the above, contradiction has the type False = True. It should be possible to replace it with impossible. The following should compile:

module Equality

equalityReflexive : Eq a => (x : a) -> (x == x) = True
equalityReflexive x with (x == x)
  equalityReflexive x | True = Refl
  equalityReflexive x | False impossible

Observed Behavior

Idris2 complains: with block in equalityReflexive a _ x False is not a valid impossible case

Idris1 complains:

  |
6 |   equalityReflexive x | False impossible
  |                               ~~~~~~~~~~
with block in Equality.equalityReflexive False _ x _ is a valid case

[ziman]

Idris is right to complain there. You can't assume that == is reflexive; the following is a valid program.

data MyType = A | B
Eq MyType where
  (==) _ _ = False

I recommend using DecEq whenever this matters.

[ziman]

(DecEq does not suffer from Boolean Blindness.)

[rgrover]

Thank you so much!

[gallais]

In the above, contradiction has the type False = True. It should be possible to replace it with impossible

Note that contradiction is a goal. As such it is your responsibility to provide a proof of the right type. By contrast, impossible's job is to dismiss an hypothesis with an impossible type. That is why it cannot be used here.