constraints 0.4.1.3 → 0.6

raw patch · 10 files changed

+1322/−711 lines, 10 filesdep +binarydep +deepseqdep +hashabledep ~basedep ~ghc-primPVP ok

version bump matches the API change (PVP)

Dependencies added: binary, deepseq, hashable, mtl, tagged, transformers, transformers-compat

Dependency ranges changed: base, ghc-prim

API changes (from Hackage documentation)

Files

• Data/Constraint.hs +0/−578
• Data/Constraint/Forall.hs +0/−70
• Data/Constraint/Unsafe.hs +0/−55
• LICENSE +1/−1
• constraints.cabal +24/−7
• src/Data/Constraint.hs +580/−0
• src/Data/Constraint/Deferrable.hs +66/−0
• src/Data/Constraint/Forall.hs +132/−0
• src/Data/Constraint/Lifting.hs +454/−0
• src/Data/Constraint/Unsafe.hs +65/−0

@@ -1,578 +0,0 @@-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE RoleAnnotations #-}-#endif--------------------------------------------------------------------------------- |--- Module      :  Data.Constraint--- Copyright   :  (C) 2011-2014 Edward Kmett,--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  experimental--- Portability :  non-portable------ @ConstraintKinds@ made type classes into types of a new kind, @Constraint@.------ @--- 'Eq' :: * -> 'Constraint'--- 'Ord' :: * -> 'Constraint'--- 'Monad' :: (* -> *) -> 'Constraint'--- @------ The need for this extension was first publicized in the paper------ <http://research.microsoft.com/pubs/67439/gmap3.pdf Scrap your boilerplate with class: extensible generic functions>------ by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the--- things they needed into a custom 'Sat' typeclass.------ With @ConstraintKinds@ we can put into code a lot of tools for manipulating--- these new types without such awkward workarounds.------------------------------------------------------------------------------module Data.Constraint-  (-  -- * The Kind of Constraints-    Constraint-  -- * Dictionary-  , Dict(Dict)-  -- * Entailment-  , (:-)(Sub)-  , (\\)-  , weaken1, weaken2, contract-  , (&&&), (***)-  , trans, refl-  , top, bottom-  -- * Dict is fully faithful-  , mapDict-  , unmapDict-  -- * Reflection-  , Class(..)-  , (:=>)(..)-  ) where-import Control.Monad-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-import Control.Category-#endif-import Control.Applicative-import Data.Monoid-import Data.Complex-import Data.Ratio-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-import Data.Data-#endif-import GHC.Prim (Constraint)---- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@.------ e.g.------ @--- 'Dict' :: 'Dict' ('Eq' 'Int')--- @------ captures a dictionary that proves we have an:------ @--- instance 'Eq' 'Int--- @------ Pattern matching on the 'Dict' constructor will bring this instance into scope.----data Dict :: Constraint -> * where-  Dict :: a => Dict a-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-  deriving Typeable---instance (Typeable p, p) => Data (Dict p) where-  gfoldl _ z Dict = z Dict-  toConstr _ = dictConstr-  gunfold _ z c = case constrIndex c of-    1 -> z Dict-    _ -> error "gunfold"-  dataTypeOf _ = dictDataType--dictConstr :: Constr-dictConstr = mkConstr dictDataType "Dict" [] Prefix--dictDataType :: DataType-dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]-#endif--deriving instance Eq (Dict a)-deriving instance Ord (Dict a)-deriving instance Show (Dict a)--infixr 9 :----- | This is the type of entailment.------ @a ':-' b@ is read as @a@ \"entails\" @b@.------ With this we can actually build a category for 'Constraint' resolution.------ e.g.------ Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@--- entails @'Eq' a@.------ Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@--- entails @'Ord' [a]@ as well.------ This relationship is captured in the ':-' entailment type here.------ Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category'--- of constraints. However, 'Category' only because sufficiently general to support this--- instance in GHC 7.8, so prior to 7.8 this instance is unavailable.------ But due to the coherence of instance resolution in Haskell, this 'Category'--- has some very interesting properties. Notably, in the absence of--- @IncoherentInstances@, this category is \"thin\", which is to say that--- between any two objects (constraints) there is at most one distinguishable--- arrow.------ This means that for instance, even though there are two ways to derive--- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by--- construction be equal. This is a property that Haskell offers that is--- pretty much unique in the space of languages with things they call \"type--- classes\".------ What are the two ways?------ Well, we can go from @'Ord' a ':-' 'Eq' a@ via the--- superclass relationship, and them from @'Eq' a ':-' 'Eq' [a]@ via the--- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance--- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship--- and this diagram by definition must \"commute\".------ Diagrammatically,------ >                    Ord a--- >                ins /     \ cls--- >                   v       v--- >             Ord [a]     Eq a--- >                cls \     / ins--- >                     v   v--- >                    Eq [a]------ This safety net ensures that pretty much anything you can write with this--- library is sensible and can't break any assumptions on the behalf of--- library authors.-newtype a :- b = Sub (a => Dict b)-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-  deriving Typeable--type role (:-) nominal nominal---- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_.------ This is admissable, but not present by default---- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q)-instance (Typeable p, Typeable q, p, q) => Data (p :- q) where-  gfoldl _ z (Sub Dict) = z (Sub Dict)-  toConstr _ = subConstr-  gunfold _ z c = case constrIndex c of-    1 -> z (Sub Dict)-    _ -> error "gunfold"-  dataTypeOf _ = subDataType--subConstr :: Constr-subConstr = mkConstr dictDataType "Sub" [] Prefix--subDataType :: DataType-subDataType = mkDataType "Data.Constraint.:-" [subConstr]---- | Possible since GHC 7.8, when 'Category' was made polykinded.-instance Category (:-) where-  id  = refl-  (.) = trans-#endif---- | Assumes 'IncoherentInstances' doesn't exist.-instance Eq (a :- b) where-  _ == _ = True---- | Assumes 'IncoherentInstances' doesn't exist.-instance Ord (a :- b) where-  compare _ _ = EQ--instance Show (a :- b) where-  showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"--infixl 1 \\ -- required comment---- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@-(\\) :: a => (b => r) -> (a :- b) -> r-r \\ Sub Dict = r------------------------------------------------------------------------------------- Constraints form a Category------------------------------------------------------------------------------------- | Transitivity of entailment------ If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@-trans :: (b :- c) -> (a :- b) -> a :- c-trans f g = Sub $ Dict \\ f \\ g---- | Reflexivity of entailment------ If we view @(':-')@ as a Constraint-indexed category, then this is 'id'-refl :: a :- a-refl = Sub Dict------------------------------------------------------------------------------------- (,) is a Bifunctor------------------------------------------------------------------------------------- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually--- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a--- bifunctor on the category of constraints. This lets us map over both sides.-(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)-f *** g = Sub $ Dict \\ f \\ g------------------------------------------------------------------------------------- Constraints are Cartesian------------------------------------------------------------------------------------- | Weakening a constraint product------ The category of constraints is Cartesian. We can forget information.-weaken1 :: (a, b) :- a-weaken1 = Sub Dict---- | Weakening a constraint product------ The category of constraints is Cartesian. We can forget information.-weaken2 :: (a, b) :- b-weaken2 = Sub Dict---- | Contracting a constraint / diagonal morphism------ The category of constraints is Cartesian. We can reuse information.-contract :: a :- (a, a)-contract = Sub Dict---- | Constraint product------ > trans weaken1 (f &&& g) = f--- > trans weaken2 (f &&& g) = g-(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)-f &&& g = Sub $ Dict \\ f \\ g------------------------------------------------------------------------------------- Initial and terminal morphisms------------------------------------------------------------------------------------- | Every constraint implies truth------ These are the terminal arrows of the category, and @()@ is the terminal object.------ Given any constraint there is a unique entailment of the @()@ constraint from that constraint.-top :: a :- ()-top = Sub Dict--type family Ex (a :: *) (c :: Constraint) :: Constraint-type instance Ex () c = ()-type instance Ex Bool c = c--falso :: (() ~ a) :- Ex a c-falso = Sub Dict---- |--- A bad type coercion lets you derive any constraint you want.------ These are the initial arrows of the category and @(() ~ Bool)@ is the initial object------ This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">-bottom :: (() ~ Bool) :- c-bottom = falso------------------------------------------------------------------------------------- Dict is fully faithful------------------------------------------------------------------------------------- | Apply an entailment to a dictionary.------ From a category theoretic perspective 'Dict' is a functor that maps from the category--- of constraints (with arrows in ':-') to the category Hask of Haskell data types.-mapDict :: (a :- b) -> Dict a -> Dict b-mapDict p Dict = case p of Sub q -> q---- |--- This functor is fully faithful, which is to say that given any function you can write--- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints--- that you can build.-unmapDict :: (Dict a -> Dict b) -> a :- b-unmapDict f = Sub (f Dict)--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-type role Dict nominal-#endif------------------------------------------------------------------------------------- Reflection------------------------------------------------------------------------------------- | Reify the relationship between a class and its superclass constraints as a class------ Given a definition such as------ @--- class Foo a => Bar a--- @------ you can capture the relationship between 'Bar a' and its superclass 'Foo a' with------ @--- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict'--- @------ Now the user can use 'cls :: Bar a :- Foo a'-class Class b h | h -> b where-  cls :: h :- b--infixr 9 :=>--- | Reify the relationship between an instance head and its body as a class------ Given a definition such as------ @--- instance Foo a => Foo [a]--- @------ you can capture the relationship between the instance head and its body with------ @--- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict'--- @-class b :=> h | h -> b where-  ins :: b :- h---- Bootstrapping--instance Class () (Class b a) where cls = Sub Dict-instance Class () (b :=> a) where cls = Sub Dict--instance Class b a => () :=> Class b a where ins = Sub Dict-instance (b :=> a) => () :=> b :=> a where ins = Sub Dict--instance Class () () where cls = Sub Dict-instance () :=> () where ins = Sub Dict---- Local, Prelude, Applicative, C.M.I and Data.Monoid instances---- Eq-instance Class () (Eq a) where cls = Sub Dict-instance () :=> Eq () where ins = Sub Dict-instance () :=> Eq Int where ins = Sub Dict-instance () :=> Eq Bool where ins = Sub Dict-instance () :=> Eq Integer where ins = Sub Dict-instance () :=> Eq Float where ins = Sub Dict-instance () :=> Eq Double where ins = Sub Dict-instance Eq a :=> Eq [a] where ins = Sub Dict-instance Eq a :=> Eq (Maybe a) where ins = Sub Dict-instance Eq a :=> Eq (Complex a) where ins = Sub Dict-instance Eq a :=> Eq (Ratio a) where ins = Sub Dict-instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict-instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict-instance () :=> Eq (Dict a) where ins = Sub Dict-instance () :=> Eq (a :- b) where ins = Sub Dict---- Ord-instance Class (Eq a) (Ord a) where cls = Sub Dict-instance () :=> Ord () where ins = Sub Dict-instance () :=> Ord Bool where ins = Sub Dict-instance () :=> Ord Int where ins = Sub Dict-instance ():=> Ord Integer where ins = Sub Dict-instance () :=> Ord Float where ins = Sub Dict-instance ():=> Ord Double where ins = Sub Dict-instance () :=> Ord Char where ins = Sub Dict-instance Ord a :=> Ord (Maybe a) where ins = Sub Dict-instance Ord a :=> Ord [a] where ins = Sub Dict-instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict-instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict-instance Integral a :=> Ord (Ratio a) where ins = Sub Dict-instance () :=> Ord (Dict a) where ins = Sub Dict-instance () :=> Ord (a :- b) where ins = Sub Dict---- Show-instance Class () (Show a) where cls = Sub Dict-instance () :=> Show () where ins = Sub Dict-instance () :=> Show Bool where ins = Sub Dict-instance () :=> Show Ordering where ins = Sub Dict-instance () :=> Show Char where ins = Sub Dict-instance Show a :=> Show (Complex a) where ins = Sub Dict-instance Show a :=> Show [a] where ins = Sub Dict-instance Show a :=> Show (Maybe a) where ins = Sub Dict-instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict-instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict-instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict-instance () :=> Show (Dict a) where ins = Sub Dict-instance () :=> Show (a :- b) where ins = Sub Dict---- Read-instance Class () (Read a) where cls = Sub Dict-instance () :=> Read () where ins = Sub Dict-instance () :=> Read Bool where ins = Sub Dict-instance () :=> Read Ordering where ins = Sub Dict-instance () :=> Read Char where ins = Sub Dict-instance Read a :=> Read (Complex a) where ins = Sub Dict-instance Read a :=> Read [a] where ins = Sub Dict-instance Read a :=> Read (Maybe a) where ins = Sub Dict-instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict-instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict-instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict---- Enum-instance Class () (Enum a) where cls = Sub Dict-instance () :=> Enum () where ins = Sub Dict-instance () :=> Enum Bool where ins = Sub Dict-instance () :=> Enum Ordering where ins = Sub Dict-instance () :=> Enum Char where ins = Sub Dict-instance () :=> Enum Int where ins = Sub Dict-instance () :=> Enum Integer where ins = Sub Dict-instance () :=> Enum Float where ins = Sub Dict-instance () :=> Enum Double where ins = Sub Dict-instance Integral a :=> Enum (Ratio a) where ins = Sub Dict---- Bounded-instance Class () (Bounded a) where cls = Sub Dict-instance () :=> Bounded () where ins = Sub Dict-instance () :=> Bounded Ordering where ins = Sub Dict-instance () :=> Bounded Bool where ins = Sub Dict-instance () :=> Bounded Int where ins = Sub Dict-instance () :=> Bounded Char where ins = Sub Dict-instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict---- Num-instance Class () (Num a) where cls = Sub Dict-instance () :=> Num Int where ins = Sub Dict-instance () :=> Num Integer where ins = Sub Dict-instance () :=> Num Float where ins = Sub Dict-instance () :=> Num Double where ins = Sub Dict-instance RealFloat a :=> Num (Complex a) where ins = Sub Dict-instance Integral a :=> Num (Ratio a) where ins = Sub Dict---- Real-instance Class (Num a, Ord a) (Real a) where cls = Sub Dict-instance () :=> Real Int where ins = Sub Dict-instance () :=> Real Integer where ins = Sub Dict-instance () :=> Real Float where ins = Sub Dict-instance () :=> Real Double where ins = Sub Dict-instance Integral a :=> Real (Ratio a) where ins = Sub Dict---- Integral-instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict-instance () :=> Integral Int where ins = Sub Dict-instance () :=> Integral Integer where ins = Sub Dict---- Fractional-instance Class (Num a) (Fractional a) where cls = Sub Dict-instance () :=> Fractional Float where ins = Sub Dict-instance () :=> Fractional Double where ins = Sub Dict-instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict-instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict---- Floating-instance Class (Fractional a) (Floating a) where cls = Sub Dict-instance () :=> Floating Float where ins = Sub Dict-instance () :=> Floating Double where ins = Sub Dict-instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict---- RealFrac-instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict-instance () :=> RealFrac Float where ins = Sub Dict-instance () :=> RealFrac Double where ins = Sub Dict-instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict---- RealFloat-instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict-instance () :=> RealFloat Float where ins = Sub Dict-instance () :=> RealFloat Double where ins = Sub Dict---- Monoid-instance Class () (Monoid a) where cls = Sub Dict-instance () :=> Monoid () where ins = Sub Dict-instance () :=> Monoid Ordering where ins = Sub Dict-instance () :=> Monoid [a] where ins = Sub Dict-instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict-instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict---- Functor-instance Class () (Functor f) where cls = Sub Dict-instance () :=> Functor [] where ins = Sub Dict-instance () :=> Functor Maybe where ins = Sub Dict-instance () :=> Functor (Either a) where ins = Sub Dict-instance () :=> Functor ((->) a) where ins = Sub Dict-instance () :=> Functor ((,) a) where ins = Sub Dict-instance () :=> Functor IO where ins = Sub Dict-instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict---- Applicative-instance Class (Functor f) (Applicative f) where cls = Sub Dict-instance () :=> Applicative [] where ins = Sub Dict-instance () :=> Applicative Maybe where ins = Sub Dict-instance () :=> Applicative (Either a) where ins = Sub Dict-instance () :=> Applicative ((->)a) where ins = Sub Dict-instance () :=> Applicative IO where ins = Sub Dict-instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict-instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict---- Alternative-instance Class (Applicative f) (Alternative f) where cls = Sub Dict-instance () :=> Alternative [] where ins = Sub Dict-instance () :=> Alternative Maybe where ins = Sub Dict-instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict---- Monad-instance Class () (Monad f) where cls = Sub Dict-instance () :=> Monad [] where ins = Sub Dict-instance () :=> Monad ((->) a) where ins = Sub Dict-instance () :=> Monad (Either a) where ins = Sub Dict-instance () :=> Monad IO where ins = Sub Dict---- MonadPlus-instance Class (Monad f) (MonadPlus f) where cls = Sub Dict-instance () :=> MonadPlus [] where ins = Sub Dict-instance () :=> MonadPlus Maybe where ins = Sub Dict------------------------------------------------------------------------------------- UndecidableInstances-----------------------------------------------------------------------------------instance a :=> Enum (Dict a) where ins = Sub Dict-instance a => Enum (Dict a) where-  toEnum _ = Dict-  fromEnum Dict = 0--instance a :=> Bounded (Dict a) where ins = Sub Dict-instance a => Bounded (Dict a) where-  minBound = Dict-  maxBound = Dict--instance a :=> Read (Dict a) where ins = Sub Dict-deriving instance a => Read (Dict a)--instance a :=> Monoid (Dict a) where ins = Sub Dict-instance a => Monoid (Dict a) where-  mappend Dict Dict = Dict-  mempty = Dict

