{- Data/Singletons/TH/Promote/Type.hs

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

This file implements promotion of types into kinds.
-}

module Data.Singletons.TH.Promote.Type
  ( promoteType, promoteType_NC, promoteType_options
  , PromoteTypeOptions(..), defaultPromoteTypeOptions
  , promoteTypeArg_NC, promoteUnraveled
  ) where

import Control.Monad (when)
import Language.Haskell.TH (pprint)
import Language.Haskell.TH.Desugar
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Util

-- | Promote a 'DType' to the kind level and invoke 'checkVanillaDType'.
-- See @Note [Vanilla-type validity checking during promotion]@.
promoteType :: OptionsMonad m => DType -> m DKind
promoteType :: forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType = PromoteTypeOptions -> DType -> m DType
forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
defaultPromoteTypeOptions{ptoCheckVanilla :: Bool
ptoCheckVanilla = Bool
True}

-- | Promote a 'DType' to the kind level. This is suffixed with \"_NC\" because
-- we do not invoke 'checkVanillaDType' here.
-- See @Note [Vanilla-type validity checking during promotion]@.
promoteType_NC :: forall m. OptionsMonad m => DType -> m DKind
promoteType_NC :: forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC = PromoteTypeOptions -> DType -> m DType
forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
defaultPromoteTypeOptions

-- | Options for controlling how types are promoted at a fine granularity.
data PromoteTypeOptions = PromoteTypeOptions
  { PromoteTypeOptions -> Bool
ptoCheckVanilla :: Bool
    -- ^ If 'True', invoke 'checkVanillaDType' on the argument type being
    --   promoted. See @Note [Vanilla-type validity checking during promotion]@.
  , PromoteTypeOptions -> Bool
ptoAllowWildcards :: Bool
    -- ^ If 'True', allow promoting wildcard types. Otherwise, throw an error.
    --   In most places, GHC disallows kind-level wildcard types, so rather
    --   than promoting such wildcards and getting an error message from GHC
    --   /post facto/, we can catch such wildcards early and give a more
    --   descriptive error message instead.
  } deriving Int -> PromoteTypeOptions -> ShowS
[PromoteTypeOptions] -> ShowS
PromoteTypeOptions -> String
(Int -> PromoteTypeOptions -> ShowS)
-> (PromoteTypeOptions -> String)
-> ([PromoteTypeOptions] -> ShowS)
-> Show PromoteTypeOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PromoteTypeOptions -> ShowS
showsPrec :: Int -> PromoteTypeOptions -> ShowS
$cshow :: PromoteTypeOptions -> String
show :: PromoteTypeOptions -> String
$cshowList :: [PromoteTypeOptions] -> ShowS
showList :: [PromoteTypeOptions] -> ShowS
Show

-- | The default 'PromoteTypeOptions':
--
-- * 'checkVanillaDType' is not invoked.
--
-- * Throw an error when attempting to promote a wildcard type.
defaultPromoteTypeOptions :: PromoteTypeOptions
defaultPromoteTypeOptions :: PromoteTypeOptions
defaultPromoteTypeOptions = PromoteTypeOptions
  { ptoCheckVanilla :: Bool
ptoCheckVanilla = Bool
False
  , ptoAllowWildcards :: Bool
ptoAllowWildcards = Bool
False
  }

-- | Promote a 'DType' to the kind level. This is the workhorse for
-- 'promoteType' and 'promoteType_NC'.
promoteType_options :: forall m. OptionsMonad m => PromoteTypeOptions -> DType -> m DKind
promoteType_options :: forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
pto DType
typ = do
  -- See Note [Vanilla-type validity checking during promotion]
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PromoteTypeOptions -> Bool
ptoCheckVanilla PromoteTypeOptions
pto) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    DType -> m ()
forall (m :: * -> *). MonadFail m => DType -> m ()
checkVanillaDType DType
typ
  [DTypeArg] -> DType -> m DType
