    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE DeriveDataTypeable #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RankNTypes #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE TypeOperators #-}

    -- |
    -- Copyright   :  (C) 2015-2021 Edward Kmett
    -- License     :  BSD-style (see the file LICENSE)
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  experimental
    -- Portability :  non-portable
    --
    -- The idea for this trick comes from Dimitrios Vytiniotis.

    module Data.Constraint.Deferrable
      ( UnsatisfiedConstraint(..)
      , Deferrable(..)
      , defer
      , deferred
      , (:~~:)(HRefl)
      , (:~:)(Refl)
      ) where

    import Control.Exception
    import Control.Monad
    import Data.Constraint
    import Data.Proxy
    import Data.Typeable (Typeable, cast, typeRep)
    import Data.Type.Equality ((:~:)(Refl))

    import GHC.Types (type (~~))
    import Data.Type.Equality ((:~~:)(HRefl))

    newtype UnsatisfiedConstraint = UnsatisfiedConstraint String
      deriving (Typeable, Int -> UnsatisfiedConstraint -> ShowS
    [UnsatisfiedConstraint] -> ShowS
    UnsatisfiedConstraint -> String
    (Int -> UnsatisfiedConstraint -> ShowS)
    -> (UnsatisfiedConstraint -> String)
    -> ([UnsatisfiedConstraint] -> ShowS)
    -> Show UnsatisfiedConstraint
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UnsatisfiedConstraint -> ShowS
    showsPrec :: Int -> UnsatisfiedConstraint -> ShowS
    $cshow :: UnsatisfiedConstraint -> String
    show :: UnsatisfiedConstraint -> String
    $cshowList :: [UnsatisfiedConstraint] -> ShowS
    showList :: [UnsatisfiedConstraint] -> ShowS
    Show)

    instance Exception UnsatisfiedConstraint

    -- | Allow an attempt at resolution of a constraint at a later time
    class Deferrable p where
      -- | Resolve a 'Deferrable' constraint with observable failure.
      deferEither :: (p => r) -> Either String r

    deferred :: forall p. Deferrable p :- p
    deferred :: forall (p :: Constraint). Deferrable p :- p
    deferred = (Deferrable p => Dict p) -> Deferrable p :- p
    forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
    Sub ((Deferrable p => Dict p) -> Deferrable p :- p)
    -> (Deferrable p => Dict p) -> Deferrable p :- p
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r. Deferrable p => (p => r) -> r
    defer @p Dict p
    p => Dict p
    forall (a :: Constraint). a => Dict a
    Dict

    defer :: forall p r. Deferrable p => (p => r) -> r
    defer :: forall (p :: Constraint) r. Deferrable p => (p => r) -> r
    defer p => r
    r = (String -> r) -> (r -> r) -> Either String r -> r
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (UnsatisfiedConstraint -> r
    forall a e. (HasCallStack, Exception e) => e -> a
    throw (UnsatisfiedConstraint -> r)
    -> (String -> UnsatisfiedConstraint) -> String -> r
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> UnsatisfiedConstraint
    UnsatisfiedConstraint) r -> r
    forall a. a -> a
    id (Either String r -> r) -> Either String r -> r
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @p r
    p => r
    r

    showTypeRep :: forall t. Typeable t => String
    showTypeRep :: forall {k} (t :: k). Typeable t => String
    showTypeRep = TypeRep -> String
    forall a. Show a => a -> String
    show (TypeRep -> String) -> TypeRep -> String
    forall a b. (a -> b) -> a -> b
    $ Proxy t -> TypeRep
    forall {k} (proxy :: k -> *) (a :: k).
    Typeable a =>
    proxy a -> TypeRep
    typeRep (forall (t :: k). Proxy t
    forall {k} (t :: k). Proxy t
    Proxy @t)

    instance Deferrable () where
      deferEither :: forall r. ((() :: Constraint) => r) -> Either String r
    deferEither (() :: Constraint) => r
    r = r -> Either String r
    forall a b. b -> Either a b
    Right r
    (() :: Constraint) => r
    r

    -- | Deferrable homogeneous equality constraints.
    --
    -- Note that due to a GHC bug (https://ghc.haskell.org/trac/ghc/ticket/10343),
    -- using this instance on GHC 7.10 will only work with @*@-kinded types.
    instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where
      deferEither :: forall r. ((a ~ b) => r) -> Either String r
    deferEither (a ~ b) => r
    r = case (a :~: a) -> Maybe (a :~: b)
    forall a b. (Typeable a, Typeable b) => a -> Maybe b
    cast (a :~: a
    forall {k} (a :: k). a :~: a
    Refl :: a :~: a) :: Maybe (a :~: b) of
        Just a :~: b
    Refl -> r -> Either String r
    forall a b. b -> Either a b
    Right r
    (a ~ b) => r
    r
        Maybe (a :~: b)
    Nothing   -> String -> Either String r
    forall a b. a -> Either a b
    Left (String -> Either String r) -> String -> Either String r
    forall a b. (a -> b) -> a -> b
    $
          String
    "deferred type equality: type mismatch between `" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ forall (t :: k). Typeable t => String
    forall {k} (t :: k). Typeable t => String
    showTypeRep @a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "’ and `"  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ forall (t :: k). Typeable t => String
    forall {k} (t :: k). Typeable t => String
    showTypeRep @b String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"

    -- | Deferrable heterogenous equality constraints.
    --
    -- Only available on GHC 8.0 or later.
    instance (Typeable i, Typeable j, Typeable (a :: i), Typeable (b :: j)) => Deferrable (a ~~ b) where
      deferEither :: forall r. ((a ~~ b) => r) -> Either String r
    deferEither (a ~~ b) => r
    r = case (a :~~: a) -> Maybe (a :~~: b)
    forall a b. (Typeable a, Typeable b) => a -> Maybe b
    cast (a :~~: a
    forall {k1} (a :: k1). a :~~: a
    HRefl :: a :~~: a) :: Maybe (a :~~: b) of
        Just a :~~: b
    HRefl -> r -> Either String r
    forall a b. b -> Either a b
    Right r
    (a ~~ b) => r
    r
        Maybe (a :~~: b)
    Nothing   -> String -> Either String r
    forall a b. a -> Either a b
    Left (String -> Either String r) -> String -> Either String r
    forall a b. (a -> b) -> a -> b
    $
          String
    "deferred type equality: type mismatch between `" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ forall (t :: i). Typeable t => String
    forall {k} (t :: k). Typeable t => String
    showTypeRep @a String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "’ and `"  String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ forall (t :: j). Typeable t => String
    forall {k} (t :: k). Typeable t => String
    showTypeRep @b String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "'"

    instance (Deferrable a, Deferrable b) => Deferrable (a, b) where
      deferEither :: forall r. ((a, b) => r) -> Either String r
    deferEither (a, b) => r
    r = Either String (Either String r) -> Either String r
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (Either String (Either String r) -> Either String r)
    -> Either String (Either String r) -> Either String r
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @a ((a => Either String r) -> Either String (Either String r))
    -> (a => Either String r) -> Either String (Either String r)
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @b r
    b => r
    (a, b) => r
    r

    instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where
      deferEither :: forall r. ((a, b, c) => r) -> Either String r
    deferEither (a, b, c) => r
    r = Either String (Either String r) -> Either String r
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (Either String (Either String r) -> Either String r)
    -> Either String (Either String r) -> Either String r
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @a ((a => Either String r) -> Either String (Either String r))
    -> (a => Either String r) -> Either String (Either String r)
    forall a b. (a -> b) -> a -> b
    $ Either String (Either String r) -> Either String r
    forall (m :: * -> *) a. Monad m => m (m a) -> m a
    join (Either String (Either String r) -> Either String r)
    -> Either String (Either String r) -> Either String r
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @b ((b => Either String r) -> Either String (Either String r))
    -> (b => Either String r) -> Either String (Either String r)
    forall a b. (a -> b) -> a -> b
    $ forall (p :: Constraint) r.
    Deferrable p =>
    (p => r) -> Either String r
    deferEither @c r
    c => r
    (a, b, c) => r
    r