constraints 0.13.4 → 0.14

raw patch · 12 files changed

+449/−560 lines, 12 filesdep +boringdep −semigroupsdep −transformers-compatdep ~basedep ~mtldep ~transformersPVP ok

version bump matches the API change (PVP)

Dependencies added: boring

Dependencies removed: semigroups, transformers-compat

Dependency ranges changed: base, mtl, transformers

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +17/−0
• constraints.cabal +34/−35
• src/Data/Constraint.hs +69/−134
• src/Data/Constraint/Char.hs +60/−0
• src/Data/Constraint/Deferrable.hs +19/−58
• src/Data/Constraint/Forall.hs +30/−102
• src/Data/Constraint/Lifting.hs +1/−79
• src/Data/Constraint/Nat.hs +80/−81
• src/Data/Constraint/Symbol.hs +33/−33
• src/Data/Constraint/Unsafe.hs +70/−26
• tests/GH117Spec.hs +34/−0
• tests/GH55Spec.hs +2/−12

@@ -1,3 +1,20 @@+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

@@ -1,15 +1,15 @@+cabal-version: 2.4 name:          constraints category:      Constraints-version:       0.13.4-license:       BSD2-cabal-version: >= 1.10+version:       0.14+license:       BSD-2-Clause license-file:  LICENSE author:        Edward A. Kmett maintainer:    Edward A. Kmett <ekmett@gmail.com> stability:     experimental homepage:      http://github.com/ekmett/constraints/ bug-reports:   http://github.com/ekmett/constraints/issues-copyright:     Copyright (C) 2011-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,22 +17,23 @@   This package provides a vocabulary for working with them.  build-type:    Simple-tested-with:   GHC == 7.8.4-             , GHC == 7.10.3-             , GHC == 8.0.2-             , GHC == 8.2.2-             , GHC == 8.4.4-             , GHC == 8.6.5-             , GHC == 8.8.4-             , GHC == 8.10.7-             , GHC == 9.0.2-             , GHC == 9.2.1++tested-with:+  GHC == 9.8.1+  GHC == 9.6.3+  GHC == 9.4.7+  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@@ -51,33 +52,30 @@     GADTs    build-depends:-    base >= 4.7 && < 5,-    binary >= 0.7.1 && < 0.9,-    deepseq >= 1.3 && < 1.5,-    ghc-prim,-    hashable >= 1.2 && < 1.5,-    mtl >= 2.1.2 && < 2.4,-    transformers >= 0.3.0.0 && < 0.7,-    transformers-compat >= 0.5 && < 1,-    type-equality >= 1 && < 2-  if impl(ghc < 8.0)-    build-depends: semigroups >= 0.17 && < 0.21+    , base           >= 4.12  && < 5+    , binary         >= 0.7.1 && < 0.9+    , boring         >= 0.2   && < 0.3+    , deepseq        >= 1.3   && < 1.6+    , ghc-prim+    , hashable       >= 1.2   && < 1.5+    , mtl            >= 2.2   && < 2.4+    , transformers   >= 0.5   && < 0.7+    , type-equality  >= 1     && < 2    exposed-modules:     Data.Constraint     Data.Constraint.Deferrable     Data.Constraint.Forall     Data.Constraint.Lifting+    Data.Constraint.Nat+    Data.Constraint.Symbol     Data.Constraint.Unsafe -  if impl(ghc >= 8)+  if impl(ghc >= 9.2)     exposed-modules:-      Data.Constraint.Nat-      Data.Constraint.Symbol+      Data.Constraint.Char -  ghc-options: -Wall-  if impl(ghc >= 8.6)-    ghc-options: -Wno-star-is-type+  ghc-options: -Wall -Wno-star-is-type  test-suite spec   type: exitcode-stdio-1.0@@ -85,9 +83,10 @@   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 >= 4.7 && < 5,-    constraints,-    hspec >= 2+    , base+    , constraints+    , hspec >= 2

