IRC.hs

{-# LANGUAGE GADTs
           , KindSignatures
           , DataKinds
           , PolyKinds
           , TypeFamilies
           #-}

import GHC.TypeLits hiding (Nat)

-- | Store a dict saying that one symbol is smaller than another
data SymLT (s :: Symbol) (s' :: Symbol) where
  MkSymLT :: (CmpSymbol s s' ~ LT) => SymLT s s'

type family GetSymLTHelper (s :: Symbol) (s' :: Symbol) (o :: Ordering)
  :: Maybe (SymLT s s') where
  GetSymLTHelper s s' LT = Just MkSymLT
  GetSymLTHelper s s' o  = Nothing

-- | Given two symbols, maybe construct a SymLT if the first one is smaller
type family GetSymLT (s :: Symbol) (s' :: Symbol) :: Maybe (SymLT s s') where
  GetSymLT s s' = GetSymLTHelper s s' (CmpSymbol s s')
  
{- error:
IRC.hs:16:33: error:
    • Couldn't match expected kind ‘'LT’
                  with actual kind ‘CmpSymbol s s'’
    • In the first argument of ‘Just’, namely ‘MkSymLT’
      In the type ‘Just MkSymLT’
      In the type family declaration for ‘GetSymLTHelper’
   |
16 |   GetSymLTHelper s s' LT = Just MkSymLT
   |
-}