[Agda] Proof of False

[Dan Doel]

Greetings,

I was playing around a bit this morning, and noticed that Agda accepts the 
following.

---- snip ----

module Injective where

data _≡_ {a : Set} : a → a → Set where
  ≡-refl : (x : a) → x ≡ x

injective : ∀{a b} → (a → b) → Set
injective f = ∀{x y} → f x ≡ f y → x ≡ y

inj-all : ∀{a b} {f : a → b} → injective f
inj-all {a} {b} {f} {.y} {y} (≡-refl .(f y)) = ≡-refl y

---- snip ----

This appears to be a proof that all functions are injective (Agda even did 
most of the writing, as I only performed a C-c C-c on the left-hand proof, and 
filled in the obvious right-hand side). I showed it to a cohort, who verified 
that it was still accepted by a more recent snapshot than mine, and furnished 
me with the following:

---- snip ----

data XY : Set where
 X : XY
 Y : XY

const : {a b : Set} -> a -> b -> a
const k n = k

test-1 : injective (const X)
test-1 = inj-all {XY} {XY} {const X}

test-2 : X ≡ Y
test-2 = test-1 (≡-refl (const X X))

data bot : Set where

test-3 : X ≡ Y -> bot
test-3 ()

test-4 : bot
test-4 = test-3 test-2

---- snip ----

which looks undesirable. :)

Cheers,
-- Dan