@@ -1,41 +1,28 @@-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE RoleAnnotations #-}-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UnicodeSyntax #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 706 {-# LANGUAGE PolyKinds #-}-#endif-#if __GLASGOW_HASKELL__ >= 800-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE UndecidableSuperClasses #-}-#endif-#if __GLASGOW_HASKELL__ >= 708 && __GLASGOW_HASKELL__ < 710-{-# LANGUAGE NullaryTypeClasses #-}-#endif-#if __GLASGOW_HASKELL__ >= 806 {-# LANGUAGE QuantifiedConstraints #-}-#endif------------------------------------------------------------------------------+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE UnicodeSyntax #-}+ -- |--- Module      :  Data.Constraint -- Copyright   :  (C) 2011-2015 Edward Kmett, -- License     :  BSD-style (see the file LICENSE)--- -- Maintainer  :  Edward Kmett <ekmett@gmail.com> -- Stability   :  experimental -- Portability :  non-portable@@ -57,7 +44,7 @@ -- -- 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@@ -70,13 +57,13 @@   -- * Entailment   , (:-)(Sub)   , type (⊢)+  , type (|-)+  , type (&)   , weaken1, weaken2, contract   , strengthen1, strengthen2   , (&&&), (***)   , trans, refl-#if __GLASGOW_HASKELL__ >= 806   , implied-#endif   , Bottom(no)   , top, bottom   -- * Dict is fully faithful@@ -91,33 +78,19 @@ import Control.DeepSeq import Control.Monad import Data.Complex-#if __GLASGOW_HASKELL__ >= 800 && __GLASGOW_HASKELL__ < 806-import Data.Kind-#endif import Data.Ratio-#if !MIN_VERSION_base(4,11,0)-import Data.Semigroup-#endif 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)-#if MIN_VERSION_base(4,8,0) import Numeric.Natural (Natural)-#endif-#if !MIN_VERSION_base(4,8,0)-import Data.Word (Word)-#endif import Data.Coerce (Coercible) import Data.Type.Coercion(Coercion(..))-#if MIN_VERSION_base(4,9,0) import Data.Type.Equality (type (~~)) import qualified Data.Type.Equality.Hetero as Hetero-#endif-#if MIN_VERSION_base(4,10,0) import Type.Reflection (TypeRep, typeRepKind, withTypeable)-#endif+import Data.Boring (Boring (..))  -- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. --@@ -139,7 +112,15 @@   Dict :: a => Dict a   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@@ -153,10 +134,8 @@  dictDataType :: DataType dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]+-} -deriving instance Eq (Dict a)-deriving instance Ord (Dict a)-deriving instance Show (Dict a)  instance NFData (Dict c) where   rnf Dict = ()@@ -179,15 +158,11 @@ instance HasDict (a ~ b) (a :~: b) where   evidence Refl = Dict -#if MIN_VERSION_base(4,9,0) instance HasDict (a ~~ b) (a Hetero.:~~: b) where   evidence Hetero.HRefl = Dict-#endif -#if MIN_VERSION_base(4,10,0) instance HasDict (Typeable k, Typeable a) (TypeRep (a :: k)) where   evidence tr = withTypeable tr $ withTypeable (typeRepKind tr) Dict-#endif  -- | From a 'Dict', takes a value in an environment where the instance -- witnessed by the 'Dict' is in scope, and evaluates it.@@ -272,28 +247,23 @@ -- library is sensible and can't break any assumptions on the behalf of -- library authors. newtype a :- b = Sub (a => Dict b)-  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@@ -334,19 +304,43 @@ -- QuantifiedConstraints -------------------------------------------------------------------------------- -#if __GLASGOW_HASKELL__ >= 806 -- | Convert a quantified constraint into an entailment.------ Only available on GHC 8.6 or later. implied :: forall a b. (a => b) => a :- b implied = Sub (Dict :: Dict b)-#endif +-- | 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)@@ -498,10 +492,8 @@ 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-#if MIN_VERSION_base(4,8,0) instance Eq a :=> Eq (Const a b) where ins = Sub Dict instance () :=> Eq Natural where ins = Sub Dict-#endif  -- Ord instance Class (Eq a) (Ord a) where cls = Sub Dict@@ -521,10 +513,8 @@ 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-#if MIN_VERSION_base(4,8,0) instance Ord a :=> Ord (Const a b) where ins = Sub Dict instance () :=> Ord Natural where ins = Sub Dict-#endif  -- Show instance Class () (Show a) where cls = Sub Dict@@ -543,10 +533,8 @@ 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-#if MIN_VERSION_base(4,8,0) instance Show a :=> Show (Const a b) where ins = Sub Dict instance () :=> Show Natural where ins = Sub Dict-#endif  -- Read instance Class () (Read a) where cls = Sub Dict@@ -563,10 +551,8 @@ 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-#if MIN_VERSION_base(4,8,0) instance Read a :=> Read (Const a b) where ins = Sub Dict instance () :=> Read Natural where ins = Sub Dict-#endif  -- Enum instance Class () (Enum a) where cls = Sub Dict@@ -580,13 +566,9 @@ instance () :=> Enum Double where ins = Sub Dict instance Integral a :=> Enum (Ratio a) where ins = Sub Dict instance () :=> Enum Word where ins = Sub Dict-#if MIN_VERSION_base(4,9,0) instance Enum a :=> Enum (Identity a) where ins = Sub Dict instance Enum a :=> Enum (Const a b) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,8,0) instance () :=> Enum Natural where ins = Sub Dict-#endif  -- Bounded instance Class () (Bounded a) where cls = Sub Dict@@ -597,10 +579,8 @@ 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-#if MIN_VERSION_base(4,9,0) instance Bounded a :=> Bounded (Identity a) where ins = Sub Dict instance Bounded a :=> Bounded (Const a b) where ins = Sub Dict-#endif  -- Num instance Class () (Num a) where cls = Sub Dict@@ -611,13 +591,9 @@ 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-#if MIN_VERSION_base(4,9,0) instance Num a :=> Num (Identity a) where ins = Sub Dict instance Num a :=> Num (Const a b) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,8,0) instance () :=> Num Natural where ins = Sub Dict-#endif  -- Real instance Class (Num a, Ord a) (Real a) where cls = Sub Dict@@ -627,26 +603,18 @@ instance () :=> Real Double where ins = Sub Dict instance Integral a :=> Real (Ratio a) where ins = Sub Dict instance () :=> Real Word where ins = Sub Dict-#if MIN_VERSION_base(4,9,0) instance Real a :=> Real (Identity a) where ins = Sub Dict instance Real a :=> Real (Const a b) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,8,0) instance () :=> Real Natural where ins = Sub Dict-#endif  -- 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-#if MIN_VERSION_base(4,9,0) instance Integral a :=> Integral (Identity a) where ins = Sub Dict instance Integral a :=> Integral (Const a b) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,8,0) instance () :=> Integral Natural where ins = Sub Dict-#endif  -- Bits instance Class (Eq a) (Bits a) where cls = Sub Dict@@ -654,13 +622,9 @@ instance () :=> Bits Int where ins = Sub Dict instance () :=> Bits Integer where ins = Sub Dict instance () :=> Bits Word where ins = Sub Dict-#if MIN_VERSION_base(4,9,0) instance Bits a :=> Bits (Identity a) where ins = Sub Dict instance Bits a :=> Bits (Const a b) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,8,0) instance () :=> Bits Natural where ins = Sub Dict-#endif  -- Fractional instance Class (Num a) (Fractional a) where cls = Sub Dict@@ -668,39 +632,31 @@ 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-#if MIN_VERSION_base(4,9,0) instance Fractional a :=> Fractional (Identity a) where ins = Sub Dict instance Fractional a :=> Fractional (Const a b) where ins = Sub Dict-#endif  -- 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-#if MIN_VERSION_base(4,9,0) instance Floating a :=> Floating (Identity a) where ins = Sub Dict instance Floating a :=> Floating (Const a b) where ins = Sub Dict-#endif  -- 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-#if MIN_VERSION_base(4,9,0) instance RealFrac a :=> RealFrac (Identity a) where ins = Sub Dict instance RealFrac a :=> RealFrac (Const a b) where ins = Sub Dict-#endif  -- 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-#if MIN_VERSION_base(4,9,0) instance RealFloat a :=> RealFloat (Identity a) where ins = Sub Dict instance RealFloat a :=> RealFloat (Const a b) where ins = Sub Dict-#endif  -- Semigroup instance Class () (Semigroup a) where cls = Sub Dict@@ -710,29 +666,19 @@ 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-#if MIN_VERSION_base(4,9,0) instance Semigroup a :=> Semigroup (Identity a) where ins = Sub Dict-#endif-#if MIN_VERSION_base(4,10,0) instance Semigroup a :=> Semigroup (IO a) where ins = Sub Dict-#endif  -- Monoid-#if MIN_VERSION_base(4,11,0) instance Class (Semigroup a) (Monoid a) where cls = Sub Dict-#else-instance Class () (Monoid a) where cls = Sub Dict-#endif 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-#if MIN_VERSION_base(4,9,0) instance Monoid a :=> Monoid (Identity a) where ins = Sub Dict instance Monoid a :=> Monoid (IO a) where ins = Sub Dict-#endif  -- Functor instance Class () (Functor f) where cls = Sub Dict@@ -764,11 +710,7 @@ instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict  -- Monad-#if MIN_VERSION_base(4,8,0) instance Class (Applicative f) (Monad f) where cls = Sub Dict-#else-instance Class () (Monad f) where cls = Sub Dict-#endif instance () :=> Monad [] where ins = Sub Dict instance () :=> Monad ((->) a) where ins = Sub Dict instance () :=> Monad (Either a) where ins = Sub Dict@@ -776,11 +718,7 @@ instance () :=> Monad Identity where ins = Sub Dict  -- MonadPlus-#if MIN_VERSION_base(4,8,0) instance Class (Monad f, Alternative f) (MonadPlus f) where cls = Sub Dict-#else-instance Class (Monad f) (MonadPlus f) where cls = Sub Dict-#endif instance () :=> MonadPlus [] where ins = Sub Dict instance () :=> MonadPlus Maybe where ins = Sub Dict @@ -807,7 +745,4 @@  instance a :=> Monoid (Dict a) where ins = Sub Dict instance a => Monoid (Dict a) where-#if !(MIN_VERSION_base(4,11,0))-  mappend = (<>)-#endif   mempty = Dict

