Always use QuantifiedConstraints, support inductive GADTs

.travis.yml

@@ -8,7 +8,7 @@
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.10.2
+# version: 0.10.3
 #
 version: ~> 1.0
 language: c
@@ -42,15 +42,6 @@ jobs:
     - compiler: ghc-8.6.5
       addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.6.5","cabal-install-3.2"]}}
       os: linux
-    - compiler: ghc-8.4.4
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.4.4","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.2.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.2.2","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.0.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.0.2","cabal-install-3.2"]}}
-      os: linux
 before_install:
   - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')
   - WITHCOMPILER="-w $HC"
@@ -99,8 +90,8 @@ install:
   - touch cabal.project
   - |
     echo "packages: ." >> cabal.project
-  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package constraints-extras' >> cabal.project ; fi
-  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - echo 'package constraints-extras' >> cabal.project
+  - "echo '  ghc-options: -Werror=missing-methods' >> cabal.project"
   - |
   - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(constraints-extras)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
   - cat cabal.project || true
@@ -126,8 +117,8 @@ script:
   - touch cabal.project
   - |
     echo "packages: ${PKGDIR_constraints_extras}" >> cabal.project
-  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package constraints-extras' >> cabal.project ; fi
-  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
+  - echo 'package constraints-extras' >> cabal.project
+  - "echo '  ghc-options: -Werror=missing-methods' >> cabal.project"
   - |
   - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(constraints-extras)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
   - cat cabal.project || true
@@ -146,5 +137,5 @@ script:
   - rm -f cabal.project.local
   - ${CABAL} v2-build $WITHCOMPILER --disable-tests --disable-benchmarks all
 
-# REGENDATA ("0.10.2",["constraints-extras.cabal"])
+# REGENDATA ("0.10.3",["constraints-extras.cabal"])
 # EOF

ChangeLog.md

@@ -13,6 +13,8 @@
 * 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
 
+* Overhaul to allow working with recursive GADTs.
+
 ## 0.3.0.3 - 2020-06-22
 
 * Update version bounds for GHC 8.10

README.md

@@ -5,42 +5,68 @@ 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 FlexibleContexts #-}
-> {-# 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.
+
+```haskell
 > data A :: * -> * where
 >   A_a :: A Int
 >   A_b :: Int -> A ()
 >
 > deriveArgDict ''A
->
+```
+
+A GADT which uses `A`.
+
+
+```haskell
 > 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.
+
+
+```haskell
 > data V :: (* -> *) -> * where
 >   V_a :: A Int -> V A
 >
 > deriveArgDict ''V
->
+```
+
+Now let's actually use them
+
+
+```haskell
 > data DSum k f = forall a. DSum (k a) (f a)
 >
 > -- Derive a ToJSON instance for our 'DSum'
@@ -62,7 +88,125 @@ 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.
+
+
+```haskell
+> 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:
+
+
+```haskell
+> abstractConstraintWitnesses :: Has c SimpleExpr => Dict (c Int, c Bool, c [Int], c [Bool], c [[Int]], c [[Bool]])
+> abstractConstraintWitnesses = Dict
+```
+
+
+```haskell
+> concreteClassSmokeTest :: Dict (Has Show SimpleExpr)
+> concreteClassSmokeTest = Dict
+```
+
+Even in when we have no "slack" (instances beyond what `Has` requires):
+
+
+```haskell
+> class Minimal a
+> instance Minimal Int
+> instance Minimal Bool
+> instance Minimal a => Minimal [a]
+```
+
+```haskell
+> 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:
+
+
+```haskell
+> 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
+
+```haskell
+> 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`:
+
+
+```haskell
+> useThisOrd :: WithOrd a -> a -> a -> Ordering
+> useThisOrd wo x y = has @Ord wo $ x `compare` y
+```
+
+and things derivable from it:
+
+
+```haskell
+> useThisOrdImplication :: WithOrd a -> [a] -> [a] -> (Bool, Bool)
+> useThisOrdImplication wo x y =
+>  ( has @Ord wo $ x == y      -- implicit way
+>  , has' @Eq @[] wo $ x == y  -- explicit way
+>  )
+```
+
+Oh, and let's make this README build
+
+
+```haskell
 > main :: IO ()
 > main = return ()
 ```

constraints-extras.cabal

@@ -1,5 +1,5 @@
 name: constraints-extras
-version: 0.3.2.0
+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
@@ -13,7 +13,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 || ==8.8.1 || ==8.10.1 || ==9.0.1 || ==9.2.1
+  GHC  ==8.6.5 || ==8.8.1 || ==8.10.1 || ==9.0.1 || ==9.2.1
 extra-source-files: README.md
                     ChangeLog.md