Base.hs

{-# LANGUAGE EmptyDataDecls, TypeFamilies, PolyKinds, TemplateHaskell, TypeOperators #-}

module Type.Spine.Base where

import Language.Haskell.TH

import Type.Spine.TH (tyConSignature)



--type family Reify (t :: k)
type family Spine (t :: k)



data Atom (t :: k) :: *
infixl 9 :@
data (tc :: k) :@ (t :: l) :: *



-- works in 7.4, but not in 7.6 :(
--type instance Spine ((tc :: k -> l) (t :: k)) = Spine tc :@ Spine t

-- | @spineType_d n@ generates the @Spine@ instance for the type named @n@.
spineType_d :: Name -> Q [Dec]
spineType_d n = tyConSignature n >>= spineType_d_ n . fst


-- | @spineType_d_ n ks@ generates the @Spine@ instance for the type named @n@
-- that has parameters with kinds @ks@.
spineType_d_ :: Name -> [Kind] -> Q [Dec]
spineType_d_ = spineType_gen_ . ConT




-- | @spineType_pro n@ generates the @Spine@ instance for the promoted data constructor named @n@.
spineType_pro :: Name -> Q [Dec]
spineType_pro n = tyConSignature n >>= spineType_d_ n . fst

-- | @spineType_pro_ n ks@ generates the @Spine@ instance for the promoted data
-- constructor named @n@ that has parameters with kinds @ks@.
spineType_pro_ :: Name -> [Kind] -> Q [Dec]
spineType_pro_ = spineType_gen_ . PromotedT



-- | @spineType_gen_ ty ks@ generates the @Spine@ instance for the type @ty@
-- that has parameters with kinds @ks@.
spineType_gen_ :: Type -> [Kind] -> Q [Dec]
spineType_gen_ t ks = do
  let rhs = ConT ''Atom `AppT` t
      vars = [VarT $ mkName $ "t" ++ show i | i <- [0..]]
  let snoc ty1 ty2 = ConT ''(:@) `AppT` ty1 `AppT` ty2
  return $ TySynInstD ''Spine [t] rhs :
    [ case take n vars of
        vars -> TySynInstD ''Spine [foldl AppT t vars] $ foldl snoc t $ vars
      | n <- [1..length ks] ]