Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 21 additions & 7 deletions src/Data/Constraint/Extras.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,13 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FlexibleInstances #-}

module Data.Constraint.Extras where

import Data.Constraint
import Data.Constraint.Compose
import Data.Constraint.Forall

-- | Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will
Expand All @@ -24,18 +27,29 @@ import Data.Constraint.Forall
-- want to go quite that far at the time of writing.
class ArgDict f where
type ConstraintsFor f (c :: k -> Constraint) :: Constraint
type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) :: Constraint
argDict :: ConstraintsFor f c => f a -> Dict (c a)
argDict' :: ConstraintsFor' f c g => f a -> Dict (c (g a))

-- | This places a tighter restriction on the kind of f, and so needs to be a separate class.
class ArgDictV f where
type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) :: Constraint
argDictV :: ConstraintsForV f c g => f v -> Dict (c (v g))
type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)

argDict' :: forall f c g a. (ArgDict f, ConstraintsFor' f c g) => f a -> Dict (c (g a))
argDict' tag = case argDict tag of
(Dict :: Dict (ComposeC c g a)) -> Dict

class c h g => FlipC (c :: k -> k' -> Constraint) (g :: k') (h :: k)
instance c h g => FlipC c g h

type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)

argDictV :: forall f c g v. (ArgDict f, ConstraintsForV f c 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 = ArgDict f

type Has (c :: k -> Constraint) f = (ArgDict f, ConstraintsFor f c)
type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict f, ConstraintsFor' f c g)
type HasV c f g = (ArgDictV f, ConstraintsForV f c g)
type HasV c f g = (ArgDict f, ConstraintsForV f c g)

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
Expand Down
21 changes: 2 additions & 19 deletions src/Data/Constraint/Extras/TH.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,33 +24,16 @@ deriveArgDict n = do
Right t -> AppT (VarT c) (AppT (VarT g) t)
l = length xs
constraints = foldl AppT (TupleT l) 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 $(pure n') where
type ConstraintsFor $(pure n') $(varT c) = $(pure constraints)
type ConstraintsFor' $(pure n') $(varT c) $(varT g) = $(pure constraints')
argDict = $(LamCaseE <$> matches n 'argDict)
argDict' = $(LamCaseE <$> matches n 'argDict')
|]

deriveArgDictV :: Name -> Q [Dec]
deriveArgDictV n = do
vs <- gadtIndices n
c <- newName "c"
g <- newName "g"
let xs = flip map vs $ \case
Left t -> AppT (AppT (AppT (ConT ''ConstraintsForV) t) (VarT c)) (VarT g)
Right v -> AppT (VarT c) $ AppT v (VarT g)
l = length xs
constraints = foldl AppT (TupleT l) xs
ds <- deriveArgDict n
d <- [d| instance ArgDictV $(pure $ ConT n) where
type ConstraintsForV $(conT n) $(varT c) $(varT g) = $(pure constraints)
argDictV = $(LamCaseE <$> matches n 'argDictV)
|]
return (d ++ ds)
{-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-}
deriveArgDictV = deriveArgDict

matches :: Name -> Name -> Q [Match]
matches n argDictName = do
Expand Down