Agda accepts incorrect (?) code, subject reduction broken

[nad]

The following example was distilled from code written by @simhu:

open import Agda.Builtin.Equality

ap : {A B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

infix 30 _∙_

_∙_ : {A : Set} {B : A → Set} {f g : (a : A) → B a} →
      f ≡ g → (x : A) → f x ≡ g x
refl ∙ x = refl

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans p refl = p

const : {A B : Set} → B → (A → B)
const = λ x _ → x

dotap : {A B : Set} {f g : A → B} (p : f ≡ g) (a : A) →
        p ∙ a ≡ ap (λ f → f a) p
dotap refl x = refl

module _ {A B : Set} {x y : B}
         (p : const x ≡ const y) (a₁ a₂ : A)
         where

  -- Why is the following code accepted?

  accepted : p ∙ a₁ ≡ ap (λ f → f a₂) p
  accepted = trans (dotap p a₁) (refl {x = ap (λ f → f a₂) p})

  -- The following code is rejected: "a₁ != a₂".

  rejected : p ∙ a₁ ≡ ap (λ f → f a₂) p
  rejected = trans (dotap p a₁) refl

  -- The following code is also rejected: "a₁ != a₂".

  also-rejected : p ∙ a₁ ≡ ap (λ f → f a₂) p
  also-rejected = dotap p a₁

Note that accepted reduces to (the body of) also-rejected.

The problem seems to go back to Agda 2.3.2.

[nad]

The bug can be used to prove a statement to which it seems as if @coquand has found a counterexample, so I suspect that this bug makes Agda inconsistent.

[nad]

Bisection suggests that the problem was introduced by @andreasabel in one of the following commits:

• fb89f9c23b5a60ca9e364975414f7e088532e519: "Code for new polarity Nonvariant. However, it is unused still, so no outside effect."
• 41e59c645710fb5a8dad8d3ad2395a0539fc6910: "Addition of polarity Nonvariant and relevance UnusedArg. Fixing issue 44 and 691."

[jespercockx]

Here's a reduced version:

open import Agda.Builtin.Equality

postulate
  A B : Set

ap : (A : Set) (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap A f refl = refl

const : B → (A → B)
const = λ x _ → x

postulate
  x y : B
  p : const x ≡ const y
  a₁ a₂ : A

accepted : ap _ (λ f → f a₁) p ≡ ap _ (λ f → f a₂) p
accepted = refl

This is accepted, and if you ask Agda for the type of accepted you get ap (A → B) (λ f → f a₁) p ≡ ap (A → B) (λ f → f a₂) p. However, filling in this type manually results in a type error:

a₁ != a₂ of type A
when checking that the expression refl has type
ap (A → B) (λ f → f a₁) p ≡ ap (A → B) (λ f → f a₂) p

[andreasabel]

Agda accepts

test0 : {A B : Set} {x y : B} (p : const x ≡ const y) (a₁ a₂ : A) → 
  cong (λ f → f a₁) p ≡ cong (λ f → f a₂) p
test0 p a₁ a₂ = refl 

the rest is transitivity. (cong is ap)

@nad: Please add the prove of absurdity.

[jespercockx]

I guess internally Agda fills in the type of constant functions A →c B instead of the regular function space A → B. This causes the arguments a₁ and a₂ to be marked as UnusedArgs, so they are skipped when comparing λ f → f a₁ to λ f → f a₂.

It seems to be bad practice to solve a metavariable with a solution the user has no hope of writing. However, I don't see how this could lead to an inconsistency. @nad , do you have a link to the counterexample?

[nad]

I wrote that I suspect that this makes Agda inconsistent. I don't currently have Agda code demonstrating an inconsistency. Do you need such an example?

[jespercockx]

Not necessarily, I'm just saying that the fact that you can prove this seems to be a consequence of a feature of Agda (namely constant function types). There's a difference between the situation where a new feature allows us to prove new but consistent theorems (in which case we either want to keep it, or make it an option), and the situation where the feature leads to inconsistency (in which case we probably want to remove or restrict the feature). So I was just wondering which of those two cases this was.

[andreasabel]

@nad: Well, the "false" flag is waving over this issue. And for the foundational debate, it would be interesting whether this makes Agda inconsistent or only inconsistent in the presence of postulates (we thought to be consistent with Agda).

[nad]

Subject reduction is broken, so this is a bug, not a feature.

I am fairly certain that I can construct a counterexample that depends on univalence (which should now be provable if --cubical is used). However, the counterexample I have in mind is not small.

[jespercockx]

You're right, there's definitely also a bug here. The core issue seems to be that the following is accepted:

open import Agda.Builtin.Equality

const : (A B : Set) → B → (A → B)
const A B = λ x _ → x

ap : (A : Set) (B : Set) (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap A B f refl = refl

postulate
  A B   : Set
  a₁ a₂ : A
  x y   : B
  p     : const A B x ≡ const A B y

accepted : ap (A → B) B (λ f → f a₁) p ≡ ap (A → B) B (λ f → f a₂) p
accepted = refl {x = ap _ B (λ f → f a₁) p}

Here, the underscore _ is filled in with the constant function type A →c B (which the user is not allowed to write). There seems to be some strange subtyping going on here, as ap (A →c B) B (λ f → f a₁) p ≡ ap (A →c B) B (λ f → f a₂) p (the type of refl) is considered to be a subtype of ap (A → B) B (λ f → f a₁) p ≡ ap (A → B) B (λ f → f a₂) p (the type of accepted).

[jespercockx]

And BOOM:

open import Agda.Builtin.Equality

data Bool : Set where
  tt ff : Bool

const : Bool → (Bool → Bool)
const = λ x _ → x

ap : {A : Set} {B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

mutual
  Bool→cBool : Set
  Bool→cBool = _

  accepted : (p : const tt ≡ const ff) → ap (λ f → f tt) p ≡ ap (λ f → f ff) p
  accepted p = refl {x = ap {A = Bool→cBool} (λ f → f tt) p}

constant : (f : Bool→cBool) (x y : Bool) → f x ≡ f y
constant f x y = refl

swap : Bool→cBool
swap tt = ff
swap ff = tt

BOOM : tt ≡ ff
BOOM = constant swap ff tt

It's a party!

[andreasabel]

swap is definitely not constant. I can easily spoil this party!

Please find a better exploit.

[andreasabel]

The strange subtyping is because ignoreForced also ignores UnusedArg, see file Conversion.hs:

compareDom cmp dom1@(Dom i1 a1) dom2@(Dom i2 a2) b1 b2 errH errR cont
  | getHiding dom1 /= getHiding dom2 = errH
  -- Andreas 2010-09-21 compare r1 and r2, but ignore forcing annotations!
  | not $ compareRelevance cmp (ignoreForced $ getRelevance dom1)
                               (ignoreForced $ getRelevance dom2) = errR

The whole UnusedArg machinery is brittle. I should be removed, after we find a better solution for issue #44.

[simhu]

While this seems to fix both @nad's and @jespercockx's snippets, my original file still is accepted:

{-# OPTIONS --without-K #-}

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

ap : {A B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

-- \bub
_•_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
p • refl = p

infixr 30 _•_

! : {A : Set} {a b : A} → a ≡ b → b ≡ a
! refl = refl

-- \.  (NB: not • aka \bub)
_∙_ : {A : Set} {B : A → Set}
      {f g : (a : A) → B a} →
      f ≡ g →
      (x : A) → f x ≡ g x
refl ∙ x = refl

infix 30 _∙_

dotap : {A B : Set} {f g : A → B} 
        (p : f ≡ g) (x : A)
      → p  ∙ x ≡ ap (λ F → F x) p
dotap refl x = refl

apcomp : {A B C : Set} (f : B → C) (g : A → B)
         {x y : A} (p : x ≡ y)
       → ap (λ a → f (g a)) p ≡ ap f (ap g p)
apcomp f g refl = refl

-- combinators for equality reasoning
_≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ p ⟩ q = p • q

infixr 2 _≡⟨_⟩_

_□ : {A : Set} (x : A) → x ≡ x
x □ = refl

module Wrong (A B : Set) (a0 : A) where
  const : B → (A → B)
  const = λ x _ → x 

  to : {x y : B} → x ≡ y → const x ≡ const y
  to = ap const

  from : {x y : B} → const x ≡ const y → x ≡ y
  from = ap (λ F → F a0)

  -- This lemma should not typecheck:
  lem : {x y : B} (p : const x ≡ const y) (a : A)
      → p ∙ a ≡ to (from p) ∙ a
  lem p a = p ∙ a
            ≡⟨ dotap p a ⟩ 
            ap (λ F → F a) p
            ≡⟨ refl ⟩
            ap (λ F → const (F a) a) p 
            ≡⟨ apcomp _ _ p ⟩
            ap (λ G → G a) (ap (λ F → const (F a)) p)
            ≡⟨ ap (ap (λ G → G a)) (apcomp const (λ F → F a) p) ⟩
            ap(λ G → G a) (ap const (ap (λ (F : A → B) → F a) p))
            ≡⟨ ! (dotap (ap const (ap (λ F → F a) p)) a) ⟩
            (to (from p) ∙ a) □

I'm on Agda version 2.6.0-912061b

[andreasabel]

Well @nad's code is still accepted.
How do you derive a contradiction now (probably you need the univalence axiom)?

[jespercockx]

Still too easy:

open import Agda.Builtin.Equality

data Bool : Set where
  tt ff : Bool

const : Bool → (Bool → Bool)
const = λ x _ → x

mutual
  Bool→cBool : Set
  Bool→cBool = _

  const-tt : Bool→cBool
  const-tt = const tt

constant : (f : Bool→cBool) (x y : Bool) → f x ≡ f y
constant f x y = refl

constant' : (f : Bool → Bool) (x y : Bool) → f x ≡ f y
constant' = constant

swap : Bool → Bool
swap tt = ff
swap ff = tt

fireworks : tt ≡ ff
fireworks = constant' swap ff tt

And the party goes on!

[Saizan]

@andreasabel regarding getting rid of UnusedArg, compareElims already makes use of the Polarity of a definition when we compare applications with the same head, wouldn't that be enough for #44 ?

[simhu]

Oops, sorry, of course @andreasabel. Here comes a proof of UIP using funext:

{-# OPTIONS --without-K #-}

-- Some basic definitions

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

ap : {A B : Set} (f : A → B) {a b : A} (p : a ≡ b) → f a ≡ f b
ap f refl = refl

-- \bub
_•_ : {A : Set} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
p • refl = p

infixr 30 _•_

! : {A : Set} {a b : A} → a ≡ b → b ≡ a
! refl = refl

-- \.  (NB: not • aka \bub)
_∙_ : {A : Set} {B : A → Set}
      {f g : (a : A) → B a} →
      f ≡ g →
      (x : A) → f x ≡ g x
p ∙ x = ap (λ F → F x) p

infix 30 _∙_

data Bool : Set where
  true : Bool
  false : Bool

-- NB: given funext, one can derive a funext' for which the
-- corresponding funextapp holds
postulate
  funext : {A : Set} {B : A → Set}
           {f g : (a : A) → B a}
           (ptw : (x : A) → f x ≡ g x)
         → f ≡ g

  funextapp : {A : Set} {B : A → Set}
              {f g : (a : A) → B a} →
              {ptw : (x : A) → f x ≡ g x}
              (x : A)
            → funext ptw ∙ x ≡ ptw x

module UIP (B : Set) where
  const : B → (Bool → B)
  const = λ x _ → x 

  bad : {x y : B} (p : const x ≡ const y) (a b : Bool)
      →  ap (λ F → F a) p ≡ ap (λ F → F b) p
  bad p a b = refl

  [_,_] : {a b : B} (p q : a ≡ b) → const a ≡ const b
  [ p , q ] = funext ( λ {true → p ; false → q})

  fst : {a b : B} (p q : a ≡ b) → [ p , q ] ∙ true ≡ p
  fst p q = funextapp true 

  snd : {a b : B} (p q : a ≡ b) → [ p , q ] ∙ false ≡ q
  snd p q = funextapp false

  setB : {a b : B} (p q : a ≡ b) → p ≡ q
  setB p q = !(fst p q) • bad [ p , q ] true false • snd p q

[andreasabel]

@Saizan : right, and we could add a traversal that replaces any UnusedArg-ument by Sort Prop, to be consistent in the free variable analysis (which is outside of TCM). (Lunch discussion with @UlfNorell.)