[Agda] Absurd patterns inconsistent with function extensionality

[Andreas Abel]

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

Fixed on maintenance branch and master branch of the development version.

Thanks for reporting and congrats to score in the false-golfing tournament!

--Andreas

On 02.05.2015 08:46, Nicolas Pouillard wrote:
> On 05/01/2015 02:46 PM, Gabe Dijkstra wrote:
>> 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.

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/