How to prove that the boolean inequality of a type with itself is uninhabited in Idris?

I was wondering how to prove that (So (not (y == y))) is an instance of Uninhabited, and I'm not sure how to go about it. Is it provable in Idris, or is not provable due to the possibility of a weird Eq implementation for y?

Solution

The Eq interface does not require an implementation to follow the normal laws of equality. But, we can define an extended LawfulEq interface which does:

%default total

is_reflexive : (t -> t -> Bool) -> Type
is_reflexive {t} rel = (x : t) -> rel x x = True

is_symmetric : (t -> t -> Bool) -> Type
is_symmetric {t} rel = (x : t) -> (y : t) -> rel x y = rel y x

is_transitive : (t -> t -> Bool) -> Type
is_transitive {t} rel = (x : t) -> (y : t) -> (z : t) -> rel x y = True -> rel x z = rel y z

interface Eq t => LawfulEq t where
  eq_is_reflexive : is_reflexive {t} (==)
  eq_is_symmetric : is_symmetric {t} (==)
  eq_is_transitive : is_transitive {t} (==)

The result asked for in the question can be proved for type Bool:

so_false_is_void : So False -> Void
so_false_is_void Oh impossible

so_not_y_eq_y_is_void : (y : Bool) -> So (not (y == y)) -> Void
so_not_y_eq_y_is_void False = so_false_is_void
so_not_y_eq_y_is_void True = so_false_is_void

The result can be proved not true for the following Weird type:

data Weird = W

Eq Weird where
  W == W = False

weird_so_not_y_eq_y : (y : Weird) -> So (not (y == y))
weird_so_not_y_eq_y W = Oh

The Weird (==) can be shown to be not reflexive, so an implementation of LawfulEq Weird is not possible:

weird_eq_not_reflexive : is_reflexive {t=Weird} (==) -> Void
weird_eq_not_reflexive is_reflexive_eq = 
  let w_eq_w_is_true = is_reflexive_eq W in
    trueNotFalse $ trans (sym w_eq_w_is_true) (the (W == W = False) Refl)