[Agda] Simple contradiction from type-in-type

[Andreas Abel]

Samuel, this paradox was discovered and fixed in September...
Cheers, Andreas

Thu Sep 13 09:52:35 CEST 2012  Andreas Abel <andreas.abel at ifi.lmu.de>
   * Fixed a bug in the positivity analysis for data type indices.

-------- Original Message --------
Subject: Forget Hurken's Paradox, Agda has a quicker route to success
Date: Thu, 06 Sep 2012 17:21:50 +0200
From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Agda List <Agda at lists.chalmers.se>

   {-# OPTIONS --type-in-type #-}
   module ForgetHurkens where

   infix 4 _≡_

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

   data ⊥ : Set where

   data D : Set where
     abs : ∀ {E : Set} → D ≡ E → (E → ⊥) → D

   lam : (D → ⊥) → D
   lam f = abs refl f

   app : D → D → ⊥
   app (abs refl f) d = f d

   omega : D
   omega = lam (λ x → app x x)

   Omega : ⊥
   Omega = app omega omega

The problem is that Agda considers

   F D = \Sigma E : Set. (D ≡ E) * (E → ⊥)

as strictly positive in D.  Funnily, it complains when I swap the
arguments to equality; the same thing with E ≡ D is rejected (correctly).

Note: I am not using the full Set : Set, just an impredicative Set.

If I try the same in Coq, it is rejected because the definition of D is
not considered strictly positiv.

   Inductive Id {A : Type} (x : A) : A -> Prop :=
   | refl : Id x x.

   Definition cast {P Q : Prop}(eq : Id P Q) : P -> Q :=
     match eq with
     | refl => fun x => x
     end.

   Inductive False : Prop :=.

   Inductive D : Prop :=
   | abs : forall (E : Prop), Id D E -> (E -> False) -> D.

   Definition lam (f : D -> False) : D := abs D (refl D) f.
   Definition app (f : D) (d : D) : False :=
     match f with
     | abs E eq g => g (cast eq d)
     end.

   Definition omega : D     := lam (fun x => app x x).
   Definition Omega : False := app omega omega.


On 14.03.2013 15:37, Dominique Devriese wrote:
> Samuel,
>
> 2013/3/14 Samuel Gélineau <gelisam at gmail.com>:
>>      data Con : Set where
>>        -- curry's paradox would use this.
>>        --   mkCon : (Con → ⊥) → Con
>>        -- since we have type-in-type but not negative occurrences,
>>        -- fake it using propositional equality.
>>        con : (A : Set) → Con ≡ A → (A → ⊥) → Con
>
> Interesting!  But actually, the above does not seem to be accepted by
> the latest (darcs) version of Agda, even when I specify to allow
> type-in-type.  I need to also turn off the positivity checker, despite
> what your comment suggests.
>
> Regards,
> Dominique
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/