Always use QuantifiedConstraints, support inductive GADTs

ChangeLog.md

@@ -1,5 +1,9 @@
 # Revision history for constraints-extras
 
+## unreleased 2019-09-11
+
+* Remove extra parameter added in 0.3. We use a forall constraint instead to solve the problem.
+
 ## 0.3.0.1 - 2019-05-17
 
 * Drop markdown-unlit in favor of using regular "Bird"-style LHS to avoid some cross-compilation problems

README.md

@@ -4,42 +4,57 @@ constraints-extras [![travis-ci](https://api.travis-ci.org/obsidiansystems/const
 Example usage:
 --------------
 
-```haskell
-
+> {-# LANGUAGE ConstraintKinds #-}
+> {-# LANGUAGE ExistentialQuantification #-}
+> {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE FlexibleInstances #-}
 > {-# LANGUAGE GADTs #-}
 > {-# LANGUAGE KindSignatures #-}
+> {-# LANGUAGE LambdaCase #-}
+> {-# LANGUAGE MultiParamTypeClasses #-}
 > {-# LANGUAGE PolyKinds #-}
+> {-# LANGUAGE QuantifiedConstraints #-}
 > {-# LANGUAGE ScopedTypeVariables #-}
 > {-# LANGUAGE TemplateHaskell #-}
 > {-# LANGUAGE TypeApplications  #-}
 > {-# LANGUAGE TypeFamilies #-}
-> {-# LANGUAGE FlexibleInstances #-}
-> {-# LANGUAGE MultiParamTypeClasses #-}
 > {-# LANGUAGE UndecidableInstances #-}
-> {-# LANGUAGE ExistentialQuantification #-}
+> {-# LANGUAGE UndecidableSuperClasses #-}
+>
+> {-# OPTIONS_GHC -Wno-unused-top-binds #-}
 >
 > import Data.Aeson
+> import Data.Constraint
 > import Data.Constraint.Forall
 > import Data.Constraint.Extras
 > import Data.Constraint.Extras.TH
 >
+
+A "simple" GADT.
+
 > data A :: * -> * where
 >   A_a :: A Int
 >   A_b :: Int -> A ()
 >
 > deriveArgDict ''A
->
+
+A GADT which uses `A`.
+
 > data B :: * -> * where
 >   B_a :: A a -> A a -> B a
 >   B_x :: Int -> B Int
 >
 > deriveArgDict ''B
->
+
+A GADT which has a non-`Type` parameter.
+
 > data V :: (* -> *) -> * where
 >   V_a :: A Int -> V A
 >
 > deriveArgDict ''V
->
+
+Now let's actually use them
+
 > data DSum k f = forall a. DSum (k a) (f a)
 >
 > -- Derive a ToJSON instance for our 'DSum'
@@ -61,7 +76,97 @@ Example usage:
 >     Some (f :: f a) <- parseJSON jf
 >     g <- has' @FromJSON @g f (parseJSON jg)
 >     return $ DSum f g
+
+We can hand-write an instance for there being non-finite indices.
+
+> data SimpleExpr :: * -> * where
+>   SimpleExpr_BoolLit :: Bool -> SimpleExpr Bool
+>   SimpleExpr_IntLit :: Int -> SimpleExpr Int
+>   -- crude non-empty list
+>   SimpleExpr_ListLit :: SimpleExpr a -> [SimpleExpr a] -> SimpleExpr [a]
 >
+> class
+>   ( c Int
+>   , c Bool
+>   , (forall a. (forall c'. ConstraintsFor SimpleExpr c' => c' a) => c [a])
+>   ) => ConstraintsForSimpleExpr c
+> instance
+>   ( c Int
+>   , c Bool
+>   , (forall a. (forall c'. ConstraintsFor SimpleExpr c' => c' a) => c [a])
+>   ) => ConstraintsForSimpleExpr c
+>
+> instance ArgDict SimpleExpr where
+>   type ConstraintsFor SimpleExpr c = ConstraintsForSimpleExpr c
+>   argDictAll = go
+>     where
+>       go :: forall c a. ConstraintsFor SimpleExpr c => SimpleExpr a -> Dict (c a)
+>       go = \case
+>         SimpleExpr_BoolLit _ -> Dict
+>         SimpleExpr_IntLit _ -> Dict
+>         SimpleExpr_ListLit h _ -> hasAll h Dict
+
+We have the instances we want:
+
+> abstractConstraintWitnesses :: Has c SimpleExpr => Dict (c Int, c Bool, c [Int], c [Bool], c [[Int]], c [[Bool]])
+> abstractConstraintWitnesses = Dict
+
+> concreteClassSmokeTest :: Dict (Has Show SimpleExpr)
+> concreteClassSmokeTest = Dict
+
+Even in when we have no "slack" (instances beyond what `Has` requires):
+
+> class Minimal a
+> instance Minimal Int
+> instance Minimal Bool
+> instance Minimal a => Minimal [a]
+
+> minimalWitness :: Dict (Has Minimal SimpleExpr)
+> minimalWitness = Dict
+
+The funny "Leibnitz-style" `forall c'` is so fancier things than Minimal
+(which also might not be satisfied for other args) also work:
+
+> class MinimalPing a
+> class MinimalPong a
+> instance MinimalPing Int
+> instance MinimalPong Int
+> instance MinimalPing Bool
+> instance MinimalPong Bool
+> instance MinimalPing a => MinimalPong [a]
+> instance MinimalPong a => MinimalPing [a]
+
+> minimalPingPongWitness :: Dict (Has MinimalPing SimpleExpr, Has MinimalPong SimpleExpr)
+> minimalPingPongWitness = Dict
+
+We can also hand-write instances which take advantage of constructor's dictionaries
+
+> data WithOrd a where
+>   WithOrd :: Ord a => WithOrd a
+>
+> -- class to avoid impredicativity
+> class (forall a. Ord a => c a) => ConstraintsForWithOrd c
+> instance (forall a. Ord a => c a) => ConstraintsForWithOrd c
+>
+> instance ArgDict WithOrd where
+>   type ConstraintsFor WithOrd c = ConstraintsForWithOrd c
+>   argDictAll WithOrd = Dict
+
+Now we can use the constructor dictionary to discharge constraints.
+We can get out `Ord a`:
+
+> useThisOrd :: WithOrd a -> a -> a -> Ordering
+> useThisOrd wo x y = has @Ord wo $ x `compare` y
+
+and things derivable from it:
+
+> useThisOrdSuperclass :: WithOrd a -> a -> a -> Bool
+> useThisOrdSuperclass wo x y = has @Eq wo $ x == y
+
+> useThisOrdImplication :: WithOrd a -> [a] -> [a] -> Bool
+> useThisOrdImplication wo x y = has @Eq wo $ x == y
+
+Oh, and let's make this README build
+
 > main :: IO ()
 > main = return ()
-```

constraints-extras.cabal

@@ -1,5 +1,5 @@
 name: constraints-extras
-version: 0.3.0.1
+version: 0.4
 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
@@ -11,7 +11,7 @@ copyright: Obsidian Systems LLC
 build-type: Simple
 cabal-version: 2.0
 tested-with:
-  GHC  ==8.0.2 || ==8.2.2 || ==8.4.4 || ==8.6.5
+  GHC  ==8.6.5
 extra-source-files: README.md
                     ChangeLog.md
 

src/Data/Constraint/Extras.hs

@@ -1,10 +1,10 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -18,38 +18,55 @@ import Data.Constraint.Compose
 import Data.Constraint.Flip
 import Data.Constraint.Forall
 
--- | 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.
-
-class ArgDict (c :: k -> Constraint) (f :: k -> *) where
+-- | Morally, this class is for GADTs whose indices can be 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.
+--
+-- The class constraint is there to enforce the law that '@ConstraintsFor@ X'
+-- only enumerates the indices of '@X@'. In the most general case, all types are
+-- possible GADT indices, so we should always be able to '@ConstraintsFor@ X'
+-- from 'forall a. c a'.
+--
+-- 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.
+class (forall c. (forall a. c a) => ConstraintsFor f c) => ArgDict f where
   type ConstraintsFor f (c :: k -> Constraint) :: Constraint
-  argDict :: ConstraintsFor f c => f a -> Dict (c a)
+  argDictAll :: f a -> Dict (Extract f a)
 
 type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)
 
-argDict' :: forall f c g a. (Has' c f g) => f a -> Dict (c (g a))
+-- Helper class to avoid impredicative type
+class (forall c. ConstraintsFor f c => c a) => Extract f a
+instance (forall c. ConstraintsFor f c => c a) => Extract f a
+
+argDict :: forall f c a. (ArgDict f, ConstraintsFor f c) => f a -> Dict (c a)
+argDict tag = case argDictAll tag of
+  (Dict :: Dict (Extract f a)) -> Dict
+
+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
-
 type ConstraintsForV (f :: (k -> k') -> *) (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 :: 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 c = ArgDict f c
+type ArgDictV f = ArgDict f
 
-type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)
-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)
+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 = (ArgDict f, ConstraintsForV f c g)
+
+hasAll :: forall f a r. ArgDict f => f a -> ((forall c. Has c f => c a) => r) -> r
+hasAll k r | (Dict :: Dict (Extract f a)) <- argDictAll k = r
 
 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
@@ -66,4 +83,3 @@ whichever r = r \\ (instF :: ForallF c t :- c (t a))
 -- | Allows explicit specification of constraint implication
 class Implies1 c d where
   implies1 :: c a :- d a
-

src/Data/Constraint/Extras/TH.hs

@@ -10,10 +10,11 @@ import Data.Maybe
 import Control.Monad
 import Language.Haskell.TH
 
+
 deriveArgDict :: Name -> Q [Dec]
 deriveArgDict n = do
+  ts <- gadtIndices n
   c <- newName "c"
-  ts <- gadtIndices c n
   let xs = flip map ts $ \case
         Left t -> AppT (AppT (ConT ''ConstraintsFor) t) (VarT c)
         Right t -> (AppT (VarT c) t)
@@ -22,17 +23,17 @@ deriveArgDict n = do
   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
+  [d| instance ArgDict $(pure n') where
         type ConstraintsFor  $(pure n') $(varT c) = $(pure constraints)
-        argDict = $(LamCaseE <$> matches c n 'argDict)
+        argDictAll = $(LamCaseE <$> matches n 'argDictAll)
     |]
 
 {-# DEPRECATED deriveArgDictV "Just use 'deriveArgDict'" #-}
 deriveArgDictV :: Name -> Q [Dec]
 deriveArgDictV = deriveArgDict
 
-matches :: Name -> Name -> Name -> Q [Match]
-matches c n argDictName = do
+matches :: Name -> Name -> Q [Match]
+matches n argDictName = do
   x <- newName "x"
   reify n >>= \case
     TyConI (DataD _ _ _ _ constrs _) -> fmap concat $ forM constrs $ \case
@@ -41,7 +42,7 @@ matches c n argDictName = do
       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 ''ArgDict [t]
             return $ if hasArgDictInstance
               then Just x
               else Nothing
@@ -55,7 +56,9 @@ matches c n argDictName = do
                     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)) []]
+                eta = CaseE (AppE (VarE argDictName) (VarE v))
+                  [Match (RecP 'Dict []) (NormalB $ ConE 'Dict) []]
+            in [Match (ConP name pat) (NormalB eta) []]
       ForallC _ _ (GadtC [name] _ _) -> return $
         [Match (RecP name []) (NormalB $ ConE 'Dict) []]
       a -> error $ "deriveArgDict matches: Unmatched 'Dec': " ++ show a
@@ -74,15 +77,15 @@ 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
 
-gadtIndices :: Name -> Name -> Q [Either Type Type]
-gadtIndices c n = reify n >>= \case
+gadtIndices :: Name -> Q [Either Type Type]
+gadtIndices 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]
+        hasArgDictInstance <- fmap (not . null) $ reifyInstances ''ArgDict [t]
         return $ if hasArgDictInstance then [Left t] else []
       _ -> return []
     ForallC _ _ (GadtC _ _ (AppT _ typ)) -> return [Right typ]
     _ -> return []
-  a -> error $ "gadtIndices: Unmatched 'Info': " ++ show a
+  a -> error $ "gadtResults: Unmatched 'Info': " ++ show a