{-# LANGUAGE CPP, DataKinds, TemplateHaskell, QuasiQuotes, TypeApplications, TypeOperators #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_HADDOCK hide #-}
module Data.Sum.Templates
( mkElemIndexTypeFamily
, mkApplyInstance
) where
import Control.Monad
import Data.Kind
import Data.Traversable
import Language.Haskell.TH hiding (Type)
import qualified Language.Haskell.TH as TH (Type)
import Language.Haskell.TH.Quote
import Unsafe.Coerce (unsafeCoerce)
import GHC.TypeLits
mkElemIndexTypeFamily :: Integer -> DecsQ
mkElemIndexTypeFamily paramN = do
let [elemIndex, t, ts] = mkName <$> ["ElemIndex", "t", "ts"]
mkT = pure . VarT . mkName . ('t' :) . show
binders = [kindedTV t <$> [t| Type -> Type |] , kindedTV ts <$> [t| [Type -> Type] |] ]
resultKind = kindSig <$> [t| Nat |]
equations = fmap buildEquation [0..pred paramN] ++ [errorCase]
errorBody = [t|
TypeError ('Text "'" ':<>: ('ShowType $(varT t)) ':<>:
'Text "' is not a member of the type-level list" ':$$:
'ShowType $(varT ts))
|]
#if MIN_VERSION_template_haskell(2,15,0)
buildEquation n = tySynEqn Nothing (lhsMatch n) . litT . numTyLit $ n
lhsMatch n = [t| $(conT elemIndex) $(mkT n) $(typeListT WildCardT <$> traverse mkT [0..n]) |]
errorCase = tySynEqn Nothing [t| $(conT elemIndex) $(varT t) $(varT ts) |] errorBody
#else
buildEquation n = tySynEqn (lhsMatch n) (litT . numTyLit $ n)
lhsMatch n = [mkT n, typeListT WildCardT <$> traverse mkT [0..n] ]
errorCase = tySynEqn [varT t, varT ts] errorBody
#endif
fmap pure =<< closedTypeFamilyD elemIndex
<$> sequenceA binders
<*> resultKind
<*> pure Nothing
<*> pure equations
mkApplyInstance :: Integer -> Dec
mkApplyInstance paramN =
InstanceD Nothing (AppT constraint <$> typeParams) (AppT (AppT (ConT applyC) constraint) (typeListT PromotedNilT typeParams))
[ FunD apply (zipWith mkClause [0..] typeParams)
, PragmaD (InlineP apply Inlinable FunLike AllPhases)
]
where typeParams = VarT . mkName . ('f' :) . show <$> [0..pred paramN]
[applyC, apply, f, r, union] = mkName <$> ["Apply", "apply", "f", "r", "Sum"]
[constraint, a] = VarT . mkName <$> ["constraint", "a"]
mkClause i nthType = Clause
[ VarP f, ConP union [ LitP (IntegerL i), VarP r ] ]
(NormalB (AppE (VarE f) (SigE (AppE (VarE 'unsafeCoerce) (VarE r)) (AppT nthType a))))
[]
typeListT :: TH.Type -> [TH.Type] -> TH.Type
typeListT = foldr (AppT . AppT PromotedConsT)