@@ -1,70 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE Trustworthy #-}-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-{-# LANGUAGE RoleAnnotations #-}-#endif--------------------------------------------------------------------------------- |--- Module      :  Data.Constraint.Forall--- Copyright   :  (C) 2011-2013 Edward Kmett,--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  experimental--- Portability :  non-portable------ This module uses a trick to provide quantification over constraints.-------------------------------------------------------------------------------module Data.Constraint.Forall-  ( Forall, inst-  , ForallF, instF-  , Forall1, inst1-  , ForallT, instT-  ) where--import Data.Constraint-import Data.Constraint.Unsafe---- skolem variables, do not export!-data A-data B--- | A quantified constraint-type Forall (p :: * -> Constraint) = (p A, p B)--type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B))--data F a-data M a--type Forall1 (p :: (* -> *) -> Constraint) = (p F, p M)--type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B))--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-type role F nominal-type role M nominal-#endif----- | instantiate a quantified constraint on kind @*@-inst :: forall p a. Forall p :- p a-inst = trans (unsafeCoerceConstraint :: p A :- p a) weaken1--instF :: forall p f a. ForallF p f :- p (f a)-instF = trans (unsafeCoerceConstraint :: p (f A) :- p (f a)) weaken1---- | instantiate a quantified constraint on kind @* -> *@-inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall1 p :- p f-inst1 = trans (unsafeCoerceConstraint :: p F :- p f) weaken1--instT :: forall (p :: * -> Constraint) (t :: (* -> *) -> * -> *) (f :: * -> *) a. ForallT p t :- p (t f a)-instT = trans (unsafeCoerceConstraint :: p (t F A) :- p (t f a)) weaken1-

