8000 Cumulativity `Prop <= Set` loses canonicity · Issue #7503 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Cumulativity Prop <= Set loses canonicity #7503

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.

Sign up for GitHub

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

Jump to bottom
Closed
andreasabel opened this issue Sep 19, 2024 · 1 comment · Fixed by #7504
Closed

Cumulativity Prop <= Set loses canonicity #7503

andreasabel opened this issue Sep 19, 2024 · 1 comment · Fixed by #7504
Assignees
@jespercockx
Labels
canonicity Computation that should be happening, but isn't. cumulativity "Universe subtyping", inference of levels with --cumulativity, etc prop Prop, definitional proof irrelevance
Milestone
2.8.0

Comments

@andreasabel
Copy link
Member
andreasabel commented Sep 19, 2024 •
edited
Loading

Extracted from #5948:

{-# OPTIONS --prop --cumulativity #-}

-- This combination of options breaks canonicity.
-- Counterexample by Szumi, based on a fragment by Andreas.
-- Issue #5948 discussion, 2024-09-18.

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data Foo : Prop where
  tt ff : Foo

-- Outright matching on Foo is rejected.

-- rejected : Foo → Bool
-- rejected tt = true
-- rejected ff = false

-- -- Cannot split on datatype in Prop unless target is in Prop
-- -- when checking that the pattern tt has type Foo

-- But we can sneak it in via Prop <= Set cumulativity:

Boo : Set
Boo = Foo

allowed : Boo → Bool
allowed tt = true
allowed ff = false

foo-to-boo : Foo → Boo
foo-to-boo x = x

f : Foo → Bool
f x = allowed (foo-to-boo x)

-- This leads to non-canoncial booleans.

_ : f tt ≡ true
_ = refl 

-- Error: allowed _ != true of type Bool

Coq does not have SProp <= Type, according to https://coq.inria.fr/doc/V8.18.0/refman/language/cic.html#subtyping-rules:

note: SProp is not related by cumulativity to any other term

They have Prop <= Type though but I vaguely remember some talk in the 2000s that this isn't entirely unproblematic either. (I couldn't easily google something on this, though.)
@andreasabel andreasabel added canonicity Computation that should be happening, but isn't. prop Prop, definitional proof irrelevance cumulativity "Universe subtyping", inference of levels with --cumulativity, etc labels Sep 19, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 19, 2024
@andreasabel andreasabel mentioned this issue Sep 19, 2024
Open
@jespercockx
Copy link
Member

This looks like me as a problem with pattern matching in the presence of --cumulativity rather than a problem with Prop =< Set per se.

jespercockx added a commit to jespercockx/agda that referenced this issue Sep 19, 2024
@jespercockx
[ fix agda#7503 ] Use principal sort of datatype for checking if spli…
a65f4b5 
…t is ok
@jespercockx jespercockx mentioned this issue Sep 19, 2024
Merged
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@jespercockx @fredins
[ fix agda#7503 ] Use principal sort of datatype for checking if spli…
fa7c5c5 
…t is ok
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jespercockx jespercockx

Labels
canonicity Computation that should be happening, but isn't. cumulativity "Universe subtyping", inference of levels with --cumulativity, etc prop Prop, definitional proof irrelevance
Projects
None yet
Milestone
2.8.0
Development

Successfully merging a pull request may close this issue.

[ fix #7503 ] Use principal sort of datatype for checking if split is ok jespercockx/agda
2 participants
@andreasabel @jespercockx
0