-----------------------------------------------------------------------------

-- |

-- Module      :  Data.Singletons.TH.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.TH.Deriving.Infer ( inferConstraints, inferConstraintsDef ) where

import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.TH.Deriving.Util
import Data.Singletons.TH.Util
import Data.List (nub)
import Data.Maybe (fromJust)

-- @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-th@ 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 :: forall (q :: * -> *).
DsMonad q =>
DPred -> DPred -> [DCon] -> q DCxt
inferConstraints DPred
pr DPred
inst_ty = (DCxt -> DCxt) -> q DCxt -> q DCxt
forall a b. (a -> b) -> q a -> q b
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 [DTyVarBndrSpec]
_ DCxt
_ Name
_ DConFields
fields 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 String
"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
                      Maybe DSubst
Nothing -> String -> q DCxt
forall a. String -> q a
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 String
"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 Int
11 DPred
res_ty'
                                      ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" 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 Int
11 DPred
inst_ty'
                                      ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
""
                      Just 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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 a. a -> q a
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 `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 DCxt
fields 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 (DPred
_, [DTypeArg]
res_ty_args)     = DPred -> (DPred, [DTypeArg])
unfoldDType DPred
res_ty
          (DCxt
_, 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
          last_tv :: Name
last_tv              = Maybe Name -> Name
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ 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 a. a -> q a
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 `DAppT`) DCxt
deep_subtypes

    is_functor_like :: Bool
    is_functor_like :: Bool
is_functor_like
      | (DConT Name
pr_class_name, [DTypeArg]
_) <- 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 :: forall (q :: * -> *).
DsMonad q =>
Maybe DCxt -> DPred -> DPred -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt DPred
pr DPred
inst_ty [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 a. a -> q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DCxt
mb_ctxt