Created

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

How Agda's --type-in-type can lead to a contradiction.

View Main.agda
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
{-# 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 σ)
Owner

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.