@@ -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

@@ -1,42 +1,28 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-}--#if __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE TypeInType #-}-#endif+{-# LANGUAGE TypeOperators #-} ------------------------------------------------------------------------------ -- |--- Module      :  Data.Constraint.Deferrable--- Copyright   :  (C) 2015-2016 Edward Kmett+-- Copyright   :  (C) 2015-2021 Edward Kmett -- License     :  BSD-style (see the file LICENSE)--- -- Maintainer  :  Edward Kmett <ekmett@gmail.com> -- Stability   :  experimental -- Portability :  non-portable -- -- The idea for this trick comes from Dimitrios Vytiniotis.------------------------------------------------------------------------------  module Data.Constraint.Deferrable   ( UnsatisfiedConstraint(..)   , Deferrable(..)   , defer   , deferred-#if __GLASGOW_HASKELL__ >= 800-  , defer_-  , deferEither_   , (:~~:)(HRefl)-#endif   , (:~:)(Refl)   ) where @@ -47,10 +33,8 @@ import Data.Typeable (Typeable, cast, typeRep) import Data.Type.Equality ((:~:)(Refl)) -#if __GLASGOW_HASKELL__ >= 800 import GHC.Types (type (~~)) import Data.Type.Equality.Hetero ((:~~:)(HRefl))-#endif  newtype UnsatisfiedConstraint = UnsatisfiedConstraint String   deriving (Typeable, Show)@@ -60,64 +44,41 @@ -- | Allow an attempt at resolution of a constraint at a later time 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 p r proxy. 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--#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+deferred = Sub $ defer @p Dict --- | 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+defer :: forall p r. Deferrable p => (p => r) -> r+defer r = either (throw . UnsatisfiedConstraint) id $ deferEither @p r -showTypeRep :: Typeable t => Proxy t -> String-showTypeRep = show . typeRep+showTypeRep :: forall t. Typeable t => String+showTypeRep = show $ typeRep (Proxy @t)  instance Deferrable () where-  deferEither _ r = Right r+  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+  deferEither r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of     Just Refl -> Right r     Nothing   -> Left $-      "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `"  ++ showTypeRep (Proxy :: Proxy b) ++ "'"+      "deferred type equality: type mismatch between `" ++ showTypeRep @a ++ "’ and `"  ++ showTypeRep @b ++ "'" -#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+  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 b) ++ "'"-#endif+      "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

