constraints-extras 0.3.2.1 → 0.4.0.0

raw patch · 6 files changed

+99/−98 lines, 6 filesdep ~basedep ~constraintsdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, constraints, template-haskell

API changes (from Hackage documentation)

Files

• ChangeLog.md +6/−0
• README.lhs +11/−0
• README.md +11/−0
• constraints-extras.cabal +3/−3
• src/Data/Constraint/Extras.hs +53/−81
• src/Data/Constraint/Extras/TH.hs +15/−14

@@ -1,5 +1,11 @@ # Revision history for constraints-extras +## 0.4.0.0 - 2022-11-18++* Make `Has` from a type synonym into the class upon which everything else is based. Instances may define either `has` or `argDict` which are now both methods of `Has`. This should hopefully improve the readability of type errors involving the library a fair bit, as everything wanted to use `Has`, but it was defined in terms of the less commonly appearing `ArgDict` and `ConstraintsFor`.+* The `ConstraintsFor` type family has been removed as it is now unnecessary, as instances of `Has` can simply be constrained directly. This has the added benefit of allowing `QuantifiedConstraints` in those instance heads that formerly would not have been allowed as part of the result of a type family.+* The `ArgDict` class has also been removed, as it was also basically never used on its own.+ ## 0.3.2.1 - 2021-12-17  * Support GHC 9.2

