TElem.hs

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS -Wall -Wno-unticked-promoted-constructors #-}

module Talk where

import Data.Kind
import Data.Type.Equality
import Data.Proxy
import GHC.Exts
import GHC.Generics
import GHC.TypeLits
import Unsafe.Coerce (unsafeCoerce)

{-------------------------------------------------------------------------------
  Goals
-------------------------------------------------------------------------------}

-- Part 1

data Con a = MkCon { conModl :: a, conName :: a }

newtype Usr (c :: Con Symbol) = Usr Any

unsafeCastUsr :: ConOf a c => Usr c -> a
unsafeCastUsr = unsafeCoerce

class ConOf_ a c

-- Part 2

data IsConOf a c where
  IsConOf :: ConOf a c => IsConOf a c

_checkConOf :: Maybe (IsConOf a c)
_checkConOf = undefined

{-------------------------------------------------------------------------------
  Part 1: computing all constructors
-------------------------------------------------------------------------------}

type family Cons a :: [Con Symbol] where
  Cons a = GCons (Rep a)

type family GCons f :: [Con Symbol] where
  GCons (M1 D ('MetaData _ m _ _) f) = GConsOf m f '[]

type family GConsOf m f acc :: [Con Symbol] where
  GConsOf m (f :+: g) acc = GConsOf m g (GConsOf m f acc)
  GConsOf m (M1 C ('MetaCons c _ _) f) acc = 'MkCon m c ': acc

-- Version 1
-- type family Elem x xs :: Bool where
--   Elem x '[]       = False
--   Elem x (x ': _)  = True
--   Elem x (_ ': xs) = Elem x xs

type family Assert (b :: Bool) :: Constraint where
  Assert True  = ()
  Assert False = TypeError (Text "No")

type family ConOf a c :: Constraint where
  ConOf a c = Assert (Elem c (Cons a))

{-------------------------------------------------------------------------------
  Example
-------------------------------------------------------------------------------}

data T1 = MkT1 Int  deriving (Generic)
data T2 = MkT2 Bool deriving (Generic)

-- toT1 :: Usr (MkCon "A" "B") -> T1
-- toT1 = unsafeCastUsr

toT2 :: Usr (MkCon "Talk" "MkT2") -> T2
toT2 = unsafeCastUsr

{-------------------------------------------------------------------------------
  Part 2
-------------------------------------------------------------------------------}

data family Sing (a :: k)

data instance Sing (b :: Bool) where
  STrue  :: Sing True
  SFalse :: Sing False

class SingI (a :: k) where
  sing :: Sing a

instance SingI 'True  where sing = STrue
instance SingI 'False where sing = SFalse

checkConOf :: forall a c. SingI (Elem c (Cons a)) => Maybe (IsConOf a c)
checkConOf =
    case sing :: Sing (Elem c (Cons a)) of
      STrue  -> Just IsConOf
      SFalse -> Nothing

example :: forall c. (
       SingI (Elem c (Cons T1))
     , SingI (Elem c (Cons T2))
     )
  => Usr c -> Maybe (Either T1 T2)
example u =
    case (checkConOf @T1 @c, checkConOf @T2 @c) of
      (Just IsConOf, _) -> Just (Left  (unsafeCastUsr u))
      (_, Just IsConOf) -> Just (Right (unsafeCastUsr u))
      _otherwise        -> Nothing

{-------------------------------------------------------------------------------
  Part 2, improved
-------------------------------------------------------------------------------}

class TEq k where
  teq :: Sing (a :: k) -> Sing (b :: k) -> Maybe (a :~: b)

data instance Sing (n :: Symbol) where
  SSym :: KnownSymbol n => Sing n

instance KnownSymbol n => SingI (n :: Symbol) where
  sing = SSym

instance TEq Symbol where
  teq SSym SSym = sameSymbol Proxy Proxy

data instance Sing (xs :: [k]) where
  SNil  :: Sing '[]
  SCons :: Sing x -> Sing xs -> Sing (x ': xs)

instance SingI '[] where
  sing = SNil
instance (SingI x, SingI xs) => SingI (x ': xs) where
  sing = SCons sing sing

data IsElem x xs where
  IsElem :: Elem x xs ~ True => IsElem x xs

shift :: IsElem x ys -> IsElem x (y ': ys)
shift IsElem = IsElem

telem :: TEq k => Sing (x :: k) -> Sing (xs :: [k]) -> Maybe (IsElem x xs)
telem _ SNil         = Nothing
telem x (SCons y ys) =
    case teq x y of
      Just Refl -> Just IsElem
      Nothing   -> shift <$> telem x ys

type family Equal (x :: k) (y :: k) where
  Equal x x = 'True
  Equal x y = 'False

-- Version 1
-- type family Or (a :: Bool) (b :: Bool) where
--   Or True b = True
--   Or _    b = b

type family Elem (x :: k) (xs :: [k]) where
  Elem x '[]       = 'False
  Elem x (y ': ys) = Or (Equal x y) (Elem x ys)

type family Or (a :: Bool) (b :: Bool) where
  Or 'True b     = 'True
  Or a     'True = 'True
  Or _     _     = 'False

{-------------------------------------------------------------------------------
  TEq for Con
-------------------------------------------------------------------------------}

type family ConModl (c :: Con k) :: k where ConModl (MkCon m _) = m
type family ConName (c :: Con k) :: k where ConName (MkCon _ n) = n

type KnownCon c = (
    KnownSymbol (ConModl c)
  , KnownSymbol (ConName c)
  , c ~ MkCon (ConModl c) (ConName c)
  )

data instance Sing (c :: Con Symbol) where
  SCon :: KnownCon c => Sing (c :: Con Symbol)

instance KnownCon c => SingI (c :: Con Symbol) where
  sing = SCon

instance TEq (Con Symbol) where
  teq :: forall c c'.
       Sing (c  :: Con Symbol)
    -> Sing (c' :: Con Symbol)
    -> Maybe (c :~: c')
  teq SCon SCon = do
      Refl <- teq (sing @_ @(ConModl c)) (sing @_ @(ConModl c'))
      Refl <- teq (sing @_ @(ConName c)) (sing @_ @(ConName c'))
      return Refl

checkConOf' :: forall a c. (SingI c, SingI (Cons a)) => Maybe (IsConOf a c)
checkConOf' = do
    IsElem <- telem (sing @_ @c) (sing @_ @(Cons a))
    return IsConOf

example'  :: forall c. SingI c => Usr c -> Maybe (Either T1 T2)
example' u =
    case (checkConOf' @T1 @c, checkConOf' @T2 @c) of
      (Just IsConOf, _) -> Just (Left  (unsafeCastUsr u))
      (_, Just IsConOf) -> Just (Right (unsafeCastUsr u))
      _otherwise        -> Nothing