@@ -1,55 +0,0 @@-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE Unsafe #-}--------------------------------------------------------------------------------- |--- Module      :  Data.Constraint.Unsafe--- Copyright   :  (C) 2011-2013 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- Stability   :  experimental--- Portability :  non-portable---------------------------------------------------------------------------------module Data.Constraint.Unsafe-  ( unsafeCoerceConstraint-  , unsafeDerive-  , unsafeUnderive-  -- * Sugar-  , unsafeApplicative-  , unsafeAlternative-  ) where--import Control.Applicative-import Control.Monad-import Control.Newtype-import Data.Constraint-import Unsafe.Coerce---- | Coerce a dictionary unsafely from one type to another-unsafeCoerceConstraint :: a :- b-unsafeCoerceConstraint = unsafeCoerce refl---- | Coerce a dictionary unsafely from one type to a newtype of that type-unsafeDerive :: Newtype n o => (o -> n) -> t o :- t n-unsafeDerive _ = unsafeCoerceConstraint---- | Coerce a dictionary unsafely from a newtype of a type to the base type-unsafeUnderive :: Newtype n o => (o -> n) -> t n :- t o-unsafeUnderive _ = unsafeCoerceConstraint---- | Construct an Applicative instance from a Monad-unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a-unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins---- | Construct an Alternative instance from a MonadPlus-unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a-unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins

@@ -1,4 +1,4 @@-Copyright 2011-2013 Edward Kmett+Copyright 2011-2015 Edward Kmett  All rights reserved. 

@@ -1,6 +1,6 @@ name:          constraints category:      Constraints-version:       0.4.1.3+version:       0.6 license:       BSD3 cabal-version: >= 1.10 license-file:  LICENSE@@ -9,7 +9,7 @@ stability:     experimental homepage:      http://github.com/ekmett/constraints/ bug-reports:   http://github.com/ekmett/constraints/issues-copyright:     Copyright (C) 2011-2014 Edward A. Kmett+copyright:     Copyright (C) 2011-2015 Edward A. Kmett synopsis:      Constraint manipulation description:   GHC 7.4 gave us the ability to talk about @ConstraintKinds@. They stopped crashing the compiler in GHC 7.6.@@ -17,7 +17,7 @@   This package provides a vocabulary for working with them.  build-type:    Simple-tested-with:   GHC == 7.8.3, GHC == 7.7.20131027, GHC == 7.7.20131025, GHC == 7.6.3+tested-with:   GHC == 7.8.3, GHC == 7.7.20131027, GHC == 7.7.20131025 extra-source-files: README.markdown  source-repository head@@ -25,6 +25,8 @@   location: git://github.com/ekmett/constraints.git  library+  hs-source-dirs: src+   default-language: Haskell2010   other-extensions:     FunctionalDependencies,@@ -39,12 +41,27 @@     GADTs    build-depends:-    base >= 4.5 && < 5,-    newtype >= 0.2 && < 0.3,-    ghc-prim+    base >= 4.6 && < 5,+    binary >= 0.7.3 && < 0.8,+    deepseq >= 1.3 && < 1.5,+    ghc-prim,+    hashable >= 1.2 && < 1.3,+    mtl >= 2 && < 2.3,+    transformers >= 0.2 && < 0.5,+    transformers-compat >= 0.4 && < 1++  if impl(ghc < 7.8)+    build-depends:+      newtype >= 0.2 && < 0.3,+      tagged >= 0.2 && < 1+  else+    exposed-modules:+      Data.Constraint.Forall+   exposed-modules:     Data.Constraint-    Data.Constraint.Forall+    Data.Constraint.Deferrable+    Data.Constraint.Lifting     Data.Constraint.Unsafe    ghc-options: -Wall

