New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Disunifying non-fully applied constructors is inconsistent with function extensionality #1497

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 2 comments

Comments

Projects
None yet
2 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

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

open import Common.Prelude
open import Common.Equality

data T : Set where
  c0 : ⊥ → T
  c1 : ⊥ → T

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

postulate
  fun-ext : {A B : Set} → (f g : A → B) → ((x : A) → f x ≡ g x) → f ≡ g

c0=c1 : c0 ≡ c1
c0=c1 = fun-ext c0 c1 (λ ())

wrong : ⊥
wrong = c0≠c1 c0=c1

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

Original issue reported on code.google.com by andreas....@gmail.com on 2 May 2015 at 8:04

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 2 May 2015 at 8:25

  • Changed state: Started
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed by 480ce2a.

Original comment by andreas....@gmail.com on 2 May 2015 at 8:51

  • Changed state: Fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment