constraints-extras 0.3.0.2 → 0.3.1.0

raw patch · 4 files changed

+194/−77 lines, 4 filesdep ~basedep ~constraintsdep ~template-haskellPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base, constraints, template-haskell

API changes (from Hackage documentation)

Files

• ChangeLog.md +9/−0
• constraints-extras.cabal +8/−8
• src/Data/Constraint/Extras.hs +107/−19
• src/Data/Constraint/Extras/TH.hs +70/−50

@@ -1,5 +1,14 @@ # Revision history for constraints-extras +## 0.3.1.0++* Allow deriving instances with `deriveArgDict` for data and newtype family instances by supplying the name of one of its constructors+* Support GHC 9.0.1++## 0.3.0.3 - 2020-06-22++* Update version bounds for GHC 8.10+ ## 0.3.0.2 - 2019-09-30  * Update version bounds for GHC 8.8

@@ -1,5 +1,5 @@ name: constraints-extras-version: 0.3.0.2+version: 0.3.1.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@@ -13,7 +13,7 @@ build-type: Simple cabal-version: 2.0 tested-with:-  GHC  ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1+  GHC  ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5 || ==8.8.1 || ==8.10.1 || ==9.0.1 extra-source-files: README.md                     ChangeLog.md @@ -24,7 +24,7 @@   exposed-modules: Data.Constraint.Extras                  , Data.Constraint.Extras.TH                  , Data.Constraint.Compose-  other-modules: Data.Constraint.Flip+                 , Data.Constraint.Flip   other-extensions: LambdaCase                   , MultiParamTypeClasses                   , QuasiQuotes@@ -32,18 +32,18 @@                   , TypeOperators                   , ConstraintKinds                   , TemplateHaskell-  build-depends: base >=4.9 && <4.14-               , constraints >= 0.9 && < 0.12-               , template-haskell >=2.11 && <2.16+  build-depends: base >=4.9 && <4.16+               , constraints >= 0.9 && < 0.13+               , template-haskell >=2.11 && <2.18   hs-source-dirs:  src   default-language: Haskell2010  executable readme   if !flag(build-readme)     buildable: False-  build-depends: base >=4.9 && <4.14+  build-depends: base                , aeson-               , constraints >= 0.9 && < 0.12+               , constraints                , constraints-extras   main-is: README.lhs   ghc-options: -Wall -optL -q

