public
Created

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

  • Download Gist
Main.agda
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 σ)

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.

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.