[Agda] Agda master is anti-classical, injective type constructors are back

[Andreas Abel]

This concerns only the unreleased Agda master development branch.

Using heterogeneous equality and big forced indices in a data type SING, 
I manage to prove injectivity of type constructor

   SING : (Set -> Set) -> Set

The rest follows Chung-Kil Hur's refutation of excluded middle, as 
published in January 2010 on the Coq and Agda lists.

My development was fathered by my surprise that I could prove

   inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m

but not by directly matching on the heterogeneous equality (which Agda 
refuses as Fin n = Fin m does not yield n = m), but by first matching on 
i and j, which exposes n and m in the constructor patterns and makes 
then available for unification.

   inj-Fin-≅ {i = zero}  {zero} ≅refl = refl  -- matching on ≅refl succeeds!
   inj-Fin-≅ {i = zero}  {suc j} ()
   inj-Fin-≅ {i = suc i} {zero} ()
   inj-Fin-≅ {i = suc i} {suc j} p = {!p!}   -- Splitting on p succeeds!

This is weird.

A fix would be to not generate any unification constraints for forced 
constructor arguments, for instance

   fzero : (n : Nat) -> Fin (suc n)

   fzero n : Fin (suc n) =?= fzero m : Fin (suc m)

would not simplify to n =?= m : Nat.

This change would break a lot of developments using heterogeneous 
equality, as did the fix of issue 292 
(https://code.google.com/p/agda/issues/detail?id=292).  In particular, 
heterogeneous equality would not imply the equality of the types, but 
the equality of the types has to be given in order to sensibly work with 
heterogeneous equality.  In case of Fin, one would work with telescopes

   {n m : Nat} (p : n == m) {i : Fin n} {j : Fin m} (q : i ~= j)

rather than being able to derive p from q.

This is Conor McBride's proposal for heterogeneous equality, if I am not 
mistaken.

RFC,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
-------------- next part --------------
-- Andreas, 2014-01-16
-- Agda with K again is inconsistent with classical logic

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

open import Common.Level
open import Common.Prelude
open import Common.Equality

cast : {A B : Set} (p : A ≡ B) (a : A) → B
cast refl a = a

data HEq {α} {A : Set α} (a : A) : {B : Set α} (b : B) → Set (lsuc α) where
  refl : HEq a a

mkHet : {A B : Set} (eq : A ≡ B) (a : A) → HEq a (cast eq a)
mkHet refl a = refl

-- Type with a big forced index. (Allowed unless --without-K.)
-- This definition is allowed in Agda master since 2014-10-17
-- https://github.com/agda/agda/commit/9a4ebdd372dc0510e2d77e726fb0f4e6f56781e8
-- However, probably the consequences of this new feature have not
-- been grasped fully yet.

data SING : (F : Set → Set) → Set where
  sing : (F : Set → Set) → SING F

-- The following theorem is the culprit.
-- It needs K.
-- It allows us to unify forced indices, which I think is wrong.

thm : ∀{F G : Set → Set} (a : SING F) (b : SING G) (p : HEq a b) → F ≡ G
thm (sing F) (sing .F) refl = refl

-- Note that a direct matching fails, as it generates heterogeneous constraints.
--   thm a .a refl = refl
-- However, by matching on the constructor sing, the forced index
-- is exposed to unification.

-- As a consequence of thm,
-- SING is injective which it clearly should not be.

SING-inj : ∀ (F G : Set → Set) (p : SING F ≡ SING G) → F ≡ G
SING-inj F G p = thm (sing F) _ (mkHet p (sing F))

-- The rest is an adaption of Chung-Kil Hur's proof (2010)

data Either {α} (A B : Set α) : Set α where
  inl : A → Either A B
  inr : B → Either A B

data Inv (A : Set) : Set1 where
  inv : (F : Set → Set) (eq : SING F ≡ A) → Inv A

¬ : ∀{α} → Set α → Set α
¬ A = A → ⊥

-- Classical logic

postulate em : ∀{α} (A : Set α) → Either A (¬ A)

Cantor' : (A : Set) → Either (Inv A) (¬ (Inv A)) → Set
Cantor' A (inl (inv F eq)) = ¬ (F A)
Cantor' A (inr _)          = ⊤

Cantor : Set → Set
Cantor A = Cantor' A (em (Inv A))

C : Set
C = SING Cantor

ic : Inv C
ic = inv Cantor refl

cast' : ∀{F G} → SING F ≡ SING G → ¬ (F C) → ¬ (G C)
cast' eq = subst (λ F → ¬ (F C)) (SING-inj _ _ eq)

-- Self application 1
diag : ¬ (Cantor C)
diag c with em (Inv C)  | c
diag c | inl (inv F eq) | c' = cast' eq c' c
diag _ | inr f          | _  = f ic

-- Self application 2
diag' : Cantor C
diag' with em (Inv C)
diag' | inl (inv F eq) = cast' (sym eq) diag
diag' | inr _          = _

absurd : ⊥
absurd = diag diag'