@@ -11,34 +11,86 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} -module Data.Constraint.Extras where+-- | Throughout this module, we use the following GADT and @ArgDict@ instance+-- in our examples:+--+-- > {-# LANGUAGE StandaloneDeriving #-}+-- >+-- > data Tag a where+-- >   I :: Tag Int+-- >   B :: Tag Bool+-- > deriving instance Show (Tag a)+-- >+-- > $(deriveArgDict ''Tag)+--+-- The constructors of @Tag@ mean that a type variable @a@ in @Tag a@+-- 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'+  , argDict'+  , ConstraintsForV+  , argDictV+    -- * Bringing instances into scope+  , Has+  , has+  , Has'+  , has'+  , HasV+  , hasV+  , whichever+    -- * Misc+  , Implies1(..)+    -- * Deprecated+  , ArgDictV+  ) where  import Data.Constraint import Data.Constraint.Compose import Data.Constraint.Flip import Data.Constraint.Forall+import Data.Kind --- | Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will--- select the appropriate type class dictionary from among a list of contenders based on a value of the type.--- There are a few different variations of this which we'd like to be able to support, and they're all implemented--- in the same fashion at the term level, by pattern matching on the constructors of the GADT, and producing Dict--- as the result.--- It would be nice to have some way to stop the proliferation of these variants and unify the existing ones, but--- at the moment, it appears to require honest type level functions. (Closed type families which must be fully--- applied didn't quite cut it when I tried). Some symbolic type-level application could do the trick, but I didn't--- want to go quite that far at the time of writing.+-- | 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@.+  --+  -- > ConstraintsFor Show Tag = (Show Int, Show Bool)+  type ConstraintsFor f c :: Constraint -class ArgDict (c :: k -> Constraint) (f :: k -> *) where-  type ConstraintsFor f (c :: k -> Constraint) :: Constraint+  -- | Use an @f a@ to select a specific dictionary from @ConstraintsFor f c@.+  --+  -- > argDict I :: Dict (Show Int)   argDict :: ConstraintsFor f c => f a -> Dict (c a) +-- | \"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') -> *) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)+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@@ -47,23 +99,59 @@ {-# DEPRECATED ArgDictV "Just use 'ArgDict'" #-} type ArgDictV f c = ArgDict f c +-- | @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)++-- | @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)@.+--+-- > 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) -has :: forall c f a r. (Has c f) => f a -> (c a => r) -> r+-- | 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 -has' :: forall c g f a r. (Has' c f g) => f a -> (c (g a) => r) -> r+-- | Like 'has', but we get a @c (g a)@ instance brought into scope+-- instead. Use @-XTypeApplications@ to specify @c@ and @g@.+--+-- > -- From dependent-sum:Data.Dependent.Sum+-- > data DSum tag f = forall a. !(tag a) :=> f a+-- >+-- > -- 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 -hasV :: forall c g f v r. (HasV c f g) => f v -> (c (v g) => r) -> 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 -whichever :: forall c t a r. (ForallF c t) => (c (t a) => r) -> 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+-- specify @c@, @t@ and @a@.+--+-- > -- Show the tag of a dependent sum, even though we don't know the tag type.+-- > showDSumKey :: forall tag f . ForallF Show tag => DSum tag f -> String+-- > showDSumKey ((tag :: tag a) :=> fa) = whichever @Show @tag @a $ show tag+whichever :: forall c t a r. ForallF c t => (c (t a) => r) -> r whichever r = r \\ (instF :: ForallF c t :- c (t a)) --- | Allows explicit specification of constraint implication+-- | Allows explicit specification of constraint implication. class Implies1 c d where   implies1 :: c a :- d a-

@@ -12,54 +12,50 @@  deriveArgDict :: Name -> Q [Dec] deriveArgDict n = do+  (typeHead, constrs) <- getDeclInfo n   c <- newName "c"-  ts <- gadtIndices c n+  ts <- gadtIndices c constrs   let xs = flip map ts $ \case         Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c)         Right t -> (AppT (VarT c) t)       l = length xs       constraints = foldl AppT (TupleT l) xs-  arity <- tyConArity n-  tyVars <- replicateM (arity - 1) (newName "a")-  let n' = foldr (\v x -> AppT x (VarT v)) (ConT n) tyVars-  [d| instance ArgDict $(varT c) $(pure n') where-        type ConstraintsFor  $(pure n') $(varT c) = $(pure constraints)-        argDict = $(LamCaseE <$> matches c n 'argDict)+  [d| instance ArgDict $(varT c) $(pure typeHead) where+        type ConstraintsFor  $(pure typeHead) $(varT c) = $(pure constraints)+        argDict = $(LamCaseE <$> matches c constrs 'argDict)     |]  {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-} deriveArgDictV :: Name -> Q [Dec] deriveArgDictV = deriveArgDict -matches :: Name -> Name -> Name -> Q [Match]-matches c n argDictName = do+matches :: Name -> [Con] -> Name -> Q [Match]+matches c constrs argDictName = do   x <- newName "x"-  reify n >>= \case-    TyConI (DataD _ _ _ _ constrs _) -> 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]-            return $ if hasArgDictInstance-              then Just x-              else Nothing-          _ -> return Nothing-        return $ case catMaybes ps of-          [] -> [Match (RecP name []) (NormalB $ ConE 'Dict) []]-          (v:_) ->-            let patf = \v' rest done -> if done-                  then WildP : rest done-                  else case v' of-                    Nothing -> WildP : rest done-                    Just _ -> VarP v : rest True-                pat = foldr patf (const []) ps False-            in [Match (ConP name pat) (NormalB $ AppE (VarE argDictName) (VarE v)) []]-      ForallC _ _ (GadtC [name] _ _) -> return $-        [Match (RecP name []) (NormalB $ ConE 'Dict) []]-      a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a-    a -> error $ "deriveArgDict matches: Unmatched 'Info': " ++ show a+  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]+          return $ if hasArgDictInstance+            then Just x+            else Nothing+        _ -> return Nothing+      return $ case catMaybes ps of+        [] -> [Match (RecP name []) (NormalB $ ConE 'Dict) []]+        (v:_) ->+          let patf = \v' rest done -> if done+                then WildP : rest done+                else case v' of+                  Nothing -> WildP : rest done+                  Just _ -> VarP v : rest True+              pat = foldr patf (const []) ps False+          in [Match (ConP name pat) (NormalB $ AppE (VarE argDictName) (VarE v)) []]+    ForallC _ _ (GadtC [name] _ _) -> return $+      [Match (RecP name []) (NormalB $ ConE 'Dict) []]+    a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a  kindArity :: Kind -> Int kindArity = \case@@ -69,20 +65,44 @@   ParensT t -> kindArity t   _ -> 0 -tyConArity :: Name -> Q Int-tyConArity n = reify n >>= return . \case-   TyConI (DataD _ _ ts mk _ _) -> fromMaybe 0 (fmap kindArity mk) + length ts-   _ -> error $ "tyConArity: Supplied name reified to something other than a data declaration: " ++ show n+getDeclInfo :: Name -> Q (Type, [Con])+getDeclInfo n = reify n >>= \case+  TyConI (DataD _ _ ts mk constrs _) -> do+    let arity = fromMaybe 0 (fmap kindArity mk) + length ts+    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+      FamilyI _ instances -> do+        let instCons :: InstanceDec -> [Con]+            instCons = \case+              DataInstD _ _ _ _ cons _ -> cons+              NewtypeInstD _ _ _ _ con _ -> [con]+              _ -> error $ "getDeclInfo: Expected a data or newtype family instance"+            conNames :: Con -> [Name]+            conNames = \case+              NormalC other _ -> [other]+              RecC other _ -> [other]+              InfixC _ other _ -> [other]+              ForallC _ _ con -> conNames con+              GadtC others _ _ -> others+              RecGadtC others _ _ -> others+            instHasThisConstructor i = any (== n) $ conNames =<< instCons i+        case filter instHasThisConstructor instances of+          [] -> error $ "getDeclInfo: Couldn't find data family instance for constructor " ++ show n+          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 -> Name -> Q [Either Type Type]-gadtIndices c n = reify n >>= \case-  TyConI (DataD _ _ _ _ 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]-        return $ if hasArgDictInstance then [Left t] else []-      _ -> return []-    ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]+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]+      return $ if hasArgDictInstance then [Left t] else []     _ -> return []-  a -> error $ "gadtIndices: Unmatched 'Info': " ++ show a+  ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]+  _ -> return []