Skip to content

@gelisam /Main.agda

Embed URL


Subversion checkout URL

You can clone with
Download ZIP
How Agda's --type-in-type can lead to a contradiction.
{-# OPTIONS --type-in-type #-}
module Main where
open import Data.Empty
data _≡_ (A : Set) : Set → Set where
refl : A ≡ A
subst : {P : Set Set} {x y : Set} x ≡ y P y P x
subst refl p = p
data Con : Set where
con : (A : Set) Con ≡ A (A ⊥) Con
mkCon : (Con ⊥) Con
mkCon f = con Con refl f
unCon : Con (Con ⊥)
unCon (con A eq f) = subst {\x x ⊥} eq f
σ : Con
σ c = unCon c c
ω :
ω = σ (mkCon σ)

Turns out this was a bug in the type-checker; with the latest version of Agda, the above program is no longer accepted unless --no-positivity-check is also added.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.