@@ -1,22 +1,21 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE Trustworthy #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-}-#if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-}-#endif------------------------------------------------------------------------------+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE GADTs #-}+ -- |--- Module      :  Data.Constraint.Forall--- Copyright   :  (C) 2011-2015 Edward Kmett,+-- Copyright   :  (C) 2011-2021 Edward Kmett, --                (C) 2015 Ørjan Johansen, --                (C) 2016 David Feuer -- License     :  BSD-style (see the file LICENSE)@@ -26,7 +25,6 @@ -- Portability :  non-portable -- -- This module uses a trick to provide quantification over constraints.-----------------------------------------------------------------------------  module Data.Constraint.Forall   ( Forall, inst@@ -34,95 +32,27 @@   , Forall1, inst1   , ForallT, instT   , ForallV, InstV (instV)-  , forall+  , forall_   ) where  import Data.Constraint import Unsafe.Coerce (unsafeCoerce) -#if __GLASGOW_HASKELL__ >= 806-# define KVS(kvs) kvs-#else-# define KVS(kvs)-#endif--{- 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.- -- - 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:- -- - 1. Using closed type families, it is possible to test whether two concrete- - types are equal, even if one of them is not directly importable.- -- - 2. Using just open type families, it is possible to test "at least 2 of- - these n+1 types are equal", thus using the pigeonhole principle to thwart- - any scheme based on having only a finite number of shared skolem types.- -- - 3. Using just pattern matching of types by unification, it is possible- - to extract the skolem types from the application the `Forall p` expands- - to. (Although type families are probably still needed to exploit this.)- -- - András Kovács and Ørjan Johansen independently realized that skolems- - themselves made as type family applications can be used to solve the first- - two problems (and discovered the third problem in the process). As a bonus,- - the resulting code is easy to make polykinded.- -- - Problem 1 is solved by making the type family have no instances, forcing- - GHC to make no assumption about what type a skolem is.- -- - Problem 2 is solved by parametrizing the skolem on the predicate tested- - for. (This is a known trick in predicate logic.)- -- - Problem 3 is solved by making the `Forall p` application expand to a type- - class, and have the *actual* test constraint be a superclass constraint on- - that type class, thus preventing the user directly accessing it.- -- - An unfortunate side effect of the new method is that it tends to trigger- - spurious errors from GHC test for cycles in superclass constraints. András- - Kovács discovered that these can be silenced by yet another use of a type- - family.- -- - David Feuer points out a remaining doubt about the soundness of this scheme:- - GHC *does* know that the skolems created from a single predicate `p` are- - equal. This could in theory apply even if the skolems come from two- - *distinct* invocations of `Forall p`.- -- - However, we don't know any way of bringing two such skolems in contact with- - each other to create an actual exploit. It would seem to require `p` to- - already contain its own skolem, despite there being (hopefully) no way to- - extract it from `Forall p` in order to tie the knot.- -}---- The `Skolem` type family represents skolem variables; do not export!--- If GHC supports it, these might be made closed with no instances.+class (forall a. p a) => Forall (p :: k -> Constraint)+instance (forall a. p a) => Forall (p :: k -> Constraint) -type family Skolem (p :: k -> Constraint) :: k+-- | Instantiate a quantified @'Forall' p@ constraint at type @a@.+inst :: forall p a. Forall p :- p a+inst = Sub Dict --- The outer `Forall` type family prevents GHC from giving a spurious--- superclass cycle error.--- The inner `Forall_` class prevents the skolem from leaking to the user,--- which would be disastrous.+data Dict1 p where+  Dict1 :: (forall a. p a) => Dict1 p --- | 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)+forallish :: forall p. Dict1 p -> Dict (Forall p)+forallish Dict1 = Dict --- | 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))+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)@@ -149,7 +79,7 @@ instance Forall (Q p t) => ForallT p t  -- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.-instT :: forall KVS(k1 k2 k3 k4) (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)+instT :: 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@@ -173,25 +103,23 @@ -- | 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+  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+  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+  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+  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

