TypeRep tomfoolery

Basics.hs

{-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications,
             ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
             TypeInType, ConstraintKinds, UndecidableInstances,
             FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
             FlexibleContexts, StandaloneDeriving, InstanceSigs  #-}

module Basics where

import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
import Data.Proxy
import GHC.Exts
import Data.Kind
import Data.Functor.Compose

data (a :: k1) :~~: (b :: k2) where
  HRefl :: a :~~: a

data Dict :: Constraint -> Type where
  Dict :: c => Dict c

-- Type-level inequality
type a /= b = Not (a == b)

-- append two schemas
type family s1 ++ s2 where
  '[]       ++ s2 = s2
  (s ': s1) ++ s2 = s ': (s1 ++ s2)

natValue :: forall n. KnownNat n => Integer
natValue = natVal @n Proxy

type family All c tys where
  All _ '[] = (() :: Constraint)
  All c (ty ': tys) = (c ty, All c tys)

type family Sing = (r :: k -> Type) | r -> k

data SList :: forall k. [k] -> Type where
  SNil :: SList '[]
  SCons :: Sing h -> SList t -> SList (h ': t)
type instance Sing = SList

data TypeRep (a :: k) where
  TyCon :: Primitive a => TyCon a -> TypeRep a
  TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)

type family Primitive (a :: k) :: Constraint where
  Primitive (_ _) = (False ~ True) -- TypeError (ShowType (a b) :<>: Text " is not primitive")
  Primitive _     = (() :: Constraint)

data TyCon (a :: k) where
  Int :: TyCon Int
  Bool :: TyCon Bool
  Char :: TyCon Char
  List :: TyCon []
  Maybe :: TyCon Maybe
  Arrow :: TyCon (->)
  TYPE  :: TyCon TYPE
  Levity :: TyCon Levity
  Lifted' :: TyCon 'Lifted
  Unlifted' :: TyCon 'Unlifted
  -- add to eqTyCon too


eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
eqTyCon Int Int = Just HRefl
eqTyCon Bool Bool = Just HRefl
eqTyCon Char Char = Just HRefl
eqTyCon List List = Just HRefl
eqTyCon Maybe Maybe = Just HRefl
eqTyCon Arrow Arrow = Just HRefl
eqTyCon TYPE TYPE = Just HRefl
eqTyCon Levity Levity = Just HRefl
eqTyCon Lifted' Lifted' = Just HRefl
eqTyCon Unlifted' Unlifted' = Just HRefl
eqTyCon _ _ = Nothing

tcType :: TypeRep Type
tcType = TyApp (TyCon TYPE) (TyCon Lifted')

data TypeRepX :: (forall k. k -> Constraint) -> Type where
  TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
              c a => TypeRep a -> TypeRepX c

-- TypeRepX ((~~) Type)
-- (~~) :: forall k1 k2. k1 -> k2 -> Constraint
-- I need: (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint

data TyConX where
  TyConX :: Primitive a => TyCon a -> TyConX

instance Read TyConX where
  readsPrec _ "Int" = [(TyConX Int, "")]
  readsPrec _ "Bool" = [(TyConX Bool, "")]
  readsPrec _ _ = []

class ConstTrue (a :: k) -- RAE: needs the :: k to make it a specified tyvar
instance ConstTrue a

instance Read (TypeRepX ConstTrue) where
  readsPrec _ "String" = [(TypeRepX (typeRep @String), "")]
  readsPrec p s = case readsPrec p s of
    [(TyConX tc, "")] -> [(TypeRepX (TyCon tc), "")]
    _ -> []

-- instance Read (TypeRepX ((~~) Type))  RAE: need (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
-- RAE: need kind signatures on classes

class k ~~ Type => IsType (x :: k)
instance k ~~ Type => IsType (x :: k)

eqT :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqT (TyCon tc1) (TyCon tc2) = eqTyCon tc1 tc2
eqT (TyApp f1 a1) (TyApp f2 a2) = do
  HRefl <- eqT f1 f2
  HRefl <- eqT a1 a2
  return HRefl
eqT _ _ = Nothing


instance Read (TypeRepX IsType) where
  readsPrec p s = case readsPrec @(TypeRepX ConstTrue) p s of
    [(TypeRepX tr, "")]
      | Just HRefl <- eqT (kindRep tr) tcType
      -> [(TypeRepX tr, "")]
    _ -> error "wrong kind"

type instance Sing = (TypeRep :: Type -> Type)

data SSymbol :: Symbol -> Type where
  SSym :: KnownSymbol s => SSymbol s
type instance Sing = SSymbol

kindRep :: TypeRep (a :: k) -> TypeRep k
kindRep (TyCon tc) = tcKindRep tc
kindRep (TyApp (f :: TypeRep (tf :: k1 -> k)) _) = case kindRep f :: TypeRep (k1 -> k) of
  TyApp _ res -> res

tcArrow :: TypeRep (->)
tcArrow = TyCon Arrow

mkFunTy :: TypeRep a -> TypeRep b -> TypeRep (a -> b)
mkFunTy arg res = tcArrow `TyApp` arg `TyApp` res
infixr 0 `mkFunTy`

tcKindRep :: TyCon (a :: k) -> TypeRep k
tcKindRep Int = tcType
tcKindRep Bool = tcType
tcKindRep Char = tcType
tcKindRep List = mkFunTy tcType tcType
tcKindRep Maybe = mkFunTy tcType tcType
tcKindRep Arrow = tcType `mkFunTy` tcType `mkFunTy` tcType
tcKindRep TYPE = TyCon Levity `mkFunTy` tcType
tcKindRep Unlifted' = TyCon Levity
tcKindRep Lifted' = TyCon Levity
tcKindRep Levity = tcType

class TyConAble a where
  tyCon :: TyCon a

instance TyConAble Int where tyCon = Int
instance TyConAble Bool where tyCon = Bool
instance TyConAble Char where tyCon = Char
instance TyConAble [] where tyCon = List
instance TyConAble Maybe where tyCon = Maybe
instance TyConAble (->) where tyCon = Arrow
instance TyConAble TYPE where tyCon = TYPE
instance TyConAble 'Unlifted where tyCon = Unlifted'
instance TyConAble 'Lifted where tyCon = Lifted'
instance TyConAble Levity where tyCon = Levity

type family CheckPrim a where
  CheckPrim (_ _) = 'False
  CheckPrim _     = 'True

class Typeable' a (b :: Bool) where
  typeRep' :: TypeRep a

type Typeable a = Typeable' a (CheckPrim a)

instance (Primitive a, TyConAble a) => Typeable' a 'True where
  typeRep' = TyCon tyCon

instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
  typeRep' = TyApp typeRep typeRep

typeRep :: forall a. Typeable a => TypeRep a
typeRep = typeRep' @_ @_ @(CheckPrim a) -- RAE: #11512 says we need the extra @_.

instance Show (TypeRep a) where
  show (TyCon tc) = show tc
  show (TyApp tr1 tr2) = show tr1 ++ " " ++ show tr2

deriving instance Show (TyCon a)

instance TestEquality SSymbol where
  testEquality :: forall s1 s2. SSymbol s1 -> SSymbol s2 -> Maybe (s1 :~: s2)
  testEquality SSym SSym = sameSymbol @s1 @s2 Proxy Proxy

instance TestEquality TypeRep where
  testEquality tr1 tr2
    | Just HRefl <- eqT tr1 tr2
    = Just Refl
    | otherwise
    = Nothing

instance Show (SSymbol name) where
  show s@SSym = symbolVal s