Skip to content
Create a gist now

Instantly share code, notes, and snippets.

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 σ)
gelisam commented Mar 15, 2013

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.