    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Single.Defun
    -- Copyright   :  (C) 2018 Ryan Scott
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Creates 'SingI' instances for promoted types' defunctionalization symbols.
    --
    -----------------------------------------------------------------------------

    module Data.Singletons.Single.Defun (singDefuns) where

    import Data.List
    import Data.Singletons.Names
    import Data.Singletons.Promote.Defun
    import Data.Singletons.Single.Monad
    import Data.Singletons.Single.Type
    import Data.Singletons.Util
    import Language.Haskell.TH.Desugar
    import Language.Haskell.TH.Syntax

    -- Given the Name of something, take the defunctionalization symbols for its
    -- promoted counterpart and create SingI instances for them. As a concrete
    -- example, if you have:
    --
    --   foo :: Eq a => a -> a -> Bool
    --
    -- Then foo's promoted counterpart, Foo, will have two defunctionalization
    -- symbols:
    --
    --   FooSym0 :: a ~> a ~> Bool
    --   FooSym1 :: a -> a ~> Bool
    --
    -- We can declare SingI instances for these two symbols like so:
    --
    --   instance SEq a => SingI (FooSym0 :: a ~> a ~> Bool) where
    --     sing = singFun2 sFoo
    --
    --   instance (SEq a, SingI x) => SingI (FooSym1 x :: a ~> Bool) where
    --     sing = singFun1 (sFoo (sing @_ @x))
    --
    -- Note that singDefuns takes Maybe DKinds for the promoted argument and result
    -- types, in case we have an entity whose type needs to be inferred.
    -- See Note [singDefuns and type inference].
    --
    -- Note that in the particular case of a data constructor, we actually generate
    -- /two/ SingI instances partial application—one for the defunctionalization
    -- symbol, and one for the data constructor placed inside TyCon{N}.
    -- See Note [SingI instances for partially applied constructors].
    singDefuns :: Name      -- The Name of the thing to promote.
               -> NameSpace -- Whether the above Name is a value, data constructor,
                            -- or a type constructor.
                            -- See Note [SingI instances for partially applied constructors]
               -> DCxt      -- The type's context.
               -> [Maybe DKind] -- The promoted argument types (if known).
               -> Maybe DKind   -- The promoted result type (if known).
               -> SgM [DDec]
    singDefuns n ns ty_ctxt mb_ty_args mb_ty_res =
      case mb_ty_args of
        [] -> pure [] -- If a function has no arguments, then it has no
                      -- defunctionalization symbols, so there's nothing to be done.
        _  -> do sty_ctxt <- mapM singPred ty_ctxt
                 go 0 sty_ctxt [] mb_ty_args
      where
        num_ty_args :: Int
        num_ty_args = length mb_ty_args

        -- Sadly, this algorithm is quadratic, because in each iteration of the loop
        -- we must:
        --
        -- * Construct an arrow type of the form (a ~> ... ~> z), using a suffix of
        --   the promoted argument types.
        -- * Append a new type variable to the end of an ordered list.
        --
        -- In practice, this is unlikely to be a bottleneck, as singletons does not
        -- support functions with more than 7 or so arguments anyways.
        go :: Int -> DCxt -> [DTyVarBndr] -> [Maybe DKind] -> SgM [DDec]
        go sym_num sty_ctxt tvbs mb_tyss
          | sym_num < num_ty_args
          , mb_ty:mb_tys <- mb_tyss
          = do new_tvb_name <- qNewName "d"
               let new_tvb = inferMaybeKindTV new_tvb_name mb_ty
               insts <- go (sym_num + 1) sty_ctxt (tvbs ++ [new_tvb]) mb_tys
               pure $ new_insts ++ insts
          | otherwise
          = pure []
          where
            sing_fun_num :: Int
            sing_fun_num = num_ty_args - sym_num

            mk_sing_fun_expr :: DExp -> DExp
            mk_sing_fun_expr sing_expr =
              foldl' (\f tvb_n -> f `DAppE` (DVarE singMethName `DAppTypeE` DVarT tvb_n))
                     sing_expr
                     (map extractTvbName tvbs)

            singI_ctxt :: DCxt
            singI_ctxt = map (DAppPr (DConPr singIName) . tvbToType) tvbs

            mk_inst_ty :: DType -> DType
            mk_inst_ty inst_head
              = case mb_inst_kind of
                  Just inst_kind -> inst_head `DSigT` inst_kind
                  Nothing        -> inst_head

            tvb_tys :: [DType]
            tvb_tys = map dTyVarBndrToDType tvbs

            -- Construct the arrow kind used to annotate the defunctionalization
            -- symbol (e.g., the `a ~> a ~> Bool` in
            -- `SingI (FooSym0 :: a ~> a ~> Bool)`).
            -- If any of the argument kinds or result kind isn't known (i.e., is
            -- Nothing), then we opt not to construct this arrow kind altogether.
            -- See Note [singDefuns and type inference]
            mb_inst_kind :: Maybe DType
            mb_inst_kind = foldr buildTyFunArrow_maybe mb_ty_res mb_tyss

            new_insts :: [DDec]
            new_insts
              | DataName <- ns
              = -- See Note [SingI instances for partially applied constructors]
                let s_data_con = DConE $ singDataConName n in
                [ mk_inst defun_inst_ty s_data_con
                , mk_inst tycon_inst_ty s_data_con ]
              | otherwise
              = [mk_inst defun_inst_ty $ DVarE $ singValName n]
              where
                mk_inst :: DType -> DExp -> DDec
                mk_inst inst_head sing_exp
                  = DInstanceD Nothing
                               (sty_ctxt ++ singI_ctxt)
                               (DConT singIName `DAppT` mk_inst_ty inst_head)
                               [DLetDec $ DValD (DVarPa singMethName)
                                        $ wrapSingFun sing_fun_num inst_head
                                        $ mk_sing_fun_expr sing_exp ]

                defun_inst_ty, tycon_inst_ty :: DType
                defun_inst_ty = foldType (DConT (promoteTySym n sym_num)) tvb_tys
                tycon_inst_ty = DConT (mkTyConName sing_fun_num) `DAppT`
                                foldType (DConT n) tvb_tys

    {-
    Note [singDefuns and type inference]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the following function:

      foo :: a -> Bool
      foo _ = True

    singDefuns would give the following SingI instance for FooSym0, with an
    explicit kind signature:

      instance SingI (FooSym0 :: a ~> Bool) where ...

    What happens if we leave off the type signature for foo?

      foo _ = True

    Can singDefuns still do its job? Yes! It will simply generate:

      instance SingI FooSym0 where ...

    In general, if any of the promoted argument or result types given to singDefun
    are Nothing, then we avoid crafting an explicit kind signature. You might worry
    that this could lead to SingI instances being generated that GHC cannot infer
    the type for, such as:

      bar x = x == x
      ==>
      instance SingI BarSym0 -- Missing an SEq constraint?

    This is true, but also not unprecedented, as the singled version of bar, sBar,
    will /also/ fail to typecheck due to a missing SEq constraint. Therefore, this
    design choice fits within the existing tradition of type inference in
    singletons.

    Note [SingI instances for partially applied constructors]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Unlike normal functions, where we generate one SingI instance for each of its
    partial applications (one per defunctionalization symbol), we generate *two*
    SingI instances for each partial application of a data constructor. That is,
    if we have:

      data D a where
        K :: a -> D a

    K has an partial application, so we will generate the following two SingI
    instances:

      instance SingI KSym0          where sing = singFun1 SK
      instance SingI (TyCon1 KSym0) where sing = singFun1 SK

    The first instance is exactly the same as what we'd generate for a normal,
    partially applied function's defun symbol. The second one, while functionally
    equivalent, is a bit dissatisfying: in general, adopting this approach means
    that we end up generating many instances of the form:

      instance SingI (TyCon1 S1)
      instance SingI (TyCon1 S2)
      ...

    Ideally, we'd have a single instance SingI (TyCon1 s) to rule them all. But
    doing so would require writing something akin to:

      instance (forall a. SingI a => SingI (f a)) => SingI (TyCon1 f) where
        sing = SLambda $ \(x :: Sing a) -> withSingI x $ sing @_ @(f a)

    But this would require quantified constraints. Until GHC gains these, we
    compensate by generating out several SingI (TyCon1 s) instances.
    -}