Paradox.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UnicodeSyntax #-}

import Data.Bifunctor
import Data.Bool
import Data.Type.Equality
import Data.Kind
import Data.Singletons
import Data.Singletons.Sigma
import Data.Proxy
import Data.Void

data Unit = Unit

data SET where
    Set :: Proxy a -> (a -> SET) -> SET

v0 :: SET
v0 = Set (Proxy :: Proxy Void) absurd

v1 :: SET
v1 = Set (Proxy :: Proxy Unit) (const v0)

v2 :: SET
v2 = Set (Proxy :: Proxy Bool) (bool v0 v1)

v3 :: SET
v3 = Set (Proxy :: Proxy (Maybe Bool)) (maybe v2 (bool v0 v1))

type family UnProxy p where
    UnProxy (Proxy a) = a

type family ElPred a f b where
    ElPred a f b = a :~: f b

type family El (s1 :: SET) (s2 :: SET) :: Type where
    El a (Set x f) = Sigma ('UnProxy x) (ElPred a f) 

-- Paradox.hs:45:29: error:
--     Not in scope: data constructor ‘UnProxy’
--     Perhaps you meant one of these:
--       ‘Proxy’ (imported from Data.Proxy),
--       ‘KProxy’ (imported from Data.Proxy)
--    |
-- 45 |     El a (Set x f) = Sigma ('UnProxy x) (ElPred a f)
--    |                             ^^^^^^^^
-- Failed, no modules loaded.