{-# LANGUAGE AllowAmbiguousTypes, DataKinds, GADTs, QuantifiedConstraints, CPP #-}

{-|
Description : Find a class instance at runtime
Copyright   : Richard Eisenberg
License     : MIT
Maintainer  : rae@richarde.dev
Stability   : experimental

The key innovation in this library is the 'Instances' type, which is a database
of instances that can be queried at runtime. More specifically, an @'Instances' tt c@
is a mapping from elements of type @tt@ to instances of class @c@.

It is expected
that @tt@ be an instance of the 'TypeText' class, which controls how types are rendered
into text. A good initial choice for @tt@ is 'Unqualified', which will render all types
as unqualified names. This is simple, but potentially ambiguous, if you have multiple
types with the same name (declared in different modules). See "Type.Reflection.Name"
for other alternatives.

An important restriction is that 'Instances' can hold only /ground/ instances: instances
with no type variables or type families. Maybe we can accommodate non-ground instances
in the future, but not today. (There seems to be no fundamental reason we cannot support
non-ground instances, but doing so would be a good deal harder than ground instances.)
The instance declarations may have variables, even though
the 'Instances' database will hold those instances' instantiations. For example, while
we have @instance Eq a => Eq (Maybe a)@, that polymorphic instance cannot be stored in
'Instances'. Instead, you can build an @'Instances' 'Unqualified' 'Eq'@
with, say, @Eq (Maybe Int)@, @Eq (Maybe Bool)@, and @Eq (Maybe Double)@. Looking up
@Maybe Int@, @Maybe Bool@, and @Maybe Double@ will all succeed, but looking up @Maybe Char@
would fail.

To create an `Instances`, use the @instancesFor...@ functions. The @Invisible@ variants
accept a type argument specifying the (ground) types which should be used to populate the
`Instances` database. The @TypeRep@ variant expects a 'TypeRep'. In the future, we expect
to offer a @instancesFor@ function which will use [visible dependent quantification](https://github.com/ghc-proposals/ghc-proposals/pull/281) to accept the list of types. Note that 'Instances'
is a 'Monoid', so you can combine the results of several calls.

In order to build an 'Instances' containing all instances in scope, see "Instance.Runtime.TH".

To use an 'Instances', use the 'withInstanceProxy' function. This function looks up an instance
in the database and, if successful, passes that instance to a callback function. In the future,
once we have the ability to [bind type variables in a lambda](https://github.com/ghc-proposals/ghc-proposals/pull/448), we expect 'withInstance' to be a better interface.
-}

module Instance.Runtime (
  Instances,

  -- ** Creation

  instanceForTypeRep, instanceForInvisible,
  instancesForInvisible,

  -- ** Usage

  withInstance, withInstanceProxy, withInstanceTypeRep,

  -- ** Folding

  foldInstances,
  ) where

import qualified Data.Map.Lazy as M
import Data.SOP.NP
import Data.SOP.Constraint ( All )

import Type.Reflection.List
import Type.Reflection.Name

import Data.Proxy
import Data.Kind
import Type.Reflection
import Data.Functor

#if __GLASGOW_HASKELL__ < 904
import Unsafe.Coerce
#endif

-- | A database of instances available for runtime queries. An @Instances tn c@ contains
-- instances of the class @c@, indexed by type names rendered according to the rules for @tn@.
type Instances :: forall k. Type -> (k -> Constraint) -> Type
newtype Instances type_namer c = MkInstances (M.Map type_namer (EDict c))
  deriving (NonEmpty (Instances type_namer c) -> Instances type_namer c
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall b.
Integral b =>
b -> Instances type_namer c -> Instances type_namer c
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
NonEmpty (Instances type_namer c) -> Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall type_namer k (c :: k -> Constraint) b.
(Ord type_namer, Integral b) =>
b -> Instances type_namer c -> Instances type_namer c
stimes :: forall b.
Integral b =>
b -> Instances type_namer c -> Instances type_namer c
$cstimes :: forall type_namer k (c :: k -> Constraint) b.
(Ord type_namer, Integral b) =>
b -> Instances type_namer c -> Instances type_namer c
sconcat :: NonEmpty (Instances type_namer c) -> Instances type_namer c
$csconcat :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
NonEmpty (Instances type_namer c) -> Instances type_namer c
<> :: Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
$c<> :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
Semigroup, Instances type_namer c
[Instances type_namer c] -> Instances type_namer c
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Semigroup (Instances type_namer c)
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
[Instances type_namer c] -> Instances type_namer c
forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
mconcat :: [Instances type_namer c] -> Instances type_namer c
$cmconcat :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
[Instances type_namer c] -> Instances type_namer c
mappend :: Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
$cmappend :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
-> Instances type_namer c -> Instances type_namer c
mempty :: Instances type_namer c
$cmempty :: forall type_namer k (c :: k -> Constraint).
Ord type_namer =>
Instances type_namer c
Monoid)

-- | for debugging only
instance (Show type_namer, Typeable c) => Show (Instances type_namer c) where
  show :: Instances type_namer c -> String
show (MkInstances Map type_namer (EDict c)
m) = String
"(Instances for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @c) forall a. [a] -> [a] -> [a]
++ String
" for types " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> [k]
M.keys Map type_namer (EDict c)
m) forall a. [a] -> [a] -> [a]
++ String
")"

type EDict :: forall k. (k -> Constraint) -> Type
data EDict c where
  PackDict :: forall x c. c x => EDict c

-- | Create an 'Instances' for a type denoted by the given 'TypeRep'.
instanceForTypeRep ::
  forall {k} (x :: k) (c :: k -> Constraint) tn.
  c x =>
  TypeText tn =>
  TypeRep x ->
  Instances tn c
instanceForTypeRep :: forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep TypeRep x
tr = forall k type_namer (c :: k -> Constraint).
Map type_namer (EDict c) -> Instances type_namer c
MkInstances (forall k a. k -> a -> Map k a
M.singleton (forall tt {k} (t :: k). TypeText tt => TypeRep t -> tt
renderTypeRep TypeRep x
tr) (forall {k} (x :: k) (c :: k -> Constraint). c x => EDict c
PackDict @x))

-- | Create an 'Instances' for a type passed invisibly. Example: @instanceForInvisible @Int@.
instanceForInvisible ::
  forall {k} (x :: k) (c :: k -> Constraint) tn.
  Typeable x =>
  c x =>
  TypeText tn =>
  Instances tn c
instanceForInvisible :: forall {k} (x :: k) (c :: k -> Constraint) tn.
(Typeable x, c x, TypeText tn) =>
Instances tn c
instanceForInvisible = forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @x)

-- | Create an 'Instances' for a list of types passed invisibly.
-- Example: @instancesForInvisible @[Int, Bool, Double]@.
instancesForInvisible ::
  forall {k} (xs :: [k]) (c :: k -> Constraint) tn.
  Typeable xs =>
  All c xs =>
  TypeText tn =>
  Instances tn c
instancesForInvisible :: forall {k} (xs :: [k]) (c :: k -> Constraint) tn.
(Typeable xs, All c xs, TypeText tn) =>
Instances tn c
instancesForInvisible = forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go NP TypeRep xs
all_trs
  where
    tr_xs :: TypeRep xs
tr_xs   = forall {k} (a :: k). Typeable a => TypeRep a
typeRep @xs
    all_trs :: NP TypeRep xs
all_trs = forall {k} (xs :: [k]). TypeRep xs -> NP TypeRep xs
typeRepList TypeRep xs
tr_xs

    go :: forall (inner_xs :: [k]). All c inner_xs => NP TypeRep inner_xs -> Instances tn c
    go :: forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go (TypeRep x
tr :* NP TypeRep xs
trs) = forall {k} (x :: k) (c :: k -> Constraint) tn.
(c x, TypeText tn) =>
TypeRep x -> Instances tn c
instanceForTypeRep TypeRep x
tr forall a. Semigroup a => a -> a -> a
<> forall (inner_xs :: [k]).
All c inner_xs =>
NP TypeRep inner_xs -> Instances tn c
go NP TypeRep xs
trs
    go NP TypeRep inner_xs
Nil         = forall a. Monoid a => a
mempty

-- | Look up an instance in 'Instances', making the instance available for use in the continuation
-- function. If the lookup fails, this returns Nothing. Until https://github.com/ghc-proposals/ghc-proposals/pull/448
-- is implemented, there is no way to bind a type variable to the found type, so this function is likely
-- impossible to use well. For now, see 'withInstanceProxy' instead.
withInstance :: Ord tn => Instances tn c -> tn -> (forall x. c x => r) -> Maybe r
withInstance :: forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c -> tn -> (forall (x :: k). c x => r) -> Maybe r
withInstance Instances tn c
inst_db tn
type_name forall (x :: k). c x => r
f = forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy Instances tn c
inst_db tn
type_name (\ (Proxy x
_ :: Proxy x) -> forall (x :: k). c x => r
f @x)

-- | Look up an instance in 'Instances', making the instance available for use in the continuation
-- function. If the lookup fails, this returns Nothing. If https://github.com/ghc-proposals/ghc-proposals/pull/448
-- has been implemented in your GHC, you may prefer 'withInstance'.
withInstanceProxy :: Ord tn => Instances tn c -> tn -> (forall x. c x => Proxy x -> r) -> Maybe r
withInstanceProxy :: forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy (MkInstances Map tn (EDict c)
mapping) tn
type_name forall (x :: k). c x => Proxy x -> r
f =
  forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup tn
type_name Map tn (EDict c)
mapping forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ (PackDict @_ @x) -> forall (x :: k). c x => Proxy x -> r
f (forall {k} (t :: k). Proxy t
Proxy @x)
    -- The @_ in PackDict above is a GHC bug (GitLab is wonky at the moment, so I can't search for
    -- ticket #, but I'm pretty sure I remember this one and that it's fixed in HEAD)

-- | Look up an instance in 'Instances', when you already have a 'TypeRep' for the type to look up.
-- To use this function, the class @c@ used in your @Instances@ must imply 'Typeable'; the 'Typeable'
-- instance is used to check that the retrieved type is actually the one you want. If it's not,
-- this function throws an exception (this really shouldn't happen).
-- (In GHCs before 9.4, this check is skipped, because of a bug around 'Typeable' and quantified
-- constraints.)
-- If the lookup fails, this returns Nothing.
withInstanceTypeRep ::
  forall t c tn r.
  TypeText tn =>
#if __GLASGOW_HASKELL__ >= 904
  (forall x. c x => Typeable x) =>
#endif
  Instances tn c -> TypeRep t -> (c t => r) -> Maybe r
withInstanceTypeRep :: forall {k} (t :: k) (c :: k -> Constraint) tn r.
TypeText tn =>
Instances tn c -> TypeRep t -> (c t => r) -> Maybe r
withInstanceTypeRep Instances tn c
instances TypeRep t
type_rep c t => r
action =
  forall {k} tn (c :: k -> Constraint) r.
Ord tn =>
Instances tn c
-> tn -> (forall (x :: k). c x => Proxy x -> r) -> Maybe r
withInstanceProxy Instances tn c
instances (forall tt {k} (t :: k). TypeText tt => TypeRep t -> tt
renderTypeRep TypeRep t
type_rep) forall a b. (a -> b) -> a -> b
$ \ (Proxy x
_ :: Proxy t') ->
    let
        type_rep' :: TypeRep t'
#if __GLASGOW_HASKELL__ >= 904
        type_rep' = typeRep
#else
        type_rep' :: TypeRep x
type_rep' = forall a b. a -> b
unsafeCoerce TypeRep t
type_rep
#endif
    in
    case TypeRep t
type_rep forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
`eqTypeRep` TypeRep x
type_rep' of
      Just t :~~: x
HRefl -> c t => r
action
      Maybe (t :~~: x)
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Retrieved type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep x
type_rep' forall a. [a] -> [a] -> [a]
++
                         String
" different from expected type " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TypeRep t
type_rep forall a. [a] -> [a] -> [a]
++ String
"."

-- | Perform a computation for each instance in the database, accumulating results
-- in a monoid. Your monoid should be commutative, because there is no predictable
-- order of instances in the 'Instances'.
foldInstances ::
  Monoid m =>
  Instances tn c ->
  (forall x. c x => Proxy x -> m) ->
  m
foldInstances :: forall {k} m tn (c :: k -> Constraint).
Monoid m =>
Instances tn c -> (forall (x :: k). c x => Proxy x -> m) -> m
foldInstances (MkInstances Map tn (EDict c)
mapping) forall (x :: k). c x => Proxy x -> m
action =
  forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\ (PackDict @_ @x) -> forall (x :: k). c x => Proxy x -> m
action @x forall {k} (t :: k). Proxy t
Proxy) Map tn (EDict c)
mapping