Injective.hs

{-# LANGUAGE GADTs #-}
-- nontermination without any recursion, even in types
-- possible because of impredicativity + injectivity
-- based on https://gist.github.com/leodemoura/0c88341bb585bf9a72e6
-- see also https://github.com/idris-lang/Idris-dev/issues/3687

data False

data I (f :: * -> *) where

data P (x :: *) where
  MkP :: (a (I a) -> False) -> P (I a)

falsePIP :: P (I P) -> False
falsePIP h@(MkP np) = np h

false :: a
false = case falsePIP (MkP falsePIP) of {}

main = putStrLn false

https://okmij.org/ftp/Haskell/impredicativity-bites.html