Exploit: Injective type constructors and abstract prove false

[andreasabel]

{-# OPTIONS --injective-type-constructors #-}

open import Common.Prelude
open import Common.Equality

abstract
  f : Bool → Bool
  f x = true

  same : f true ≡ f false
  same = refl

not-same : f true ≡ f false → ⊥
not-same ()

absurd : ⊥
absurd = not-same same

[gallais]

While working on #3959, I have found a way to revive this proof of false
using the INJECTIVE pragma:

{-# OPTIONS --safe #-}

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

data ⊥ : Set where

abstract
  f : Bool → Bool
  f x = true
  {-# INJECTIVE f #-}

  same : f true ≡ f false
  same = refl

not-same : f true ≡ f false → ⊥
not-same ()

absurd : ⊥
absurd = not-same same

[JacquesCarette]

I don't get it -- you chose to lie to Agda, in ways that are outside the logic (with a pragma), and tried to hide your track (with abstract), and you're somehow surprised that this gets you into trouble? Is the point that this shouldn't have happened under --safe?

[gallais]

Yes. The point is that --safe should reject any use of INJECTIVE just like
it rejects uses of TERMINATING.