[Agda] Absurd patterns inconsistent with function extensionality

[Nicolas Pouillard]

On 05/01/2015 02:46 PM, Gabe Dijkstra wrote:
> Hi,

Hi,

> It turns out that if we postulate function extensionality, we can derive
> bottom using absurd patterns as follows:

Congrats!

> c0≠c1 : c0 ≡ c1 → ⊥
> c0≠c1 ()

The dubious part seems to be here. Indeed to prove the two constructor 
distinct one needs a value of the type T to start with.
I renamed your type T into D to avoid the confusion with ⊤ (top):

open import Data.Unit

is-c0 : D → Set
is-c0 (c0 _) = ⊤
is-c0 (c1 _) = ⊥

c0≠c1' : (x : ⊥) → c0 x ≡ c1 x → ⊥
c0≠c1' x e = subst is-c0 e _

c0≠c1'' : ⊥ → c0 ≡ c1 → ⊥
c0≠c1'' x e = subst (λ c → is-c0 (c x)) e _

In both cases the proofs are under the assumption ⊥.

As a safe measure I would recommend to only trigger the rule of distinct 
constructors when they are fully applied.

Best regards,

-- NP