@@ -0,0 +1,580 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE CPP #-}+#if __GLASGOW_HASKELL__ >= 707+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE RoleAnnotations #-}+#endif+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Constraint+-- Copyright   :  (C) 2011-2015 Edward Kmett,+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+-- @ConstraintKinds@ made type classes into types of a new kind, @Constraint@.+--+-- @+-- 'Eq' :: * -> 'Constraint'+-- 'Ord' :: * -> 'Constraint'+-- 'Monad' :: (* -> *) -> 'Constraint'+-- @+--+-- The need for this extension was first publicized in the paper+--+-- <http://research.microsoft.com/pubs/67439/gmap3.pdf Scrap your boilerplate with class: extensible generic functions>+--+-- by Ralf Lämmel and Simon Peyton Jones in 2005, which shoehorned all the+-- things they needed into a custom 'Sat' typeclass.+--+-- With @ConstraintKinds@ we can put into code a lot of tools for manipulating+-- these new types without such awkward workarounds.+----------------------------------------------------------------------------+module Data.Constraint+  (+  -- * The Kind of Constraints+    Constraint+  -- * Dictionary+  , Dict(Dict)+  -- * Entailment+  , (:-)(Sub)+  , (\\)+  , weaken1, weaken2, contract+  , (&&&), (***)+  , trans, refl+  , top, bottom+  -- * Dict is fully faithful+  , mapDict+  , unmapDict+  -- * Reflection+  , Class(..)+  , (:=>)(..)+  ) where+import Control.Monad+#if __GLASGOW_HASKELL__ >= 707+import Control.Category+#endif+import Control.Applicative+#if __GLASGOW_HASKELL__ < 710+import Data.Monoid+#endif+import Data.Complex+import Data.Ratio+#if __GLASGOW_HASKELL__ >= 707+import Data.Data+#endif+import GHC.Prim (Constraint)++-- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@.+--+-- e.g.+--+-- @+-- 'Dict' :: 'Dict' ('Eq' 'Int')+-- @+--+-- captures a dictionary that proves we have an:+--+-- @+-- instance 'Eq' 'Int+-- @+--+-- Pattern matching on the 'Dict' constructor will bring this instance into scope.+--+data Dict :: Constraint -> * where+  Dict :: a => Dict a+#if __GLASGOW_HASKELL__ >= 707+  deriving Typeable+++instance (Typeable p, p) => Data (Dict p) where+  gfoldl _ z Dict = z Dict+  toConstr _ = dictConstr+  gunfold _ z c = case constrIndex c of+    1 -> z Dict+    _ -> error "gunfold"+  dataTypeOf _ = dictDataType++dictConstr :: Constr+dictConstr = mkConstr dictDataType "Dict" [] Prefix++dictDataType :: DataType+dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]+#endif++deriving instance Eq (Dict a)+deriving instance Ord (Dict a)+deriving instance Show (Dict a)++infixr 9 :-++-- | This is the type of entailment.+--+-- @a ':-' b@ is read as @a@ \"entails\" @b@.+--+-- With this we can actually build a category for 'Constraint' resolution.+--+-- e.g.+--+-- Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@+-- entails @'Eq' a@.+--+-- Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@+-- entails @'Ord' [a]@ as well.+--+-- This relationship is captured in the ':-' entailment type here.+--+-- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category'+-- of constraints. However, 'Category' only because sufficiently general to support this+-- instance in GHC 7.8, so prior to 7.8 this instance is unavailable.+--+-- But due to the coherence of instance resolution in Haskell, this 'Category'+-- has some very interesting properties. Notably, in the absence of+-- @IncoherentInstances@, this category is \"thin\", which is to say that+-- between any two objects (constraints) there is at most one distinguishable+-- arrow.+--+-- This means that for instance, even though there are two ways to derive+-- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by+-- construction be equal. This is a property that Haskell offers that is+-- pretty much unique in the space of languages with things they call \"type+-- classes\".+--+-- What are the two ways?+--+-- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the+-- superclass relationship, and them from @'Eq' a ':-' 'Eq' [a]@ via the+-- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance+-- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship+-- and this diagram by definition must \"commute\".+--+-- Diagrammatically,+--+-- >                    Ord a+-- >                ins /     \ cls+-- >                   v       v+-- >             Ord [a]     Eq a+-- >                cls \     / ins+-- >                     v   v+-- >                    Eq [a]+--+-- This safety net ensures that pretty much anything you can write with this+-- library is sensible and can't break any assumptions on the behalf of+-- library authors.+newtype a :- b = Sub (a => Dict b)+#if __GLASGOW_HASKELL__ >= 707+  deriving Typeable++type role (:-) nominal nominal++-- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_.+--+-- This is admissable, but not present by default++-- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q)+instance (Typeable p, Typeable q, p, q) => Data (p :- q) where+  gfoldl _ z (Sub Dict) = z (Sub Dict)+  toConstr _ = subConstr+  gunfold _ z c = case constrIndex c of+    1 -> z (Sub Dict)+    _ -> error "gunfold"+  dataTypeOf _ = subDataType++subConstr :: Constr+subConstr = mkConstr dictDataType "Sub" [] Prefix++subDataType :: DataType+subDataType = mkDataType "Data.Constraint.:-" [subConstr]++-- | Possible since GHC 7.8, when 'Category' was made polykinded.+instance Category (:-) where+  id  = refl+  (.) = trans+#endif++-- | Assumes 'IncoherentInstances' doesn't exist.+instance Eq (a :- b) where+  _ == _ = True++-- | Assumes 'IncoherentInstances' doesn't exist.+instance Ord (a :- b) where+  compare _ _ = EQ++instance Show (a :- b) where+  showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"++infixl 1 \\ -- required comment++-- | Given that @a :- b@, derive something that needs a context @b@, using the context @a@+(\\) :: a => (b => r) -> (a :- b) -> r+r \\ Sub Dict = r++--------------------------------------------------------------------------------+-- Constraints form a Category+--------------------------------------------------------------------------------++-- | Transitivity of entailment+--+-- If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@+trans :: (b :- c) -> (a :- b) -> a :- c+trans f g = Sub $ Dict \\ f \\ g++-- | Reflexivity of entailment+--+-- If we view @(':-')@ as a Constraint-indexed category, then this is 'id'+refl :: a :- a+refl = Sub Dict++--------------------------------------------------------------------------------+-- (,) is a Bifunctor+--------------------------------------------------------------------------------++-- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually+-- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a+-- bifunctor on the category of constraints. This lets us map over both sides.+(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)+f *** g = Sub $ Dict \\ f \\ g++--------------------------------------------------------------------------------+-- Constraints are Cartesian+--------------------------------------------------------------------------------++-- | Weakening a constraint product+--+-- The category of constraints is Cartesian. We can forget information.+weaken1 :: (a, b) :- a+weaken1 = Sub Dict++-- | Weakening a constraint product+--+-- The category of constraints is Cartesian. We can forget information.+weaken2 :: (a, b) :- b+weaken2 = Sub Dict++-- | Contracting a constraint / diagonal morphism+--+-- The category of constraints is Cartesian. We can reuse information.+contract :: a :- (a, a)+contract = Sub Dict++-- | Constraint product+--+-- > trans weaken1 (f &&& g) = f+-- > trans weaken2 (f &&& g) = g+(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)+f &&& g = Sub $ Dict \\ f \\ g++--------------------------------------------------------------------------------+-- Initial and terminal morphisms+--------------------------------------------------------------------------------++-- | Every constraint implies truth+--+-- These are the terminal arrows of the category, and @()@ is the terminal object.+--+-- Given any constraint there is a unique entailment of the @()@ constraint from that constraint.+top :: a :- ()+top = Sub Dict++type family Ex (a :: *) (c :: Constraint) :: Constraint+type instance Ex () c = ()+type instance Ex Bool c = c++falso :: (() ~ a) :- Ex a c+falso = Sub Dict++-- |+-- A bad type coercion lets you derive any constraint you want.+--+-- These are the initial arrows of the category and @(() ~ Bool)@ is the initial object+--+-- This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">+bottom :: (() ~ Bool) :- c+bottom = falso++--------------------------------------------------------------------------------+-- Dict is fully faithful+--------------------------------------------------------------------------------++-- | Apply an entailment to a dictionary.+--+-- From a category theoretic perspective 'Dict' is a functor that maps from the category+-- of constraints (with arrows in ':-') to the category Hask of Haskell data types.+mapDict :: (a :- b) -> Dict a -> Dict b+mapDict p Dict = case p of Sub q -> q++-- |+-- This functor is fully faithful, which is to say that given any function you can write+-- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints+-- that you can build.+unmapDict :: (Dict a -> Dict b) -> a :- b+unmapDict f = Sub (f Dict)++#if __GLASGOW_HASKELL__ >= 707+type role Dict nominal+#endif++--------------------------------------------------------------------------------+-- Reflection+--------------------------------------------------------------------------------++-- | Reify the relationship between a class and its superclass constraints as a class+--+-- Given a definition such as+--+-- @+-- class Foo a => Bar a+-- @+--+-- you can capture the relationship between 'Bar a' and its superclass 'Foo a' with+--+-- @+-- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict'+-- @+--+-- Now the user can use 'cls :: Bar a :- Foo a'+class Class b h | h -> b where+  cls :: h :- b++infixr 9 :=>+-- | Reify the relationship between an instance head and its body as a class+--+-- Given a definition such as+--+-- @+-- instance Foo a => Foo [a]+-- @+--+-- you can capture the relationship between the instance head and its body with+--+-- @+-- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict'+-- @+class b :=> h | h -> b where+  ins :: b :- h++-- Bootstrapping++instance Class () (Class b a) where cls = Sub Dict+instance Class () (b :=> a) where cls = Sub Dict++instance Class b a => () :=> Class b a where ins = Sub Dict+instance (b :=> a) => () :=> b :=> a where ins = Sub Dict++instance Class () () where cls = Sub Dict+instance () :=> () where ins = Sub Dict++-- Local, Prelude, Applicative, C.M.I and Data.Monoid instances++-- Eq+instance Class () (Eq a) where cls = Sub Dict+instance () :=> Eq () where ins = Sub Dict+instance () :=> Eq Int where ins = Sub Dict+instance () :=> Eq Bool where ins = Sub Dict+instance () :=> Eq Integer where ins = Sub Dict+instance () :=> Eq Float where ins = Sub Dict+instance () :=> Eq Double where ins = Sub Dict+instance Eq a :=> Eq [a] where ins = Sub Dict+instance Eq a :=> Eq (Maybe a) where ins = Sub Dict+instance Eq a :=> Eq (Complex a) where ins = Sub Dict+instance Eq a :=> Eq (Ratio a) where ins = Sub Dict+instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict+instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict+instance () :=> Eq (Dict a) where ins = Sub Dict+instance () :=> Eq (a :- b) where ins = Sub Dict++-- Ord+instance Class (Eq a) (Ord a) where cls = Sub Dict+instance () :=> Ord () where ins = Sub Dict+instance () :=> Ord Bool where ins = Sub Dict+instance () :=> Ord Int where ins = Sub Dict+instance ():=> Ord Integer where ins = Sub Dict+instance () :=> Ord Float where ins = Sub Dict+instance ():=> Ord Double where ins = Sub Dict+instance () :=> Ord Char where ins = Sub Dict+instance Ord a :=> Ord (Maybe a) where ins = Sub Dict+instance Ord a :=> Ord [a] where ins = Sub Dict+instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict+instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict+instance Integral a :=> Ord (Ratio a) where ins = Sub Dict+instance () :=> Ord (Dict a) where ins = Sub Dict+instance () :=> Ord (a :- b) where ins = Sub Dict++-- Show+instance Class () (Show a) where cls = Sub Dict+instance () :=> Show () where ins = Sub Dict+instance () :=> Show Bool where ins = Sub Dict+instance () :=> Show Ordering where ins = Sub Dict+instance () :=> Show Char where ins = Sub Dict+instance Show a :=> Show (Complex a) where ins = Sub Dict+instance Show a :=> Show [a] where ins = Sub Dict+instance Show a :=> Show (Maybe a) where ins = Sub Dict+instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict+instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict+instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict+instance () :=> Show (Dict a) where ins = Sub Dict+instance () :=> Show (a :- b) where ins = Sub Dict++-- Read+instance Class () (Read a) where cls = Sub Dict+instance () :=> Read () where ins = Sub Dict+instance () :=> Read Bool where ins = Sub Dict+instance () :=> Read Ordering where ins = Sub Dict+instance () :=> Read Char where ins = Sub Dict+instance Read a :=> Read (Complex a) where ins = Sub Dict+instance Read a :=> Read [a] where ins = Sub Dict+instance Read a :=> Read (Maybe a) where ins = Sub Dict+instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict+instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict+instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict++-- Enum+instance Class () (Enum a) where cls = Sub Dict+instance () :=> Enum () where ins = Sub Dict+instance () :=> Enum Bool where ins = Sub Dict+instance () :=> Enum Ordering where ins = Sub Dict+instance () :=> Enum Char where ins = Sub Dict+instance () :=> Enum Int where ins = Sub Dict+instance () :=> Enum Integer where ins = Sub Dict+instance () :=> Enum Float where ins = Sub Dict+instance () :=> Enum Double where ins = Sub Dict+instance Integral a :=> Enum (Ratio a) where ins = Sub Dict++-- Bounded+instance Class () (Bounded a) where cls = Sub Dict+instance () :=> Bounded () where ins = Sub Dict+instance () :=> Bounded Ordering where ins = Sub Dict+instance () :=> Bounded Bool where ins = Sub Dict+instance () :=> Bounded Int where ins = Sub Dict+instance () :=> Bounded Char where ins = Sub Dict+instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict++-- Num+instance Class () (Num a) where cls = Sub Dict+instance () :=> Num Int where ins = Sub Dict+instance () :=> Num Integer where ins = Sub Dict+instance () :=> Num Float where ins = Sub Dict+instance () :=> Num Double where ins = Sub Dict+instance RealFloat a :=> Num (Complex a) where ins = Sub Dict+instance Integral a :=> Num (Ratio a) where ins = Sub Dict++-- Real+instance Class (Num a, Ord a) (Real a) where cls = Sub Dict+instance () :=> Real Int where ins = Sub Dict+instance () :=> Real Integer where ins = Sub Dict+instance () :=> Real Float where ins = Sub Dict+instance () :=> Real Double where ins = Sub Dict+instance Integral a :=> Real (Ratio a) where ins = Sub Dict++-- Integral+instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict+instance () :=> Integral Int where ins = Sub Dict+instance () :=> Integral Integer where ins = Sub Dict++-- Fractional+instance Class (Num a) (Fractional a) where cls = Sub Dict+instance () :=> Fractional Float where ins = Sub Dict+instance () :=> Fractional Double where ins = Sub Dict+instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict+instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict++-- Floating+instance Class (Fractional a) (Floating a) where cls = Sub Dict+instance () :=> Floating Float where ins = Sub Dict+instance () :=> Floating Double where ins = Sub Dict+instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict++-- RealFrac+instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict+instance () :=> RealFrac Float where ins = Sub Dict+instance () :=> RealFrac Double where ins = Sub Dict+instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict++-- RealFloat+instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict+instance () :=> RealFloat Float where ins = Sub Dict+instance () :=> RealFloat Double where ins = Sub Dict++-- Monoid+instance Class () (Monoid a) where cls = Sub Dict+instance () :=> Monoid () where ins = Sub Dict+instance () :=> Monoid Ordering where ins = Sub Dict+instance () :=> Monoid [a] where ins = Sub Dict+instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict+instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict++-- Functor+instance Class () (Functor f) where cls = Sub Dict+instance () :=> Functor [] where ins = Sub Dict+instance () :=> Functor Maybe where ins = Sub Dict+instance () :=> Functor (Either a) where ins = Sub Dict+instance () :=> Functor ((->) a) where ins = Sub Dict+instance () :=> Functor ((,) a) where ins = Sub Dict+instance () :=> Functor IO where ins = Sub Dict+instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict++-- Applicative+instance Class (Functor f) (Applicative f) where cls = Sub Dict+instance () :=> Applicative [] where ins = Sub Dict+instance () :=> Applicative Maybe where ins = Sub Dict+instance () :=> Applicative (Either a) where ins = Sub Dict+instance () :=> Applicative ((->)a) where ins = Sub Dict+instance () :=> Applicative IO where ins = Sub Dict+instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict+instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict++-- Alternative+instance Class (Applicative f) (Alternative f) where cls = Sub Dict+instance () :=> Alternative [] where ins = Sub Dict+instance () :=> Alternative Maybe where ins = Sub Dict+instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict++-- Monad+instance Class () (Monad f) where cls = Sub Dict+instance () :=> Monad [] where ins = Sub Dict+instance () :=> Monad ((->) a) where ins = Sub Dict+instance () :=> Monad (Either a) where ins = Sub Dict+instance () :=> Monad IO where ins = Sub Dict++-- MonadPlus+instance Class (Monad f) (MonadPlus f) where cls = Sub Dict+instance () :=> MonadPlus [] where ins = Sub Dict+instance () :=> MonadPlus Maybe where ins = Sub Dict++--------------------------------------------------------------------------------+-- UndecidableInstances+--------------------------------------------------------------------------------++instance a :=> Enum (Dict a) where ins = Sub Dict+instance a => Enum (Dict a) where+  toEnum _ = Dict+  fromEnum Dict = 0++instance a :=> Bounded (Dict a) where ins = Sub Dict+instance a => Bounded (Dict a) where+  minBound = Dict+  maxBound = Dict++instance a :=> Read (Dict a) where ins = Sub Dict+deriving instance a => Read (Dict a)++instance a :=> Monoid (Dict a) where ins = Sub Dict+instance a => Monoid (Dict a) where+  mappend Dict Dict = Dict+  mempty = Dict

