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 σ)

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