Hello community, here is the log from the commit of package ghc-constraints for openSUSE:Factory checked in at 2017-03-14 10:04:32 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/ghc-constraints (Old) and /work/SRC/openSUSE:Factory/.ghc-constraints.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "ghc-constraints" Tue Mar 14 10:04:32 2017 rev:5 rq:461618 version:0.9 Changes: -------- --- /work/SRC/openSUSE:Factory/ghc-constraints/ghc-constraints.changes 2016-07-21 08:14:53.000000000 +0200 +++ /work/SRC/openSUSE:Factory/.ghc-constraints.new/ghc-constraints.changes 2017-03-14 10:04:34.081190767 +0100 @@ -1,0 +2,5 @@ +Sun Feb 12 14:08:44 UTC 2017 - [email protected] + +- Update to version 0.9 with cabal2obs. + +------------------------------------------------------------------- Old: ---- constraints-0.8.tar.gz New: ---- constraints-0.9.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ ghc-constraints.spec ++++++ --- /var/tmp/diff_new_pack.dnu0Yn/_old 2017-03-14 10:04:34.697103553 +0100 +++ /var/tmp/diff_new_pack.dnu0Yn/_new 2017-03-14 10:04:34.701102988 +0100 @@ -1,7 +1,7 @@ # # spec file for package ghc-constraints # -# Copyright (c) 2016 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2017 SUSE LINUX GmbH, Nuernberg, Germany. # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -18,15 +18,14 @@ %global pkg_name constraints Name: ghc-%{pkg_name} -Version: 0.8 +Version: 0.9 Release: 0 Summary: Constraint manipulation License: BSD-2-Clause -Group: System/Libraries +Group: Development/Languages/Other Url: https://hackage.haskell.org/package/%{pkg_name} Source0: https://hackage.haskell.org/package/%{pkg_name}-%{version}/%{pkg_name}-%{version}.tar.gz BuildRequires: ghc-Cabal-devel -# Begin cabal-rpm deps: BuildRequires: ghc-binary-devel BuildRequires: ghc-deepseq-devel BuildRequires: ghc-hashable-devel @@ -35,7 +34,6 @@ BuildRequires: ghc-transformers-compat-devel BuildRequires: ghc-transformers-devel BuildRoot: %{_tmppath}/%{name}-%{version}-build -# End cabal-rpm deps %description GHC 7.4 gave us the ability to talk about 'ConstraintKinds'. They stopped @@ -57,15 +55,12 @@ %prep %setup -q -n %{pkg_name}-%{version} - %build %ghc_lib_build - %install %ghc_lib_install - %post devel %ghc_pkg_recache @@ -78,6 +73,6 @@ %files devel -f %{name}-devel.files %defattr(-,root,root,-) -%doc README.markdown +%doc CHANGELOG.markdown README.markdown %changelog ++++++ constraints-0.8.tar.gz -> constraints-0.9.tar.gz ++++++ diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/CHANGELOG.markdown new/constraints-0.9/CHANGELOG.markdown --- old/constraints-0.8/CHANGELOG.markdown 1970-01-01 01:00:00.000000000 +0100 +++ new/constraints-0.9/CHANGELOG.markdown 2017-01-26 03:31:25.000000000 +0100 @@ -0,0 +1,85 @@ +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` diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/README.markdown new/constraints-0.9/README.markdown --- old/constraints-0.8/README.markdown 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/README.markdown 2017-01-26 03:31:25.000000000 +0100 @@ -1,6 +1,8 @@ constraints =========== +[](https://hackage.haskell.org/package/constraints) [](http://travis-ci.org/ekmett/constraints) + This package provides data types and classes for manipulating the 'ConstraintKinds' exposed by GHC in 7.4. Contact Information diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/constraints.cabal new/constraints-0.9/constraints.cabal --- old/constraints-0.8/constraints.cabal 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/constraints.cabal 2017-01-26 03:31:25.000000000 +0100 @@ -1,7 +1,7 @@ name: constraints category: Constraints -version: 0.8 -license: BSD3 +version: 0.9 +license: BSD2 cabal-version: >= 1.10 license-file: LICENSE author: Edward A. Kmett @@ -17,8 +17,9 @@ This package provides a vocabulary for working with them. build-type: Simple -tested-with: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.1, GHC == 7.10.2 +tested-with: GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2 extra-source-files: README.markdown + , CHANGELOG.markdown source-repository head type: git @@ -50,11 +51,6 @@ transformers >= 0.2 && < 0.6, transformers-compat >= 0.4 && < 1 - if impl(ghc < 7.8) - build-depends: - newtype >= 0.2 && < 0.3, - tagged >= 0.2 && < 1 - exposed-modules: Data.Constraint Data.Constraint.Deferrable @@ -62,4 +58,9 @@ Data.Constraint.Lifting Data.Constraint.Unsafe + if impl(ghc >= 8) + exposed-modules: + Data.Constraint.Nat + Data.Constraint.Symbol + ghc-options: -Wall diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint/Deferrable.hs new/constraints-0.9/src/Data/Constraint/Deferrable.hs --- old/constraints-0.8/src/Data/Constraint/Deferrable.hs 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint/Deferrable.hs 2017-01-26 03:31:25.000000000 +0100 @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ConstraintKinds #-} @@ -5,11 +6,18 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE PolyKinds #-} + +#if __GLASGOW_HASKELL__ >= 800 +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeInType #-} +#endif ----------------------------------------------------------------------------- -- | -- Module : Data.Constraint.Deferrable --- Copyright : (C) 2015 Edward Kmett +-- Copyright : (C) 2015-2016 Edward Kmett -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Edward Kmett <[email protected]> @@ -24,13 +32,24 @@ , Deferrable(..) , defer , deferred +#if __GLASGOW_HASKELL__ >= 800 + , defer_ + , deferEither_ + , (:~~:)(HRefl) +#endif + , (:~:)(Refl) ) where import Control.Exception import Control.Monad import Data.Constraint import Data.Proxy -import Data.Typeable (Typeable, cast) +import Data.Typeable (Typeable, cast, typeRep) +import Data.Type.Equality ((:~:)(Refl)) + +#if __GLASGOW_HASKELL__ >= 800 +import GHC.Types (type (~~)) +#endif data UnsatisfiedConstraint = UnsatisfiedConstraint String deriving (Typeable, Show) @@ -38,26 +57,73 @@ instance Exception UnsatisfiedConstraint -- | Allow an attempt at resolution of a constraint at a later time -class Deferrable (p :: Constraint) where +class Deferrable p where -- | Resolve a 'Deferrable' constraint with observable failure. deferEither :: proxy p -> (p => r) -> Either String r -- | Defer a constraint for later resolution in a context where we want to upgrade failure into an error -defer :: forall proxy p r. Deferrable p => proxy p -> (p => r) -> r -defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r +defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r +defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r deferred :: forall p. Deferrable p :- p deferred = Sub $ defer (Proxy :: Proxy p) Dict --- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6. -data a :~: b where - Refl :: a :~: a +#if __GLASGOW_HASKELL__ >= 800 +-- | A version of 'defer' that uses visible type application in place of a 'Proxy'. +-- +-- Only available on GHC 8.0 or later. +defer_ :: forall p r. Deferrable p => (p => r) -> r +defer_ r = defer @p Proxy r + +-- | A version of 'deferEither' that uses visible type application in place of a 'Proxy'. +-- +-- Only available on GHC 8.0 or later. +deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r +deferEither_ r = deferEither @p Proxy r +#endif + +#if __GLASGOW_HASKELL__ >= 800 +-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is +-- inhabited by a terminating value if and only if @a@ is the same type as @b@. +-- +-- Only available on GHC 8.0 or later. +data (a :: i) :~~: (b :: j) where + HRefl :: a :~~: a deriving Typeable +#endif +showTypeRep :: Typeable t => Proxy t -> String +showTypeRep = show . typeRep + +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. +#if __GLASGOW_HASKELL__ >= 800 +instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where +#elif __GLASGOW_HASKELL__ == 710 +instance (Typeable a, Typeable b) => Deferrable ((a :: *) ~ (b :: *)) where +#else instance (Typeable a, Typeable b) => Deferrable (a ~ b) where +#endif deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of Just Refl -> Right r - Nothing -> Left "deferred type equality: type mismatch" + Nothing -> Left $ + "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `" ++ showTypeRep (Proxy :: Proxy a) ++ "'" + +#if __GLASGOW_HASKELL__ >= 800 +-- | Deferrable heterogenous equality constraints. +-- +-- Only available on GHC 8.0 or later. +instance (Typeable i, Typeable j, Typeable (a :: i), Typeable (b :: j)) => Deferrable (a ~~ b) where + deferEither _ r = case cast (HRefl :: a :~~: a) :: Maybe (a :~~: b) of + Just HRefl -> Right r + Nothing -> Left $ + "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `" ++ showTypeRep (Proxy :: Proxy a) ++ "'" +#endif instance (Deferrable a, Deferrable b) => Deferrable (a, b) where deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint/Forall.hs new/constraints-0.9/src/Data/Constraint/Forall.hs --- old/constraints-0.8/src/Data/Constraint/Forall.hs 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint/Forall.hs 2017-01-26 03:31:25.000000000 +0100 @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -7,6 +8,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Trustworthy #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} #if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-} @@ -15,7 +17,8 @@ -- | -- Module : Data.Constraint.Forall -- Copyright : (C) 2011-2015 Edward Kmett, --- (C) 2015 Ørjan Johansen +-- (C) 2015 Ørjan Johansen, +-- (C) 2016 David Feuer -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Edward Kmett <[email protected]> @@ -30,6 +33,8 @@ , ForallF, instF , Forall1, inst1 , ForallT, instT + , ForallV, InstV (instV) + , forall ) where import Data.Constraint @@ -39,6 +44,14 @@ - for whether a class predicate holds, and if so assume that it holds for all - types, unsafely coercing the typeclass dictionary. - + - The particular technique used to implement 'Forall' appears to have been + - discovered first by Nicolas Frisby and is + - <https://csks.wordpress.com/2012/10/22/safe-polykinded-universally-quantified-constraints-part-3-of-3/ discussed in some detail> + - on his blog. + - + - However, his discovery did not directly affect the development of this + - module. + - - A previous version of this module used concrete, unexported types as the - skolems. This turned out to be unsound in the presence of type families. - There were 3 somewhat distinct issues: @@ -85,17 +98,14 @@ - extract it from `Forall p` in order to tie the knot. -} --- the `Skolem*` type families represent skolem variables, do not export! --- if GHC supports it, these might be made closed with no instances. +-- The `Skolem` type family represents skolem variables; do not export! +-- If GHC supports it, these might be made closed with no instances. type family Skolem (p :: k -> Constraint) :: k -type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1 -type family SkolemT1 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k1 -type family SkolemT2 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k2 --- The outer `Forall*` type families prevent GHC from giving a spurious +-- The outer `Forall` type family prevents GHC from giving a spurious -- superclass cycle error. --- The inner `Forall*_` classes prevent the skolem from leaking to the user, +-- The inner `Forall_` class prevents the skolem from leaking to the user, -- which would be disastrous. -- | A representation of the quantified constraint @forall a. p a@. @@ -104,33 +114,78 @@ class p (Skolem p) => Forall_ (p :: k -> Constraint) instance p (Skolem p) => Forall_ (p :: k -> Constraint) --- | A representation of the quantified constraint @forall a. p (f a)@. -type family ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) :: Constraint -type instance ForallF p f = ForallF_ p f -class p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2) -instance p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2) - -type Forall1 p = Forall p - --- | A representation of the quantified constraint @forall f a. p (t f a)@. -type family ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: Constraint -type instance ForallT p t = ForallT_ p t -class p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) -instance p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) - -- | Instantiate a quantified @'Forall' p@ constraint at type @a@. inst :: forall p a. Forall p :- p a inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p)) +-- | 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 = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f))) +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 (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 --- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@. -instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a) -instT = unsafeCoerce (Sub Dict :: ForallT p t :- p (t (SkolemT1 p t) (SkolemT2 p t))) +-- | 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 + +forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p) +forall d = case d :: Dict (p (Skolem p)) of Dict -> Dict diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint/Nat.hs new/constraints-0.9/src/Data/Constraint/Nat.hs --- old/constraints-0.8/src/Data/Constraint/Nat.hs 1970-01-01 01:00:00.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint/Nat.hs 2017-01-26 03:31:25.000000000 +0100 @@ -0,0 +1,323 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE Trustworthy #-} +-- | 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 + , plusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat + , plusZero, 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 + , dividesDef + , timesDiv + , eqLe, leEq, leId, leTrans + , leZero, zeroLe + ) where + +import Data.Constraint +import Data.Proxy +import GHC.TypeLits +import Unsafe.Coerce + +type family Min :: Nat -> Nat -> Nat where +type family Max :: Nat -> Nat -> Nat where +type family Div :: Nat -> Nat -> Nat where +type family Mod :: Nat -> Nat -> Nat where +type family Gcd :: Nat -> Nat -> Nat where +type family Lcm :: Nat -> Nat -> Nat where + +type Divides n m = n ~ Gcd n m + +newtype Magic n r = Magic (KnownNat n => r) + +magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o +magic f = Sub $ unsafeCoerce (Magic id) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m)) + +axiom :: forall a b. Dict (a ~ b) +axiom = unsafeCoerce (Dict :: Dict (a ~ a)) + +axiomLe :: forall a b. Dict (a <= b) +axiomLe = axiom + +eqLe :: (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 axiom + +dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c +dividesLcm = Sub axiom + +gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a) +gcdCommutes = axiom + +lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a) +lcmCommutes = axiom + +gcdZero :: forall a. Dict (Gcd 0 a ~ a) +gcdZero = axiom + +gcdOne :: forall a. Dict (Gcd 1 a ~ 1) +gcdOne = axiom + +lcmZero :: forall a. Dict (Lcm 0 a ~ 0) +lcmZero = axiom + +lcmOne :: forall a. Dict (Lcm 1 a ~ a) +lcmOne = axiom + +gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m) +gcdNat = magic gcd + +lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m) +lcmNat = magic lcm + +plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m) +plusNat = magic (+) + +minNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m) +minNat = magic min + +maxNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m) +maxNat = magic max + +timesNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m) +timesNat = magic (*) + +powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m) +powNat = magic (^) + +divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m) +divNat = Sub $ case magic @n @m div of Sub r -> r + +modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m) +modNat = Sub $ case magic @n @m mod of Sub r -> r + +plusZero :: forall n. Dict ((n + 0) ~ n) +plusZero = axiom + +timesZero :: forall n. Dict ((n * 0) ~ 0) +timesZero = axiom + +timesOne :: forall n. Dict ((n * 1) ~ n) +timesOne = axiom + +minZero :: forall n. Dict (Min n 0 ~ 0) +minZero = axiom + +maxZero :: forall n. Dict (Max n 0 ~ n) +maxZero = axiom + +powZero :: forall n. Dict ((n ^ 0) ~ 1) +powZero = axiom + +leZero :: forall a. (a <= 0) :- (a ~ 0) +leZero = Sub axiom + +zeroLe :: forall a. Dict (0 <= a) +zeroLe = axiom + +plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c) +plusMonotone1 = Sub axiom + +plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c) +plusMonotone2 = Sub axiom + +powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c)) +powMonotone1 = Sub axiom + +powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c)) +powMonotone2 = Sub axiom + +divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c) +divMonotone1 = Sub axiom + +divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b) +divMonotone2 = Sub axiom + +timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c) +timesMonotone1 = Sub axiom + +timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c) +timesMonotone2 = Sub axiom + +minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c) +minMonotone1 = Sub axiom + +minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c) +minMonotone2 = Sub axiom + +maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c) +maxMonotone1 = Sub axiom + +maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c) +maxMonotone2 = Sub axiom + +powOne :: forall n. Dict ((n ^ 1) ~ n) +powOne = axiom + +plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c) +plusMod = Sub axiom + +timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c) +timesMod = Sub axiom + +modBound :: forall m n. (1 <= n) :- (Mod m n <= n) +modBound = Sub axiom + +euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c)) +euclideanNat = Sub axiom + +plusCommutes :: forall n m. Dict ((m + n) ~ (n + m)) +plusCommutes = axiom + +timesCommutes :: forall n m. Dict ((m * n) ~ (n * m)) +timesCommutes = axiom + +minCommutes :: forall n m. Dict (Min m n ~ Min n m) +minCommutes = axiom + +maxCommutes :: forall n m. Dict (Min m n ~ Min n m) +maxCommutes = axiom + +plusAssociates :: forall n m o. Dict (((m + n) + o) ~ (m + (n + o))) +plusAssociates = axiom + +timesAssociates :: forall n m o. Dict (((m * n) * o) ~ (m * (n * o))) +timesAssociates = axiom + +minAssociates :: forall n m o. Dict (Min (Min m n) o ~ Min m (Min n o)) +minAssociates = axiom + +maxAssociates :: forall n m o. Dict (Max (Max m n) o ~ Max m (Max n o)) +maxAssociates = axiom + +gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c ~ Gcd a (Gcd b c)) +gcdAssociates = axiom + +lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c)) +lcmAssociates = axiom + +minIsIdempotent :: forall n. Dict (Min n n ~ n) +minIsIdempotent = axiom + +maxIsIdempotent :: forall n. Dict (Max n n ~ n) +maxIsIdempotent = axiom + +gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n) +gcdIsIdempotent = axiom + +lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n) +lcmIsIdempotent = axiom + +minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o)) +minDistributesOverPlus = axiom + +minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o)) +minDistributesOverTimes = axiom + +minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o)) +minDistributesOverPow1 = axiom + +minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o)) +minDistributesOverPow2 = axiom + +minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o)) +minDistributesOverMax = axiom + +maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o)) +maxDistributesOverPlus = axiom + +maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o)) +maxDistributesOverTimes = axiom + +maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o)) +maxDistributesOverPow1 = axiom + +maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o)) +maxDistributesOverPow2 = axiom + +maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o)) +maxDistributesOverMin = axiom + +plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o)) +plusDistributesOverTimes = axiom + +timesDistributesOverPow :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o)) +timesDistributesOverPow = axiom + +timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o)) +timesDistributesOverGcd = axiom + +timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o)) +timesDistributesOverLcm = axiom + +plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o) +plusIsCancellative = Sub axiom + +timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o) +timesIsCancellative = Sub axiom + +gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c)) +gcdDistributesOverLcm = axiom + +lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c)) +lcmDistributesOverGcd = axiom + +dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c) +dividesPlus = Sub axiom + +dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c) +dividesTimes = Sub axiom + +dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c) +dividesMin = Sub axiom + +dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c) +dividesMax = Sub axiom + +dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ a) +dividesDef = Sub axiom + +dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n) +dividesPow = Sub axiom + +timesDiv :: forall a b. Dict ((a * Div b a) <= a) +timesDiv = axiom + +-- (<=) is an internal category in the category of constraints. + +leId :: forall a. Dict (a <= a) +leId = Dict + +leEq :: forall a b. (a <= b, b <= a) :- (a ~ b) +leEq = Sub axiom + +leTrans :: forall a b c. (b <= c, a <= b) :- (a <= c) +leTrans = Sub (axiomLe @a @c) diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint/Symbol.hs new/constraints-0.9/src/Data/Constraint/Symbol.hs --- old/constraints-0.8/src/Data/Constraint/Symbol.hs 1970-01-01 01:00:00.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint/Symbol.hs 2017-01-26 03:31:25.000000000 +0100 @@ -0,0 +1,119 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +-- | Utilities for working with 'KnownSymbol' constraints. +-- +-- This module is only available on GHC 8.0 or later. +module Data.Constraint.Symbol + ( 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.Proxy +import GHC.TypeLits +import Unsafe.Coerce + +type family (++) :: Symbol -> Symbol -> Symbol where +type family Take :: Nat -> Symbol -> Symbol where +type family Drop :: Nat -> Symbol -> Symbol where +type family Length :: Symbol -> Nat where + +-- implementation details + +newtype Magic n r = Magic (KnownSymbol n => r) + +magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o +magicNSS f = Sub $ unsafeCoerce (Magic id) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m)) + +magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o +magicSSS f = Sub $ unsafeCoerce (Magic id) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m)) + +magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n +magicSN f = Sub $ unsafeCoerce (Magic id) (toInteger (f (symbolVal (Proxy :: Proxy a)))) + +axiom :: forall a b. Dict (a ~ b) +axiom = unsafeCoerce (Dict :: Dict (a ~ a)) + +-- axioms and operations + +appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b) +appendSymbol = magicSSS (++) + +appendUnit1 :: forall a. Dict (("" ++ a) ~ a) +appendUnit1 = axiom + +appendUnit2 :: forall a. Dict ((a ++ "") ~ a) +appendUnit2 = axiom + +appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c))) +appendAssociates = axiom + +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 (Take n a ++ Drop n a ~ a) +takeAppendDrop = axiom + +lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a) +lengthSymbol = magicSN length + +takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a) +takeLength = Sub axiom + +take0 :: forall a. Dict (Take 0 a ~ "") +take0 = axiom + +takeEmpty :: forall n. Dict (Take n "" ~ "") +takeEmpty = axiom + +dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "") +dropLength = Sub axiom + +drop0 :: forall a. Dict (Drop 0 a ~ a) +drop0 = axiom + +dropEmpty :: forall n. Dict (Drop n "" ~ "") +dropEmpty = axiom + +lengthTake :: forall n a. Dict (Length (Take n a) <= n) +lengthTake = axiom + +lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n)) +lengthDrop = axiom + +dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a) +dropDrop = axiom + +takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a) +takeTake = axiom diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint/Unsafe.hs new/constraints-0.9/src/Data/Constraint/Unsafe.hs --- old/constraints-0.8/src/Data/Constraint/Unsafe.hs 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint/Unsafe.hs 2017-01-26 03:31:25.000000000 +0100 @@ -32,21 +32,10 @@ import Control.Applicative import Control.Monad +import Data.Coerce import Data.Constraint import Unsafe.Coerce -#if __GLASGOW_HASKELL__ >= 708 - -import Data.Coerce - -#else - -import Control.Newtype - -type Coercible = Newtype - -#endif - -- | Coerce a dictionary unsafely from one type to another unsafeCoerceConstraint :: a :- b unsafeCoerceConstraint = unsafeCoerce refl diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn' '--exclude=.svnignore' old/constraints-0.8/src/Data/Constraint.hs new/constraints-0.9/src/Data/Constraint.hs --- old/constraints-0.8/src/Data/Constraint.hs 2016-01-17 03:10:38.000000000 +0100 +++ new/constraints-0.9/src/Data/Constraint.hs 2017-01-26 03:31:25.000000000 +0100 @@ -1,10 +1,13 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} @@ -13,11 +16,6 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE CPP #-} -#if __GLASGOW_HASKELL__ >= 707 -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE RoleAnnotations #-} -#endif #if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-} #endif @@ -58,10 +56,12 @@ Constraint -- * Dictionary , Dict(Dict) + , withDict -- * Entailment , (:-)(Sub) , (\\) , weaken1, weaken2, contract + , strengthen1, strengthen2 , (&&&), (***) , trans, refl , Bottom @@ -73,25 +73,17 @@ , Class(..) , (:=>)(..) ) where -import Control.Monad -#if __GLASGOW_HASKELL__ >= 707 -import Control.Category -#endif import Control.Applicative +import Control.Category +import Control.Monad #if __GLASGOW_HASKELL__ < 710 import Data.Monoid #endif import Data.Complex import Data.Ratio -#if __GLASGOW_HASKELL__ >= 707 import Data.Data -#endif -#if __GLASGOW_HASKELL__ <= 710 -import GHC.Prim (Constraint) -#else -import GHC.Types (Constraint) -#endif -import qualified GHC.Prim as Prim +import qualified GHC.Exts as Exts (Any) +import GHC.Exts (Constraint) -- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. -- @@ -111,7 +103,6 @@ -- data Dict :: Constraint -> * where Dict :: a => Dict a -#if __GLASGOW_HASKELL__ >= 707 deriving Typeable @@ -128,12 +119,21 @@ dictDataType :: DataType dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr] -#endif deriving instance Eq (Dict a) deriving instance Ord (Dict a) deriving instance Show (Dict a) +-- | 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. +-- +withDict :: Dict a -> (a => r) -> r +withDict d r = case d of + Dict -> r + infixr 9 :- -- | This is the type of entailment. @@ -152,9 +152,10 @@ -- -- This relationship is captured in the ':-' entailment type here. -- --- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category' --- of constraints. However, 'Category' only because sufficiently general to support this --- instance in GHC 7.8, so prior to 7.8 this instance is unavailable. +-- 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 @@ -190,7 +191,6 @@ -- library is sensible and can't break any assumptions on the behalf of -- library authors. newtype a :- b = Sub (a => Dict b) -#if __GLASGOW_HASKELL__ >= 707 deriving Typeable type role (:-) nominal nominal @@ -218,7 +218,6 @@ instance Category (:-) where id = refl (.) = trans -#endif -- | Assumes 'IncoherentInstances' doesn't exist. instance Eq (a :- b) where @@ -279,6 +278,12 @@ 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. @@ -305,8 +310,8 @@ top = Sub Dict -- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance. -class Prim.Any => Bottom where - no :: Dict a +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"> @@ -331,9 +336,7 @@ unmapDict :: (Dict a -> Dict b) -> a :- b unmapDict f = Sub (f Dict) -#if __GLASGOW_HASKELL__ >= 707 type role Dict nominal -#endif -------------------------------------------------------------------------------- -- Reflection
