Generic Reflection (v0)

GenericReflection.hs

{-# language GADTs #-}
{-# language PolyKinds #-}
{-# language DataKinds #-}
{-# language ConstraintKinds #-}
{-# language KindSignatures #-}
{-# language TypeOperators #-}
{-# language FlexibleInstances #-}
{-# language MultiParamTypeClasses #-}
{-# language TypeApplications #-}
{-# language ScopedTypeVariables #-}

import GHC.Generics
import GHC.Types
import Data.Proxy

-- reflection

data SBool (t :: Bool) where
  STrue :: SBool 'True
  SFalse :: SBool 'False

instance Show (SBool t) where
  showsPrec _ STrue = showString "STrue"
  showsPrec _ SFalse = showString "SFalse"

class ReifiedBool (t :: Bool) where
  reflectBool :: SBool t

instance ReifiedBool 'True where
  reflectBool = STrue

instance ReifiedBool 'False where
  reflectBool = SFalse

data SDecidedStrictness (t :: DecidedStrictness) where
  SDecidedLazy :: SDecidedStrictness 'DecidedLazy
  SDecidedStrict :: SDecidedStrictness 'DecidedStrict
  SDecidedUnpack :: SDecidedStrictness 'DecidedUnpack

instance Show (SDecidedStrictness t) where
  showsPrec d SDecidedLazy = showString "SDecidedLazy"
  showsPrec d SDecidedStrict = showString "SDecidedStrict"
  showsPrec d SDecidedUnpack = showString "SDecidedUnpack"

class ReifiedDecidedStrictness (t :: DecidedStrictness) where
  reflectDecidedStrictness :: SDecidedStrictness t

instance ReifiedDecidedStrictness DecidedLazy where
  reflectDecidedStrictness = SDecidedLazy

instance ReifiedDecidedStrictness DecidedStrict where
  reflectDecidedStrictness = SDecidedStrict

instance ReifiedDecidedStrictness DecidedUnpack where
  reflectDecidedStrictness = SDecidedUnpack

data Ty p t where
  Ty :: SBool nt -> Cons p t -> Ty p (M1 D ('MetaData dc mdl pkg nt) t)

instance Show (Ty p t) where
  showsPrec d (Ty nt cs) = showParen (d > 10) $
    showString "Ty " . showsPrec 11 nt . showChar ' ' . showsPrec 11 cs

class GTy p t where
  gty :: Ty p t

instance (ReifiedBool nt, GCons p t) => GTy p (M1 D ('MetaData dc md pkg nt) t) where
  gty = Ty reflectBool (gcons @p)

data Cons p t where
  S :: Cons p l -> Cons p r -> Cons p (l :+: r)
  Con :: Fields p t -> Cons p (M1 C ci t)

instance Show (Cons p t) where
  showsPrec d (S l r) = showParen (d > 10) $
    showString "S " . showsPrec 11 l . showChar ' ' . showsPrec 11 r
  showsPrec d (Con b) = showParen (d > 10) $
    showString "Con " . showsPrec 11 b

class GCons p t where
  gcons :: Cons p t

instance (GCons p l, GCons p r) => GCons p (l :+: r) where
  gcons = S (gcons @p) (gcons @p)

instance GFields p t => GCons p (M1 C ci t) where
  gcons = Con (gfields @p)

data Fields p t where
  P :: Fields p l -> Fields p r -> Fields p (l :*: r)
  Sel :: SDecidedStrictness ds -> Field p t -> Fields p (M1 S ('MetaSel fn su ss ds) t)
  U :: Fields p U1

instance Show (Fields p t) where
  showsPrec d (P l r) = showParen (d > 10) $
    showString "P " . showsPrec 11 l . showChar ' ' . showsPrec 11 r
  showsPrec d (Sel s b) = showParen (d > 10) $
    showString "Sel " . showsPrec 11 s . showChar ' ' . showsPrec 11 b
  showsPrec _ U = showString "U"

class GFields p t where
  gfields :: Fields p t 

instance (GFields p l, GFields p r) => GFields p (l :*: r) where
  gfields = P (gfields @p) (gfields @p)

instance (ReifiedDecidedStrictness ds, GField p t) => GFields p (M1 S ('MetaSel fn su ss ds) t) where
  gfields = Sel reflectDecidedStrictness gfield

instance GFields p U1 where
  gfields = U

data Field (p :: * -> Constraint) (t :: * -> *) where
  K :: p c => Proxy c -> Field p (K1 i c)

instance Show (Field p t) where
  showsPrec d (K Proxy) = showParen (d > 10) $ showString "K Proxy"

class GField p t where
  gfield :: Field p t

instance p c => GField p (K1 i c) where
  gfield = K Proxy