[Agda] How safe is Type:Type?

[Andreas Abel]

{-# OPTIONS --type-in-type #-} is sometimes chosen to avoid the fiddling 
with universe levels.  After all, Hurkens' Paradox is quite 
sophisticated, one should not by chance exploit the inconsistency of 
Type:Type in an innocent Agda project, no?

Well, that's the folklore.  I want to bring to mind that at least in 
Agda, with data types and structural recursion, there are much quicker 
routes to inconsistency than Hurkens' Paradox.

1. One is Thierry's 1992 example that impredicative data types are 
inconsistent with structural recursion:

   {-# OPTIONS --type-in-type #-}

   data ⊥ : Set where

   -- An impredicative data type

   data D : Set where
     c : (f : (A : Set) → A → A) → D

   -- Structural recursion with  f args < c f  is no longer valid.
   -- We should not be able to demonstrated that D is empty.

   empty : D → ⊥
   empty (c f) = empty (f D (c f))

   -- This gets us to absurdity quickly:

   absurd : ⊥
   absurd = empty (c λ A x → x)

2. There is also Russell's paradox, written down by Paolo Capriotti.

   https://github.com/agda/agda/blob/master/test/Succeed/Russell.agda

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

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

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/