{-# LANGUAGE TemplateHaskellQuotes #-}

{-|
Description : Build a runtime-instance database of all instances in scope
Copyright   : Richard Eisenberg
License     : MIT
Maintainer  : rae@richarde.dev
Stability   : experimental

TODO: write description

-}

module Instance.Runtime.TH (
  allGroundInstances, allGroundInstanceTypes,

  -- * Utilities
  promotedList,
  ) where

import Instance.Runtime

import TH.Utilities
import Language.Haskell.TH
import Data.List ( uncons )

-- | Build an 'Instances' containing all in-scope ground instances for the given
-- class. A /ground instance/ is one that includes no type variables. Example
-- usage:
--
-- > instanceDatabase :: Instances Unqualified MyClass
-- > instanceDatabase = $(allGroundInstances [t| MyClass |])
--
-- It is an infelicity in the design of Template Haskell that requires repeating
-- the @MyClass@ part; it should be inferrable.
--
-- Note that this just looks at instance declarations to determine whether an
-- instance is ground. So it would not pick up, e.g. @Eq (Maybe Int)@, because
-- the instance declaration looks like @Eq (Maybe a)@.
--
-- Due to a limitation of Template Haskell, this will find only instances declared
-- in other modules or before a declaration splice in the current module.
-- If you want to find instances declared in the current module, you can add a line
--
-- > $(pure [])
--
-- above the use of 'allGroundInstances' in the file. This line forces GHC to finish
-- processing everything above the line before looking at anything below the line,
-- so those instances declared above the line are available below it.
allGroundInstances :: Q Type   -- ^ The class whose instances to include.
                               -- This type must have the kind @k -> Constraint@ for some @k@
                               -- and include no variables.
                   -> Q Exp
allGroundInstances :: Q Type -> Q Exp
allGroundInstances Q Type
q_constraint = do
  Type
constraint <- Q Type
q_constraint
  [Type]
ground_instance_types <- Type -> Q [Type]
allGroundInstanceTypes Type
constraint
  let ty_list :: Type
ty_list = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Type
h Type
t -> Type
PromotedConsT Type -> Type -> Type
`AppT` Type
h Type -> Type -> Type
`AppT` Type
t) Type
PromotedNilT [Type]
ground_instance_types
  forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Exp
VarE 'instancesForInvisible Exp -> Type -> Exp
`AppTypeE` Type
ty_list)

-- | Returns a list of ground (= no variables) types that satisfy the given constraint.
-- The passed-in 'Type' must have kind @k -> Constraint@ for some @k@; all the returned
-- types will then have kind @k@.
--
-- This finds only types that appear in ground instances. So if you look for @Eq@, you'll
-- get @Int@, and @Double@, but not @Maybe Int@, even though @Maybe Int@ is a ground type:
-- it comes from @instance ... => Eq (Maybe a)@, which is not a ground instance.
--
-- See also 'allGroundInstances', for more usage information.
allGroundInstanceTypes :: Type -> Q [Type]
allGroundInstanceTypes :: Type -> Q [Type]
allGroundInstanceTypes Type
constraint = do
  (Name
class_name, [Type]
ct_args) <- case Type -> Maybe (Name, [Type])
typeToNamedCon Type
constraint of
    Maybe (Name, [Type])
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail (forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr Type
constraint) forall a. [a] -> [a] -> [a]
++ String
" is not headed by a class.")
    Just (Name
nm, [Type]
args) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name
nm, [Type]
args)
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> Q ()
checkForVariables [Type]
ct_args

  [InstanceDec]
instances <- Name -> [Type] -> Q [InstanceDec]
reifyInstances Name
class_name ([Type]
ct_args forall a. [a] -> [a] -> [a]
++ [Name -> Type
VarT (String -> Name
mkName String
"a")])
  forall (m :: * -> *) a. Monad m => a -> m a
return [ Type
ty
         | InstanceD Maybe Overlap
_ [Type]
_ Type
instance_ty [InstanceDec]
_ <- [InstanceDec]
instances
         , Just (Name
_, [Type]
args) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe (Name, [Type])
typeToNamedCon Type
instance_ty)
         , Just (Type
ty, [Type]
_) <- forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> Maybe (a, [a])
uncons (forall a. [a] -> [a]
reverse [Type]
args))
         , Type -> Bool
hasNoVariables Type
ty
         ]

-- | Issues an error if the type provided has any variables. Never fails.
checkForVariables :: Type -> Q ()
checkForVariables :: Type -> Q ()
checkForVariables Type
ty
  | Type -> Bool
hasNoVariables Type
ty = forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise         = String -> Q ()
reportError (String
"`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Ppr a => a -> Doc
ppr Type
ty) forall a. [a] -> [a] -> [a]
++ String
"' has variables; this is not allowed.")

-- | Checks whether a 'Type' has no variables.
hasNoVariables :: Type -> Bool
hasNoVariables :: Type -> Bool
hasNoVariables (ForallT {}) = Bool
False
hasNoVariables (ForallVisT {}) = Bool
False
hasNoVariables (AppT Type
ty1 Type
ty2) = Type -> Bool
hasNoVariables Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
hasNoVariables Type
ty2
hasNoVariables (AppKindT Type
ty1 Type
ki2) = Type -> Bool
hasNoVariables Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
hasNoVariables Type
ki2
hasNoVariables (SigT Type
ty Type
ki) = Type -> Bool
hasNoVariables Type
ty Bool -> Bool -> Bool
&& Type -> Bool
hasNoVariables Type
ki
hasNoVariables (VarT {}) = Bool
False
hasNoVariables (ConT {}) = Bool
True
hasNoVariables (PromotedT {}) = Bool
True
hasNoVariables (InfixT Type
ty1 Name
_ Type
ty2) = Type -> Bool
hasNoVariables Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
hasNoVariables Type
ty2
hasNoVariables (UInfixT Type
ty1 Name
_ Type
ty2) = Type -> Bool
hasNoVariables Type
ty1 Bool -> Bool -> Bool
&& Type -> Bool
hasNoVariables Type
ty2
hasNoVariables (ParensT Type
ty) = Type -> Bool
hasNoVariables Type
ty
hasNoVariables (TupleT {}) = Bool
True
hasNoVariables (UnboxedTupleT {}) = Bool
True
hasNoVariables (UnboxedSumT {}) = Bool
True
hasNoVariables Type
ArrowT = Bool
True
hasNoVariables Type
MulArrowT = Bool
True
hasNoVariables Type
EqualityT = Bool
True
hasNoVariables Type
ListT = Bool
True
hasNoVariables (PromotedTupleT {}) = Bool
True
hasNoVariables Type
PromotedConsT = Bool
True
hasNoVariables Type
PromotedNilT = Bool
True
hasNoVariables Type
StarT = Bool
True
hasNoVariables Type
ConstraintT = Bool
True
hasNoVariables (LitT {}) = Bool
True
hasNoVariables Type
WildCardT = Bool
True
hasNoVariables (ImplicitParamT String
_ Type
ty) = Type -> Bool
hasNoVariables Type
ty

------------------------------------
-- Utilities

-- | Constructs a promoted list type from a list of types. Useful for
-- synthesizing calls to 'instancesForInvisible' using Template Haskell.
promotedList :: [Type] -> Type
promotedList :: [Type] -> Type
promotedList = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Type
h Type
t -> Type
PromotedConsT Type -> Type -> Type
`AppT` Type
h Type -> Type -> Type
`AppT` Type
t) Type
PromotedNilT