constraints 0.3.5 → 0.14.4
raw patch · 18 files changed
Files
- CHANGELOG.markdown +247/−0
- Data/Constraint.hs +0/−359
- Data/Constraint/Forall.hs +0/−69
- Data/Constraint/Unsafe.hs +0/−55
- LICENSE +1/−1
- README.markdown +2/−0
- constraints.cabal +65/−12
- src/Data/Constraint.hs +747/−0
- src/Data/Constraint/Char.hs +60/−0
- src/Data/Constraint/Deferrable.hs +82/−0
- src/Data/Constraint/Forall.hs +125/−0
- src/Data/Constraint/Lifting.hs +404/−0
- src/Data/Constraint/Nat.hs +396/−0
- src/Data/Constraint/Symbol.hs +138/−0
- src/Data/Constraint/Unsafe.hs +110/−0
- tests/GH117Spec.hs +34/−0
- tests/GH55Spec.hs +47/−0
- tests/Spec.hs +1/−0
+ CHANGELOG.markdown view
@@ -0,0 +1,247 @@+0.14.4 [2026.01.26]+-------------------+* Depend on `ghc-bignum` instead of `integer-gmp` on recent versions GHC.++0.14.3 [2026.01.10]+-------------------+* Remove unused `ghc-prim` dependency.++0.14.2 [2024.05.12]+-------------------+* Re-export `Log2` from `Data.Constraint.Nat`.+* Add `log2Nat` and `log2Pow` to `Data.Constraint.Nat`.++0.14.1 [2024.04.29]+-------------------+* Remove an unused dependency on the `type-equality` library.++0.14 [2023.10.11]+-----------------+* Drop support for GHCs older than 8.6.+* The `forall` function in `Data.Constraint.Forall` has been renamed to+ `forall_`, since a future version of GHC will make the use of `forall` as+ an identifier an error.+* Implement `Data.Constraint.Forall` using `QuantifiedConstraints`.+* Remove `Lifting` instances for `ErrorT` and `ListT`, which were removed+ in `transformers-0.6.*`.+* Add a `c => Boring (Dict c)` instance.+* Add the `Data.Constraint.Char` module, which contains utilities for working+ with `KnownChar` constraints. This module is only available on GHC 9.2 or+ later.+* Add `unsafeAxiom` to `Data.Constraint.Unsafe`.+* Add `unsafeSChar`, `unsafeSNat`, and `unsafeSSymbol` to+ `Data.Constraint.Unsafe` when building with `base-4.18` (GHC 9.6) or later.++0.13.4 [2022.05.19]+-------------------+* Correct the CPP introduced in `constraints-0.13.3` such that it works when+ building with `mtl-2.3.*` or later combined with `transformers < 0.6`.++0.13.3 [2022.01.31]+-------------------+* Allow building with `transformers-0.6.*` and `mtl-2.3.*`.++0.13.2 [2021.11.10]+-------------------+* Allow building on GHC HEAD.++0.13.1 [2021.10.31]+-------------------+* Allow building with GHC 9.2.++0.13 [2021.02.17]+-----------------+* `Data.Constraint.Symbol` now reexports the `GHC.TypeLits.AppendSymbol` type+ family from recent versions of `base` (or, on old versions of `base`, it+ defines a backwards-compatibile version of `AppendSymbol`). The existing+ `(++)` type family for `Data.Constraint.Symbol` is now a synonym for+ `AppendSymbol`.++ This is technically a breaking change, as `(++)` was previously defined like+ so:++ ```hs+ type family (++) :: Symbol -> Symbol -> Symbol+ ```++ This meant that `(++)` could be partially applied. However, for compatibility+ with the way that `AppendSymbol` is defined, `(++)` is now defined like so:++ ```hs+ type m ++ n = AppendSymbol m n+ ```++ As a result, `(++)` can no longer be partially applied.+* Make the `(++)` type family in `Data.Constraint.Symbol` be `infixr 5`.+* Add `implied :: (a => b) -> (a :- b)` to `Data.Constraint`, which converts+ a quantified constraint into an entailment. This is only available when+ compiled with GHC 8.6 or later.++0.12 [2020.02.03]+-----------------+* Relax the type signature for `divideTimes`:++ ```diff+ -dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)+ +dividesTimes :: Divides a b :- Divides a (b * c)+ ```++* Simplify the type signature of `dividesDef`:++ ```diff+ -dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)+ +dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)+ ```++ The original type of `diviesDef` can be (partially) recovered by defining+ it in terms of the new `dividesDef`:++ ```hs+ dividesDef' :: forall a b. (1 <= a, Divides a b) :- ((a * Div b a) ~ b)+ dividesDef' = Sub $ case (dividesDef @a @b, euclideanNat @a @b) of+ (Sub Dict, Sub Dict) -> Dict+ ```++0.11.2 [2019.09.06]+-------------------+* Depend on the `type-equality` compatibility library so that `(:~~:)` may be+ used when compiling this library with GHC 8.0. This avoids having to redefine+ `(:~~:)` directly in the internals of `constraints` itself.++0.11.1 [2019.08.27]+-------------------+* Make `Data.Constraint.Deferrable.UnsatisfiedConstraint` a newtype.++0.11 [2019.05.10]+-----------------+* Introduce a `HasDict` type class for types that witness evidence of+ constraints, such as `Dict`, `(:-)`, `Coercion`, `(:~:)`, `(:~~:)`, and+ `TypeRep`.+* Generalize the types of `withDict` and `(\\)` to be polymorphic over+ any `HasDict` instance.+* Add `type (⊢) = (:-)`.+* Fix unsafe mistakes in the statements of `dividesDef` and `timesDiv` in+ `Data.Constraint.Nat`.+* Make the implementations of `Min` and `Max` reduce on more inputs in+ `Data.Constraint.Nat`.+* Add `minusNat` and `minusZero` functions to `Data.Constraint.Nat`.+* Support `hashable-1.3.*` and `semigroups-0.19.*`.++0.10.1 [2018.07.02]+-------------------+* Allow building with GHC 8.6.+* Add three axioms about `(+)` and `(-)` to `Data.Constraint.Nat`.++0.10+----+* Adapt to the `Semigroup`–`Monoid` Proposal (introduced in `base-4.11`):+ * Add a `Semigroup` instance for `Dict`+ * Add the appropriate `(:=>)` instances involving `Semigroup`, and change the+ `Class () (Monoid a)` instance to `Class (Semigroup a) (Monoid a)` when+ `base` is recent enough+ * Add the appropriate `Lifting(2)` instances involving `Semigroup`+* `Data.Constraint.Nat` now reexports the `Div` and `Mod` type families from+ `GHC.TypeLits` on `base-4.11` or later+* Fix the type signature of `maxCommutes`+* Export the `no` method of `Bottom`+* Add `NFData` instances for `Dict` and `(:-)`++0.9.1+-----+* Correct an improper use of `unsafeCoerce` in the internals of+ `Data.Constraint.Nat` and `Data.Constraint.Symbol`+* Correctly identify the mismatched types when you defer an unsatisfiable+ equality constraint through `Data.Constraint.Deferrable`+* Re-export the `(:~~:)` defined in `base` from `Data.Constraint.Deferred` with+ GHC 8.2 or later+* Add several new `(:=>)` instances for `Bits`, `Identity`, `Const`, `Natural`,+ `IO`, and `Word`.+* Modernize some existing `Class` and `(:=>)` instances to reflect the fact+ that `Applicative` is now a superclass of `Monad` on recent versions of+ `base`.++0.9+---+* Changes to `Data.Constraint`:+ * Add `strengthen1` and `strengthen2`+* Changes to `Data.Constraint.Deferrable`:+ * Add a `Deferrable ()` instance+ * The `Deferrable (a ~ b)` instance now shows the `TypeRep`s of `a` and `b`+ when a type mismatch error is thrown+ * Add `defer_` and `deferEither_`, counterparts to `defer` and `deferEither`+ which do not require proxy arguments+ * Enable `PolyKinds`. This allows the `Deferrable (a ~ b)` instance to be+ polykinded on all supported versions of GHC _except_ 7.10, where the kinds+ must be `*` due to an old GHC bug+ * Introduce a heterogeneous equality type `(:~~:)`, and use it to define a+ `Deferrable (a ~~ b)` instance on GHC 8.0 or later+* Changes to `Data.Constraint.Forall`:+ * Implement `ForallF` and `ForallT` in terms of `Forall`+ * Add `ForallV` and `InstV` (supporting a variable number of parameters)+ * Add a `forall` combinator+* Introduce `Data.Constraint.Nat` and `Data.Constraint.Symbol`, which contain+ utilities for working with `KnownNat` and `KnownSymbol` constraints,+ respectively. These modules are only available on GHC 8.0 or later.++0.8+-----+* GHC 8 compatibility+* `transformers` 0.5 compatibility+* `binary` 0.8 compatibility+* Dropped support for GHC 7.6 in favor of a nicer Bottom representation.++0.7+---+* Found a nicer encoding of the initial object in the category of constraints using a [nullary constraint](https://ghc.haskell.org/trac/ghc/ticket/7642).++0.6.1+-----+* Remove the need for closed type families from the new `Forall`.++0.6+---+* Completely redesigned `Data.Constraint.Forall`. The old design is unsound and can be abused to define `unsafeCoerce`!+ The new design requires closed type families, so this module now requires GHC 7.8+++0.5.1+-----+* Added `Data.Constraint.Deferrable`.++0.5+-----+* Added `Data.Constraint.Lifting`.++0.4.1.3+-------+* Acknowledge we actually need at least base 4.5++0.4.1.2+-------+* Restore support for building on older GHCs++0.4.1.1+-------+* Minor documentation fixes.++0.4.1+-----+* Added `mapDict` and `unmapDict`.+* Added a lot of documentation.++0.4+---+* `Typeable` and `Data`. The `Data` instance for `(:-)` is a conservative approximation that avoids having to turn (:-) into a cartesian closed category.+ If it becomes a pain point for users, I know how to do that, and have done so in other libraries -- see [hask](http://github.com/ekmett/hask), but I'm hesitant to bring such heavy machinery to bear and it isn't clear how to do it in a way that is compatible with those other libraries.++0.3.5+-----+* Explicit role annotations++0.3.4.1+-------+* Fixed build failures.+* Fixed an unused import warning on older GHCs.++0.3.4+-----+* Added `bottom`
− Data/Constraint.hs
@@ -1,359 +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 RoleAnnotations #-}-#endif--------------------------------------------------------------------------------- |--- Module : Data.Constraint--- 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- (- -- * Constraints- Constraint- -- * Dictionary- , Dict(Dict)- -- * Entailment- , (:-)(Sub)- , (\\)- , weaken1, weaken2, contract- , (&&&), (***)- , trans, refl- , top, bottom- -- * 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-import GHC.Prim (Constraint)---- | Capture a dictionary for a given constraint-data Dict :: Constraint -> * where- Dict :: a => Dict a--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-type role Dict nominal-#endif--deriving instance Eq (Dict a)-deriving instance Ord (Dict a)-deriving instance Show (Dict a)--infixr 9 :--newtype a :- b = Sub (a => Dict b)-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-type role (:-) nominal nominal-#endif--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707-instance Category (:-) where- id = refl- (.) = trans-#endif--instance Eq (a :- b) where- _ == _ = True--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---- | due to the hack for the kind of (,) in the current version of GHC we can't actually--- make instances for (,) :: Constraint -> Constraint -> Constraint-(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)-f *** g = Sub $ Dict \\ f \\ g---- | Weakening a constraint product-weaken1 :: (a, b) :- a-weaken1 = Sub Dict---- | Weakening a constraint product-weaken2 :: (a, b) :- b-weaken2 = Sub Dict---- | Contracting a constraint / diagonal morphism-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---- ?--- / \--- (#) ?? ???--- / \ / \--- # * Constraint---- | 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---- | Every constraint implies truth------ These are the terminal arrows of the category, and () is the terminal object.-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 type you want.------ These are the initial arrows of the category and (() ~ Bool) is the initial object------ This demonstrates the law of classical logical <http://en.wikipedia.org/wiki/Principle_of_explosion ex falso quodlibet>-bottom :: (() ~ Bool) :- c-bottom = falso---- | Reify the relationship between a class and its superclass constraints as a class-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-class b :=> h | h -> b where- ins :: b :- h--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--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--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--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--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--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--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--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--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--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--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--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--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--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--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--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--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--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-
− Data/Constraint/Forall.hs
@@ -1,69 +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----------------------------------------------------------------------------------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-
− Data/Constraint/Unsafe.hs
@@ -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
LICENSE view
@@ -1,4 +1,4 @@-Copyright 2011-2013 Edward Kmett+Copyright 2011-2015 Edward Kmett All rights reserved.
README.markdown view
@@ -1,6 +1,8 @@ constraints =========== +[](https://hackage.haskell.org/package/constraints) [](https://github.com/ekmett/constraints/actions?query=workflow%3AHaskell-CI)+ This package provides data types and classes for manipulating the 'ConstraintKinds' exposed by GHC in 7.4. Contact Information
constraints.cabal view
@@ -1,28 +1,48 @@+cabal-version: 2.4 name: constraints category: Constraints-version: 0.3.5-license: BSD3-cabal-version: >= 1.10+version: 0.14.4+license: BSD-2-Clause license-file: LICENSE author: Edward A. Kmett maintainer: Edward A. Kmett <ekmett@gmail.com> stability: experimental homepage: http://github.com/ekmett/constraints/ bug-reports: http://github.com/ekmett/constraints/issues-copyright: Copyright (C) 2011-2013 Edward A. Kmett+copyright: Copyright (C) 2011-2021 Edward A. Kmett synopsis: Constraint manipulation-description: Constraint manipulation+description:+ GHC 7.4 gave us the ability to talk about @ConstraintKinds@. They stopped crashing the compiler in GHC 7.6.+ .+ This package provides a vocabulary for working with them.+ build-type: Simple-tested-with: GHC == 7.7.20131027, GHC == 7.7.20131025, GHC == 7.6.3++tested-with:+ GHC == 9.14.1+ GHC == 9.12.2+ GHC == 9.10.3+ GHC == 9.8.4+ GHC == 9.6.7+ GHC == 9.4.8+ GHC == 9.2.8+ GHC == 9.0.2+ GHC == 8.10.7+ GHC == 8.8.4+ GHC == 8.6.5+ extra-source-files: README.markdown+ , CHANGELOG.markdown source-repository head type: git- location: git://github.com/ekmett/constraints.git+ location: https://github.com/ekmett/constraints.git library+ hs-source-dirs: src+ default-language: Haskell2010- other-extensions+ other-extensions: FunctionalDependencies, ScopedTypeVariables, StandaloneDeriving,@@ -35,12 +55,45 @@ GADTs build-depends:- base >= 4.4 && < 5,- newtype >= 0.2 && < 0.3,- ghc-prim+ , base >= 4.12 && < 5+ , binary >= 0.7.1 && < 0.9+ , boring >= 0.2 && < 0.3+ , deepseq >= 1.3 && < 1.6+ , hashable >= 1.2 && < 1.6+ , mtl >= 2.2 && < 2.4+ , transformers >= 0.5 && < 0.7+ if impl(ghc >= 9.15)+ build-depends:+ ghc-bignum+ elif impl(ghc < 9.0)+ build-depends:+ integer-gmp+ exposed-modules: Data.Constraint+ Data.Constraint.Deferrable Data.Constraint.Forall+ Data.Constraint.Lifting+ Data.Constraint.Nat+ Data.Constraint.Symbol Data.Constraint.Unsafe - ghc-options: -Wall+ if impl(ghc >= 9.2)+ exposed-modules:+ Data.Constraint.Char++ ghc-options: -Wall -Wno-star-is-type++test-suite spec+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ hs-source-dirs: tests+ main-is: Spec.hs+ other-modules: GH55Spec+ GH117Spec+ ghc-options: -Wall -threaded -rtsopts+ build-tool-depends: hspec-discover:hspec-discover >= 2+ build-depends:+ , base+ , constraints+ , hspec >= 2
+ src/Data/Constraint.hs view
@@ -0,0 +1,747 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE UnicodeSyntax #-}++-- |+-- 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+--+-- <https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/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)+ , HasDict(..)+ , withDict+ , (\\)+ -- * Entailment+ , (:-)(Sub)+ , type (⊢)+ , type (|-)+ , type (&)+ , weaken1, weaken2, contract+ , strengthen1, strengthen2+ , (&&&), (***)+ , trans, refl+ , implied+ , Bottom(no)+ , top, bottom+ -- * Dict is fully faithful+ , mapDict+ , unmapDict+ -- * Reflection+ , Class(..)+ , (:=>)(..)+ ) where+import Control.Applicative+import Control.Category+import Control.DeepSeq+import Control.Monad+import Data.Complex+import Data.Ratio+import Data.Data hiding (TypeRep)+import qualified GHC.Exts as Exts (Any)+import GHC.Exts (Constraint)+import Data.Bits (Bits)+import Data.Functor.Identity (Identity)+import Numeric.Natural (Natural)+import Data.Coerce (Coercible)+import Data.Type.Coercion(Coercion(..))+import Data.Type.Equality (type (~~))+import qualified Data.Type.Equality as Hetero+import Type.Reflection (TypeRep, typeRepKind, withTypeable)+import Data.Boring (Boring (..))++-- | 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++deriving stock instance (Typeable p, p) => Data (Dict p)+deriving stock instance Eq (Dict a)+deriving stock instance Ord (Dict a)+deriving stock instance Show (Dict a)++instance c => Boring (Dict c) where+ boring = Dict++{-+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]+-}+++instance NFData (Dict c) where+ rnf Dict = ()++-- | Witnesses that a value of type @e@ contains evidence of the constraint @c@.+--+-- Mainly intended to allow ('\\') to be overloaded, since it's a useful operator.+class HasDict c e | e -> c where+ evidence :: e -> Dict c++instance HasDict a (Dict a) where+ evidence = Prelude.id++instance a => HasDict b (a :- b) where+ evidence (Sub x) = x++instance HasDict (Coercible a b) (Coercion a b) where+ evidence Coercion = Dict++instance HasDict (a ~ b) (a :~: b) where+ evidence Refl = Dict++instance HasDict (a ~~ b) (a Hetero.:~~: b) where+ evidence Hetero.HRefl = Dict++instance HasDict (Typeable k, Typeable a) (TypeRep (a :: k)) where+ evidence tr = withTypeable tr $ withTypeable (typeRepKind tr) Dict++-- | From a 'Dict', takes a value in an environment where the instance+-- witnessed by the 'Dict' is in scope, and evaluates it.+--+-- Essentially a deconstruction of a 'Dict' into its continuation-style+-- form.+--+-- Can also be used to deconstruct an entailment, @a ':-' b@, using a context @a@.+--+-- @+-- withDict :: 'Dict' c -> (c => r) -> r+-- withDict :: a => (a ':-' c) -> (c => r) -> r+-- @+withDict :: HasDict c e => e -> (c => r) -> r+withDict d r = case evidence d of+ Dict -> r++infixl 1 \\ -- required comment++-- | Operator version of 'withDict', with the arguments flipped+(\\) :: HasDict c e => (c => r) -> e -> r+r \\ d = withDict d r++infixr 9 :-+infixr 9 ⊢++-- | Type entailment, as written with a single character.+type (⊢) = (:-)++-- | 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 became 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 then 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)++type role (:-) nominal nominal++instance (Typeable p, Typeable q, p => q) => Data (p :- q) where+ gfoldl _ z d = z d+ gunfold _ z c = case constrIndex c of+ 1 -> z (Sub Dict)+ _ -> error "Data.Data.Data: Data.Constraint.:- constructor out of bounds"+ toConstr _ = subCon+ dataTypeOf _ = subTy++subCon :: Constr+subCon = mkConstr subTy "Sub Dict" [] Prefix+{-# noinline subCon #-}+subTy :: DataType+subTy = mkDataType "Data.Constraint.:-" [subCon]+{-# noinline subTy #-}++-- | Possible since GHC 7.8, when 'Category' was made polykinded.+instance Category (:-) where+ id = refl+ (.) = trans++-- | 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"++instance a => NFData (a :- b) where+ rnf (Sub Dict) = ()++--------------------------------------------------------------------------------+-- 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++--------------------------------------------------------------------------------+-- QuantifiedConstraints+--------------------------------------------------------------------------------++-- | Convert a quantified constraint into an entailment.+implied :: forall a b. (a => b) => a :- b+implied = Sub (Dict :: Dict b)++-- | The internal hom for the category of constraints.+--+-- This version can be passed around inside Dict, whereas (a => b) is impredicative+--+-- @+-- foo :: Dict (Ord a => Eq a)+-- foo = Dict+-- @+--+-- fails to typecheck due to the lack of impredicative polymorphism, but+--+-- @+-- foo :: Dict (Ord a |- Eq a)+-- foo = Dict+-- @+--+-- typechecks just fine.++class (p => q) => p |- q+instance (p => q) => p |- q+++--------------------------------------------------------------------------------+-- (,) 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 we can define+-- an equivalent type, that converts back and forth to @(,)@, and lets you hang instances.+class (p,q) => p & q+instance (p,q) => p & q++-- | 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++strengthen1 :: Dict b -> a :- c -> a :- (b,c)+strengthen1 d e = unmapDict (const d) &&& e++strengthen2 :: Dict b -> a :- c -> a :- (c,b)+strengthen2 d e = e &&& unmapDict (const d)++-- | 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++-- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance.+class Exts.Any => Bottom where+ no :: a++-- |+-- This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">+bottom :: Bottom :- a+bottom = Sub no++--------------------------------------------------------------------------------+-- 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)++type role Dict nominal++--------------------------------------------------------------------------------+-- 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+instance () :=> Eq Word where ins = Sub Dict+instance Eq a :=> Eq (Identity a) where ins = Sub Dict+instance Eq a :=> Eq (Const a b) where ins = Sub Dict+instance () :=> Eq Natural 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+instance () :=> Ord Word where ins = Sub Dict+instance Ord a :=> Ord (Identity a) where ins = Sub Dict+instance Ord a :=> Ord (Const a b) where ins = Sub Dict+instance () :=> Ord Natural 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 Int 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+instance () :=> Show Word where ins = Sub Dict+instance Show a :=> Show (Identity a) where ins = Sub Dict+instance Show a :=> Show (Const a b) where ins = Sub Dict+instance () :=> Show Natural 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 Int 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+instance () :=> Read Word where ins = Sub Dict+instance Read a :=> Read (Identity a) where ins = Sub Dict+instance Read a :=> Read (Const a b) where ins = Sub Dict+instance () :=> Read Natural 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+instance () :=> Enum Word where ins = Sub Dict+instance Enum a :=> Enum (Identity a) where ins = Sub Dict+instance Enum a :=> Enum (Const a b) where ins = Sub Dict+instance () :=> Enum Natural 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+instance () :=> Bounded Word where ins = Sub Dict+instance Bounded a :=> Bounded (Identity a) where ins = Sub Dict+instance Bounded a :=> Bounded (Const 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+instance () :=> Num Word where ins = Sub Dict+instance Num a :=> Num (Identity a) where ins = Sub Dict+instance Num a :=> Num (Const a b) where ins = Sub Dict+instance () :=> Num Natural 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+instance () :=> Real Word where ins = Sub Dict+instance Real a :=> Real (Identity a) where ins = Sub Dict+instance Real a :=> Real (Const a b) where ins = Sub Dict+instance () :=> Real Natural 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+instance () :=> Integral Word where ins = Sub Dict+instance Integral a :=> Integral (Identity a) where ins = Sub Dict+instance Integral a :=> Integral (Const a b) where ins = Sub Dict+instance () :=> Integral Natural where ins = Sub Dict++-- Bits+instance Class (Eq a) (Bits a) where cls = Sub Dict+instance () :=> Bits Bool where ins = Sub Dict+instance () :=> Bits Int where ins = Sub Dict+instance () :=> Bits Integer where ins = Sub Dict+instance () :=> Bits Word where ins = Sub Dict+instance Bits a :=> Bits (Identity a) where ins = Sub Dict+instance Bits a :=> Bits (Const a b) where ins = Sub Dict+instance () :=> Bits Natural 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+instance Fractional a :=> Fractional (Identity a) where ins = Sub Dict+instance Fractional a :=> Fractional (Const a b) 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+instance Floating a :=> Floating (Identity a) where ins = Sub Dict+instance Floating a :=> Floating (Const a b) 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+instance RealFrac a :=> RealFrac (Identity a) where ins = Sub Dict+instance RealFrac a :=> RealFrac (Const a b) 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+instance RealFloat a :=> RealFloat (Identity a) where ins = Sub Dict+instance RealFloat a :=> RealFloat (Const a b) where ins = Sub Dict++-- Semigroup+instance Class () (Semigroup a) where cls = Sub Dict+instance () :=> Semigroup () where ins = Sub Dict+instance () :=> Semigroup Ordering where ins = Sub Dict+instance () :=> Semigroup [a] where ins = Sub Dict+instance Semigroup a :=> Semigroup (Maybe a) where ins = Sub Dict+instance (Semigroup a, Semigroup b) :=> Semigroup (a, b) where ins = Sub Dict+instance Semigroup a :=> Semigroup (Const a b) where ins = Sub Dict+instance Semigroup a :=> Semigroup (Identity a) where ins = Sub Dict+instance Semigroup a :=> Semigroup (IO a) where ins = Sub Dict++-- Monoid+instance Class (Semigroup a) (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+instance Monoid a :=> Monoid (Const a b) where ins = Sub Dict+instance Monoid a :=> Monoid (Identity a) where ins = Sub Dict+instance Monoid a :=> Monoid (IO a) 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+instance () :=> Functor Identity where ins = Sub Dict+instance () :=> Functor (Const a) 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 Monoid a :=> Applicative (Const 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 (Applicative f) (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+instance () :=> Monad Identity where ins = Sub Dict++-- MonadPlus+instance Class (Monad f, Alternative 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 () :=> Semigroup (Dict a) where ins = Sub Dict+instance Semigroup (Dict a) where+ Dict <> Dict = Dict++instance a :=> Monoid (Dict a) where ins = Sub Dict+instance a => Monoid (Dict a) where+ mempty = Dict
+ src/Data/Constraint/Char.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE CPP #-}+-- | Utilities for working with 'KnownChar' constraints.+--+-- This module is only available on GHC 9.2 or later.+module Data.Constraint.Char+ ( CharToNat+ , NatToChar+ , charToNat+ , natToChar+ ) where++import Data.Char+import Data.Constraint+import Data.Proxy+import GHC.TypeLits+#if MIN_VERSION_base(4,18,0)+import Data.Constraint.Unsafe+import qualified GHC.TypeNats as TN+#else+import Unsafe.Coerce+#endif++-- implementation details++#if !MIN_VERSION_base(4,18,0)+newtype Magic c = Magic (KnownChar c => Dict (KnownChar c))+#endif++magicCN :: forall c n. (Char -> Int) -> KnownChar c :- KnownNat n+#if MIN_VERSION_base(4,18,0)+magicCN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (charVal (Proxy @c))))) Dict+#else+magicCN f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral @Int @Natural (f (charVal (Proxy @c))))+#endif++magicNC :: forall n c. (Int -> Char) -> KnownNat n :- KnownChar c+#if MIN_VERSION_base(4,18,0)+magicNC f = Sub $ withKnownChar (unsafeSChar @c (f (fromIntegral (natVal (Proxy @n))))) Dict+#else+magicNC f = Sub $ unsafeCoerce (Magic Dict) (f (fromIntegral (natVal (Proxy @n))))+#endif++-- operations++charToNat :: forall c. KnownChar c :- KnownNat (CharToNat c)+charToNat = magicCN ord++-- NB: 0x10FFFF the maximum value for a Unicode code point. Calling `chr` on+-- anything greater will throw an exception.+natToChar :: forall n. (n <= 0x10FFFF, KnownNat n) :- KnownChar (NatToChar n)+natToChar = Sub $ case magicNC @n @(NatToChar n) chr of Sub r -> r
+ src/Data/Constraint/Deferrable.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++-- |+-- Copyright : (C) 2015-2021 Edward Kmett+-- License : BSD-style (see the file LICENSE)+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : non-portable+--+-- The idea for this trick comes from Dimitrios Vytiniotis.++module Data.Constraint.Deferrable+ ( UnsatisfiedConstraint(..)+ , Deferrable(..)+ , defer+ , deferred+ , (:~~:)(HRefl)+ , (:~:)(Refl)+ ) where++import Control.Exception+import Control.Monad+import Data.Constraint+import Data.Proxy+import Data.Typeable (Typeable, cast, typeRep)+import Data.Type.Equality ((:~:)(Refl))++import Data.Type.Equality (type (~~), (:~~:)(HRefl))++newtype UnsatisfiedConstraint = UnsatisfiedConstraint String+ deriving Show++instance Exception UnsatisfiedConstraint++-- | Allow an attempt at resolution of a constraint at a later time+class Deferrable p where+ -- | Resolve a 'Deferrable' constraint with observable failure.+ deferEither :: (p => r) -> Either String r++deferred :: forall p. Deferrable p :- p+deferred = Sub $ defer @p Dict++defer :: forall p r. Deferrable p => (p => r) -> r+defer r = either (throw . UnsatisfiedConstraint) id $ deferEither @p r++showTypeRep :: forall t. Typeable t => String+showTypeRep = show $ typeRep (Proxy @t)++instance Deferrable () where+ deferEither r = Right r++-- | Deferrable homogeneous equality constraints.+--+-- Note that due to a GHC bug (https://ghc.haskell.org/trac/ghc/ticket/10343),+-- using this instance on GHC 7.10 will only work with @*@-kinded types.+instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where+ deferEither r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of+ Just Refl -> Right r+ Nothing -> Left $+ "deferred type equality: type mismatch between `" ++ showTypeRep @a ++ "’ and `" ++ showTypeRep @b ++ "'"++-- | 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 r = case cast (HRefl :: a :~~: a) :: Maybe (a :~~: b) of+ Just HRefl -> Right r+ Nothing -> Left $+ "deferred type equality: type mismatch between `" ++ showTypeRep @a ++ "’ and `" ++ showTypeRep @b ++ "'"++instance (Deferrable a, Deferrable b) => Deferrable (a, b) where+ deferEither r = join $ deferEither @a $ deferEither @b r++instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where+ deferEither r = join $ deferEither @a $ join $ deferEither @b $ deferEither @c r
+ src/Data/Constraint/Forall.hs view
@@ -0,0 +1,125 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE GADTs #-}++-- |+-- Copyright : (C) 2011-2021 Edward Kmett,+-- (C) 2015 Ørjan Johansen,+-- (C) 2016 David Feuer+-- 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+ , ForallV, InstV (instV)+ , forall_+ ) where++import Data.Constraint+import Unsafe.Coerce (unsafeCoerce)++class (forall a. p a) => Forall (p :: k -> Constraint)+instance (forall a. p a) => Forall (p :: k -> Constraint)++-- | Instantiate a quantified @'Forall' p@ constraint at type @a@.+inst :: forall p a. Forall p :- p a+inst = Sub Dict++data Dict1 p where+ Dict1 :: (forall a. p a) => Dict1 p++forallish :: forall p. Dict1 p -> Dict (Forall p)+forallish Dict1 = Dict++forall_ :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)+forall_ d = forallish (unsafeCoerce d)++-- | Composition for constraints.+class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)+instance p (f a) => ComposeC p f a++-- | A representation of the quantified constraint @forall a. p (f a)@.+class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)+instance Forall (ComposeC p f) => ForallF p f++-- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@.+instF :: forall p f a . ForallF p f :- p (f a)+instF = Sub $+ case inst :: Forall (ComposeC p f) :- ComposeC p f a of+ Sub Dict -> Dict++-- Classes building up to ForallT+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++-- | A representation of the quantified constraint @forall f a. p (t f a)@.+class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)+instance Forall (Q p t) => ForallT p t++-- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.+instT :: forall 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 = Sub $+ case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->+ case inst :: Forall (R p t f) :- R p t f a of+ Sub Dict -> Dict }++type Forall1 p = Forall p+-- | 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++-- | A representation of the quantified constraint+-- @forall a1 a2 ... an . p a1 a2 ... an@, supporting a variable number of+-- parameters.+type family ForallV :: k -> Constraint+type instance ForallV = ForallV_++class ForallV' p => ForallV_ (p :: k)+instance ForallV' p => ForallV_ p++-- | Instantiate a quantified @'ForallV' p@ constraint as @c@, where+-- @c ~ p a1 a2 ... an@.+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 = Sub Dict++-- Treating 1 argument specially rather than recursing as a bit of (premature?)+-- optimization+instance p a ~ c => InstV (p :: k -> Constraint) c where+ type ForallV' (p :: k -> Constraint) = Forall p+ instV = Sub $ case inst :: Forall p :- c of+ Sub Dict -> Dict++instance InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c where+ type ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p+ instV = Sub $ case instF :: ForallF ForallV p :- ForallV (p a) of+ Sub Dict -> case instV :: ForallV (p a) :- c of+ Sub Dict -> Dict+
+ src/Data/Constraint/Lifting.hs view
@@ -0,0 +1,404 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}++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.Except+import Control.Monad.Trans.Identity+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+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+import Data.Ratio+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 Semigroup 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 Semigroup ((->) a) 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 Semigroup a => Lifting Semigroup ((,) 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 Show1 f => Lifting Show1 (Compose f) where lifting = Sub Dict+instance Eq1 f => Lifting Eq1 (Compose f) where lifting = Sub Dict+instance Ord1 f => Lifting Ord1 (Compose f) where lifting = Sub Dict+instance Read1 f => Lifting Read1 (Compose f) where lifting = Sub Dict+instance (Eq1 f, Eq1 g) => Lifting Eq (Compose f g) where lifting = Sub Dict+instance (Ord1 f, Ord1 g) => Lifting Ord (Compose f g) where lifting = Sub Dict+instance (Read1 f, Read1 g) => Lifting Read (Compose f g) where lifting = Sub Dict+instance (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 (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 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 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 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) 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 Lifting (MonadRWS r w s) (ExceptT e) where lifting = Sub Dict++instance Lifting (MonadReader r) MaybeT 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 Lifting (MonadReader r) (ContT r') where lifting = Sub Dict++instance Lifting (MonadState s) MaybeT 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 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 Semigroup (,) 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
+ src/Data/Constraint/Nat.hs view
@@ -0,0 +1,396 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoStarIsType #-}+-- | Utilities for working with 'KnownNat' constraints.+--+-- This module is only available on GHC 8.0 or later.+module Data.Constraint.Nat+ ( Min, Max, Lcm, Gcd, Divides, Div, Mod, Log2+ , plusNat, minusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat, log2Nat+ , plusZero, minusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne+ , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates+ , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes+ , plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm+ , minDistributesOverPlus, minDistributesOverTimes, minDistributesOverPow1, minDistributesOverPow2, minDistributesOverMax+ , maxDistributesOverPlus, maxDistributesOverTimes, maxDistributesOverPow1, maxDistributesOverPow2, maxDistributesOverMin+ , gcdDistributesOverLcm, lcmDistributesOverGcd+ , minIsIdempotent, maxIsIdempotent, lcmIsIdempotent, gcdIsIdempotent+ , plusIsCancellative, timesIsCancellative+ , dividesPlus, dividesTimes, dividesMin, dividesMax, dividesPow, dividesGcd, dividesLcm+ , plusMonotone1, plusMonotone2+ , timesMonotone1, timesMonotone2+ , powMonotone1, powMonotone2+ , minMonotone1, minMonotone2+ , maxMonotone1, maxMonotone2+ , divMonotone1, divMonotone2+ , euclideanNat+ , plusMod, timesMod+ , modBound+ , log2Pow+ , dividesDef+ , timesDiv+ , eqLe, leEq, leId, leTrans+ , leZero, zeroLe+ , plusMinusInverse1, plusMinusInverse2, plusMinusInverse3+ ) where++import Data.Constraint+import Data.Constraint.Unsafe+import Data.Proxy+import Data.Type.Bool+import GHC.TypeNats+import qualified Numeric.Natural as Nat++#if MIN_VERSION_base(4,15,0)+import GHC.Num.Natural (naturalLog2)+#else+import GHC.Exts (Int(..))+import GHC.Integer.Logarithms (integerLog2#)+#endif++#if !MIN_VERSION_base(4,18,0)+import Unsafe.Coerce+#endif++type family Min (m::Nat) (n::Nat) :: Nat where+ Min m n = If (n <=? m) n m+type family Max (m::Nat) (n::Nat) :: Nat where+ Max m n = If (n <=? m) m n+type family Gcd (m::Nat) (n::Nat) :: Nat where+ Gcd m m = m+type family Lcm (m::Nat) (n::Nat) :: Nat where+ Lcm m m = m++type Divides n m = n ~ Gcd n m++#if !MIN_VERSION_base(4,18,0)+newtype Magic n = Magic (KnownNat n => Dict (KnownNat n))+#endif++magicNNN :: forall n m o. (Nat.Natural -> Nat.Natural -> Nat.Natural) -> (KnownNat n, KnownNat m) :- KnownNat o+#if MIN_VERSION_base(4,18,0)+magicNNN f = Sub $ withKnownNat @o (unsafeSNat (natVal (Proxy @n) `f` natVal (Proxy @m))) Dict+#else+magicNNN f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy @n) `f` natVal (Proxy @m))+#endif++magicNN :: forall n m. (Nat.Natural -> Nat.Natural) -> KnownNat n :- KnownNat m+#if MIN_VERSION_base(4,18,0)+magicNN f = Sub $ withKnownNat @m (unsafeSNat (f (natVal (Proxy @n)))) Dict+#else+magicNN f = Sub $ unsafeCoerce (Magic Dict) (f (natVal (Proxy :: Proxy n)))+#endif++axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)+axiomLe = unsafeAxiom++eqLe :: forall (a :: Nat) (b :: Nat). (a ~ b) :- (a <= b)+eqLe = Sub Dict++dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)+dividesGcd = Sub unsafeAxiom++dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c+dividesLcm = Sub unsafeAxiom++gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)+gcdCommutes = unsafeAxiom++lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)+lcmCommutes = unsafeAxiom++gcdZero :: forall a. Dict (Gcd 0 a ~ a)+gcdZero = unsafeAxiom++gcdOne :: forall a. Dict (Gcd 1 a ~ 1)+gcdOne = unsafeAxiom++lcmZero :: forall a. Dict (Lcm 0 a ~ 0)+lcmZero = unsafeAxiom++lcmOne :: forall a. Dict (Lcm 1 a ~ a)+lcmOne = unsafeAxiom++gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)+gcdNat = magicNNN gcd++lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)+lcmNat = magicNNN lcm++plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)+plusNat = magicNNN (+)++minusNat :: forall n m. (KnownNat n, KnownNat m, m <= n) :- KnownNat (n - m)+minusNat = Sub $ case magicNNN @n @m (-) of Sub r -> r++minNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)+minNat = magicNNN min++maxNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)+maxNat = magicNNN max++timesNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)+timesNat = magicNNN (*)++powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)+powNat = magicNNN (^)++divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)+divNat = Sub $ case magicNNN @n @m div of Sub r -> r++modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)+modNat = Sub $ case magicNNN @n @m mod of Sub r -> r++log2Nat :: forall n. (KnownNat n, 1 <= n) :- KnownNat (Log2 n)+log2Nat = Sub $ case magicNN @n log2 of Sub r -> r+ where+ log2 :: Nat.Natural -> Nat.Natural+#if MIN_VERSION_base(4,15,0)+ log2 n = fromIntegral (naturalLog2 n)+#else+ log2 n = fromIntegral (I# (integerLog2# (toInteger n)))+#endif++plusZero :: forall n. Dict ((n + 0) ~ n)+plusZero = Dict++minusZero :: forall n. Dict ((n - 0) ~ n)+minusZero = Dict++timesZero :: forall n. Dict ((n * 0) ~ 0)+timesZero = Dict++timesOne :: forall n. Dict ((n * 1) ~ n)+timesOne = Dict++minZero :: forall n. Dict (Min n 0 ~ 0)+#if MIN_VERSION_base(4,16,0)+minZero = unsafeAxiom+#else+minZero = Dict+#endif++maxZero :: forall n. Dict (Max n 0 ~ n)+#if MIN_VERSION_base(4,16,0)+maxZero = unsafeAxiom+#else+maxZero = Dict+#endif++powZero :: forall n. Dict ((n ^ 0) ~ 1)+powZero = Dict++leZero :: forall a. (a <= 0) :- (a ~ 0)+leZero = Sub unsafeAxiom++zeroLe :: forall (a :: Nat). Dict (0 <= a)+#if MIN_VERSION_base(4,16,0)+zeroLe = unsafeAxiom+#else+zeroLe = Dict+#endif++plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)+plusMinusInverse1 = unsafeAxiom++plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)+plusMinusInverse2 = Sub unsafeAxiom++plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)+plusMinusInverse3 = Sub unsafeAxiom++plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)+plusMonotone1 = Sub unsafeAxiom++plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)+plusMonotone2 = Sub unsafeAxiom++powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))+powMonotone1 = Sub unsafeAxiom++powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))+powMonotone2 = Sub unsafeAxiom++divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)+divMonotone1 = Sub unsafeAxiom++divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)+divMonotone2 = Sub unsafeAxiom++timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)+timesMonotone1 = Sub unsafeAxiom++timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)+timesMonotone2 = Sub unsafeAxiom++minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)+minMonotone1 = Sub unsafeAxiom++minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)+minMonotone2 = Sub unsafeAxiom++maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)+maxMonotone1 = Sub unsafeAxiom++maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)+maxMonotone2 = Sub unsafeAxiom++powOne :: forall n. Dict ((n ^ 1) ~ n)+powOne = unsafeAxiom++plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)+plusMod = Sub unsafeAxiom++timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)+timesMod = Sub unsafeAxiom++modBound :: forall m n. (1 <= n) :- (Mod m n <= n)+modBound = Sub unsafeAxiom++log2Pow :: forall n. Dict (Log2 (2 ^ n) ~ n)+log2Pow = unsafeAxiom++euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))+euclideanNat = Sub unsafeAxiom++plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))+plusCommutes = unsafeAxiom++timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))+timesCommutes = unsafeAxiom++minCommutes :: forall n m. Dict (Min m n ~ Min n m)+minCommutes = unsafeAxiom++maxCommutes :: forall n m. Dict (Max m n ~ Max n m)+maxCommutes = unsafeAxiom++plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))+plusAssociates = unsafeAxiom++timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))+timesAssociates = unsafeAxiom++minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))+minAssociates = unsafeAxiom++maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))+maxAssociates = unsafeAxiom++gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c))+gcdAssociates = unsafeAxiom++lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))+lcmAssociates = unsafeAxiom++minIsIdempotent :: forall n. Dict (Min n n ~ n)+minIsIdempotent = Dict++maxIsIdempotent :: forall n. Dict (Max n n ~ n)+maxIsIdempotent = Dict++gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)+gcdIsIdempotent = Dict++lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)+lcmIsIdempotent = Dict++minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))+minDistributesOverPlus = unsafeAxiom++minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))+minDistributesOverTimes = unsafeAxiom++minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))+minDistributesOverPow1 = unsafeAxiom++minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))+minDistributesOverPow2 = unsafeAxiom++minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))+minDistributesOverMax = unsafeAxiom++maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))+maxDistributesOverPlus = unsafeAxiom++maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))+maxDistributesOverTimes = unsafeAxiom++maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))+maxDistributesOverPow1 = unsafeAxiom++maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))+maxDistributesOverPow2 = unsafeAxiom++maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))+maxDistributesOverMin = unsafeAxiom++plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))+plusDistributesOverTimes = unsafeAxiom++timesDistributesOverPow :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))+timesDistributesOverPow = unsafeAxiom++timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))+timesDistributesOverGcd = unsafeAxiom++timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))+timesDistributesOverLcm = unsafeAxiom++plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)+plusIsCancellative = Sub unsafeAxiom++timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)+timesIsCancellative = Sub unsafeAxiom++gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))+gcdDistributesOverLcm = unsafeAxiom++lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))+lcmDistributesOverGcd = unsafeAxiom++dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)+dividesPlus = Sub unsafeAxiom++dividesTimes :: Divides a b :- Divides a (b * c)+dividesTimes = Sub unsafeAxiom++dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)+dividesMin = Sub unsafeAxiom++dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)+dividesMax = Sub unsafeAxiom++-- This `dividesDef` is simpler and more convenient than Divides a b :- ((a * Div b a) ~ b)+-- because the latter can be easily derived via 'euclideanNat', but not vice versa.++dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)+dividesDef = Sub unsafeAxiom++dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)+dividesPow = Sub unsafeAxiom++timesDiv :: forall a b. Dict ((a * Div b a) <= b)+timesDiv = unsafeAxiom++-- (<=) is an internal category in the category of constraints.++leId :: forall (a :: Nat). Dict (a <= a)+leId = Dict++leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)+leEq = Sub unsafeAxiom++leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c)+leTrans = Sub (axiomLe @a @c)
+ src/Data/Constraint/Symbol.hs view
@@ -0,0 +1,138 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE CPP #-}+-- | Utilities for working with 'KnownSymbol' constraints.+module Data.Constraint.Symbol+ ( type AppendSymbol+ , type (++)+ , type Take+ , type Drop+ , type Length+ , appendSymbol+ , appendUnit1+ , appendUnit2+ , appendAssociates+ , takeSymbol+ , dropSymbol+ , takeAppendDrop+ , lengthSymbol+ , takeLength+ , take0+ , takeEmpty+ , dropLength+ , drop0+ , dropEmpty+ , lengthTake+ , lengthDrop+ , dropDrop+ , takeTake+ ) where++import Data.Constraint+import Data.Constraint.Nat+import Data.Constraint.Unsafe+import Data.Proxy+import GHC.TypeLits+#if MIN_VERSION_base(4,18,0)+import qualified GHC.TypeNats as TN+#else+import Unsafe.Coerce+#endif++-- | An infix synonym for 'AppendSymbol'.+type (m :: Symbol) ++ (n :: Symbol) = AppendSymbol m n+infixr 5 ++++type family Take :: Nat -> Symbol -> Symbol where+type family Drop :: Nat -> Symbol -> Symbol where+type family Length :: Symbol -> Nat where++-- implementation details++#if !MIN_VERSION_base(4,18,0)+newtype Magic n = Magic (KnownSymbol n => Dict (KnownSymbol n))+#endif++magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o+#if MIN_VERSION_base(4,18,0)+magicNSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))) Dict+#else+magicNSS f = Sub $ unsafeCoerce (Magic Dict) (fromIntegral (natVal (Proxy @n)) `f` symbolVal (Proxy @m))+#endif++magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o+#if MIN_VERSION_base(4,18,0)+magicSSS f = Sub $ withKnownSymbol (unsafeSSymbol @o (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))) Dict+#else+magicSSS f = Sub $ unsafeCoerce (Magic Dict) (symbolVal (Proxy @n) `f` symbolVal (Proxy @m))+#endif++magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n+#if MIN_VERSION_base(4,18,0)+magicSN f = Sub $ TN.withKnownNat (unsafeSNat @n (fromIntegral (f (symbolVal (Proxy :: Proxy a))))) Dict+#else+magicSN f = Sub $ unsafeCoerce (Magic Dict) (toInteger (f (symbolVal (Proxy @a))))+#endif++-- operations++appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)+appendSymbol = magicSSS (++)++appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)+appendUnit1 = Dict++appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)+appendUnit2 = Dict++appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))+appendAssociates = unsafeAxiom++takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)+takeSymbol = magicNSS take++dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)+dropSymbol = magicNSS drop++takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)+takeAppendDrop = unsafeAxiom++lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)+lengthSymbol = magicSN length++takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)+takeLength = Sub unsafeAxiom++take0 :: forall a. Dict (Take 0 a ~ "")+take0 = unsafeAxiom++takeEmpty :: forall n. Dict (Take n "" ~ "")+takeEmpty = unsafeAxiom++dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")+dropLength = Sub unsafeAxiom++drop0 :: forall a. Dict (Drop 0 a ~ a)+drop0 = unsafeAxiom++dropEmpty :: forall n. Dict (Drop n "" ~ "")+dropEmpty = unsafeAxiom++lengthTake :: forall n a. Dict (Length (Take n a) <= n)+lengthTake = unsafeAxiom++lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))+lengthDrop = unsafeAxiom++dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)+dropDrop = unsafeAxiom++takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)+takeTake = unsafeAxiom
+ src/Data/Constraint/Unsafe.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Unsafe #-}+{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}++-- |+-- Copyright : (C) 2011-2021 Edward Kmett+-- License : BSD-style (see the file LICENSE)+-- Maintainer : Edward Kmett <ekmett@gmail.com>+-- Stability : experimental+-- Portability : non-portable+--+-- Unsafe utilities used throughout @constraints@. As the names suggest, these+-- functions are unsafe in general and can cause your program to segfault if+-- used improperly. Handle with care.++module Data.Constraint.Unsafe+ ( Coercible+ , unsafeAxiom+ , unsafeCoerceConstraint+ , unsafeDerive+ , unsafeUnderive++#if MIN_VERSION_base(4,18,0)+ -- * Unsafely creating @GHC.TypeLits@ singleton values+ , unsafeSChar+ , unsafeSNat+ , unsafeSSymbol+#endif+ ) where++import Data.Coerce+import Data.Constraint+import Unsafe.Coerce++#if MIN_VERSION_base(4,18,0)+import GHC.TypeLits (SChar, SNat, SSymbol)+import Numeric.Natural (Natural)+#endif++-- | Unsafely create a dictionary for any constraint.+unsafeAxiom :: Dict c+unsafeAxiom = unsafeCoerce (Dict :: Dict ())++-- | 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++#if MIN_VERSION_base(4,18,0)+-- NB: if https://gitlab.haskell.org/ghc/ghc/-/issues/23478 were implemented,+-- then we could avoid using 'unsafeCoerce' in the definitions below.++-- | Unsafely create an 'SChar' value directly from a 'Char'. Use this function+-- with care:+--+-- * The 'Char' value must match the 'Char' @c@ encoded in the return type+-- @'SChar' c@.+--+-- * Be wary of using this function to create multiple values of type+-- @'SChar' T@, where @T@ is a type family that does not reduce (e.g.,+-- @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of+-- the values and replace it with the other during a common subexpression+-- elimination pass. If the two values have different underlying 'Char'+-- values, this could be disastrous.+unsafeSChar :: Char -> SChar c+unsafeSChar = unsafeCoerce++-- | Unsafely create an 'SNat' value directly from a 'Natural'. Use this+-- function with care:+--+-- * The 'Natural' value must match the 'Nat' @n@ encoded in the return type+-- @'SNat' n@.+--+-- * Be wary of using this function to create multiple values of type+-- @'SNat' T@, where @T@ is a type family that does not reduce (e.g.,+-- @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of+-- the values and replace it with the other during a common subexpression+-- elimination pass. If the two values have different underlying 'Natural'+-- values, this could be disastrous.+unsafeSNat :: Natural -> SNat n+unsafeSNat = unsafeCoerce++-- | Unsafely create an 'SSymbol' value directly from a 'String'. Use this+-- function with care:+--+-- * The 'String' value must match the 'Symbol' @s@ encoded in the return type+-- @'SSymbol' s@.+--+-- * Be wary of using this function to create multiple values of type+-- @'SSymbol' T@, where @T@ is a type family that does not reduce (e.g.,+-- @Any@ from "GHC.Exts"). If you do, GHC is liable to optimize away one of+-- the values and replace it with the other during a common subexpression+-- elimination pass. If the two values have different underlying 'String'+-- values, this could be disastrous.+unsafeSSymbol :: String -> SSymbol s+unsafeSSymbol = unsafeCoerce+#endif
+ tests/GH117Spec.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module GH117Spec (main, spec) where++import Test.Hspec++#if __GLASGOW_HASKELL__ >= 902+import Data.Constraint+import Data.Constraint.Char+import Data.Proxy+import GHC.TypeLits++spec :: Spec+spec =+ describe "GH #117" $ do+ it "should evaluate `charToNat @'a'` to 97" $+ case charToNat @'a' of+ Sub (Dict :: Dict (KnownNat n)) ->+ natVal (Proxy @n) `shouldBe` 97+ it "should evaluate `natToChar @97` to 'a'" $+ case natToChar @97 of+ Sub (Dict :: Dict (KnownChar c)) ->+ charVal (Proxy @c) `shouldBe` 'a'+#else+spec :: Spec+spec = return ()+#endif++main :: IO ()+main = hspec spec
+ tests/GH55Spec.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}++module GH55Spec (main, spec) where++import Data.Constraint+import Data.Constraint.Nat+import GHC.TypeLits+import Test.Hspec++newtype GF (n :: Nat) = GF Integer deriving (Eq, Show)++instance KnownNat n => Num (GF n) where+ xf@(GF a) + GF b = GF $ (a+b) `mod` (natVal xf)+ xf@(GF a) - GF b = GF $ (a-b) `mod` (natVal xf)+ xf@(GF a) * GF b = GF $ (a*b) `mod` (natVal xf)+ abs = id+ signum xf@(GF a) | a==0 = xf+ | otherwise = GF 1+ fromInteger = GF++x :: GF 5+x = GF 3++y :: GF 5+y = GF 4++foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)+foo m@(GF a) n@(GF b) = GF $ (a*b) `mod` (lcm (natVal m) (natVal n))++bar :: (KnownNat m) => GF m -> GF m -> GF m+bar (a :: GF m) b = foo a b - foo b a \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m++z :: GF 5+z = bar x y++spec :: Spec+spec = describe "GH #53" $+ it "should normalize Lcm m m" $+ z `shouldBe` (GF 0 :: GF (Lcm 5 5))++main :: IO ()+main = hspec spec
+ tests/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}