{- 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, promoteType_NC
  , promoteTypeArg_NC, promoteUnraveled
  ) where

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

-- Promote a DType to the kind level.
--
-- NB: 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 DType
ty = do
  DType -> m ()
forall (m :: * -> *). MonadFail m => DType -> m ()
checkVanillaDType DType
ty
  DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
ty

-- Promote a DType to the kind level. This is suffixed with "_NC" because
-- we do not invoke checkVanillaDType here.
-- See [Vanilla-type validity checking during promotion].
promoteType_NC :: MonadFail m => DType -> m DKind
promoteType_NC :: DType -> m DType
promoteType_NC = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go []
  where
    go :: MonadFail m => [DTypeArg] -> DType -> m DKind
    go :: [DTypeArg] -> DType -> m DType
go []       (DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs DType
ty) = do
      DType
ty' <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
      DType -> m DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ ForallVisFlag -> [DTyVarBndr] -> DType -> DType
DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs DType
ty'
    -- 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 []       (DConstrainedT DCxt
_cxt DType
ty) = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
    go [DTypeArg]
args     (DAppT DType
t1 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 [DTypeArg]
args     (DAppKindT DType
ty 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 [DTypeArg]
args     (DSigT DType
ty 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 [DTypeArg]
args     (DVarT 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 -> 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 [DTypeArg]
args     (DConT Name
name)
      | Just 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 DType
k1, DTANormal DType
k2] DType
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 [DTypeArg]
_        ty :: DType
ty@DLitT{} = DType -> m DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
ty

    go [DTypeArg]
args     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
$ String
"Illegal Haskell construct encountered:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                            String
"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]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                            String
"applied to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [DTypeArg] -> String
forall a. Show a => a -> String
show [DTypeArg]
args

-- | Promote a DTypeArg to the kind level. This is suffixed with "_NC" because
-- we do not invoke checkVanillaDType here.
-- See [Vanilla-type validity checking during promotion].
promoteTypeArg_NC :: MonadFail m => DTypeArg -> m DTypeArg
promoteTypeArg_NC :: DTypeArg -> m DTypeArg
promoteTypeArg_NC (DTANormal 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_NC DType
t
promoteTypeArg_NC ta :: DTypeArg
ta@(DTyArg DType
_) = DTypeArg -> m DTypeArg
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTypeArg
ta -- Kinds are already promoted

-- | Promote a DType to the kind level, splitting it into its type variable
-- binders, argument types, and result type in the process.
promoteUnraveled :: MonadFail m
                 => DType -> m ([DTyVarBndr], [DKind], DKind)
promoteUnraveled :: DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty = do
  ([DTyVarBndr]
tvbs, DCxt
_, DCxt
arg_tys, DType
res_ty) <- DType -> m ([DTyVarBndr], DCxt, DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], DCxt, DCxt, DType)
unravelVanillaDType DType
ty
  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_NC DCxt
arg_tys
  DType
res_ki  <- DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
res_ty
  ([DTyVarBndr], DCxt, DType) -> m ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DTyVarBndr]
tvbs, DCxt
arg_kis, DType
res_ki)

{-
Note [Vanilla-type validity checking during promotion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We only support promoting (and singling) vanilla types, where a vanilla
function type is a type that:

1. Only uses a @forall@ at the top level, if used at all. That is to say, it
   does not contain any nested or higher-rank @forall@s.

2. Only uses a context (e.g., @c => ...@) at the top level, if used at all,
   and only after the top-level @forall@ if one is present. That is to say,
   it does not contain any nested or higher-rank contexts.

3. Contains no visible dependent quantification.

The checkVanillaDType function checks if a type is vanilla. Note that it is
crucial to call checkVanillaDType on the /entire/ type. For instance, it would
be incorrect to call unravelVanillaDType and then check each argument type
individually, since that loses information about which @forall@s/constraints
are higher-rank.

We make an effort to avoiding calling checkVanillaDType on the same type twice,
since checkVanillaDType must traverse the entire type. (It would not be
incorrect to do so, just wasteful.) For this certain, certain functions are
suffixed with "_NC" (short for "no checking") to indicate that they do not
invoke checkVanillaDType. These functions are used on types that have already
been validity-checked.
-}