Exists.hs

{-# LANGUAGE GADTs, DataKinds, TypeOperators #-}

import Data.Type.Equality

data Exists where
    MkExists :: a -> Exists

thm :: 'MkExists 'True :~: 'MkExists 'False
thm = Refl

{-

Exi.hs:9:7: error:
    • Couldn't match type ‘'True’ with ‘'False’
      Expected type: 'MkExists 'True :~: 'MkExists 'False
        Actual type: 'MkExists 'True :~: 'MkExists 'True
    • In the expression: Refl
      In an equation for ‘thm’: thm = Refl
  |
9 | thm = Refl
  |       ^^^^

-}