@@ -0,0 +1,66 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Constraint.Deferrable+-- Copyright   :  (C) 2015 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+  ) where++import Control.Exception+import Control.Monad+import Data.Constraint+import Data.Proxy+import Data.Typeable (Typeable, cast)++data UnsatisfiedConstraint = UnsatisfiedConstraint String+  deriving (Typeable, Show)++instance Exception UnsatisfiedConstraint++-- | Allow an attempt at resolution of a constraint at a later time+class Deferrable (p :: Constraint) 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 proxy p r. Deferrable p => proxy p -> (p => r) -> r+defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r ++deferred :: forall p. Deferrable p :- p+deferred = Sub $ defer (Proxy :: Proxy p) Dict++-- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6.+data a :~: b where+  Refl :: a :~: a+    deriving Typeable++instance (Typeable a, Typeable b) => Deferrable (a ~ b) where+  deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of+    Just Refl -> Right r+    Nothing -> Left "deferred type equality: type mismatch"++instance (Deferrable a, Deferrable b) => Deferrable (a, b) where+  deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r++instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where+  deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ join $ deferEither (Proxy :: Proxy b) $ deferEither (Proxy :: Proxy c) r

@@ -0,0 +1,132 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE PolyKinds #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Constraint.Forall+-- Copyright   :  (C) 2011-2015 Edward Kmett,+--                (C) 2015 Ørjan Johansen,+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+-- This module uses a trick to provide quantification over constraints.+----------------------------------------------------------------------------++module Data.Constraint.Forall+  ( Forall, inst+  , ForallF, instF+  , Forall1, inst1+  , ForallT, instT+  ) where++import Data.Constraint+import Unsafe.Coerce (unsafeCoerce)++{- The basic trick of this module is to use "skolem" types as test candidates+ - for whether a class predicate holds, and if so assume that it holds for all+ - types, unsafely coercing the typeclass dictionary.+ -+ - A previous version of this module used concrete, unexported types as the+ - skolems. This turned out to be unsound in the presence of type families.+ - There were 3 somewhat distinct issues:+ -+ - 1. Using closed type families, it is possible to test whether two concrete+ - types are equal, even if one of them is not directly importable.+ -+ - 2. Using just open type families, it is possible to test "at least 2 of+ - these n+1 types are equal", thus using the pigeonhole principle to thwart+ - any scheme based on having only a finite number of shared skolem types.+ -+ - 3. Using just pattern matching of types by unification, it is possible+ - to extract the skolem types from the application the `Forall p` expands+ - to. (Although type families are probably still needed to exploit this.)+ -+ - András Kovács and Ørjan Johansen independently realized that skolems+ - themselves made as type family applications can be used to solve the first+ - two problems (and discovered the third problem in the process). As a bonus,+ - the resulting code is easy to make polykinded.+ -+ - Problem 1 is solved by making the type family have no instances, forcing+ - GHC to make no assumption about what type a skolem is.+ -+ - Problem 2 is solved by parametrizing the skolem on the predicate tested+ - for. (This is a known trick in predicate logic.)+ -+ - Problem 3 is solved by making the `Forall p` application expand to a type+ - class, and have the *actual* test constraint be a superclass constraint on+ - that type class, thus preventing the user directly accessing it.+ -+ - An unfortunate side effect of the new method is that it tends to trigger+ - spurious errors from GHC test for cycles in superclass constraints. András+ - Kovács discovered that these can be silenced by yet another use of a type+ - family.+ -+ - David Feuer points out a remaining doubt about the soundness of this scheme:+ - GHC *does* know that the skolems created from a single predicate `p` are+ - equal. This could in theory apply even if the skolems come from two+ - *distinct* invocations of `Forall p`.+ -+ - However, we don't know any way of bringing two such skolems in contact with+ - each other to create an actual exploit. It would seem to require `p` to+ - already contain its own skolem, despite there being (hopefully) no way to+ - extract it from `Forall p` in order to tie the knot.+ -}++-- the `Skolem*` type families represent skolem variables, do not export!+-- if GHC supports it, these might be made closed with no instances.++type family Skolem (p :: k -> Constraint) :: k+type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1+type family SkolemT1 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k1+type family SkolemT2 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k2++-- The outer `Forall*` type families prevent GHC from giving a spurious+-- superclass cycle error.+-- The inner `Forall*_` classes prevent the skolem from leaking to the user,+-- which would be disastrous.++-- | A representation of the quantified constraint @forall a. p a@.+type family Forall (p :: k -> Constraint) :: Constraint where+    Forall p = Forall_ p+class p (Skolem p) => Forall_ (p :: k -> Constraint)+instance p (Skolem p) => Forall_ (p :: k -> Constraint)++-- | A representation of the quantified constraint @forall a. p (f a)@.+type family ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) :: Constraint where+    ForallF p f = ForallF_ p f+class p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)+instance p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)++type Forall1 p = Forall p++-- | A representation of the quantified constraint @forall f a. p (t f a)@.+type family ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: Constraint where+    ForallT p t = ForallT_ p t+class p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)+instance p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)++-- | Instantiate a quantified @'Forall' p@ constraint at type @a@.+inst :: forall p a. Forall p :- p a+inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p))++-- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@.+instF :: forall p f a. ForallF p f :- p (f a)+instF = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f)))++-- | Instantiate a quantified constraint on kind @* -> *@.+-- This is now redundant since @'inst'@ became polykinded.+inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f+inst1 = inst++-- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.+instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a)+instT = unsafeCoerce (Sub Dict :: ForallT p t :- p (t (SkolemT1 p t) (SkolemT2 p t)))

