    {-# LANGUAGE ScopedTypeVariables #-}

    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Data.Singletons.Deriving.Infer
    -- Copyright   :  (C) 2015 Richard Eisenberg
    -- License     :  BSD-style (see LICENSE)
    -- Maintainer  :  Ryan Scott
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- Infers constraints for a `deriving` class
    --
    ----------------------------------------------------------------------------

    module Data.Singletons.Deriving.Infer ( inferConstraints, inferConstraintsDef ) where

    import Language.Haskell.TH.Desugar
    import Language.Haskell.TH.Syntax
    import Data.Singletons.Deriving.Util
    import Data.Singletons.Util
    import Data.List

    -- @inferConstraints cls inst_ty cons@ infers the instance context for a
    -- derived type class instance of @cls@ for @inst_ty@, using the constructors
    -- @cons@. For instance, if @cls@ is 'Ord' and @inst_ty@ is @Either a b@, then
    -- that means we are attempting to derive the instance:
    --
    -- @
    -- instance ??? => Ord (Either a b)
    -- @
    --
    -- The role of 'inferConstraints' is to determine what @???@ should be in that
    -- derived instance. To accomplish this, the list of @cons@ (in this example,
    -- @cons@ would be @[Left a, Right b]@) is used as follows:
    --
    -- 1. For each @con@ in @cons@, find the types of each of its fields
    --    (call these @field_tys@), perhaps after renaming the type variables of
    --    @field_tys@.
    -- 2. For each @field_ty@ in @field_tys@, apply @cls@ to @field_ty@ to obtain
    --    a constraint.
    -- 3. The final instance context is the set of all such constraints obtained
    --    in step 2.
    --
    -- To complete the running example, this algorithm would produce the instance
    -- context @(Ord a, Ord b)@, since @Left a@ has one field of type @a@, and
    -- @Right b@ has one field of type @b@.
    --
    -- This algorithm is a crude approximation of what GHC actually does when
    -- deriving instances. It is crude in the sense that one can end up with
    -- redundant constraints. For instance, if the data type for which an 'Ord'
    -- instance is being derived is @data Foo = MkFoo Bool Foo@, then the
    -- inferred constraints would be @(Ord Bool, Ord Foo)@. Technically, neither
    -- constraint is necessary, but it is not simple in general to eliminate
    -- redundant constraints like these, so we do not attept to do so. (This is
    -- one reason why @singletons@ requires the use of the @UndecidableInstances@
    -- GHC extension.)
    --
    -- Observant readers will notice that the phrase \"perhaps afer renaming the
    -- type variables\" was casually dropped in step 1 of the above algorithm.
    -- For more information on what this means, refer to the documentation for
    -- infer_ct below.
    inferConstraints :: forall q. DsMonad q => DPred -> DType -> [DCon] -> q DCxt
    inferConstraints :: DPred -> DPred -> [DCon] -> q DCxt
    inferConstraints pr :: DPred
    pr inst_ty :: DPred
    inst_ty = (DCxt -> DCxt) -> q DCxt -> q DCxt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap DCxt -> DCxt
    forall a. Eq a => [a] -> [a]
    nub (q DCxt -> q DCxt) -> ([DCon] -> q DCxt) -> [DCon] -> q DCxt
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (DCon -> q DCxt) -> [DCon] -> q DCxt
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DCon -> q DCxt
    infer_ct
      where
        -- A thorny situation arises when attempting to infer an instance context
        -- for a GADT. Consider the following example:
        --
        --   newtype Bar a where
        --     MkBar :: b -> Bar b
        --   deriving Show
        --
        -- If we blindly apply 'Show' to the field type of @MkBar@, we will end up
        -- with a derived instance of:
        --
        --   instance Show b => Show (Bar a)
        --
        -- This is completely wrong, since the type variable @b@ is never used in
        -- the instance head! This reveals that we need a slightly more nuanced
        -- strategy for gathering constraints for GADT constructors. To account
        -- for this, when gathering @field_tys@ (from step 1 in the above algorithm)
        -- we perform the following extra steps:
        --
        -- 1(a). Take the return type of @con@ and match it with @inst_ty@ (e.g.,
        --       match @Bar b@ with @Bar a@). Doing so will produce a substitution
        --       that maps the universally quantified type variables in the GADT
        --       (i.e., @b@) to the corresponding type variables in the data type
        --       constructor (i.e., @a@).
        -- 1(b). Use the resulting substitution to rename the universally
        --       quantified type variables of @con@ as necessary.
        --
        -- After this renaming, the algorithm will produce an instance context of
        -- @Show a@ (since @b@ was renamed to @a@), as expected.
        infer_ct :: DCon -> q DCxt
        infer_ct :: DCon -> q DCxt
    infer_ct (DCon _ _ _ fields :: DConFields
    fields res_ty :: DPred
    res_ty) = do
          let field_tys :: DCxt
    field_tys = DConFields -> DCxt
    tysOfConFields DConFields
    fields
              -- We need to match the constructor's result type with the type given
              -- in the generated instance. But if we have:
              --
              --   data Foo a where
              --     MkFoo :: a -> Foo a
              --     deriving Functor
              --
              -- Then the generated instance will be:
              --
              --   instance Functor Foo where ...
              --
              -- Which means that if we're not careful, we might try to match the
              -- types (Foo a) and (Foo), which will fail.
              --
              -- To avoid this, we employ a grimy hack where we pad the instance
              -- type with an extra (dummy) type variable. It doesn't matter what
              -- we name it, since none of the inferred constraints will mention
              -- it anyway.
              eta_expanded_inst_ty :: DPred
    eta_expanded_inst_ty
                | Bool
    is_functor_like = DPred
    inst_ty DPred -> DPred -> DPred
    `DAppT` Name -> DPred
    DVarT (String -> Name
    mkName "dummy")
                | Bool
    otherwise       = DPred
    inst_ty
          DPred
    res_ty'  <- DPred -> q DPred
    forall (q :: * -> *). DsMonad q => DPred -> q DPred
    expandType DPred
    res_ty
          DPred
    inst_ty' <- DPred -> q DPred
    forall (q :: * -> *). DsMonad q => DPred -> q DPred
    expandType DPred
    eta_expanded_inst_ty
          DCxt
    field_tys' <- case IgnoreKinds -> DPred -> DPred -> Maybe DSubst
    matchTy IgnoreKinds
    YesIgnore DPred
    res_ty' DPred
    inst_ty' of
                          Nothing -> String -> q DCxt
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> q DCxt) -> String -> q DCxt
    forall a b. (a -> b) -> a -> b
    $ String -> ShowS
    showString "Unable to match type "
                                          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> DPred -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec 11 DPred
    res_ty'
                                          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> ShowS
    showString " with "
                                          ShowS -> ShowS -> ShowS
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> DPred -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec 11 DPred
    inst_ty'
                                          ShowS -> ShowS
    forall a b. (a -> b) -> a -> b
    $ ""
                          Just subst :: DSubst
    subst -> (DPred -> q DPred) -> DCxt -> q DCxt
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (DSubst -> DPred -> q DPred
    forall (q :: * -> *). Quasi q => DSubst -> DPred -> q DPred
    substTy DSubst
    subst) DCxt
    field_tys
          if Bool
    is_functor_like
             then DCxt -> DPred -> q DCxt
    mk_functor_like_constraints DCxt
    field_tys' DPred
    res_ty'
             else DCxt -> q DCxt
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DCxt -> q DCxt) -> DCxt -> q DCxt
    forall a b. (a -> b) -> a -> b
    $ (DPred -> DPred) -> DCxt -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map (DPred
    pr DPred -> DPred -> DPred
    `DAppT`) DCxt
    field_tys'

        -- If we derive a Functor-like class, e.g.,
        --
        --   data Foo f g h a = MkFoo (f a) (g (h a)) deriving Functor
        --
        -- Then we infer constraints by sticking Functor on the subtypes of kind
        -- (Type -> Type). In the example above, that would give us
        -- (Functor f, Functor g, Functor h).
        mk_functor_like_constraints :: [DType] -> DType -> q DCxt
        mk_functor_like_constraints :: DCxt -> DPred -> q DCxt
    mk_functor_like_constraints fields :: DCxt
    fields res_ty :: DPred
    res_ty = do
          -- This function is partial. But that's OK, because
          -- functorLikeValidityChecks ensures that this is total by the time
          -- we invoke this.
          let (_, res_ty_args :: [DTypeArg]
    res_ty_args)     = DPred -> (DPred, [DTypeArg])
    unfoldDType DPred
    res_ty
              (_, last_res_ty_arg :: DPred
    last_res_ty_arg) = DCxt -> (DCxt, DPred)
    forall a. [a] -> ([a], a)
    snocView (DCxt -> (DCxt, DPred)) -> DCxt -> (DCxt, DPred)
    forall a b. (a -> b) -> a -> b
    $ [DTypeArg] -> DCxt
    filterDTANormals [DTypeArg]
    res_ty_args
              Just last_tv :: Name
    last_tv         = DPred -> Maybe Name
    getDVarTName_maybe DPred
    last_res_ty_arg
          DCxt
    deep_subtypes <- (DPred -> q DCxt) -> DCxt -> q DCxt
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM (Name -> DPred -> q DCxt
    forall (q :: * -> *). DsMonad q => Name -> DPred -> q DCxt
    deepSubtypesContaining Name
    last_tv) DCxt
    fields
          DCxt -> q DCxt
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DCxt -> q DCxt) -> DCxt -> q DCxt
    forall a b. (a -> b) -> a -> b
    $ (DPred -> DPred) -> DCxt -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map (DPred
    pr DPred -> DPred -> DPred
    `DAppT`) DCxt
    deep_subtypes

        is_functor_like :: Bool
        is_functor_like :: Bool
    is_functor_like
          | (DConT pr_class_name :: Name
    pr_class_name, _) <- DPred -> (DPred, [DTypeArg])
    unfoldDType DPred
    pr
          = Name -> Bool
    isFunctorLikeClassName Name
    pr_class_name
          | Bool
    otherwise
          = Bool
    False

    -- For @inferConstraintsDef mb_cxt@, if @mb_cxt@ is 'Just' a context, then it will
    -- simply return that context. Otherwise, if @mb_cxt@ is 'Nothing', then
    -- 'inferConstraintsDef' will infer an instance context (using 'inferConstraints').
    inferConstraintsDef :: DsMonad q => Maybe DCxt -> DPred -> DType -> [DCon] -> q DCxt
    inferConstraintsDef :: Maybe DCxt -> DPred -> DPred -> [DCon] -> q DCxt
    inferConstraintsDef mb_ctxt :: Maybe DCxt
    mb_ctxt pr :: DPred
    pr inst_ty :: DPred
    inst_ty cons :: [DCon]
    cons =
      q DCxt -> (DCxt -> q DCxt) -> Maybe DCxt -> q DCxt
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (DPred -> DPred -> [DCon] -> q DCxt
    forall (q :: * -> *).
    DsMonad q =>
    DPred -> DPred -> [DCon] -> q DCxt
    inferConstraints DPred
    pr DPred
    inst_ty [DCon]
    cons) DCxt -> q DCxt
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe DCxt
    mb_ctxt