content: {- 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 = promoteType_options defaultPromoteTypeOptions{ptoCheckVanilla = 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 = promoteType_options defaultPromoteTypeOptions
  
  -- | Options for controlling how types are promoted at a fine granularity.
  data PromoteTypeOptions = PromoteTypeOptions
    { ptoCheckVanilla :: Bool
      -- ^ If 'True', invoke 'checkVanillaDType' on the argument type being
      --   promoted. See @Note [Vanilla-type validity checking during promotion]@.
    , 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 Show
  
  -- | The default 'PromoteTypeOptions':
  --
  -- * 'checkVanillaDType' is not invoked.
  --
  -- * Throw an error when attempting to promote a wildcard type.
  defaultPromoteTypeOptions :: PromoteTypeOptions
  defaultPromoteTypeOptions = PromoteTypeOptions
    { ptoCheckVanilla = False
    , ptoAllowWildcards = 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 pto typ = do
    -- See Note [Vanilla-type validity checking during promotion]
    when (ptoCheckVanilla pto) $
      checkVanillaDType typ
    go [] typ
    where
      go :: [DTypeArg] -> DType -> m DKind
      go []       (DForallT tele ty) = do
        ty' <- go [] ty
        pure $ DForallT tele ty'
      go args     ty@DForallT{} = illegal args 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 _cxt ty) = go [] ty
      go args     ty@DConstrainedT{} = illegal args ty
      go args     (DAppT t1 t2) = do
        k2 <- go [] t2
        go (DTANormal k2 : args) 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     (DAppKindT ty ki) = do
        ki' <- go [] ki
        go (DTyArg ki' : args) ty
      go args     (DSigT ty ki) = do
        ty' <- go [] ty
        -- No need to promote 'ki' - it is already a kind.
        return $ applyDType (DSigT ty' ki) args
      go args     (DVarT name) = return $ applyDType (DVarT name) args
      go args     (DConT name) = do
        opts <- getOptions
        return $ applyDType (DConT (promotedDataTypeOrConName opts name)) args
      go args     ty@DArrowT =
        case filterDTANormals args of
          []        -> noPartialArrows
          [_]       -> noPartialArrows
          [k1, k2]  -> return $ DConT tyFunArrowName `DAppT` k1 `DAppT` k2
          (_:_:_:_) -> illegal args ty
      go []       ty@DLitT{} = pure ty
      go args     ty@DLitT{} = illegal args ty
      go args     ty@DWildCardT{}
        | ptoAllowWildcards pto
        = pure $ applyDType ty args
        | otherwise
        = fail $ unlines
            [ "`singletons-th` does not support wildcard types"
            , "\tunless they appear in visible type patterns of data constructors"
            , "\t" ++ herald
            ]
  
      noPartialArrows :: m a
      noPartialArrows = fail $ unlines
        [ "`singletons-th` does not support partial applications of (->)"
        , "\t" ++ herald
        ]
  
      herald :: String
      herald = "In the type: " ++ pprint (sweeten typ)
  
      illegal :: [DTypeArg] -> DType -> m a
      illegal args hd = fail $ unlines
        [ "Illegal Haskell construct encountered:"
        , "\theaded by: " ++ show hd
        , "\tapplied to: " ++ show 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 (DTANormal t) = DTANormal <$> promoteType_NC t
  promoteTypeArg_NC ta@(DTyArg _) = pure 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 ty = do
    (tvbs, _, arg_tys, res_ty) <- unravelVanillaDType ty
    arg_kis <- mapM promoteType_NC arg_tys
    res_ki  <- promoteType_NC res_ty
    return (tvbs, arg_kis, 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.
  -}
  