@@ -0,0 +1,454 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# OPTIONS_GHC -fno-warn-deprecations #-}+module Data.Constraint.Lifting +  ( Lifting(..)+  , Lifting2(..)+  ) where++import Control.Applicative+import Control.Applicative.Backwards+import Control.Applicative.Lift+import Control.DeepSeq+import Control.Monad+import Control.Monad.Cont.Class+import Control.Monad.Error.Class+import Control.Monad.Fix+import Control.Monad.IO.Class+import Control.Monad.RWS.Class+import Control.Monad.Trans.Cont+import Control.Monad.Trans.Error+import Control.Monad.Trans.Except+import Control.Monad.Trans.Identity+import Control.Monad.Trans.List+import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Reader+import Control.Monad.Trans.RWS.Lazy as Lazy+import Control.Monad.Trans.RWS.Strict as Strict+import Control.Monad.Trans.State.Lazy as Lazy+import Control.Monad.Trans.State.Strict as Strict+import Control.Monad.Trans.Writer.Lazy as Lazy+import Control.Monad.Trans.Writer.Strict as Strict+import Data.Binary+import Data.Complex+import Data.Constraint+#if __GLASGOW_HASKELL__ < 710+import Data.Foldable+#endif+import Data.Functor.Classes+import Data.Functor.Compose as Functor+import Data.Functor.Identity+import Data.Functor.Product as Functor+import Data.Functor.Reverse as Functor+import Data.Functor.Sum as Functor+import Data.Hashable+#if __GLASGOW_HASKELL__ < 710+import Data.Monoid+#endif+import Data.Ratio+#if __GLASGOW_HASKELL__ < 710+import Data.Traversable+#endif+import GHC.Arr++class Lifting p f where+  lifting :: p a :- p (f a)++instance Lifting Eq [] where lifting = Sub Dict+instance Lifting Ord [] where lifting = Sub Dict+instance Lifting Show [] where lifting = Sub Dict+instance Lifting Read [] where lifting = Sub Dict+instance Lifting Hashable [] where lifting = Sub Dict+instance Lifting Binary [] where lifting = Sub Dict+instance Lifting NFData [] where lifting = Sub Dict++instance Lifting Eq Maybe where lifting = Sub Dict+instance Lifting Ord Maybe where lifting = Sub Dict+instance Lifting Show Maybe where lifting = Sub Dict+instance Lifting Read Maybe where lifting = Sub Dict+instance Lifting Hashable Maybe where lifting = Sub Dict+instance Lifting Binary Maybe where lifting = Sub Dict+instance Lifting NFData Maybe where lifting = Sub Dict+instance Lifting Monoid Maybe where lifting = Sub Dict++instance Lifting Eq Ratio where lifting = Sub Dict+-- instance Lifting Show Ratio where lifting = Sub Dict -- requires 7.10++instance Lifting Eq Complex where lifting = Sub Dict+instance Lifting Read Complex where lifting = Sub Dict+instance Lifting Show Complex where lifting = Sub Dict++instance Lifting Monoid ((->) a) where lifting = Sub Dict++instance Eq a => Lifting Eq (Either a) where lifting = Sub Dict+instance Ord a => Lifting Ord (Either a) where lifting = Sub Dict+instance Show a => Lifting Show (Either a) where lifting = Sub Dict+instance Read a => Lifting Read (Either a) where lifting = Sub Dict+instance Hashable a => Lifting Hashable (Either a) where lifting = Sub Dict+instance Binary a => Lifting Binary (Either a) where lifting = Sub Dict+instance NFData a => Lifting NFData (Either a) where lifting = Sub Dict++instance Eq a => Lifting Eq ((,) a) where lifting = Sub Dict+instance Ord a => Lifting Ord ((,) a) where lifting = Sub Dict+instance Show a => Lifting Show ((,) a) where lifting = Sub Dict+instance Read a => Lifting Read ((,) a) where lifting = Sub Dict+instance Hashable a => Lifting Hashable ((,) a) where lifting = Sub Dict+instance Binary a => Lifting Binary ((,) a) where lifting = Sub Dict+instance NFData a => Lifting NFData ((,) a) where lifting = Sub Dict+instance Monoid a => Lifting Monoid ((,) a) where lifting = Sub Dict+instance Bounded a => Lifting Bounded ((,) a) where lifting = Sub Dict+instance Ix a => Lifting Ix ((,) a) where lifting = Sub Dict++instance Functor f => Lifting Functor (Compose f) where lifting = Sub Dict+instance Foldable f => Lifting Foldable (Compose f) where lifting = Sub Dict+instance Traversable f => Lifting Traversable (Compose f) where lifting = Sub Dict+instance Applicative f => Lifting Applicative (Compose f) where lifting = Sub Dict+instance Alternative f => Lifting Alternative (Compose f) where lifting = Sub Dict -- overconstrained+instance (Functor f, Show1 f) => Lifting Show1 (Compose f) where lifting = Sub Dict+instance (Functor f, Eq1 f) => Lifting Eq1 (Compose f) where lifting = Sub Dict+instance (Functor f, Ord1 f) => Lifting Ord1 (Compose f) where lifting = Sub Dict+instance (Functor f, Read1 f) => Lifting Read1 (Compose f) where lifting = Sub Dict+instance (Functor f, Eq1 f, Eq1 g) => Lifting Eq (Compose f g) where lifting = Sub Dict+instance (Functor f, Ord1 f, Ord1 g) => Lifting Ord (Compose f g) where lifting = Sub Dict+instance (Functor f, Read1 f, Read1 g) => Lifting Read (Compose f g) where lifting = Sub Dict+instance (Functor f, Show1 f, Show1 g) => Lifting Show (Compose f g) where lifting = Sub Dict++instance Functor f => Lifting Functor (Functor.Product f) where lifting = Sub Dict+instance Foldable f => Lifting Foldable (Functor.Product f) where lifting = Sub Dict+instance Traversable f => Lifting Traversable (Functor.Product f) where lifting = Sub Dict+instance Applicative f => Lifting Applicative (Functor.Product f) where lifting = Sub Dict+instance Alternative f => Lifting Alternative (Functor.Product f) where lifting = Sub Dict+instance Monad f => Lifting Monad (Functor.Product f) where lifting = Sub Dict+instance MonadFix f => Lifting MonadFix (Functor.Product f) where lifting = Sub Dict+instance MonadPlus f => Lifting MonadPlus (Functor.Product f) where lifting = Sub Dict+instance Show1 f => Lifting Show1 (Functor.Product f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq1 (Functor.Product f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord1 (Functor.Product f) where lifting = Sub Dict+instance Read1 f => Lifting Read1 (Functor.Product f) where lifting = Sub Dict+instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Product f g) where lifting = Sub Dict+instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Product f g) where lifting = Sub Dict+instance (Read1 f, Read1 g) => Lifting Read (Functor.Product f g) where lifting = Sub Dict+instance (Show1 f, Show1 g) => Lifting Show (Functor.Product f g) where lifting = Sub Dict++instance Functor f => Lifting Functor (Functor.Sum f) where lifting = Sub Dict+instance Foldable f => Lifting Foldable (Functor.Sum f) where lifting = Sub Dict+instance Traversable f => Lifting Traversable (Functor.Sum f) where lifting = Sub Dict+instance Show1 f => Lifting Show1 (Functor.Sum f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq1 (Functor.Sum f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord1 (Functor.Sum f) where lifting = Sub Dict+instance Read1 f => Lifting Read1 (Functor.Sum f) where lifting = Sub Dict+instance (Eq1 f, Eq1 g) => Lifting Eq (Functor.Sum f g) where lifting = Sub Dict+instance (Ord1 f, Ord1 g) => Lifting Ord (Functor.Sum f g) where lifting = Sub Dict+instance (Read1 f, Read1 g) => Lifting Read (Functor.Sum f g) where lifting = Sub Dict+instance (Show1 f, Show1 g) => Lifting Show (Functor.Sum f g) where lifting = Sub Dict++instance Lifting Functor (Strict.StateT s) where lifting = Sub Dict+instance Lifting Monad (Strict.StateT s) where lifting = Sub Dict+instance Lifting MonadFix (Strict.StateT s) where lifting = Sub Dict+instance Lifting MonadIO (Strict.StateT s) where lifting = Sub Dict+instance Lifting MonadPlus (Strict.StateT s) where lifting = Sub Dict++instance Lifting Functor (Lazy.StateT s) where lifting = Sub Dict+instance Lifting Monad (Lazy.StateT s) where lifting = Sub Dict+instance Lifting MonadFix (Lazy.StateT s) where lifting = Sub Dict+instance Lifting MonadIO (Lazy.StateT s) where lifting = Sub Dict+instance Lifting MonadPlus (Lazy.StateT s) where lifting = Sub Dict++instance Lifting Functor (Lazy.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting Monad (Lazy.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadFix (Lazy.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadPlus (Lazy.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadIO (Lazy.RWST r w s) where lifting = Sub Dict++instance Lifting Functor (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting Monad (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadFix (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadPlus (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadIO (Strict.RWST r w s) where lifting = Sub Dict++instance Lifting Functor (ReaderT e) where lifting = Sub Dict+instance Lifting Applicative (ReaderT e) where lifting = Sub Dict+instance Lifting Alternative (ReaderT e) where lifting = Sub Dict+instance Lifting Monad (ReaderT e) where lifting = Sub Dict+instance Lifting MonadPlus (ReaderT e) where lifting = Sub Dict+instance Lifting MonadFix (ReaderT e) where lifting = Sub Dict+instance Lifting MonadIO (ReaderT e) where lifting = Sub Dict++instance Lifting Functor (ErrorT e) where lifting = Sub Dict+instance Lifting Foldable (ErrorT e) where lifting = Sub Dict+instance Lifting Traversable (ErrorT e) where lifting = Sub Dict+instance Error e => Lifting Monad (ErrorT e) where lifting = Sub Dict+instance Error e => Lifting MonadFix (ErrorT e) where lifting = Sub Dict+instance Error e => Lifting MonadPlus (ErrorT e) where lifting = Sub Dict -- overconstrained!+instance Error e => Lifting MonadIO (ErrorT e) where lifting = Sub Dict+instance Show e => Lifting Show1 (ErrorT e) where lifting = Sub Dict+instance Eq e => Lifting Eq1 (ErrorT e) where lifting = Sub Dict+instance Ord e => Lifting Ord1 (ErrorT e) where lifting = Sub Dict+instance Read e => Lifting Read1 (ErrorT e) where lifting = Sub Dict+instance (Show e, Show1 m) => Lifting Show (ErrorT e m) where lifting = Sub Dict+instance (Eq e, Eq1 m) => Lifting Eq (ErrorT e m) where lifting = Sub Dict+instance (Ord e, Ord1 m) => Lifting Ord (ErrorT e m) where lifting = Sub Dict+instance (Read e, Read1 m) => Lifting Read (ErrorT e m) where lifting = Sub Dict++instance Lifting Functor (ExceptT e) where lifting = Sub Dict+instance Lifting Foldable (ExceptT e) where lifting = Sub Dict+instance Lifting Traversable (ExceptT e) where lifting = Sub Dict+instance Lifting Monad (ExceptT e) where lifting = Sub Dict+instance Lifting MonadFix (ExceptT e) where lifting = Sub Dict+instance Monoid e => Lifting MonadPlus (ExceptT e) where lifting = Sub Dict -- overconstrained!+instance Lifting MonadIO (ExceptT e) where lifting = Sub Dict+instance Show e => Lifting Show1 (ExceptT e) where lifting = Sub Dict+instance Eq e => Lifting Eq1 (ExceptT e) where lifting = Sub Dict+instance Ord e => Lifting Ord1 (ExceptT e) where lifting = Sub Dict+instance Read e => Lifting Read1 (ExceptT e) where lifting = Sub Dict+instance (Show e, Show1 m) => Lifting Show (ExceptT e m) where lifting = Sub Dict+instance (Eq e, Eq1 m) => Lifting Eq (ExceptT e m) where lifting = Sub Dict+instance (Ord e, Ord1 m) => Lifting Ord (ExceptT e m) where lifting = Sub Dict+instance (Read e, Read1 m) => Lifting Read (ExceptT e m) where lifting = Sub Dict++instance Lifting Functor (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Applicative (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Alternative (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Monad (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadFix (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadPlus (Strict.WriterT w) where lifting = Sub Dict+instance Lifting Foldable (Strict.WriterT w) where lifting = Sub Dict+instance Lifting Traversable (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadIO (Strict.WriterT w) where lifting = Sub Dict+instance Show w => Lifting Show1 (Strict.WriterT w) where lifting = Sub Dict+instance Eq w => Lifting Eq1 (Strict.WriterT w) where lifting = Sub Dict+instance Ord w => Lifting Ord1 (Strict.WriterT w) where lifting = Sub Dict+instance Read w => Lifting Read1 (Strict.WriterT w) where lifting = Sub Dict+instance (Show w, Show1 m) => Lifting Show (Strict.WriterT w m) where lifting = Sub Dict+instance (Eq w, Eq1 m) => Lifting Eq (Strict.WriterT w m) where lifting = Sub Dict+instance (Ord w, Ord1 m) => Lifting Ord (Strict.WriterT w m) where lifting = Sub Dict+instance (Read w, Read1 m) => Lifting Read (Strict.WriterT w m) where lifting = Sub Dict++instance Lifting Functor (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Applicative (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Alternative (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting Monad (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadFix (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadPlus (Lazy.WriterT w) where lifting = Sub Dict+instance Lifting Foldable (Lazy.WriterT w) where lifting = Sub Dict+instance Lifting Traversable (Lazy.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadIO (Lazy.WriterT w) where lifting = Sub Dict+instance Show w => Lifting Show1 (Lazy.WriterT w) where lifting = Sub Dict+instance Eq w => Lifting Eq1 (Lazy.WriterT w) where lifting = Sub Dict+instance Ord w => Lifting Ord1 (Lazy.WriterT w) where lifting = Sub Dict+instance Read w => Lifting Read1 (Lazy.WriterT w) where lifting = Sub Dict+instance (Show w, Show1 m) => Lifting Show (Lazy.WriterT w m) where lifting = Sub Dict+instance (Eq w, Eq1 m) => Lifting Eq (Lazy.WriterT w m) where lifting = Sub Dict+instance (Ord w, Ord1 m) => Lifting Ord (Lazy.WriterT w m) where lifting = Sub Dict+instance (Read w, Read1 m) => Lifting Read (Lazy.WriterT w m) where lifting = Sub Dict++instance Lifting Functor (ContT r) where lifting = Sub Dict -- overconstrained+instance Lifting Applicative (ContT r) where lifting = Sub Dict -- overconstrained+instance Lifting Monad (ContT r) where lifting = Sub Dict -- overconstrained+instance Lifting MonadIO (ContT r) where lifting = Sub Dict++instance Lifting Functor IdentityT where lifting = Sub Dict+instance Lifting Applicative IdentityT where lifting = Sub Dict+instance Lifting Alternative IdentityT where lifting = Sub Dict+instance Lifting Monad IdentityT where lifting = Sub Dict+instance Lifting MonadPlus IdentityT where lifting = Sub Dict+instance Lifting MonadFix IdentityT where lifting = Sub Dict+instance Lifting Foldable IdentityT where lifting = Sub Dict+instance Lifting Traversable IdentityT where lifting = Sub Dict+instance Lifting MonadIO IdentityT where lifting = Sub Dict+instance Lifting Show1 IdentityT where lifting = Sub Dict+instance Lifting Read1 IdentityT where lifting = Sub Dict+instance Lifting Ord1 IdentityT where lifting = Sub Dict+instance Lifting Eq1 IdentityT where lifting = Sub Dict+instance Show1 m => Lifting Show (IdentityT m) where lifting = Sub Dict+instance Read1 m => Lifting Read (IdentityT m) where lifting = Sub Dict+instance Ord1 m => Lifting Ord (IdentityT m) where lifting = Sub Dict+instance Eq1 m => Lifting Eq (IdentityT m) where lifting = Sub Dict++instance Lifting Functor ListT where lifting = Sub Dict+instance Lifting Applicative ListT where lifting = Sub Dict+instance Lifting Alternative ListT where lifting = Sub Dict -- overconstrained+instance Lifting Monad ListT where lifting = Sub Dict+-- instance Lifting MonadFix ListT where lifting = Sub Dict+instance Lifting MonadPlus ListT where lifting = Sub Dict -- overconstrained+instance Lifting Foldable ListT where lifting = Sub Dict+instance Lifting Traversable ListT where lifting = Sub Dict+instance Lifting MonadIO ListT where lifting = Sub Dict+instance Lifting Show1 ListT where lifting = Sub Dict+instance Lifting Read1 ListT where lifting = Sub Dict+instance Lifting Ord1 ListT where lifting = Sub Dict+instance Lifting Eq1 ListT where lifting = Sub Dict+instance Show1 m => Lifting Show (ListT m) where lifting = Sub Dict+instance Read1 m => Lifting Read (ListT m) where lifting = Sub Dict+instance Ord1 m => Lifting Ord (ListT m) where lifting = Sub Dict+instance Eq1 m => Lifting Eq (ListT m) where lifting = Sub Dict++instance Lifting Functor MaybeT where lifting = Sub Dict+instance Lifting Monad MaybeT where lifting = Sub Dict+-- instance Lifting MonadFix MaybeT where lifting = Sub Dict+instance Lifting MonadPlus MaybeT where lifting = Sub Dict -- overconstrained+instance Lifting Foldable MaybeT where lifting = Sub Dict+instance Lifting Traversable MaybeT where lifting = Sub Dict+instance Lifting MonadIO MaybeT where lifting = Sub Dict+instance Lifting Show1 MaybeT where lifting = Sub Dict+instance Lifting Read1 MaybeT where lifting = Sub Dict+instance Lifting Ord1 MaybeT where lifting = Sub Dict+instance Lifting Eq1 MaybeT where lifting = Sub Dict+instance Show1 m => Lifting Show (MaybeT m) where lifting = Sub Dict+instance Read1 m => Lifting Read (MaybeT m) where lifting = Sub Dict+instance Ord1 m => Lifting Ord (MaybeT m) where lifting = Sub Dict+instance Eq1 m => Lifting Eq (MaybeT m) where lifting = Sub Dict++instance Lifting Functor Reverse where lifting = Sub Dict+instance Lifting Applicative Reverse where lifting = Sub Dict+instance Lifting Alternative Reverse where lifting = Sub Dict+instance Lifting Foldable Reverse where lifting = Sub Dict+instance Lifting Traversable Reverse where lifting = Sub Dict+instance Lifting Show1 Reverse where lifting = Sub Dict+instance Lifting Read1 Reverse where lifting = Sub Dict+instance Lifting Ord1 Reverse where lifting = Sub Dict+instance Lifting Eq1 Reverse where lifting = Sub Dict+instance Show1 f => Lifting Show (Reverse f) where lifting = Sub Dict+instance Read1 f => Lifting Read (Reverse f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord (Reverse f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq (Reverse f) where lifting = Sub Dict++instance Lifting Functor Backwards where lifting = Sub Dict+instance Lifting Foldable Backwards where lifting = Sub Dict+instance Lifting Traversable Backwards where lifting = Sub Dict+instance Lifting Applicative Backwards where lifting = Sub Dict+instance Lifting Alternative Backwards where lifting = Sub Dict+instance Lifting Show1 Backwards where lifting = Sub Dict+instance Lifting Read1 Backwards where lifting = Sub Dict+instance Lifting Ord1 Backwards where lifting = Sub Dict+instance Lifting Eq1 Backwards where lifting = Sub Dict+instance Show1 f => Lifting Show (Backwards f) where lifting = Sub Dict+instance Read1 f => Lifting Read (Backwards f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord (Backwards f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq (Backwards f) where lifting = Sub Dict++instance Lifting Functor Lift where lifting = Sub Dict+instance Lifting Foldable Lift where lifting = Sub Dict+instance Lifting Traversable Lift where lifting = Sub Dict+instance Lifting Applicative Lift where lifting = Sub Dict+instance Lifting Alternative Lift where lifting = Sub Dict+instance Lifting Show1 Lift where lifting = Sub Dict+instance Lifting Read1 Lift where lifting = Sub Dict+instance Lifting Ord1 Lift where lifting = Sub Dict+instance Lifting Eq1 Lift where lifting = Sub Dict+instance Show1 f => Lifting Show (Lift f) where lifting = Sub Dict+instance Read1 f => Lifting Read (Lift f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord (Lift f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq (Lift f) where lifting = Sub Dict++instance Lifting Eq Identity where lifting = Sub Dict+instance Lifting Ord Identity where lifting = Sub Dict+instance Lifting Show Identity where lifting = Sub Dict+instance Lifting Read Identity where lifting = Sub Dict++instance Lifting MonadCont MaybeT where lifting = Sub Dict+instance Lifting MonadCont ListT where lifting = Sub Dict+instance Lifting MonadCont IdentityT where lifting = Sub Dict+instance Monoid w => Lifting MonadCont (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting MonadCont (Lazy.WriterT w) where lifting = Sub Dict+instance Error e => Lifting MonadCont (ErrorT e) where lifting = Sub Dict+instance Lifting MonadCont (ExceptT w) where lifting = Sub Dict+instance Lifting MonadCont (Strict.StateT s) where lifting = Sub Dict+instance Lifting MonadCont (Lazy.StateT s) where lifting = Sub Dict+instance Lifting MonadCont (ReaderT e) where lifting = Sub Dict+instance Monoid w => Lifting MonadCont (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting MonadCont (Lazy.RWST r w s) where lifting = Sub Dict++instance Lifting (MonadError e) MaybeT where lifting = Sub Dict+instance Lifting (MonadError e) ListT where lifting = Sub Dict+instance Lifting (MonadError e) IdentityT where lifting = Sub Dict+instance Monoid w => Lifting (MonadError e) (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting (MonadError e) (Lazy.WriterT w) where lifting = Sub Dict+instance Lifting (MonadError e) (Strict.StateT s) where lifting = Sub Dict+instance Lifting (MonadError e) (Lazy.StateT s) where lifting = Sub Dict+instance Lifting (MonadError e) (ReaderT r) where lifting = Sub Dict+instance Monoid w => Lifting (MonadError e) (Strict.RWST r w s) where lifting = Sub Dict+instance Monoid w => Lifting (MonadError e) (Lazy.RWST r w s) where lifting = Sub Dict++instance Lifting (MonadRWS r w s) MaybeT where lifting = Sub Dict+instance Lifting (MonadRWS r w s) IdentityT where lifting = Sub Dict+instance Error e => Lifting (MonadRWS r w s) (ErrorT e) where lifting = Sub Dict+instance Lifting (MonadRWS r w s) (ExceptT e) where lifting = Sub Dict++instance Lifting (MonadReader r) MaybeT where lifting = Sub Dict+instance Lifting (MonadReader r) ListT where lifting = Sub Dict+instance Lifting (MonadReader r) IdentityT where lifting = Sub Dict+instance Monoid w => Lifting (MonadReader r) (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting (MonadReader r) (Lazy.WriterT w) where lifting = Sub Dict+instance Lifting (MonadReader r) (Strict.StateT s) where lifting = Sub Dict+instance Lifting (MonadReader r) (Lazy.StateT s) where lifting = Sub Dict+instance Lifting (MonadReader r) (ExceptT e) where lifting = Sub Dict+instance Error e => Lifting (MonadReader r) (ErrorT e) where lifting = Sub Dict+instance Lifting (MonadReader r) (ContT r') where lifting = Sub Dict++instance Lifting (MonadState s) MaybeT where lifting = Sub Dict+instance Lifting (MonadState s) ListT where lifting = Sub Dict+instance Lifting (MonadState s) IdentityT where lifting = Sub Dict+instance Monoid w => Lifting (MonadState s) (Strict.WriterT w) where lifting = Sub Dict+instance Monoid w => Lifting (MonadState s) (Lazy.WriterT w) where lifting = Sub Dict+instance Lifting (MonadState s) (ReaderT r) where lifting = Sub Dict+instance Lifting (MonadState s) (ExceptT e) where lifting = Sub Dict+instance Error e => Lifting (MonadState s) (ErrorT e) where lifting = Sub Dict+instance Lifting (MonadState s) (ContT r') where lifting = Sub Dict++class Lifting2 p f where+  lifting2 :: p a :- Lifting p (f a) -- (p a, p b) :- p (f a b)++instance Lifting2 Eq Either where lifting2 = Sub Dict+instance Lifting2 Ord Either where lifting2 = Sub Dict+instance Lifting2 Show Either where lifting2 = Sub Dict+instance Lifting2 Read Either where lifting2 = Sub Dict+instance Lifting2 Hashable Either where lifting2 = Sub Dict+instance Lifting2 Binary Either where lifting2 = Sub Dict+instance Lifting2 NFData Either where lifting2 = Sub Dict++instance Lifting2 Eq (,) where lifting2 = Sub Dict+instance Lifting2 Ord (,) where lifting2 = Sub Dict+instance Lifting2 Show (,) where lifting2 = Sub Dict+instance Lifting2 Read (,) where lifting2 = Sub Dict+instance Lifting2 Hashable (,) where lifting2 = Sub Dict+instance Lifting2 Binary (,) where lifting2 = Sub Dict+instance Lifting2 NFData (,) where lifting2 = Sub Dict+instance Lifting2 Monoid (,) where lifting2 = Sub Dict+instance Lifting2 Bounded (,) where lifting2 = Sub Dict+instance Lifting2 Ix (,) where lifting2 = Sub Dict++instance Lifting2 Functor Compose where lifting2 = Sub Dict+instance Lifting2 Foldable Compose where lifting2 = Sub Dict+instance Lifting2 Traversable Compose where lifting2 = Sub Dict+instance Lifting2 Applicative Compose where lifting2 = Sub Dict+instance Lifting2 Alternative Compose where lifting2 = Sub Dict -- overconstrained++instance Lifting2 Functor Functor.Product where lifting2 = Sub Dict+instance Lifting2 Foldable Functor.Product where lifting2 = Sub Dict+instance Lifting2 Traversable Functor.Product where lifting2 = Sub Dict+instance Lifting2 Applicative Functor.Product where lifting2 = Sub Dict+instance Lifting2 Alternative Functor.Product where lifting2 = Sub Dict+instance Lifting2 Monad Functor.Product where lifting2 = Sub Dict+instance Lifting2 MonadPlus Functor.Product where lifting2 = Sub Dict+instance Lifting2 MonadFix Functor.Product where lifting2 = Sub Dict+instance Lifting2 Show1 Functor.Product where lifting2 = Sub Dict+instance Lifting2 Eq1 Functor.Product where lifting2 = Sub Dict+instance Lifting2 Ord1 Functor.Product where lifting2 = Sub Dict+instance Lifting2 Read1 Functor.Product where lifting2 = Sub Dict++instance Lifting2 Functor Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Foldable Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Traversable Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Show1 Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Eq1 Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Ord1 Functor.Sum where lifting2 = Sub Dict+instance Lifting2 Read1 Functor.Sum where lifting2 = Sub Dict