@@ -3,14 +3,11 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-}-#if !(MIN_VERSION_transformers(0,6,0))-{-# OPTIONS_GHC -fno-warn-deprecations #-}-#endif+ module Data.Constraint.Lifting   ( Lifting(..)   , Lifting2(..)@@ -37,16 +34,9 @@ import Control.Monad.Trans.State.Strict as Strict import Control.Monad.Trans.Writer.Lazy as Lazy import Control.Monad.Trans.Writer.Strict as Strict-#if !(MIN_VERSION_transformers(0,6,0))-import Control.Monad.Trans.Error-import Control.Monad.Trans.List-#endif 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@@ -54,16 +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 !(MIN_VERSION_base(4,11,0))-import Data.Semigroup-#endif-#if __GLASGOW_HASKELL__ < 710-import Data.Traversable-#endif import GHC.Arr  class Lifting p f where@@ -122,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@@ -131,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@@ -382,54 +352,6 @@ instance Lifting (MonadState s) (ReaderT r) where lifting = Sub Dict instance Lifting (MonadState s) (ExceptT e) where lifting = Sub Dict instance Lifting (MonadState s) (ContT r') where lifting = Sub Dict--#if !(MIN_VERSION_transformers(0,6,0))-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-# if !(MIN_VERSION_mtl(2,3,0))-instance Error e => Lifting MonadCont (ErrorT e) where lifting = Sub Dict-instance Error e => Lifting (MonadRWS r w s) (ErrorT e) where lifting = Sub Dict-instance Error e => Lifting (MonadReader r) (ErrorT e) where lifting = Sub Dict-instance Error e => Lifting (MonadState s) (ErrorT e) where lifting = Sub Dict-# endif--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-# if !(MIN_VERSION_mtl(2,3,0))-instance Lifting MonadCont ListT where lifting = Sub Dict-instance Lifting (MonadError e) ListT where lifting = Sub Dict-instance Lifting (MonadReader r) ListT where lifting = Sub Dict-instance Lifting (MonadState s) ListT where lifting = Sub Dict-# endif-#endif  class Lifting2 p f where   lifting2 :: p a :- Lifting p (f a) -- (p a, p b) :- p (f a b)

