{-# LANGUAGE CPP #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PolyKinds #-}
#if __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE UndecidableSuperClasses #-}
#endif
module Data.Constraint.Forall
( Forall, inst
, ForallF, instF
, Forall1, inst1
, ForallT, instT
, ForallV, InstV (instV)
, forall
) where
import Data.Constraint
import Unsafe.Coerce (unsafeCoerce)
#if __GLASGOW_HASKELL__ >= 806
# define KVS(kvs) kvs
#else
# define KVS(kvs)
#endif
type family Skolem (p :: k -> Constraint) :: k
type family Forall (p :: k -> Constraint) :: Constraint
type instance Forall p = Forall_ p
class p (Skolem p) => Forall_ (p :: k -> Constraint)
instance p (Skolem p) => Forall_ (p :: k -> Constraint)
inst :: forall p a. Forall p :- p a
inst :: Forall p :- p a
inst = (Forall_ p :- p (Skolem p)) -> Forall_ p :- p a
forall a b. a -> b
unsafeCoerce ((Forall_ p => Dict (p (Skolem p))) -> Forall_ p :- p (Skolem p)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub Forall_ p => Dict (p (Skolem p))
forall (a :: Constraint). a => Dict a
Dict :: Forall p :- p (Skolem p))
class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)
instance p (f a) => ComposeC p f a
class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
instance Forall (ComposeC p f) => ForallF p f
instF :: forall p f a . ForallF p f :- p (f a)
instF :: ForallF p f :- p (f a)
instF = (ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a))
-> (ForallF p f => Dict (p (f a))) -> ForallF p f :- p (f a)
forall a b. (a -> b) -> a -> b
$
case Forall (ComposeC p f) :- ComposeC p f a
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst :: Forall (ComposeC p f) :- ComposeC p f a of
Sub Forall (ComposeC p f) => Dict (ComposeC p f a)
Dict -> Dict (p (f a))
forall (a :: Constraint). a => Dict a
Dict
class p (t a b) => R (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1) (b :: k2)
instance p (t a b) => R p t a b
class Forall (R p t a) => Q (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1)
instance Forall (R p t a) => Q p t a
class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)
instance Forall (Q p t) => ForallT p t
instT :: forall KVS(k1 k2 k3 k4) (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
instT :: ForallT p t :- p (t f a)
instT = (ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a))
-> (ForallT p t => Dict (p (t f a))) -> ForallT p t :- p (t f a)
forall a b. (a -> b) -> a -> b
$
case Forall (Q p t) :- Q p t f
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst :: Forall (Q p t) :- Q p t f of { Sub Forall (Q p t) => Dict (Q p t f)
Dict ->
case Forall (R p t f) :- R p t f a
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst :: Forall (R p t f) :- R p t f a of
Sub Forall (R p t f) => Dict (R p t f a)
Dict -> Dict (p (t f a))
forall (a :: Constraint). a => Dict a
Dict }
type Forall1 p = Forall p
inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f
inst1 :: Forall p :- p f
inst1 = Forall p :- p f
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst
type family ForallV :: k -> Constraint
type instance ForallV = ForallV_
class ForallV' p => ForallV_ (p :: k)
instance ForallV' p => ForallV_ p
class InstV (p :: k) c | k c -> p where
type ForallV' (p :: k) :: Constraint
instV :: ForallV p :- c
instance p ~ c => InstV (p :: Constraint) c where
type ForallV' (p :: Constraint) = p
instV :: ForallV p :- c
instV = (ForallV_ c => Dict c) -> ForallV_ c :- c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ForallV_ c => Dict c
forall (a :: Constraint). a => Dict a
Dict
instance p a ~ c => InstV (p :: k -> Constraint) c where
type ForallV' (p :: k -> Constraint) = Forall p
instV :: ForallV p :- c
instV = (ForallV_ p => Dict c) -> ForallV_ p :- c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ForallV_ p => Dict c) -> ForallV_ p :- c)
-> (ForallV_ p => Dict c) -> ForallV_ p :- c
forall a b. (a -> b) -> a -> b
$ case Forall p :- c
forall k (p :: k -> Constraint) (a :: k). Forall p :- p a
inst :: Forall p :- c of
Sub Forall p => Dict c
Dict -> Dict c
forall (a :: Constraint). a => Dict a
Dict
instance InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c where
type ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p
instV :: ForallV p :- c
instV = (ForallV_ p => Dict c) -> ForallV_ p :- c
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((ForallV_ p => Dict c) -> ForallV_ p :- c)
-> (ForallV_ p => Dict c) -> ForallV_ p :- c
forall a b. (a -> b) -> a -> b
$ case ForallF ForallV p :- ForallV (p a)
forall k2 k1 (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1).
ForallF p f :- p (f a)
instF :: ForallF ForallV p :- ForallV (p a) of
Sub ForallF ForallV p => Dict (ForallV (p a))
Dict -> case ForallV (p a) :- c
forall k (p :: k) (c :: Constraint). InstV p c => ForallV p :- c
instV :: ForallV (p a) :- c of
Sub ForallV (p a) => Dict c
Dict -> Dict c
forall (a :: Constraint). a => Dict a
Dict
forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)
forall :: (forall (a :: k). Dict (p a)) -> Dict (Forall p)
forall forall (a :: k). Dict (p a)
d = case Dict (p (Skolem p))
forall (a :: k). Dict (p a)
d :: Dict (p (Skolem p)) of Dict (p (Skolem p))
Dict -> Dict (Forall p)
forall (a :: Constraint). a => Dict a
Dict