Agda always has irrelevant projections

[dolio]

Agda always has irrelevant projections

[dolio]

BTW, this is inconsistent with cubical:

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool
open import Cubical.Data.Empty
open import Cubical.Data.Unit
open import Cubical.Relation.Nullary


variable
  A B : Type

record TSquash (A : Type) : Type where
  field .extract : Unit -> A

  .tflat : Unit -> A
  tflat x = extract x

open TSquash

emb : A -> TSquash A
emb a .extract _ = a

lemma₀ : ∀ t → PathP (λ i → TSquash (notEq i)) t t
lemma₀ t i = transport (λ j → TSquash (notEq (i ∧ j))) t

lemma₁ : ¬ (∀ A → TSquash A -> A)
lemma₁ ext = not≢const (ext Bool f) sublemma where
  f = emb false

  sublemma : not (ext Bool f) ≡ ext Bool f
  sublemma = fromPathP λ i → ext (notEq i) (lemma₀ f i)

.ext : TSquash A -> A
ext t = tflat t _

.xplode : ⊥
xplode = lemma₁ (λ _ → ext)

bad : ⊥
bad = e xplode where
  e : .⊥ -> ⊥
  e ()

[jamesmckinna]

Would fixing this (via @andreasabel 's proposal, or otherwise) invalidate agda/agda-stdlib#2199 and/or agda/agda-stdlib#2243 ?
I would be good to know before I commit to doing any more work on either of those!

[dolio]

My understanding is that the proposal is only to restrict definitions like:

.foo : ...
foo = ...

where foo itself is irrelevant. Not every definition that has irrelevance in the type. So it looks like your work there would be unaffected.

However, I don't know what a fix to the other example would entail. I guess even the most brute force option might be, 'you can't open (applied) record modules with irrelevant fields without --irrelevant-projections.' But that also doesn't affect your work, right?

[conal]

Zulip link.

[andreasabel]

Proposed fix: forbid (even irrelevant) definitions in records to use irrelevant fields unless --irrelevant-projections is on.

[dolio]

I'm not sure that's good enough due to #6359. E.G. you can do this:

open import Cubical.Foundations.Prelude
open import Cubical.Data.Bool
open import Cubical.Data.Empty
open import Cubical.Relation.Nullary

variable
  A B : Type

record TSquash (A : Type) : Type where
  constructor emb
  field .extract : A

lemma₀ : ∀ t → PathP (λ i → TSquash (notEq i)) t t
lemma₀ t i = transport (λ j → TSquash (notEq (i ∧ j))) t

lemma₁ : ¬ (∀ A → TSquash A -> A)
lemma₁ ext = not≢const (ext Bool f) sublemma where
  f = emb false

  sublemma : not (ext Bool f) ≡ ext Bool f
  sublemma = fromPathP λ i → ext (notEq i) (lemma₀ f i)

lemma₂ : ¬ (∀ A → .A -> A)
lemma₂ f = lemma₁ λ A (emb x) → f A x

bad : ⊥
bad = e (lemma₂ λ A x → let open TSquash (emb x) in extract) where
  e : .⊥ -> ⊥
  e ()

Unless what you're talking about affects opening as well. This has no irrelevant definitions.

BTW, emb being a constructor is unnecessary, too.