@@ -0,0 +1,65 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Unsafe #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.Constraint.Unsafe+-- Copyright   :  (C) 2011-2015 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  experimental+-- Portability :  non-portable+--+----------------------------------------------------------------------------+module Data.Constraint.Unsafe+  ( Coercible+  , unsafeCoerceConstraint+  , unsafeDerive+  , unsafeUnderive+  -- * Sugar+  , unsafeApplicative+  , unsafeAlternative+  ) where++import Control.Applicative+import Control.Monad+import Data.Constraint+import Unsafe.Coerce++#if __GLASGOW_HASKELL__ >= 708++import Data.Coerce++#else++import Control.Newtype++type Coercible = Newtype++#endif++-- | Coerce a dictionary unsafely from one type to another+unsafeCoerceConstraint :: a :- b+unsafeCoerceConstraint = unsafeCoerce refl++-- | Coerce a dictionary unsafely from one type to a newtype of that type+unsafeDerive :: Coercible n o => (o -> n) -> t o :- t n+unsafeDerive _ = unsafeCoerceConstraint++-- | Coerce a dictionary unsafely from a newtype of a type to the base type+unsafeUnderive :: Coercible n o => (o -> n) -> t n :- t o+unsafeUnderive _ = unsafeCoerceConstraint++-- | Construct an Applicative instance from a Monad+unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a+unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins++-- | Construct an Alternative instance from a MonadPlus+unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a+unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins