diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown new file mode 100644 --- /dev/null +++ b/CHANGELOG.markdown @@ -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` diff --git a/README.markdown b/README.markdown --- a/README.markdown +++ b/README.markdown @@ -1,6 +1,8 @@ constraints =========== +[![Hackage](https://img.shields.io/hackage/v/constraints.svg)](https://hackage.haskell.org/package/constraints) [![Build Status](https://github.com/ekmett/constraints/workflows/Haskell-CI/badge.svg)](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 diff --git a/constraints.cabal b/constraints.cabal --- a/constraints.cabal +++ b/constraints.cabal @@ -1,15 +1,15 @@ +cabal-version: 2.4 name: constraints category: Constraints -version: 0.8 -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 stability: experimental homepage: http://github.com/ekmett/constraints/ bug-reports: http://github.com/ekmett/constraints/issues -copyright: Copyright (C) 2011-2015 Edward A. Kmett +copyright: Copyright (C) 2011-2021 Edward A. Kmett synopsis: Constraint manipulation description: GHC 7.4 gave us the ability to talk about @ConstraintKinds@. They stopped crashing the compiler in GHC 7.6. @@ -17,12 +17,26 @@ 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 == 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 @@ -41,25 +55,45 @@ GADTs build-depends: - base >= 4.7 && < 5, - binary >= 0.7.3 && < 0.9, - deepseq >= 1.3 && < 1.5, - ghc-prim, - hashable >= 1.2 && < 1.3, - mtl >= 2 && < 2.3, - transformers >= 0.2 && < 0.6, - transformers-compat >= 0.4 && < 1 - - if impl(ghc < 7.8) + , 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: - newtype >= 0.2 && < 0.3, - tagged >= 0.2 && < 1 + 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 diff --git a/src/Data/Constraint.hs b/src/Data/Constraint.hs --- a/src/Data/Constraint.hs +++ b/src/Data/Constraint.hs @@ -1,35 +1,28 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE EmptyDataDecls #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Trustworthy #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE CPP #-} -#if __GLASGOW_HASKELL__ >= 707 -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE RoleAnnotations #-} -#endif -#if __GLASGOW_HASKELL__ >= 800 +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} -#endif -#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710 -{-# LANGUAGE NullaryTypeClasses #-} -#endif ------------------------------------------------------------------------------ +{-# LANGUAGE UnicodeSyntax #-} + -- | --- Module : Data.Constraint -- Copyright : (C) 2011-2015 Edward Kmett, -- License : BSD-style (see the file LICENSE) --- -- Maintainer : Edward Kmett -- Stability : experimental -- Portability : non-portable @@ -44,27 +37,34 @@ -- -- The need for this extension was first publicized in the paper -- --- +-- -- -- 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 - , Bottom + , implied + , Bottom(no) , top, bottom -- * Dict is fully faithful , mapDict @@ -73,25 +73,24 @@ , Class(..) , (:=>)(..) ) where -import Control.Monad -#if __GLASGOW_HASKELL__ >= 707 -import Control.Category -#endif import Control.Applicative -#if __GLASGOW_HASKELL__ < 710 -import Data.Monoid -#endif +import Control.Category +import Control.DeepSeq +import Control.Monad 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 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@. -- @@ -104,17 +103,23 @@ -- captures a dictionary that proves we have an: -- -- @ --- instance 'Eq' 'Int +-- instance 'Eq' 'Int' -- @ -- -- Pattern matching on the 'Dict' constructor will bring this instance into scope. -- data Dict :: Constraint -> * where Dict :: a => Dict a -#if __GLASGOW_HASKELL__ >= 707 - deriving Typeable +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 @@ -128,14 +133,64 @@ dictDataType :: DataType dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr] -#endif +-} -deriving instance Eq (Dict a) -deriving instance Ord (Dict a) -deriving instance Show (Dict a) +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@. @@ -152,9 +207,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 @@ -171,7 +227,7 @@ -- What are the two ways? -- -- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the --- superclass relationship, and them from @'Eq' a ':-' 'Eq' [a]@ via the +-- 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\". @@ -190,35 +246,28 @@ -- library is sensible and can't break any assumptions on the behalf of -- library authors. newtype a :- b = Sub (a => Dict b) -#if __GLASGOW_HASKELL__ >= 707 - deriving Typeable type role (:-) nominal nominal --- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_. --- --- This is admissable, but not present by default - --- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q) -instance (Typeable p, Typeable q, p, q) => Data (p :- q) where - gfoldl _ z (Sub Dict) = z (Sub Dict) - toConstr _ = subConstr +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 "gunfold" - dataTypeOf _ = subDataType - -subConstr :: Constr -subConstr = mkConstr dictDataType "Sub" [] Prefix + 1 -> z (Sub Dict) + _ -> error "Data.Data.Data: Data.Constraint.:- constructor out of bounds" + toConstr _ = subCon + dataTypeOf _ = subTy -subDataType :: DataType -subDataType = mkDataType "Data.Constraint.:-" [subConstr] +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 -#endif -- | Assumes 'IncoherentInstances' doesn't exist. instance Eq (a :- b) where @@ -231,11 +280,8 @@ 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 +instance a => NFData (a :- b) where + rnf (Sub Dict) = () -------------------------------------------------------------------------------- -- Constraints form a Category @@ -254,10 +300,46 @@ 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) @@ -279,6 +361,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 +393,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 @@ -331,9 +419,7 @@ unmapDict :: (Dict a -> Dict b) -> a :- b unmapDict f = Sub (f Dict) -#if __GLASGOW_HASKELL__ >= 707 type role Dict nominal -#endif -------------------------------------------------------------------------------- -- Reflection @@ -403,6 +489,10 @@ 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 @@ -420,6 +510,10 @@ 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 @@ -427,6 +521,7 @@ 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 @@ -435,6 +530,10 @@ 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 @@ -442,12 +541,17 @@ 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 @@ -460,6 +564,10 @@ 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 @@ -469,6 +577,9 @@ 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 @@ -478,6 +589,10 @@ 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 @@ -486,43 +601,83 @@ 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 () (Monoid a) where cls = Sub Dict +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 @@ -533,6 +688,8 @@ 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 @@ -542,6 +699,7 @@ 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 @@ -551,14 +709,15 @@ instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict -- Monad -instance Class () (Monad f) where cls = Sub Dict +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) (MonadPlus f) where cls = Sub Dict +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 @@ -579,7 +738,10 @@ 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 - mappend Dict Dict = Dict mempty = Dict diff --git a/src/Data/Constraint/Char.hs b/src/Data/Constraint/Char.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Char.hs @@ -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 diff --git a/src/Data/Constraint/Deferrable.hs b/src/Data/Constraint/Deferrable.hs --- a/src/Data/Constraint/Deferrable.hs +++ b/src/Data/Constraint/Deferrable.hs @@ -1,66 +1,82 @@ -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE GADTs #-} +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} ------------------------------------------------------------------------------ -- | --- Module : Data.Constraint.Deferrable --- Copyright : (C) 2015 Edward Kmett +-- Copyright : (C) 2015-2021 Edward Kmett -- License : BSD-style (see the file LICENSE) --- -- Maintainer : Edward Kmett -- 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) +import Data.Typeable (Typeable, cast, typeRep) +import Data.Type.Equality ((:~:)(Refl)) -data UnsatisfiedConstraint = UnsatisfiedConstraint String - deriving (Typeable, Show) +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 :: 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 + deferEither :: (p => r) -> Either String r deferred :: forall p. Deferrable p :- p -deferred = Sub $ defer (Proxy :: Proxy p) Dict +deferred = Sub $ defer @p Dict --- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6. -data a :~: b where - Refl :: a :~: a - deriving Typeable +defer :: forall p r. Deferrable p => (p => r) -> r +defer r = either (throw . UnsatisfiedConstraint) id $ deferEither @p r -instance (Typeable a, Typeable b) => Deferrable (a ~ b) where - deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of +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" + 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 (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r + deferEither r = join $ deferEither @a $ deferEither @b r instance (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) where - deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ join $ deferEither (Proxy :: Proxy b) $ deferEither (Proxy :: Proxy c) r + deferEither r = join $ deferEither @a $ join $ deferEither @b $ deferEither @c r diff --git a/src/Data/Constraint/Forall.hs b/src/Data/Constraint/Forall.hs --- a/src/Data/Constraint/Forall.hs +++ b/src/Data/Constraint/Forall.hs @@ -1,21 +1,23 @@ {-# LANGUAGE CPP #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} -#if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-} -#endif ------------------------------------------------------------------------------ +{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE GADTs #-} + -- | --- Module : Data.Constraint.Forall --- Copyright : (C) 2011-2015 Edward Kmett, --- (C) 2015 Ørjan Johansen +-- Copyright : (C) 2011-2021 Edward Kmett, +-- (C) 2015 Ørjan Johansen, +-- (C) 2016 David Feuer -- License : BSD-style (see the file LICENSE) -- -- Maintainer : Edward Kmett @@ -23,114 +25,101 @@ -- 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) -{- The basic trick of this module is to use "skolem" types as test candidates - - for whether a class predicate holds, and if so assume that it holds for all - - types, unsafely coercing the typeclass dictionary. - - - - A previous version of this module used concrete, unexported types as the - - skolems. This turned out to be unsound in the presence of type families. - - There were 3 somewhat distinct issues: - - - - 1. Using closed type families, it is possible to test whether two concrete - - types are equal, even if one of them is not directly importable. - - - - 2. Using just open type families, it is possible to test "at least 2 of - - these n+1 types are equal", thus using the pigeonhole principle to thwart - - any scheme based on having only a finite number of shared skolem types. - - - - 3. Using just pattern matching of types by unification, it is possible - - to extract the skolem types from the application the `Forall p` expands - - to. (Although type families are probably still needed to exploit this.) - - - - András Kovács and Ørjan Johansen independently realized that skolems - - themselves made as type family applications can be used to solve the first - - two problems (and discovered the third problem in the process). As a bonus, - - the resulting code is easy to make polykinded. - - - - Problem 1 is solved by making the type family have no instances, forcing - - GHC to make no assumption about what type a skolem is. - - - - Problem 2 is solved by parametrizing the skolem on the predicate tested - - for. (This is a known trick in predicate logic.) - - - - Problem 3 is solved by making the `Forall p` application expand to a type - - class, and have the *actual* test constraint be a superclass constraint on - - that type class, thus preventing the user directly accessing it. - - - - An unfortunate side effect of the new method is that it tends to trigger - - spurious errors from GHC test for cycles in superclass constraints. András - - Kovács discovered that these can be silenced by yet another use of a type - - family. - - - - David Feuer points out a remaining doubt about the soundness of this scheme: - - GHC *does* know that the skolems created from a single predicate `p` are - - equal. This could in theory apply even if the skolems come from two - - *distinct* invocations of `Forall p`. - - - - However, we don't know any way of bringing two such skolems in contact with - - each other to create an actual exploit. It would seem to require `p` to - - already contain its own skolem, despite there being (hopefully) no way to - - extract it from `Forall p` in order to tie the knot. - -} +class (forall a. p a) => Forall (p :: k -> Constraint) +instance (forall a. p a) => Forall (p :: k -> Constraint) --- the `Skolem*` type families represent skolem variables, do not export! --- if GHC supports it, these might be made closed with no instances. +-- | Instantiate a quantified @'Forall' p@ constraint at type @a@. +inst :: forall p a. Forall p :- p a +inst = Sub Dict -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 +data Dict1 p where + Dict1 :: (forall a. p a) => Dict1 p --- The outer `Forall*` type families prevent GHC from giving a spurious --- superclass cycle error. --- The inner `Forall*_` classes prevent the skolem from leaking to the user, --- which would be disastrous. +forallish :: forall p. Dict1 p -> Dict (Forall p) +forallish Dict1 = Dict --- | A representation of the quantified constraint @forall a. p a@. -type family Forall (p :: k -> Constraint) :: Constraint -type instance Forall p = Forall_ p -class p (Skolem p) => Forall_ (p :: k -> Constraint) -instance p (Skolem p) => Forall_ (p :: k -> Constraint) +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)@. -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) +class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) +instance Forall (ComposeC p f) => ForallF p f -type Forall1 p = Forall p +-- | 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 --- | 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) +-- 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 --- | 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)) +-- | 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 @'ForallF' p f@ constraint at type @a@. -instF :: forall p f a. ForallF p f :- p (f a) -instF = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f))) +-- | Instantiate a quantified @'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 --- | 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 + diff --git a/src/Data/Constraint/Lifting.hs b/src/Data/Constraint/Lifting.hs --- a/src/Data/Constraint/Lifting.hs +++ b/src/Data/Constraint/Lifting.hs @@ -3,13 +3,12 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} -{-# OPTIONS_GHC -fno-warn-deprecations #-} -module Data.Constraint.Lifting + +module Data.Constraint.Lifting ( Lifting(..) , Lifting2(..) ) where @@ -25,10 +24,8 @@ import Control.Monad.IO.Class import Control.Monad.RWS.Class import Control.Monad.Trans.Cont -import Control.Monad.Trans.Error import Control.Monad.Trans.Except import Control.Monad.Trans.Identity -import Control.Monad.Trans.List import Control.Monad.Trans.Maybe import Control.Monad.Trans.Reader import Control.Monad.Trans.RWS.Lazy as Lazy @@ -40,9 +37,6 @@ import Data.Binary import Data.Complex import Data.Constraint -#if __GLASGOW_HASKELL__ < 710 -import Data.Foldable -#endif import Data.Functor.Classes import Data.Functor.Compose as Functor import Data.Functor.Identity @@ -50,13 +44,7 @@ import Data.Functor.Reverse as Functor import Data.Functor.Sum as Functor import Data.Hashable -#if __GLASGOW_HASKELL__ < 710 -import Data.Monoid -#endif import Data.Ratio -#if __GLASGOW_HASKELL__ < 710 -import Data.Traversable -#endif import GHC.Arr class Lifting p f where @@ -77,6 +65,7 @@ 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 @@ -85,7 +74,7 @@ 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 @@ -103,6 +92,7 @@ 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 @@ -113,7 +103,6 @@ instance Applicative f => Lifting Applicative (Compose f) where lifting = Sub Dict instance Alternative f => Lifting Alternative (Compose f) where lifting = Sub Dict -- overconstrained -#if MIN_VERSION_transformers(0,5,0) 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 @@ -122,16 +111,6 @@ 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 -#else -instance (Functor f, Show1 f) => Lifting Show1 (Compose f) where lifting = Sub Dict -instance (Functor f, Eq1 f) => Lifting Eq1 (Compose f) where lifting = Sub Dict -instance (Functor f, Ord1 f) => Lifting Ord1 (Compose f) where lifting = Sub Dict -instance (Functor f, Read1 f) => Lifting Read1 (Compose f) where lifting = Sub Dict -instance (Functor f, Eq1 f, Eq1 g) => Lifting Eq (Compose f g) where lifting = Sub Dict -instance (Functor f, Ord1 f, Ord1 g) => Lifting Ord (Compose f g) where lifting = Sub Dict -instance (Functor f, Read1 f, Read1 g) => Lifting Read (Compose f g) where lifting = Sub Dict -instance (Functor f, Show1 f, Show1 g) => Lifting Show (Compose f g) where lifting = Sub Dict -#endif instance Functor f => Lifting Functor (Functor.Product f) where lifting = Sub Dict instance Foldable f => Lifting Foldable (Functor.Product f) where lifting = Sub Dict @@ -194,22 +173,6 @@ instance Lifting MonadFix (ReaderT e) where lifting = Sub Dict instance Lifting MonadIO (ReaderT e) where lifting = Sub Dict -instance Lifting Functor (ErrorT e) where lifting = Sub Dict -instance Lifting Foldable (ErrorT e) where lifting = Sub Dict -instance Lifting Traversable (ErrorT e) where lifting = Sub Dict -instance Error e => Lifting Monad (ErrorT e) where lifting = Sub Dict -instance Error e => Lifting MonadFix (ErrorT e) where lifting = Sub Dict -instance Error e => Lifting MonadPlus (ErrorT e) where lifting = Sub Dict -- overconstrained! -instance Error e => Lifting MonadIO (ErrorT e) where lifting = Sub Dict -instance Show e => Lifting Show1 (ErrorT e) where lifting = Sub Dict -instance Eq e => Lifting Eq1 (ErrorT e) where lifting = Sub Dict -instance Ord e => Lifting Ord1 (ErrorT e) where lifting = Sub Dict -instance Read e => Lifting Read1 (ErrorT e) where lifting = Sub Dict -instance (Show e, Show1 m) => Lifting Show (ErrorT e m) where lifting = Sub Dict -instance (Eq e, Eq1 m) => Lifting Eq (ErrorT e m) where lifting = Sub Dict -instance (Ord e, Ord1 m) => Lifting Ord (ErrorT e m) where lifting = Sub Dict -instance (Read e, Read1 m) => Lifting Read (ErrorT e m) where lifting = Sub Dict - instance Lifting Functor (ExceptT e) where lifting = Sub Dict instance Lifting Foldable (ExceptT e) where lifting = Sub Dict instance Lifting Traversable (ExceptT e) where lifting = Sub Dict @@ -285,24 +248,6 @@ instance Ord1 m => Lifting Ord (IdentityT m) where lifting = Sub Dict instance Eq1 m => Lifting Eq (IdentityT m) where lifting = Sub Dict -instance Lifting Functor ListT where lifting = Sub Dict -instance Lifting Applicative ListT where lifting = Sub Dict -instance Lifting Alternative ListT where lifting = Sub Dict -- overconstrained -instance Lifting Monad ListT where lifting = Sub Dict --- instance Lifting MonadFix ListT where lifting = Sub Dict -instance Lifting MonadPlus ListT where lifting = Sub Dict -- overconstrained -instance Lifting Foldable ListT where lifting = Sub Dict -instance Lifting Traversable ListT where lifting = Sub Dict -instance Lifting MonadIO ListT where lifting = Sub Dict -instance Lifting Show1 ListT where lifting = Sub Dict -instance Lifting Read1 ListT where lifting = Sub Dict -instance Lifting Ord1 ListT where lifting = Sub Dict -instance Lifting Eq1 ListT where lifting = Sub Dict -instance Show1 m => Lifting Show (ListT m) where lifting = Sub Dict -instance Read1 m => Lifting Read (ListT m) where lifting = Sub Dict -instance Ord1 m => Lifting Ord (ListT m) where lifting = Sub Dict -instance Eq1 m => Lifting Eq (ListT m) where lifting = Sub Dict - instance Lifting Functor MaybeT where lifting = Sub Dict instance Lifting Monad MaybeT where lifting = Sub Dict -- instance Lifting MonadFix MaybeT where lifting = Sub Dict @@ -367,11 +312,9 @@ instance Lifting Read Identity where lifting = Sub Dict instance Lifting MonadCont MaybeT where lifting = Sub Dict -instance Lifting MonadCont ListT where lifting = Sub Dict instance Lifting MonadCont IdentityT where lifting = Sub Dict instance Monoid w => Lifting MonadCont (Strict.WriterT w) where lifting = Sub Dict instance Monoid w => Lifting MonadCont (Lazy.WriterT w) where lifting = Sub Dict -instance Error e => Lifting MonadCont (ErrorT e) where lifting = Sub Dict instance Lifting MonadCont (ExceptT w) where lifting = Sub Dict instance Lifting MonadCont (Strict.StateT s) where lifting = Sub Dict instance Lifting MonadCont (Lazy.StateT s) where lifting = Sub Dict @@ -380,7 +323,6 @@ instance Monoid w => Lifting MonadCont (Lazy.RWST r w s) where lifting = Sub Dict instance Lifting (MonadError e) MaybeT where lifting = Sub Dict -instance Lifting (MonadError e) ListT where lifting = Sub Dict instance Lifting (MonadError e) IdentityT where lifting = Sub Dict instance Monoid w => Lifting (MonadError e) (Strict.WriterT w) where lifting = Sub Dict instance Monoid w => Lifting (MonadError e) (Lazy.WriterT w) where lifting = Sub Dict @@ -392,28 +334,23 @@ instance Lifting (MonadRWS r w s) MaybeT where lifting = Sub Dict instance Lifting (MonadRWS r w s) IdentityT where lifting = Sub Dict -instance Error e => Lifting (MonadRWS r w s) (ErrorT e) where lifting = Sub Dict instance Lifting (MonadRWS r w s) (ExceptT e) where lifting = Sub Dict instance Lifting (MonadReader r) MaybeT where lifting = Sub Dict -instance Lifting (MonadReader r) ListT where lifting = Sub Dict instance Lifting (MonadReader r) IdentityT where lifting = Sub Dict instance Monoid w => Lifting (MonadReader r) (Strict.WriterT w) where lifting = Sub Dict instance Monoid w => Lifting (MonadReader r) (Lazy.WriterT w) where lifting = Sub Dict instance Lifting (MonadReader r) (Strict.StateT s) where lifting = Sub Dict instance Lifting (MonadReader r) (Lazy.StateT s) where lifting = Sub Dict instance Lifting (MonadReader r) (ExceptT e) where lifting = Sub Dict -instance Error e => Lifting (MonadReader r) (ErrorT e) where lifting = Sub Dict instance Lifting (MonadReader r) (ContT r') where lifting = Sub Dict instance Lifting (MonadState s) MaybeT where lifting = Sub Dict -instance Lifting (MonadState s) ListT where lifting = Sub Dict instance Lifting (MonadState s) IdentityT where lifting = Sub Dict instance Monoid w => Lifting (MonadState s) (Strict.WriterT w) where lifting = Sub Dict instance Monoid w => Lifting (MonadState s) (Lazy.WriterT w) where lifting = Sub Dict instance Lifting (MonadState s) (ReaderT r) where lifting = Sub Dict instance Lifting (MonadState s) (ExceptT e) where lifting = Sub Dict -instance Error e => Lifting (MonadState s) (ErrorT e) where lifting = Sub Dict instance Lifting (MonadState s) (ContT r') where lifting = Sub Dict class Lifting2 p f where @@ -434,6 +371,7 @@ 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 diff --git a/src/Data/Constraint/Nat.hs b/src/Data/Constraint/Nat.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Nat.hs @@ -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) diff --git a/src/Data/Constraint/Symbol.hs b/src/Data/Constraint/Symbol.hs new file mode 100644 --- /dev/null +++ b/src/Data/Constraint/Symbol.hs @@ -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 diff --git a/src/Data/Constraint/Unsafe.hs b/src/Data/Constraint/Unsafe.hs --- a/src/Data/Constraint/Unsafe.hs +++ b/src/Data/Constraint/Unsafe.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-} @@ -6,47 +5,48 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE Unsafe #-} -#if __GLASGOW_HASKELL__ >= 800 +{-# LANGUAGE CPP #-} {-# OPTIONS_GHC -fno-warn-redundant-constraints #-} -#endif ------------------------------------------------------------------------------ + -- | --- Module : Data.Constraint.Unsafe --- Copyright : (C) 2011-2015 Edward Kmett +-- Copyright : (C) 2011-2021 Edward Kmett -- License : BSD-style (see the file LICENSE) --- -- Maintainer : Edward Kmett -- 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 - -- * Sugar - , unsafeApplicative - , unsafeAlternative + +#if MIN_VERSION_base(4,18,0) + -- * Unsafely creating @GHC.TypeLits@ singleton values + , unsafeSChar + , unsafeSNat + , unsafeSSymbol +#endif ) where -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 - +#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 @@ -59,19 +59,52 @@ 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. --- | Construct an Applicative instance from a Monad -unsafeApplicative :: forall m a. Monad m => (Applicative m => m a) -> m a -#if __GLASGOW_HASKELL__ < 710 -unsafeApplicative m = m \\ trans (unsafeCoerceConstraint :: Applicative (WrappedMonad m) :- Applicative m) ins -#else -unsafeApplicative m = m -#endif +-- | 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 --- | Construct an Alternative instance from a MonadPlus -unsafeAlternative :: forall m a. MonadPlus m => (Alternative m => m a) -> m a -#if __GLASGOW_HASKELL__ < 710 -unsafeAlternative m = m \\ trans (unsafeCoerceConstraint :: Alternative (WrappedMonad m) :- Alternative m) ins -#else -unsafeAlternative m = m +-- | 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 diff --git a/tests/GH117Spec.hs b/tests/GH117Spec.hs new file mode 100644 --- /dev/null +++ b/tests/GH117Spec.hs @@ -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 diff --git a/tests/GH55Spec.hs b/tests/GH55Spec.hs new file mode 100644 --- /dev/null +++ b/tests/GH55Spec.hs @@ -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 diff --git a/tests/Spec.hs b/tests/Spec.hs new file mode 100644 --- /dev/null +++ b/tests/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}