    {- Data/Singletons/Single/Type.hs

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

    Singletonizes types.
    -}

    module Data.Singletons.Single.Type where

    import Language.Haskell.TH.Desugar
    import qualified Language.Haskell.TH.Desugar.OSet as OSet
    import Language.Haskell.TH.Desugar.OSet (OSet)
    import Language.Haskell.TH.Syntax
    import Data.Singletons.Names
    import Data.Singletons.Single.Monad
    import Data.Singletons.Promote.Type
    import Data.Singletons.Util
    import Control.Monad
    import Data.Foldable

    singType :: OSet Name      -- the set of bound kind variables in this scope
                               -- see Note [Explicitly binding kind variables]
                               -- in Data.Singletons.Promote.Monad
             -> DType          -- the promoted version of the thing classified by...
             -> DType          -- ... this type
             -> SgM ( DType    -- the singletonized type
                    , Int      -- the number of arguments
                    , [Name]   -- the names of the tyvars used in the sing'd type
                    , DCxt     -- the context of the singletonized type
                    , [DKind]  -- the kinds of the argument types
                    , DKind )  -- the kind of the result type
    singType :: OSet Name
    -> DType -> DType -> SgM (DType, Int, [Name], DCxt, DCxt, DType)
    singType bound_kvs :: OSet Name
    bound_kvs prom :: DType
    prom ty :: DType
    ty = do
      let (_, cxt :: DCxt
    cxt, args :: DCxt
    args, res :: DType
    res) = DType -> ([DTyVarBndr], DCxt, DCxt, DType)
    unravel DType
    ty
          num_args :: Int
    num_args            = DCxt -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length DCxt
    args
      DCxt
    cxt' <- (DType -> SgM DType) -> DCxt -> SgM DCxt
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    singPred DCxt
    cxt
      [Name]
    arg_names <- Int -> SgM Name -> SgM [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    num_args (String -> SgM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "t")
      DCxt
    prom_args <- (DType -> SgM DType) -> DCxt -> SgM DCxt
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DCxt
    args
      DType
    prom_res  <- DType -> SgM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    res
      let args' :: DCxt
    args' = (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map (\n :: Name
    n -> DType
    singFamily DType -> DType -> DType
    `DAppT` (Name -> DType
    DVarT Name
    n)) [Name]
    arg_names
          res' :: DType
    res'  = DType
    singFamily DType -> DType -> DType
    `DAppT` ((DType -> DType -> DType) -> DType -> DCxt -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    apply DType
    prom ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    arg_names) DType -> DType -> DType
    `DSigT` DType
    prom_res)
          tau :: DType
    tau   = DCxt -> DType -> DType
    ravel DCxt
    args' DType
    res'
          -- Make sure to subtract out the bound variables currently in scope, lest we
          -- accidentally shadow them in this type signature.
          kv_names_to_bind :: OSet Name
    kv_names_to_bind = (DType -> OSet Name) -> DCxt -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap DType -> OSet Name
    fvDType (DCxt
    prom_args DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ DCxt
    cxt' DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ [DType
    prom_res])
                                OSet Name -> OSet Name -> OSet Name
    forall a. Ord a => OSet a -> OSet a -> OSet a
    OSet.\\ OSet Name
    bound_kvs
          kvs_to_bind :: [Name]
    kvs_to_bind      = OSet Name -> [Name]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList OSet Name
    kv_names_to_bind
      let ty' :: DType
    ty' = [DTyVarBndr] -> DCxt -> DType -> DType
    DForallT ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    kvs_to_bind [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DType -> DTyVarBndr
    DKindedTV [Name]
    arg_names DCxt
    prom_args)
                         DCxt
    cxt' DType
    tau
      (DType, Int, [Name], DCxt, DCxt, DType)
    -> SgM (DType, Int, [Name], DCxt, DCxt, DType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType
    ty', Int
    num_args, [Name]
    arg_names, DCxt
    cxt, DCxt
    prom_args, DType
    prom_res)

    singPred :: DPred -> SgM DPred
    singPred :: DType -> SgM DType
    singPred = [DTypeArg] -> DType -> SgM DType
    singPredRec []

    singPredRec :: [DTypeArg] -> DPred -> SgM DPred
    singPredRec :: [DTypeArg] -> DType -> SgM DType
    singPredRec _cxt :: [DTypeArg]
    _cxt (DForallT {}) =
      String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of quantified constraints not yet supported"
    singPredRec ctx :: [DTypeArg]
    ctx (DAppT pr :: DType
    pr ty :: DType
    ty) = [DTypeArg] -> DType -> SgM DType
    singPredRec (DType -> DTypeArg
    DTANormal DType
    ty DTypeArg -> [DTypeArg] -> [DTypeArg]
    forall a. a -> [a] -> [a]
    : [DTypeArg]
    ctx) DType
    pr
    singPredRec ctx :: [DTypeArg]
    ctx (DAppKindT pr :: DType
    pr ki :: DType
    ki) = [DTypeArg] -> DType -> SgM DType
    singPredRec (DType -> DTypeArg
    DTyArg DType
    ki DTypeArg -> [DTypeArg] -> [DTypeArg]
    forall a. a -> [a] -> [a]
    : [DTypeArg]
    ctx) DType
    pr
    singPredRec _ctx :: [DTypeArg]
    _ctx (DSigT _pr :: DType
    _pr _ki :: DType
    _ki) =
      String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of constraints with explicit kinds not yet supported"
    singPredRec _ctx :: [DTypeArg]
    _ctx (DVarT _n :: Name
    _n) =
      String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of contraint variables not yet supported"
    singPredRec ctx :: [DTypeArg]
    ctx (DConT n :: Name
    n)
      | Name
    n Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    equalityName
      = String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of type equality constraints not yet supported"
      | Bool
    otherwise = do
        [DTypeArg]
    kis <- (DTypeArg -> SgM DTypeArg) -> [DTypeArg] -> SgM [DTypeArg]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DTypeArg -> SgM DTypeArg
    forall (m :: * -> *). MonadFail m => DTypeArg -> m DTypeArg
    promoteTypeArg [DTypeArg]
    ctx
        let sName :: Name
    sName = Name -> Name
    singClassName Name
    n
        DType -> SgM DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> SgM DType) -> DType -> SgM DType
    forall a b. (a -> b) -> a -> b
    $ DType -> [DTypeArg] -> DType
    applyDType (Name -> DType
    DConT Name
    sName) [DTypeArg]
    kis
    singPredRec _ctx :: [DTypeArg]
    _ctx DWildCardT = DType -> SgM DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return DType
    DWildCardT  -- it just might work
    singPredRec _ctx :: [DTypeArg]
    _ctx DArrowT =
      String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "(->) spotted at head of a constraint"
    singPredRec _ctx :: [DTypeArg]
    _ctx (DLitT {}) =
      String -> SgM DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Type-level literal spotted at head of a constraint"