@@ -4,16 +4,13 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE UndecidableInstances #-}-#if __GLASGOW_HASKELL__ >= 805 {-# LANGUAGE NoStarIsType #-}-#endif -- | Utilities for working with 'KnownNat' constraints. -- -- This module is only available on GHC 8.0 or later.@@ -47,21 +44,20 @@   ) where  import Data.Constraint+import Data.Constraint.Unsafe import Data.Proxy import Data.Type.Bool import GHC.TypeLits+#if MIN_VERSION_base(4,18,0)+import qualified GHC.TypeNats as TN+#else 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-#if !(MIN_VERSION_base(4,11,0))-type family Div (m::Nat) (n::Nat) :: Nat where-    Div m 1 = m-type family Mod (m::Nat) (n::Nat) :: Nat where-    Mod 0 m = 0-#endif type family Gcd (m::Nat) (n::Nat) :: Nat where     Gcd m m = m type family Lcm (m::Nat) (n::Nat) :: Nat where@@ -69,43 +65,46 @@  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  magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o+#if MIN_VERSION_base(4,18,0)+magic f = Sub $ TN.withKnownNat @o (unsafeSNat (fromInteger (natVal (Proxy @n) `f` natVal (Proxy @m)))) Dict+#else magic f = Sub $ unsafeCoerce (Magic Dict) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))--axiom :: Dict c-axiom = unsafeCoerce (Dict :: Dict ())+#endif  axiomLe :: forall (a :: Nat) (b :: Nat). Dict (a <= b)-axiomLe = axiom+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 axiom+dividesGcd = Sub unsafeAxiom  dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c-dividesLcm = Sub axiom+dividesLcm = Sub unsafeAxiom  gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)-gcdCommutes = axiom+gcdCommutes = unsafeAxiom  lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)-lcmCommutes = axiom+lcmCommutes = unsafeAxiom  gcdZero :: forall a. Dict (Gcd 0 a ~ a)-gcdZero = axiom+gcdZero = unsafeAxiom  gcdOne :: forall a. Dict (Gcd 1 a ~ 1)-gcdOne = axiom+gcdOne = unsafeAxiom  lcmZero :: forall a. Dict (Lcm 0 a ~ 0)-lcmZero = axiom+lcmZero = unsafeAxiom  lcmOne :: forall a. Dict (Lcm 1 a ~ a)-lcmOne = axiom+lcmOne = unsafeAxiom  gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m) gcdNat = magic gcd@@ -151,14 +150,14 @@  minZero :: forall n. Dict (Min n 0 ~ 0) #if MIN_VERSION_base(4,16,0)-minZero = axiom+minZero = unsafeAxiom #else minZero = Dict #endif  maxZero :: forall n. Dict (Max n 0 ~ n) #if MIN_VERSION_base(4,16,0)-maxZero = axiom+maxZero = unsafeAxiom #else maxZero = Dict #endif@@ -167,104 +166,104 @@ powZero = Dict  leZero :: forall a. (a <= 0) :- (a ~ 0)-leZero = Sub axiom+leZero = Sub unsafeAxiom  zeroLe :: forall (a :: Nat). Dict (0 <= a) #if MIN_VERSION_base(4,16,0)-zeroLe = axiom+zeroLe = unsafeAxiom #else zeroLe = Dict #endif  plusMinusInverse1 :: forall n m. Dict (((m + n) - n) ~ m)-plusMinusInverse1 = axiom+plusMinusInverse1 = unsafeAxiom  plusMinusInverse2 :: forall n m. (m <= n) :- (((m + n) - m) ~ n)-plusMinusInverse2 = Sub axiom+plusMinusInverse2 = Sub unsafeAxiom  plusMinusInverse3 :: forall n m. (n <= m) :- (((m - n) + n) ~ m)-plusMinusInverse3 = Sub axiom+plusMinusInverse3 = Sub unsafeAxiom  plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)-plusMonotone1 = Sub axiom+plusMonotone1 = Sub unsafeAxiom  plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)-plusMonotone2 = Sub axiom+plusMonotone2 = Sub unsafeAxiom  powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))-powMonotone1 = Sub axiom+powMonotone1 = Sub unsafeAxiom  powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))-powMonotone2 = Sub axiom+powMonotone2 = Sub unsafeAxiom  divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)-divMonotone1 = Sub axiom+divMonotone1 = Sub unsafeAxiom  divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)-divMonotone2 = Sub axiom+divMonotone2 = Sub unsafeAxiom  timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)-timesMonotone1 = Sub axiom+timesMonotone1 = Sub unsafeAxiom  timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)-timesMonotone2 = Sub axiom+timesMonotone2 = Sub unsafeAxiom  minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)-minMonotone1 = Sub axiom+minMonotone1 = Sub unsafeAxiom  minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)-minMonotone2 = Sub axiom+minMonotone2 = Sub unsafeAxiom  maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)-maxMonotone1 = Sub axiom+maxMonotone1 = Sub unsafeAxiom  maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)-maxMonotone2 = Sub axiom+maxMonotone2 = Sub unsafeAxiom  powOne :: forall n. Dict ((n ^ 1) ~ n)-powOne = axiom+powOne = unsafeAxiom  plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)-plusMod = Sub axiom+plusMod = Sub unsafeAxiom  timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)-timesMod = Sub axiom+timesMod = Sub unsafeAxiom  modBound :: forall m n. (1 <= n) :- (Mod m n <= n)-modBound = Sub axiom+modBound = Sub unsafeAxiom  euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))-euclideanNat = Sub axiom+euclideanNat = Sub unsafeAxiom  plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))-plusCommutes = axiom+plusCommutes = unsafeAxiom  timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))-timesCommutes = axiom+timesCommutes = unsafeAxiom  minCommutes :: forall n m. Dict (Min m n ~ Min n m)-minCommutes = axiom+minCommutes = unsafeAxiom  maxCommutes :: forall n m. Dict (Max m n ~ Max n m)-maxCommutes = axiom+maxCommutes = unsafeAxiom  plusAssociates :: forall m n o. Dict (((m + n) + o) ~ (m + (n + o)))-plusAssociates = axiom+plusAssociates = unsafeAxiom  timesAssociates :: forall m n o. Dict (((m * n) * o) ~ (m * (n * o)))-timesAssociates = axiom+timesAssociates = unsafeAxiom  minAssociates :: forall m n o. Dict (Min (Min m n) o ~ Min m (Min n o))-minAssociates = axiom+minAssociates = unsafeAxiom  maxAssociates :: forall m n o. Dict (Max (Max m n) o ~ Max m (Max n o))-maxAssociates = axiom+maxAssociates = unsafeAxiom  gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))-gcdAssociates = axiom+gcdAssociates = unsafeAxiom  lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))-lcmAssociates = axiom+lcmAssociates = unsafeAxiom  minIsIdempotent :: forall n. Dict (Min n n ~ n) minIsIdempotent = Dict@@ -279,82 +278,82 @@ lcmIsIdempotent = Dict  minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))-minDistributesOverPlus = axiom+minDistributesOverPlus = unsafeAxiom  minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))-minDistributesOverTimes = axiom+minDistributesOverTimes = unsafeAxiom  minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))-minDistributesOverPow1 = axiom+minDistributesOverPow1 = unsafeAxiom  minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))-minDistributesOverPow2 = axiom+minDistributesOverPow2 = unsafeAxiom  minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))-minDistributesOverMax = axiom+minDistributesOverMax = unsafeAxiom  maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))-maxDistributesOverPlus = axiom+maxDistributesOverPlus = unsafeAxiom  maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))-maxDistributesOverTimes = axiom+maxDistributesOverTimes = unsafeAxiom  maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))-maxDistributesOverPow1 = axiom+maxDistributesOverPow1 = unsafeAxiom  maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))-maxDistributesOverPow2 = axiom+maxDistributesOverPow2 = unsafeAxiom  maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))-maxDistributesOverMin = axiom+maxDistributesOverMin = unsafeAxiom  plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))-plusDistributesOverTimes = axiom+plusDistributesOverTimes = unsafeAxiom  timesDistributesOverPow  :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))-timesDistributesOverPow = axiom+timesDistributesOverPow = unsafeAxiom  timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))-timesDistributesOverGcd = axiom+timesDistributesOverGcd = unsafeAxiom  timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))-timesDistributesOverLcm = axiom+timesDistributesOverLcm = unsafeAxiom  plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)-plusIsCancellative = Sub axiom+plusIsCancellative = Sub unsafeAxiom  timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)-timesIsCancellative = Sub axiom+timesIsCancellative = Sub unsafeAxiom  gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))-gcdDistributesOverLcm = axiom+gcdDistributesOverLcm = unsafeAxiom  lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))-lcmDistributesOverGcd = axiom+lcmDistributesOverGcd = unsafeAxiom  dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)-dividesPlus = Sub axiom+dividesPlus = Sub unsafeAxiom  dividesTimes :: Divides a b :- Divides a (b * c)-dividesTimes = Sub axiom+dividesTimes = Sub unsafeAxiom  dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)-dividesMin = Sub axiom+dividesMin = Sub unsafeAxiom  dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)-dividesMax = Sub axiom+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 axiom+dividesDef = Sub unsafeAxiom  dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)-dividesPow = Sub axiom+dividesPow = Sub unsafeAxiom  timesDiv :: forall a b. Dict ((a * Div b a) <= b)-timesDiv = axiom+timesDiv = unsafeAxiom  -- (<=) is an internal category in the category of constraints. @@ -362,7 +361,7 @@ leId = Dict  leEq :: forall (a :: Nat) (b :: Nat). (a <= b, b <= a) :- (a ~ b)-leEq = Sub axiom+leEq = Sub unsafeAxiom  leTrans :: forall (a :: Nat) (b :: Nat) (c :: Nat). (b <= c, a <= b) :- (a <= c) leTrans = Sub (axiomLe @a @c)