go [] DType
typ
  where
    go :: [DTypeArg] -> DType -> m DKind
    go :: [DTypeArg] -> DType -> m DType
go []       (DForallT DForallTelescope
tele DType
ty) = do
      DType
ty' <- [DTypeArg] -> DType -> m DType
go [] DType
ty
      DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DForallTelescope -> DType -> DType
DForallT DForallTelescope
tele DType
ty'
    go [DTypeArg]
args     ty :: DType
ty@DForallT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args 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
go [] DType
ty
    go [DTypeArg]
args     ty :: DType
ty@DConstrainedT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
    go [DTypeArg]
args     (DAppT DType
t1 DType
t2) = do
      DType
k2 <- [DTypeArg] -> DType -> m DType
go [] DType
t2
      [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
go [] DType
ki
      [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
go [] DType
ty
      -- No need to promote 'ki' - it is already a kind.
      DType -> m DType
forall a. a -> m a
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 a. a -> m a
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 [DTypeArg]
args     (DConT Name
name) = do
      Options
opts <- m Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      DType -> m DType
forall a. a -> m a
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 (Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name)) [DTypeArg]
args
    go [DTypeArg]
args     ty :: DType
ty@DType
DArrowT =
      case [DTypeArg] -> DCxt
filterDTANormals [DTypeArg]
args of
        []        -> m DType
forall a. m a
noPartialArrows
        [DType
_]       -> m DType
forall a. m a
noPartialArrows
        [DType
k1, DType
k2]  -> DType -> m DType
forall a. a -> m a
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
        (DType
_:DType
_:DType
_:DCxt
_) -> [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
    go []       ty :: DType
ty@DLitT{} = DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
ty
    go [DTypeArg]
args     ty :: DType
ty@DLitT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
    go [DTypeArg]
args     ty :: DType
ty@DWildCardT{}
      | PromoteTypeOptions -> Bool
ptoAllowWildcards PromoteTypeOptions
pto
      = DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType DType
ty [DTypeArg]
args
      | Bool
otherwise
      = String -> m DType
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m DType) -> String -> m DType
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
          [ String
"`singletons-th` does not support wildcard types"
          , String
"\tunless they appear in visible type patterns of data constructors"
          , String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
herald
          ]

    noPartialArrows :: m a
    noPartialArrows :: forall a. m a
noPartialArrows = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"`singletons-th` does not support partial applications of (->)"
      , String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
herald
      ]

    herald :: String
    herald :: String
herald = String
"In the type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
pprint (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
typ)

    illegal :: [DTypeArg] -> DType -> m a
    illegal :: forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
hd = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"Illegal Haskell construct encountered:"
      , String
"\theaded by: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DType -> String
forall a. Show a => a -> String
show DType
hd
      , String
"\tapplied to: " String -> ShowS
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 @Note [Vanilla-type validity checking during promotion]@.
promoteTypeArg_NC :: OptionsMonad m => DTypeArg -> m DTypeArg
promoteTypeArg_NC :: forall (m :: * -> *). OptionsMonad m => 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 :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DType
t
promoteTypeArg_NC ta :: DTypeArg
ta@(DTyArg DType
_) = DTypeArg -> m DTypeArg
forall a. a -> m a
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 :: OptionsMonad m
                 => DType -> m ([DTyVarBndrSpec], [DKind], DKind)
promoteUnraveled :: forall (m :: * -> *).
OptionsMonad m =>
DType -> m ([DTyVarBndrSpec], DCxt, DType)
promoteUnraveled DType
ty = do
  ([DTyVarBndrSpec]
tvbs, DCxt
_, DCxt
arg_tys, DType
res_ty) <- DType -> m ([DTyVarBndrSpec], DCxt, DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndrSpec], 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM DType -> m DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DCxt
arg_tys
  DType
res_ki  <- DType -> m DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DType
res_ty
  ([DTyVarBndrSpec], DCxt, DType)
-> m ([DTyVarBndrSpec], DCxt, DType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DTyVarBndrSpec]
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.
-}