    {- 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