{- Data/Singletons/Type.hs

(c) Richard Eisenberg 2013
rae@cs.brynmawr.edu

This file implements promotion of types into kinds.
-}

module Data.Singletons.Promote.Type
  ( promoteType, promoteTypeArg, promoteUnraveled
  ) where

import Language.Haskell.TH.Desugar
import Data.Singletons.Names
import Language.Haskell.TH

-- the only monadic thing we do here is fail. This allows the function
-- to be used from the Singletons module
promoteType :: MonadFail m => DType -> m DKind
promoteType :: DType -> m DType
promoteType = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go []
  where
    go :: MonadFail m => [DTypeArg] -> DType -> m DKind
    -- We don't need to worry about constraints: they are used to express
    -- static guarantees at runtime. But, because we don't need to do
    -- anything special to keep static guarantees at compile time, we don't
    -- need to promote them.
    go :: [DTypeArg] -> DType -> m DType
go []       (DForallT _tvbs :: [DTyVarBndr]
_tvbs _cxt :: DCxt
_cxt ty :: DType
ty) = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
    go []       (DAppT (DAppT DArrowT (DForallT (_:_) _ _)) _) =
      String -> m DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Cannot promote types of rank above 1."
    go args :: [DTypeArg]
args     (DAppT t1 :: DType
t1 t2 :: DType
t2) = do
      DType
k2 <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
t2
      [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go (DType -> DTypeArg
DTANormal DType
k2 DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DType
t1
       -- NB: This next case means that promoting something like
       --   (((->) a) :: Type -> Type) b
       -- will fail because the pattern below won't recognize the
       -- arrow to turn it into a TyFun. But I'm not terribly
       -- bothered by this, and it would be annoying to fix. Wait
       -- for someone to report.
    go args :: [DTypeArg]
args     (DAppKindT ty :: DType
ty ki :: DType
ki) = do
      DType
ki' <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ki
      [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go (DType -> DTypeArg
DTyArg DType
ki' DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DType
ty
    go args :: [DTypeArg]
args     (DSigT ty :: DType
ty ki :: DType
ki) = do
      DType
ty' <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
      -- No need to promote 'ki' - it is already a kind.
      DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (DType -> DType -> DType
DSigT DType
ty' DType
ki) [DTypeArg]
args
    go args :: [DTypeArg]
args     (DVarT name :: Name
name) = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DVarT Name
name) [DTypeArg]
args
    go []       (DConT name :: Name
name)
      | Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeRepName               = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
      | Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
repName = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
    go args :: [DTypeArg]
args     (DConT name :: Name
name)
      | Just n :: Int
n <- Name -> Maybe Int
unboxedTupleNameDegree_maybe Name
name
      = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT (Int -> Name
tupleTypeName Int
n)) [DTypeArg]
args
      | Bool
otherwise
      = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT Name
name) [DTypeArg]
args
    go [DTANormal k1 :: DType
k1, DTANormal k2 :: DType
k2] DArrowT
      = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
tyFunArrowName DType -> DType -> DType
`DAppT` DType
k1 DType -> DType -> DType
`DAppT` DType
k2
    go _        ty :: DType
ty@DLitT{} = DType -> m DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
ty

    go args :: [DTypeArg]
args     hd :: DType
hd = String -> m DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m DType) -> String -> m DType
forall a b. (a -> b) -> a -> b
$ "Illegal Haskell construct encountered:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                            "headed by: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DType -> String
forall a. Show a => a -> String
show DType
hd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                            "applied to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [DTypeArg] -> String
forall a. Show a => a -> String
show [DTypeArg]
args

promoteTypeArg :: MonadFail m => DTypeArg -> m DTypeArg
promoteTypeArg :: DTypeArg -> m DTypeArg
promoteTypeArg (DTANormal t :: DType
t) = DType -> DTypeArg
DTANormal (DType -> DTypeArg) -> m DType -> m DTypeArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
t
promoteTypeArg ta :: DTypeArg
ta@(DTyArg _) = DTypeArg -> m DTypeArg
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTypeArg
ta -- Kinds are already promoted

promoteUnraveled :: MonadFail m => DType -> m ([DKind], DKind)
promoteUnraveled :: DType -> m (DCxt, DType)
promoteUnraveled ty :: DType
ty = do
  DCxt
arg_kis <- (DType -> m DType) -> DCxt -> m DCxt
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DCxt
arg_tys
  DType
res_ki  <- DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType DType
res_ty
  (DCxt, DType) -> m (DCxt, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return (DCxt
arg_kis, DType
res_ki)
  where
    (_, _, arg_tys :: DCxt
arg_tys, res_ty :: DType
res_ty) = DType -> ([DTyVarBndr], DCxt, DCxt, DType)
unravel DType
ty