@@ -9,8 +9,6 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE CPP #-} -- | Utilities for working with 'KnownSymbol' constraints.------ This module is only available on GHC 8.0 or later. module Data.Constraint.Symbol   ( type AppendSymbol   , type (++)@@ -39,12 +37,13 @@  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--#if !(MIN_VERSION_base(4,10,0))-type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol #endif  -- | An infix synonym for 'AppendSymbol'.@@ -57,43 +56,44 @@  -- 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 :: Proxy n)) `f` symbolVal (Proxy :: 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 :: Proxy n) `f` symbolVal (Proxy :: 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 :: Proxy a))))--axiom :: Dict c-axiom = unsafeCoerce (Dict :: Dict ())+#endif --- axioms and operations+-- operations  appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b) appendSymbol = magicSSS (++)  appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)-appendUnit1 =-#if MIN_VERSION_base(4,10,0)-  Dict-#else-  axiom-#endif+appendUnit1 = Dict  appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)-appendUnit2 =-#if MIN_VERSION_base(4,10,0)-  Dict-#else-  axiom-#endif+appendUnit2 = Dict  appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))-appendAssociates = axiom+appendAssociates = unsafeAxiom  takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a) takeSymbol = magicNSS take@@ -102,37 +102,37 @@ dropSymbol = magicNSS drop  takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)-takeAppendDrop = axiom+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 axiom+takeLength = Sub unsafeAxiom  take0 :: forall a. Dict (Take 0 a ~ "")-take0 = axiom+take0 = unsafeAxiom  takeEmpty :: forall n. Dict (Take n "" ~ "")-takeEmpty = axiom+takeEmpty = unsafeAxiom  dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")-dropLength = Sub axiom+dropLength = Sub unsafeAxiom  drop0 :: forall a. Dict (Drop 0 a ~ a)-drop0 = axiom+drop0 = unsafeAxiom  dropEmpty :: forall n. Dict (Drop n "" ~ "")-dropEmpty = axiom+dropEmpty = unsafeAxiom  lengthTake :: forall n a. Dict (Length (Take n a) <= n)-lengthTake = axiom+lengthTake = unsafeAxiom  lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))-lengthDrop = axiom+lengthDrop = unsafeAxiom  dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)-dropDrop = axiom+dropDrop = unsafeAxiom  takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)-takeTake = axiom+takeTake = unsafeAxiom

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-}@@ -6,36 +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 <ekmett@gmail.com> -- Stability   :  experimental -- Portability :  non-portable -------------------------------------------------------------------------------+-- Unsafe utilities used throughout @constraints@. As the names suggest, these+-- functions are unsafe in general and can cause your program to segfault if+-- used improperly. Handle with care.+ module Data.Constraint.Unsafe   ( Coercible+  , unsafeAxiom   , unsafeCoerceConstraint   , unsafeDerive   , unsafeUnderive-  -- * 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 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@@ -48,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

@@ -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

@@ -1,22 +1,16 @@-{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}--#if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE TypeApplications #-}-#endif+{-# LANGUAGE TypeOperators #-}  module GH55Spec (main, spec) where -import Test.Hspec--#if __GLASGOW_HASKELL__ >= 800 import Data.Constraint import Data.Constraint.Nat import GHC.TypeLits+import Test.Hspec  newtype GF (n :: Nat) = GF Integer deriving (Eq, Show) @@ -48,10 +42,6 @@ spec = describe "GH #53" $          it "should normalize Lcm m m" $            z `shouldBe` (GF 0 :: GF (Lcm 5 5))-#else-spec :: Spec-spec = return ()-#endif  main :: IO () main = hspec spec