@@ -14,10 +14,12 @@ > {-# LANGUAGE TypeApplications  #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE FlexibleContexts #-}+> {-# LANGUAGE ConstraintKinds #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE UndecidableInstances #-} > {-# LANGUAGE ExistentialQuantification #-}+> {-# LANGUAGE TypeFamilies #-} > > import Data.Aeson > import Data.Constraint.Forall@@ -41,6 +43,14 @@ > > deriveArgDict ''V >+> data family Fam a :: * -> *+> data instance Fam () :: * -> * where+>   FI :: Fam () Int+>   FB :: Fam () Bool+>+> deriveArgDict 'FI+> -- this derives an instance Has c (Fam ()) by looking up the associated data instance.+> > data DSum k f = forall a. DSum (k a) (f a) > > -- Derive a ToJSON instance for our 'DSum'@@ -65,4 +75,5 @@ > > main :: IO () > main = return ()+ ```

@@ -14,10 +14,12 @@ > {-# LANGUAGE TypeApplications  #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE FlexibleContexts #-}+> {-# LANGUAGE ConstraintKinds #-} > {-# LANGUAGE FlexibleInstances #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE UndecidableInstances #-} > {-# LANGUAGE ExistentialQuantification #-}+> {-# LANGUAGE TypeFamilies #-} > > import Data.Aeson > import Data.Constraint.Forall@@ -41,6 +43,14 @@ > > deriveArgDict ''V >+> data family Fam a :: * -> *+> data instance Fam () :: * -> * where+>   FI :: Fam () Int+>   FB :: Fam () Bool+>+> deriveArgDict 'FI+> -- this derives an instance Has c (Fam ()) by looking up the associated data instance.+> > data DSum k f = forall a. DSum (k a) (f a) > > -- Derive a ToJSON instance for our 'DSum'@@ -65,4 +75,5 @@ > > main :: IO () > main = return ()+ ```

@@ -1,5 +1,5 @@ name: constraints-extras-version: 0.3.2.1+version: 0.4.0.0 synopsis: Utility package for constraints description: Convenience functions and TH for working with constraints. See <https://github.com/obsidiansystems/constraints-extras/blob/develop/README.md README.md> for example usage. category: Constraints@@ -32,9 +32,9 @@                   , TypeOperators                   , ConstraintKinds                   , TemplateHaskell-  build-depends: base >=4.9 && <4.17+  build-depends: base >=4.9 && <4.18                , constraints >= 0.9 && < 0.14-               , template-haskell >=2.11 && <2.19+               , template-haskell >=2.11 && <2.20   hs-source-dirs:  src   default-language: Haskell2010 

@@ -7,6 +7,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}@@ -28,15 +29,11 @@ -- must come from the set { @Int@, @Bool@ }. We call this the "set of -- types @a@ that could be applied to @Tag@". module Data.Constraint.Extras-  ( -- * The ArgDict typeclass-    ArgDict(..)-  , ConstraintsFor'+  ( -- * The Has typeclass+    Has(..)   , argDict'-  , ConstraintsForV   , argDictV     -- * Bringing instances into scope-  , Has-  , has   , Has'   , has'   , HasV@@ -44,8 +41,6 @@   , whichever     -- * Misc   , Implies1(..)-    -- * Deprecated-  , ArgDictV   ) where  import Data.Constraint@@ -56,93 +51,69 @@ import Data.Kind import GHC.Generics ((:+:)(..)) --- | Morally, this class is for GADTs whose indices can be finitely--- enumerated. An @'ArgDict' c f@ instance allows us to do two things:------ 1. 'ConstraintsFor' requests the set of constraints @c a@ for all---    possible types @a@ that could be applied to @f@.------ 2. 'argDict' selects a specific @c a@ given a value of type @f a@.------ Use 'Data.Constraint.Extras.TH.deriveArgDict' to derive instances--- of this class.-class ArgDict (c :: k -> Constraint) (f :: k -> Type) where-  -- | Apply @c@ to each possible type @a@ that could appear in a @f a@.+-- | The constraint @Has c f@ means that given any value of type @f a@, we can determine+-- that there is an instance of @c a@. For example, @Has Show Tag@ means that given any+-- @x :: Tag a@, we can conclude @Show a@. Most commonly, the type @f@ will be a GADT,+-- where we can enumerate all the possible index types through pattern matching, and+-- discover that there is an appropriate instance in each case. In this sort of+-- situation, the @c@ can be left entirely polymorphic in the instance for @Has@, and+-- this is the sort of instance that the provided Template Haskell code writes.++-- It is also sometimes possible to hand-write instances of @Has c f@ for specific+-- classes @c@ in cases where @f@ is a data type that packs an appropriate dictionary+-- into its constructors.+class Has c f where+  -- | Use the @f a@ to show that there is an instance of @c a@, and+  -- bring it into scope.   ---  -- > ConstraintsFor Show Tag = (Show Int, Show Bool)-  type ConstraintsFor f c :: Constraint+  -- The order of type variables is chosen to work+  -- with @-XTypeApplications@.+  --+  -- > -- Hold a value of type a, along with a tag identifying the a.+  -- > data SomeTagged tag where+  -- >   SomeTagged :: a -> tag a -> SomeTagged tag+  -- >+  -- > -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we+  -- > -- have no knowledge of the tag type.+  -- > showSomeTagged :: Has Show tag => SomeTagged tag -> String+  -- > showSomeTagged (SomeTagged a tag) = has @Show tag $ show a+  has :: forall a r. f a -> (c a => r) -> r+  has x r | Dict <- argDict @c x = r -  -- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@.+  -- | Use an @f a@ to obtain a dictionary for @c a@   ---  -- > argDict I :: Dict (Show Int)-  argDict :: ConstraintsFor f c => f a -> Dict (c a)+  -- > argDict @Show I :: Dict (Show Int)+  argDict :: forall a. f a -> Dict (c a)+  argDict x = has @c x Dict+  {-# MINIMAL has | argDict #-}  -- | @since 0.3.2.0-instance (ArgDict c f, ArgDict c g) => ArgDict c (f :+: g) where-  type ConstraintsFor (f :+: g) c = (ConstraintsFor f c, ConstraintsFor g c)+instance (Has c f, Has c g) => Has c (f :+: g) where   argDict = \case     L1 f -> argDict f     R1 g -> argDict g  -- | @since 0.3.2.0-instance (ArgDict c f, ArgDict c g) => ArgDict c (Sum f g) where-  type ConstraintsFor (Sum f g) c = (ConstraintsFor f c, ConstraintsFor g c)+instance (Has c f, Has c g) => Has c (Sum f g) where   argDict = \case     InL f -> argDict f     InR g -> argDict g --- | \"Primed\" variants (@ConstraintsFor'@, 'argDict'', 'Has'',--- 'has'', &c.) use the 'ArgDict' instance on @f@ to apply constraints--- on @g a@ instead of just @a@. This is often useful when you have--- data structures parameterised by something of kind @(x -> Type) ->--- Type@, like in the @dependent-sum@ and @dependent-map@ libraries.------ > ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool))-type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)---- | Get a dictionary for a specific @g a@, using a value of type @f a@.------ > argDict' B :: Dict (Show (Identity Bool))-argDict' :: forall f c g a. (Has' c f g) => f a -> Dict (c (g a))-argDict' tag = case argDict tag of-  (Dict :: Dict (ComposeC c g a)) -> Dict--type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)--argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g))-argDictV tag = case argDict tag of-  (Dict :: Dict (FlipC (ComposeC c) g a)) -> Dict--{-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-}-type ArgDictV f c = ArgDict f c+-- | The constraint @Has' c f g@ means that given a value of type @f a@, we can satisfy the constraint @c (g a)@.+type Has' (c :: k -> Constraint) f (g :: k' -> k) = Has (ComposeC c g) f --- | @Has c f@ is a constraint which means that for every type @a@--- that could be applied to @f@, we have @c a@.------ > Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool)-type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)+-- | The constraint @HasV c f g@ means that given a value of type @f v@, we can satisfy the constraint @c (v g)@.+type HasV c f g = Has (FlipC (ComposeC c) g) f --- | @Has' c f g@ is a constraint which means that for every type @a@--- that could be applied to @f@, we have @c (g a)@.+-- | Get a dictionary for @c (g a)@, using a value of type @f a@. ----- > Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool))-type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)-type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)+-- > argDict' @Show @Identity B :: Dict (Show (Identity Bool))+argDict' :: forall c g f a. (Has' c f g) => f a -> Dict (c (g a))+argDict' x = has @(ComposeC c g) x Dict --- | Use the @a@ from @f a@ to select a specific @c a@ constraint, and--- bring it into scope. The order of type variables is chosen to work--- with @-XTypeApplications@.------ > -- Hold an a, along with a tag identifying the a.--- > data SomeTagged tag where--- >   SomeTagged :: a -> tag a -> SomeTagged tag--- >--- > -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we--- > -- have no knowledge of the tag type.--- > showSomeTagged :: Has Show tag => SomeTagged tag -> String--- > showSomeTagged (SomeTagged a tag) = has @Show tag $ show a-has :: forall c f a r. Has c f => f a -> (c a => r) -> r-has k r | (Dict :: Dict (c a)) <- argDict k = r+-- | Get a dictionary for @c (v g)@, using a value of type @f v@.+argDictV :: forall f c g v. (HasV c f g) => f v -> Dict (c (v g))+argDictV x = has @(FlipC (ComposeC c) g) x Dict  -- | Like 'has', but we get a @c (g a)@ instance brought into scope -- instead. Use @-XTypeApplications@ to specify @c@ and @g@.@@ -153,11 +124,12 @@ -- > -- Show the value from a dependent sum. (We'll need 'whichever', discussed later, to show the key.) -- > showDSumVal :: forall tag f . Has' Show tag f => DSum tag f -> String -- > showDSumVal (tag :=> fa) = has' @Show @f tag $ show fa-has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r-has' k r | (Dict :: Dict (c (g a))) <- argDict' k = r+has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r+has' k r = has @(ComposeC c g) k r -hasV :: forall c g f v r. HasV c f g => f v -> (c (v g) => r) -> r-hasV k r | (Dict :: Dict (c (v g))) <- argDictV k = r+-- | Similar to 'has', but given a value of type @f v@, we get a @c (v g)@ instance brought into scope instead.+hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> r+hasV k r = has @(FlipC (ComposeC c) g) k r  -- | Given "forall a. @c (t a)@" (the @ForallF c t@ constraint), select a -- specific @a@, and bring @c (t a)@ into scope. Use @-XTypeApplications@ to

@@ -16,15 +16,14 @@   (typeHead, constrs) <- getDeclInfo n   c <- newName "c"   ts <- gadtIndices c constrs-  let xs = flip map ts $ \case-        Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c)+  let constraints = flip map ts $ \case+        Left t -> AppT (AppT (ConT ''Has) (VarT c)) t         Right t -> (AppT (VarT c) t)-      l = length xs-      constraints = foldl AppT (TupleT l) xs-  [d| instance ArgDict $(varT c) $(pure typeHead) where-        type ConstraintsFor  $(pure typeHead) $(varT c) = $(pure constraints)-        argDict = $(LamCaseE <$> matches c constrs 'argDict)-    |]+  ms <- matches c constrs 'argDict+  return+    [ InstanceD Nothing constraints (AppT (AppT (ConT ''Has) (VarT c)) typeHead)+      [ ValD (VarP 'argDict) (NormalB (LamCaseE ms)) [] ]+    ]  {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-} deriveArgDictV :: Name -> Q [Dec]@@ -33,13 +32,13 @@ matches :: Name -> [Con] -> Name -> Q [Match] matches c constrs argDictName = do   x <- newName "x"-  fmap concat $ forM constrs $ \case+  fmap concat . forM constrs $ \case     GadtC [name] _ _ -> return $       [Match (RecP name []) (NormalB $ ConE 'Dict) []]     ForallC _ _ (GadtC [name] bts (AppT _ (VarT b))) -> do       ps <- forM bts $ \case         (_, AppT t (VarT b')) | b == b' -> do-          hasArgDictInstance <- not . null <$> reifyInstances ''ArgDict [VarT c, t]+          hasArgDictInstance <- not . null <$> reifyInstances ''Has [VarT c, t]           return $ if hasArgDictInstance             then Just x             else Nothing@@ -81,8 +80,11 @@     tyVars <- replicateM (arity - 1) (newName "a")     let typeHead = foldr (\v x -> AppT x (VarT v)) (ConT n) tyVars     return (typeHead, constrs)-  DataConI _ (ForallT _ _ (AppT typeHead _)) parent -> do-    reify parent >>= \case+  DataConI _ (AppT typeHead _) parent -> handleParent typeHead parent+  DataConI _ (ForallT _ _ (AppT typeHead _)) parent -> handleParent typeHead parent+  a -> error $ "getDeclInfo: Unmatched 'Info': " ++ show a+  where+    handleParent typeHead parent = reify parent >>= \case       FamilyI _ instances -> do         let instCons :: InstanceDec -> [Con]             instCons = \case@@ -103,14 +105,13 @@           l@(_:_:_) -> error $ "getDeclInfo: Expected one data family instance for constructor " ++ show n ++ " but found multiple: " ++ show l           [i] -> return (typeHead, instCons i)       a -> error $ "getDeclInfo: Unmatched parent of data family instance: " ++ show a-  a -> error $ "getDeclInfo: Unmatched 'Info': " ++ show a  gadtIndices :: Name -> [Con] -> Q [Either Type Type] gadtIndices c constrs = fmap concat $ forM constrs $ \case   GadtC _ _ (AppT _ typ) -> return [Right typ]   ForallC _ _ (GadtC _ bts (AppT _ (VarT _))) -> fmap concat $ forM bts $ \case     (_, AppT t (VarT _)) -> do-      hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [VarT c, t]+      hasArgDictInstance <- fmap (not . null) $ reifyInstances ''Has [VarT c, t]       return $ if hasArgDictInstance then [Left t] else []     _ -> return []   ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]