{-# LANGUAGE CPP #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PolyKinds #-}

#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeInType #-}
#endif

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Constraint.Deferrable
-- Copyright   :  (C) 2015-2016 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
#if __GLASGOW_HASKELL__ >= 800
  , defer_
  , deferEither_
  , (:~~:)(HRefl)
#endif
  , (:~:)(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))

#if __GLASGOW_HASKELL__ >= 800
import GHC.Types (type (~~))
import Data.Type.Equality.Hetero ((:~~:)(HRefl))
#endif

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 :: proxy p -> (p => r) -> Either String r

-- | Defer a constraint for later resolution in a context where we want to upgrade failure into an error
defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r
defer :: forall (p :: Constraint) r (proxy :: Constraint -> *).
Deferrable p =>
proxy p -> (p => r) -> r
defer proxy p
_ 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. 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
$ Proxy p -> (p => r) -> Either String r
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy p -> (p => r) -> Either String r
deferEither (Proxy p
forall {k} (t :: k). Proxy t
Proxy :: Proxy p) r
p => r
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
$ Proxy p -> (p => Dict p) -> Dict p
forall (p :: Constraint) r (proxy :: Constraint -> *).
Deferrable p =>
proxy p -> (p => r) -> r
defer (Proxy p
forall {k} (t :: k). Proxy t
Proxy :: Proxy p) Dict p
p => Dict p
forall (a :: Constraint). a => Dict a
Dict

#if __GLASGOW_HASKELL__ >= 800
-- | A version of 'defer' that uses visible type application in place of a 'Proxy'.
--
-- Only available on GHC 8.0 or later.
defer_ :: forall p r. Deferrable p => (p => r) -> r
defer_ :: forall (p :: Constraint) r. Deferrable p => (p => r) -> r
defer_ p => r
r = forall (p :: Constraint) r (proxy :: Constraint -> *).
Deferrable p =>
proxy p -> (p => r) -> r
defer @p Proxy p
forall {k} (t :: k). Proxy t
Proxy r
p => r
r

-- | A version of 'deferEither' that uses visible type application in place of a 'Proxy'.
--
-- Only available on GHC 8.0 or later.
deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r
deferEither_ :: forall (p :: Constraint) r.
Deferrable p =>
(p => r) -> Either String r
deferEither_ p => r
r = forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
deferEither @p Proxy p
forall {k} (t :: k). Proxy t
Proxy r
p => r
r
#endif

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

instance Deferrable () where
  deferEither :: forall (proxy :: Constraint -> *) r.
proxy (() :: Constraint)
-> ((() :: Constraint) => r) -> Either String r
deferEither proxy (() :: Constraint)
_ (() :: 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.
#if __GLASGOW_HASKELL__ >= 800
instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where
#elif __GLASGOW_HASKELL__ == 710
instance (Typeable a, Typeable b) => Deferrable ((a :: *) ~ (b :: *)) where
#else
instance (Typeable a, Typeable b) => Deferrable (a ~ b) where
#endif
  deferEither :: forall (proxy :: Constraint -> *) r.
proxy (a ~ b) -> ((a ~ b) => r) -> Either String r
deferEither proxy (a ~ b)
_ (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]
++ Proxy a -> String
forall {k} (t :: k). Typeable t => Proxy t -> String
showTypeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"’ and `"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy b -> String
forall {k} (t :: k). Typeable t => Proxy t -> String
showTypeRep (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"

#if __GLASGOW_HASKELL__ >= 800
-- | 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 (proxy :: Constraint -> *) r.
proxy (a ~~ b) -> ((a ~~ b) => r) -> Either String r
deferEither proxy (a ~~ b)
_ (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]
++ Proxy a -> String
forall {k} (t :: k). Typeable t => Proxy t -> String
showTypeRep (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"’ and `"  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proxy b -> String
forall {k} (t :: k). Typeable t => Proxy t -> String
showTypeRep (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"
#endif

instance (Deferrable a, Deferrable b) => Deferrable (a, b) where
  deferEither :: forall (proxy :: Constraint -> *) r.
proxy (a, b) -> ((a, b) => r) -> Either String r
deferEither proxy (a, b)
_ (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
$ Proxy a
-> (a => Either String r) -> Either String (Either String r)
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy a -> (a => r) -> Either String r
deferEither (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy 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
$ Proxy b -> (b => r) -> Either String r
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy b -> (b => r) -> Either String r
deferEither (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy b) r
b => r
(a, b) => r
r

instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where
  deferEither :: forall (proxy :: Constraint -> *) r.
proxy (a, b, c) -> ((a, b, c) => r) -> Either String r
deferEither proxy (a, b, c)
_ (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
$ Proxy a
-> (a => Either String r) -> Either String (Either String r)
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy a -> (a => r) -> Either String r
deferEither (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy 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
$ Proxy b
-> (b => Either String r) -> Either String (Either String r)
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy b -> (b => r) -> Either String r
deferEither (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy 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
$ Proxy c -> (c => r) -> Either String r
forall (p :: Constraint) (proxy :: Constraint -> *) r.
Deferrable p =>
proxy p -> (p => r) -> Either String r
forall (proxy :: Constraint -> *) r.
proxy c -> (c => r) -> Either String r
deferEither (Proxy c
forall {k} (t :: k). Proxy t
Proxy :: Proxy c) r
c => r
(a, b, c) => r
r