Add machinery for computing with KnownNat using reflection-like tricks to manipulate singletons:

(KnownNat n, KnownNat m) :- KnownNat (n + m)
(KnownNat n, KnownNat m) :- KnownNat (n - m)
(KnownNat n, KnownNat m) :- KnownNat (n * m)

etc.

I believe this is probably some silly problem with the file name.

Hope it's going well, do we want lift instances for Dict here?

instance Lift (Dict cls) where
 lift :: Dict cls -> Q Exp
 lift Dict = [| Dict |]

 liftTyped :: Dict cls -> Q (TExp (Dict cls))
 liftTyped Dict = [|| Dict ||]

Can it be given for a :- b?

instance Lift (a :- b) where
 lift (a :- b) -> Q Exp
 lift ..

 liftTyped :: (a :- b) -> Q (TExp (a :- b))
 liftTyped (Sub dict) = [|| Sub _ ||]

This package could provide various Constraintbuilding blocks, names / fixity from Control.Constraint.Combine

class    (c a, d a) => (c :&: d) a
instance (c a, d a) => (c :&: d) a
infixl 7 :&:

Same as :&:

type c `And` d = c :&: d
infixl 7 `And`

And the unit of :&:, the empty constraint

class    Empty a
instance Empty a

It would be good to have a standardised place for these / name / fixity (especially when I start needing to define instances of them, as for instance (HasSuperClasses c, HasSuperClasses d) => HasSuperClasses (c :&: d))

When (Typeable a, Typeable b) => Deferrable (a ~ b) fails our error is:

Nothing -> Left "deferred type equality: type mismatch"

but the user may want some information about the types (we already have their Typeable instances), so why not write:

Nothing   -> Left $
  printf "deferred type equality: type mismatch between ‘%s’ and ‘%s’" (showTr @a) (showTr @b)
  where
    showTr :: ∀t. Typeable t => String
    showTr = show (typeRep @_ @t Proxy)

Hi there,

when building the library with GHC from the git head I encounter this error:

src/Data/Constraint.hs:308:7: error:
    Not in scope: type constructor or class ‘Prim.Any’
    Module ‘GHC.Prim’ does not export ‘Any’.

I know a similar issue was fixed some time ago, but I think this is new since GHC head changed since then. Can you please look into this? I'm not experienced with GHC internals.

Axioms plusZero, timesZero, timesOne, powZero, powOne are redundant, because GHC already reduces these types. For example, in ghci:

> :t plusZero
plusZero :: Dict n ~ n

In the type declarations for plusAssociates, timesAssociates, minAssociates, maxAssociates the order of appearance of type variables is changed. For this reason, there are difficulties with using TypeApplications. For example,

plusAssociates :: forall n m o. Dict (((m + n) + o) ~ (m + (n + o))) 
plusAssociates @m1 @m2 @m3 :: Dict ( ((m2+m1)+m3) ~ (m2+(m1+m3)) )

$ cabal unpack constraints-0.11
$ cd constraints-0.11
$ cabal build -w ghc-9.2
Build profile: -w ghc-9.2.0.20210821 -O1
In order, the following will be built (use -v for more details):
 - constraints-0.11 (lib) (first run)
Preprocessing library for constraints-0.11..
Building library for constraints-0.11..
[5 of 7] Compiling Data.Constraint.Nat ( src/Data/Constraint/Nat.hs, /private/tmp/constraints-0.11/dist-newstyle/build/x86_64-osx/ghc-9.2.0.20210821/constraints-0.11/build/Data/Constraint/Nat.o, /private/tmp/constraints-0.11/dist-newstyle/build/x86_64-osx/ghc-9.2.0.20210821/constraints-0.11/build/Data/Constraint/Nat.dyn_o )

src/Data/Constraint/Nat.hs:84:12: error:
    • Could not deduce: Data.Type.Ord.OrdCond
                          (Data.Type.Ord.Compare b b) 'True 'True 'False
                        ~ 'True
        arising from a use of ‘Dict’
      from the context: a ~ b
        bound by a type expected by the context:
                   (a ~ b) =>
                   Dict
                     (Data.Type.Ord.OrdCond
                        (Data.Type.Ord.Compare a b) 'True 'True 'False
                      ~ 'True)
        at src/Data/Constraint/Nat.hs:84:12-15
    • In the first argument of ‘Sub’, namely ‘Dict’
      In the expression: Sub Dict
      In an equation for ‘eqLe’: eqLe = Sub Dict
    • Relevant bindings include
        eqLe :: (a ~ b) :- (a <= b)
          (bound at src/Data/Constraint/Nat.hs:84:1)
   |
84 | eqLe = Sub Dict
   |            ^^^^

src/Data/Constraint/Nat.hs:153:11: error:
    • Couldn't match type ‘If
                             (Data.Type.Ord.OrdCond (CmpNat 0 n) 'True 'True 'False) 0 n’
                     with ‘0’
        arising from a use of ‘Dict’
    • In the expression: Dict
      In an equation for ‘minZero’: minZero = Dict
    • Relevant bindings include
        minZero :: Dict (Min n 0 ~ 0)
          (bound at src/Data/Constraint/Nat.hs:153:1)
    |
153 | minZero = Dict
    |           ^^^^

src/Data/Constraint/Nat.hs:156:11: error:
    • Couldn't match type ‘n’
                     with ‘If
                             (Data.Type.Ord.OrdCond (CmpNat 0 n) 'True 'True 'False) n 0’
        arising from a use of ‘Dict’
      ‘n’ is a rigid type variable bound by
        the type signature for:
          maxZero :: forall (n :: Nat). Dict (Max n 0 ~ n)
        at src/Data/Constraint/Nat.hs:155:1-39
    • In the expression: Dict
      In an equation for ‘maxZero’: maxZero = Dict
    • Relevant bindings include
        maxZero :: Dict (Max n 0 ~ n)
          (bound at src/Data/Constraint/Nat.hs:156:1)
    |
156 | maxZero = Dict
    |           ^^^^

src/Data/Constraint/Nat.hs:165:10: error:
    • Couldn't match type ‘Data.Type.Ord.OrdCond
                             (CmpNat 0 a) 'True 'True 'False’
                     with ‘'True’
        arising from a use of ‘Dict’
    • In the expression: Dict
      In an equation for ‘zeroLe’: zeroLe = Dict
    • Relevant bindings include
        zeroLe :: Dict (0 <= a) (bound at src/Data/Constraint/Nat.hs:165:1)
    |
165 | zeroLe = Dict
    |          ^^^^

src/Data/Constraint/Nat.hs:347:8: error:
    • Couldn't match type ‘Data.Type.Ord.OrdCond
                             (Data.Type.Ord.Compare a a) 'True 'True 'False’
                     with ‘'True’
        arising from a use of ‘Dict’
    • In the expression: Dict
      In an equation for ‘leId’: leId = Dict
    • Relevant bindings include
        leId :: Dict (a <= a) (bound at src/Data/Constraint/Nat.hs:347:1)
    |
347 | leId = Dict
    |        ^^^^

Newer releases likely need a revision as well, but they are currently shielded by type-equality bounds.

Will the implementation of the compile-time calculation for new type families in the modules Data.Constraint.Nat and Data.Constraint.Symbol?

Now
> :t (Proxy::Proxy (Min 1 2))
(Proxy::Proxy (Min 1 2)) :: Proxy (Min 1 2)

I would like to
> :t (Proxy::Proxy (Min 1 2))
(Proxy::Proxy (Min 1 2)) :: Proxy 1

I suggest making the operator \\ polymorphic:

infixl 1 \\

class KnownConstraint c where
    type NewContext c :: Constraint
    type OldContext c :: Constraint
    (\\) :: forall r. (OldContext c => r) -> c -> (NewContext c => r)

instance KnownConstraint (Dict a) where
    type NewContext (Dict a) = ()
    type OldContext (Dict a) = a
    r \\ Dict = r

instance KnownConstraint (a :- b) where
    type NewContext (a :- b) = a
    type OldContext (a :- b) = b
    r \\ (Sub Dict) = r

This class will also be useful in other cases, for example:

instance KnownConstraint (a:~:b) where
    type NewContext (a:~:b) = ()
    type OldContext (a:~:b) = a~b
    r \\ Refl = r

Hello there. So here's a neat little thing that possibly demonstrates Dict being one half of an adjunction between the Heyting algebra of constraints and the CCC of types and functions we know and love:

data a :- b
  where
  Proof :: (a ⇒ b) => a :- b
infixr 0 :-

instance Category (:-)
  where
  id = Proof
  Proof . Proof = Proof

-- A functor Constraint -> Type
type Dict :: Constraint -> Type
data Dict c
  where
  Dict :: c => Dict c

-- A functor Type -> Constraint
type Only :: Type -> Constraint
class Only x
  where
  only :: x

instance c => Only (Dict c)
  where
  only = Dict

type M c = Only (Dict c)
type C x = Dict (Only x)

-- The unit of the adjunction
unit :: c :- M c
unit = Proof

-- The counit of the adjunction
counit :: C x -> x
counit Dict = only

I don't have a lot of time to explore this further but I figured I'd dump the beginning of the idea here and someone can tear it apart if it's wrong/build on it if it makes sense.

In the package constraints-0.9.1, module Data.Constraint.Nat, the type of maxCommutes is
forall n m. Dict (Min m n ~ Min n m)

QuantifiedConstraints makes some parts of this package rather less exciting (in particular, I believe everything currently in Data.Constraint.Forall can be made Safe). On the other hand, it introduces its own gaps. For example, we can easily write

weaken :: (c => d) => c :- d
weaken = Sub Dict

But we can't write the equally reasonable

strengthen :: ((c => d) => r) -> c :- d -> r

Doing so requires some sort of coercion that's not immediately obvious; it'd be nice if constraints could help with that.

Perhaps this is obvious, but Forall's skolemization is not typesafe in the pressence of incoherent instances. Basically, you can define

class OneOf a b c where
  oneOf :: Either (a :==: c) (b :==: c)

instance OneOf a b a where
  oneOf = Left Refl

instance OneOf a b b where
  oneOf = Right Refl

oneOfaba :: Dict (OneOf a b a)
oneOfaba = Dict

oneOfabb :: Dict (OneOf a b b)
oneOfabb = Dict

oneOfEither :: k :- (OneOf a b a,OneOf a b b)
oneOfEither = (Sub oneOfaba) &&& (Sub oneOfabb)

this really quickly becomes a problem

data Oh k where
  Oh :: (forall c. (k :- (OneOf a b c))) -> Oh k

oh :: Oh ()
oh = Oh (inst `trans` oneOfEither)

It is clear to me this type should not be inhabited, but it is. If you have this then you can essentially prove that for any three types, two are the same. Lets pick particularly evil types

newtype First a b c = First {fromFirst :: a}
newtype Second a b c = Second {fromSecond :: b}
newtype Third a b c = Third {fromThird :: c}

Given a standard equality construction like

data a :==: b where
  Refl :: a :==: a

coerce :: (a :==: b) -> a -> b
coerce Refl = id

coerce' :: (a :==: b) -> b -> a
coerce' Refl = id

we can show that of three types, two are the same like

data No where
  No :: (forall d e f. 
          ((Either (a :==: (First d e f)) (b :==: (First d e f))), 
          (Either (a :==: (Second d e f)) (b :==: (Second d e f))), 
          (Either (a :==: (Third d e f)) (b :==: (Third d e f)))))
          -> No

makeOneOf :: (() :- OneOf a b c) -> Either (a :==: c) (b :==: c)
makeOneOf f = oneOf \\ f

no :: No
no = case oh of
          Oh f -> No ((makeOneOf f),(makeOneOf f),(makeOneOf f))

this leads to an elegant unsafeCoerce

--infered type c1 -> c
unsafeCoerce 
  = case no of
         No (Right x, Right y, _      ) -> fromFirst   . (coerce x) . (coerce' y) . Second
         No (_      , Right x, Right y) -> fromSecond  . (coerce x) . (coerce' y) . Third
         No (Right x, _      , Right y) -> fromFirst   . (coerce x) . (coerce' y) . Third
         No (Left x , Left y , _     )  -> fromFirst   . (coerce x) . (coerce' y) . Second
         No (_      , Left x , Left y)  -> fromSecond  . (coerce x) . (coerce' y) . Third
         No (Left x , _      , Left y)  -> fromFirst   . (coerce x) . (coerce' y) . Third

which would work with only the first line--I know how Forall is actually implemented--but this definition should work with any way of defining forall using a tuple. My GHCi then lets me

λ: unsafeCoerce "hello world" :: Int
5188146770748711367

IncoherentInstances don't normally cause a loss of type safety (as far as I know), although they are still pretty terrible. I don't think it is unliqely though that other corners of haskell might produce the same problem--I'm think both ImplicitParams, and your reflection package as possibilities.

                     9.0.1  8.10.4  8.8.4  8.6.5  8.4.4  8.2.2  8.0.2  7.10.3  7.8.4  7.6.3  7.4.2  7.2.2  7.0.4
constraints-0.13     OK     OK      OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP
constraints-0.12     OK     OK      OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP
constraints-0.11.2   OK     OK      OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP
constraints-0.11.1   OK     OK      OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP
constraints-0.11     OK     OK      OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP
constraints-0.10.1   FAIL   FAIL    OK     OK     OK     OK     OK     OK      OK     NO-IP  NO-IP  NO-IP  NO-IP

src/Data/Constraint/Forall.hs:146:23: error:
    Not in scope: type variable ‘k4’
    |
146 | instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
    |                       ^^

src/Data/Constraint/Forall.hs:146:48: error:
    Not in scope: type variable ‘k1’
    |
146 | instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
    |                                                ^^

etc.

Here is test code

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module Lib
    ( someFunc
    ) where

import Data.Constraint
import Data.Constraint.Symbol
import Data.Proxy
import GHC.TypeLits

someFunc :: IO ()
someFunc = do
  putStrLn $ ((symbolVal (Proxy :: Proxy ("Foo" ++ "Bar")))
              \\ (appendSymbol :: ((KnownSymbol "Foo", KnownSymbol "Bar") :- KnownSymbol ("Foo" ++ "Bar")))
             )

It core dumped in GHC 8.0.1 as well in 8.0.2
Is it a bug or am I missing something here

Version 0.6 added a lot of dependencies, all of which (I think) are used for instances that Lifting has. Would you be amenable to the idea of moving Data.Constraint to a separate package (constraints-core or something like that) with fewer dependencies (since that module seems to be stable at the point and doesn't need any typeclass instances).

Data.Constraint.Class1 looks like an implementation of implication constraints (ImplicationConstraints) and allows implementing (from HHFree)

type f ~~> g = forall a b. f a b -> g a b

newtype HHFree c f a b = HHFree { runHHFree :: forall g. c g => (f ~~> g) -> g a b }

instance SuperClass1 Category c => Category (HHFree c f)
instance SuperClass1 Arrow    c => Arrow    (HHFree c f)

Does it belong here

I was trying to derive Divides a b :- (Mod b a ~ 0) and - against my expectations - it appeared to be quite convoluted.

foo :: forall a b. (Divides a b, 1 <= a) :- (Mod b a ~ 0)
foo = Sub $ case (dividesDef @a @b, euclideanNat @a @b, plusIsCancellative @b @0 @(Mod b a)) of
  (Sub Dict, Sub Dict, Sub Dict) -> Dict

This is quite frustrating, because initially I expected Mod b a ~ 0 to be the very definition of Divides. Is there a good reason to define it as type Divides n m = n ~ Gcd n m? (This also means Divides 0 0, which is wrong).

I see three ways to improve UX here:

1. (cleanest) Define type Divides a b = (Mod b a ~ 0, 1 <= a) and add an axiom Divides n m :- n ~ Gcd n m. This arguably defines Divides in the most natural way and fully in terms of vanilla GHC type families (no magic involved), and also fixes Divides 0 0.

2. Leave type Divides n m = n ~ Gcd n m in peace, but change

- dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b)
+ dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)

Here the previous behaviour of dividesDef can be easily restored by substituting it into euclideanNat. The cons are that this is still a breaking change, and makes Divides 0 0 even worse, because it now leads to Mod 0 0 ~ 0.

3. (least intrusive) Just add (Divides a b, 1 <= a) :- (Mod b a ~ 0) to Data.Constraint.Nat, so that future users would not need to reinvent it themselves.

My personal preference is option 1.

I'm not sure which way they should be, but I think something like this (and it's analogue) should be added:

strengthen1 :: Dict b -> a :- c -> a :- (b,c)
strengthen1 d e = unmapDict (const d) &&& e

Until we have type-level lambdas, the Compose for constraints is quite useful to have around. ComposeC was added in #24 but never exposed.

CC @cgibbard

With idempotent axioms and some other there is an strange error in runtime. For example

{-# LANGUAGE GADTs,PolyKinds,TypeApplications,DataKinds,TypeOperators,ScopedTypeVariables #-}

import Data.Constraint
import Data.Constraint.Nat
import GHC.TypeLits

newtype GF (n :: Nat) = GF Integer deriving Show

instance KnownNat n => Num (GF n) where
  xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
  xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
  xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
  abs = id
  signum xf@(GF x) | x==0 = xf
                   | otherwise = GF 1
  fromInteger = GF

x :: GF 5
x = GF 3

y :: GF 5
y = GF 4

foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))

bar :: (KnownNat m)  => GF m -> GF m -> GF m
bar (x :: GF m) y = foo x y - foo y x \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m 

z :: GF 5
z = bar x y

main = print z

This code is compiled, but when it runs, it produces the following error

Main.EXE: Main.hs:32:31: error:
    * Could not deduce: m ~ Lcm m m
      from the context: Lcm m m ~ m
        bound by a type expected by the context:
                   Lcm m m ~ m => GF m
        at Main.hs:32:21-69
      `m' is a rigid type variable bound by
        the type signature for:
          bar :: forall (m :: Nat). KnownNat m => GF m -> GF m -> GF m
        at Main.hs:31:8
      Expected type: GF m
        Actual type: GF (Lcm m m)
    * In the second argument of `(-)', namely `foo y x'
      In the first argument of `(\\)', namely `foo x y - foo y x'
      In the first argument of `(\\)', namely
        `foo x y - foo y x \\ Sub @() (lcmIsIdempotent @m)'
    * Relevant bindings include
        y :: GF m (bound at Main.hs:32:17)
        x :: GF m (bound at Main.hs:32:6)
        bar :: GF m -> GF m -> GF m (bound at Main.hs:32:1)
(deferred type error)

I found only such a crutch solution

{-# LANGUAGE GADTs,PolyKinds,TypeApplications,DataKinds,TypeOperators,ScopedTypeVariables #-}

import Data.Constraint
import Data.Constraint.Nat
import GHC.TypeLits
import Data.Type.Equality

newtype GF (n :: Nat) = GF Integer deriving Show

instance KnownNat n => Num (GF n) where
  xf@(GF x) + GF y = GF $ (x+y) `mod` (natVal xf)
  xf@(GF x) - GF y = GF $ (x-y) `mod` (natVal xf)
  xf@(GF x) * GF y = GF $ (x*y) `mod` (natVal xf)
  abs = id
  signum xf@(GF x) | x==0 = xf
                   | otherwise = GF 1
  fromInteger = GF

x :: GF 5
x = GF 3

y :: GF 5
y = GF 4

dictToRefl :: Dict (a ~ b) -> a :~: b
dictToRefl Dict = Refl

foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF x) n@(GF y) = GF $ (x*y) `mod` (lcm (natVal m) (natVal n))

bar :: (KnownNat m)  => GF m -> GF m -> GF m
bar (x :: GF m) y = castWith (apply Refl $ dictToRefl lcmIsIdempotent) -- gcastWith don't work
                        (foo x y - foo y x) \\ lcmNat @m @m


z :: GF 5
z = bar x y

main = print z

P.S. It would be desirable to include in the documentation information on the language extension
TypeApplications, without which it is impossible to use such axioms as plusCommutes.

Currently, Data.Constraint.Symbol contains the following:

type family (++) :: Symbol -> Symbol -> Symbol where

appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b)
appendSymbol = magicSSS (++)

appendUnit1 :: forall a. Dict (("" ++ a) ~ a)
appendUnit1 = axiom

appendUnit2 :: forall a. Dict ((a ++ "") ~ a)
appendUnit2 = axiom

appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))
appendAssociates = axiom

takeAppendDrop :: forall n a. Dict (Take n a ++ Drop n a ~ a)
takeAppendDrop = axiom

This works, but it is somewhat out of sync with modern versions of GHC.TypeLits, which provide a magic type family in the same vein as (++), called AppendSymbol. Really, constraints ought to be using AppendSymbol instead of (++) (the latter predates the former), even though doing so would be a breaking change.

I am interested in adding a few Class instances of the form:

instance Class (Functor f) (Functor f) ...
instance Class (Applicative f) (Applicative f) ...

Is there a good reason against adding them? It would require dropping the functional dependency Class f g | g -> f, so the natural question is if this functional dependency is necessary?

The Cabal file places this code under BSD3 but the LICENSE file contains a BSD2 license.

The following code compiles without any warnings:

{-# LANGUAGE TypeOperators,ScopedTypeVariables,DataKinds,TypeOperators,TypeFamilies #-}
module Main (main) where

import Data.Constraint
import GHC.TypeLits
import Data.Proxy

showAdd :: forall a. Show a => a -> a-> a
showAdd x y = (x :: a) + y \\ (undefined :: (Show a):-(Num a))

typeSubt :: (b<=a) => Proxy a -> Proxy b -> Proxy (a-b)
typeSubt _ _ = Proxy

badSubt :: Proxy a -> Proxy b -> Proxy (a-b)
badSubt (pa::Proxy a) (pb :: Proxy b) = typeSubt pa pb \\ (undefined :: ():-(b<=a))

main = do
    let
        Just s2 = someNatVal 2
        Just s3 = someNatVal 3
    case (s2,s3) of
        (SomeNat (pa :: Proxy a),SomeNat (pb :: Proxy b)) ->
                print $ badSubt pa pb -- No exception!
    putStrLn $ "2" `showAdd` "2"   -- exception Prelude.undefined

Tested on constraints version 0.8, ghc version 7.10.3

Monad is currently standing alone. Ouch!

From Oerjan:

{-# LANGUAGE Safe #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Data.Constraint
import Data.Constraint.Forall
import Data.Proxy

type family H a b x y z where
    H a b x x z = a
    H a b x y y = a
    H a b x y x = a
    H a b x y z = b

class (H a b x y z ~ a) => I a b x y z
instance (H a b x y z ~ a) => I a b x y z
class Forall (I a b x y) => J a b x y
instance Forall (I a b x y) => J a b x y
class Forall (J a b x) => K a b x
instance Forall (J a b x) => K a b x

k :: Forall (K a b) :- K a b x
k = inst
k' :: K a b x :- Forall (J a b x)
k' = Sub Dict
j :: Forall (J a b x) :- J a b x y
j = inst
j' :: J a b x y :- Forall (I a b x y)
j' = Sub Dict
i :: Forall (I a b x y) :- I a b x y z
i = inst
h :: I a b x y z :- (H a b x y z ~ a)
h = Sub Dict

a :: Forall (K a b) :- I a b x y z
a = i `trans` j' `trans` j `trans` k' `trans` k

b :: Dict (I a b x y z)
b = case a of
    Sub d -> d

c :: I a b x y z => Proxy (a,b,x,y,z) -> H a b x y z -> a
c _ = id

uc :: forall a b. b -> a
uc = case b :: Dict (I a b () Bool Int) of
    Dict -> c (Proxy :: Proxy (a,b,(),Bool,Int))

It seems to be. There is an exponential, which is (:=>), and apply and uncurry combinators:

apply :: forall a b. (a :=> b, a) :- b
apply = Sub $ (Dict :: Dict b) \\ (ins :: a :- b)

uncurry :: forall a b c. (a :- (b :=> c)) -> ((a, b) :- c)
uncurry s = unmapDict $ \Dict -> (Dict :: Dict c) \\ ((ins :: b :- c) \\ s)

But there should also be a curry combinator:

curry :: forall a b c. ((a, b) :- c) -> (a :- (b :=> c))
curry = ???

And it seems like that can't be implemented without unsafe operations.

Compiling constraints with GHC HEAD, I get an error about Prim.Any:

bash-3.2$ cabal install constraints
Resolving dependencies...
Configuring constraints-0.8...
Building constraints-0.8...
Failed to install constraints-0.8
Build log ( /Users/conal/.cabal/logs/constraints-0.8.log ):
cabal: Entering directory '/var/folders/wx/m2wn7shj0gn4q_y_wnybcsqh0000gn/T/cabal-tmp-76236/constraints-0.8'
Configuring constraints-0.8...
Building constraints-0.8...
Preprocessing library constraints-0.8...
[1 of 5] Compiling Data.Constraint  ( src/Data/Constraint.hs, dist/build/Data/Constraint.o )

src/Data/Constraint.hs:308:7: error:
    Not in scope: type constructor or class ‘Prim.Any’
    Module ‘GHC.Prim’ does not export ‘Any’.
cabal: Leaving directory '/var/folders/wx/m2wn7shj0gn4q_y_wnybcsqh0000gn/T/cabal-tmp-76236/constraints-0.8'
cabal: Error: some packages failed to install:
constraints-0.8 failed during the building phase. The exception was:
ExitFailure 1
bash-3.2$ ghc --version
The Glorious Glasgow Haskell Compilation System, version 8.1.20160405

constraints-0.8 seems to have compiled fine with GHC 8.1.20160307.

Seems like this is a recurring request on StackOverflow and Reddit, and constraints looks to me like the place where it might belong:

data Exists c where
  Exists :: c a => a -> Exists c

This supports at least one interesting operator: foggy :: forall c1 c2. (forall a. c1 a :- c2 a) -> Exists c1 -> Exists c2. You also have the trivial elimination form and some useful instances¹:

withExists :: (forall a. c a => a -> r) -> Exists c -> r
withExists f (Exists x) = f x

instance Show (Exists Show) { show = withExists show }
deriving instance Typeable (Exists Typeable)
-- instance Hashable (Exists Hashable) ...
-- instance NFData (Exists NFData) ...

And, going out on a limb, you can observe one side (or both sides, if you are on a recent version of GHC) of the isomorphism between Exists Typeable and Dynamic

exists2Dyn :: Exists Typeable -> Dynamic
exists2Dyn = withExists toDyn

-- Possible only with `Type.Reflection` since `base-4.10.0.0`
dyn2Exists :: Exists Typeable -> Dynamic
dyn2Exists (Dynamic tr x) = withTypeable tr (Exists x)

If this sounds good, I'll open a PR. In any case, thanks for such an awesome package!

¹ You can have more interesting instances like instance Ord (Exists (Ord `And` Typeable)) if you also define a type-level conjunction And :: (* -> Constraint) -> (* -> Constraint) -> * -> Constraint - but that rabbit hole journeys away from constraints.

bottom demonstrates that a particular unsatisfiable constraint, () ~ Bool, entails any constraint. This is not a particularly interesting false constraint, and there doesn't seem to be any particularly obvious way to produce it from other false constraints. I don't have anything approaching a full solution, but here are some ideas to think about, based on the notion that if a constraint can prove void, it must be wrong:

crazy :: (c => Void) -> c :- d
crazy q = Sub (absurd q)

From this, we can recover the () ~ Bool idea in a way that can be used much more generally.

-- Proof that one type doesn't unify with another
newtype (/=) a b = NE {no :: forall c . (a :~: b) -> c}

-- If two types don't unify, then the assumption that they do entails anything.
hola :: forall a b d . a /= b -> (a ~ b) :- d
hola (NE nope) = crazy $ nope (Refl :: a :~: b)

-- A type useful for proving inequality
data Yeah this that a where
  Yeah1 :: Yeah this that this
  Yeah2 :: (forall b . b) -> Yeah this that that

-- Getting to Yeah
hoop :: forall a b . (a :~: b) -> Yeah a b b
hoop Refl = Yeah1

-- The specific example of `() ~ Bool`, expressed concisely; to prove other inequations,
-- only the type signature needs to be changed.
hum :: () /= Bool
hum = NE $ \ab -> case hoop ab of Yeah2 x -> x

The fact that Forall is (still) a type family is a bit annoying for two reasons: users are required to enable TypeFamilies, and Forall itself is not first class. Would it be possible to wrap it up with one more class to fix that, or would that bring back the cycle errors?

Mostly unrelatedly, the next major version of the package should, IMO, deprecate the now-redundant Forall1 and inst1. Is there a good place to make a note of that?

Any use for

data (a::k1) :~~: (b::k2) where
  HRefl :: a :~~: a

instance (Typeable k1, Typeable k2, Typeable (a::k1), Typeable (b::k2)) => Deferrable (a ~~ b) where
  deferEither _ r = case cast (HRefl :: a :~~: a) :: Maybe (a :~~: b) of
    Just HRefl -> Right r
    Nothing    -> Left ...

in lieu of Deferrable (a ~ b), of which I believe it is a special case (k1 ~ Type, k2 ~ Type)

needed for GHC 8.4 is not implemented. Causes compile errors with GHC HEAD.

If this is fine with you I will write a PR

class Deferrable (cls :: Constraint) where
  deferEither :: proxy cls -> (cls => res) -> Either String res
  deferEither cls res =
    fmap
    (\Dict -> res)
    (deferDict cls)

  deferDict :: proxy cls -> Either String (Dict cls)
  deferDict cls = deferEither cls Dict

  {-# Minimal deferEither | deferDict #-}

If the consensus is not to add it as a method it would be nice to have it somewhere (the name is up for grabs as usual, it should be deferEitherDict or something)

These might be useful for Data.Constraint.Nat

plusMonotone1' :: forall a b c. (a + c <= b + c):-(a <= b)
plusMonotone1' = Sub axiom

plusMonotone2' :: forall a b c. (a + b <= a + c):-(b <= c)
plusMonotone2' = Sub axiom

powMonotone1' :: forall a b c. ((a^c) <= (b^c),1<=c):-(a <= b)
powMonotone1' = Sub axiom

powMonotone2' :: forall a b c. ((a^b) <= (a^c),1<=a):-(b <= c)
powMonotone2' = Sub axiom

timesMonotone1' :: forall a b c. (a * c <= b * c,1<=c):-(a <= b)
timesMonotone1' = Sub axiom

timesMonotone2' :: forall a b c. (a * b <= a * c,1<=a):-(b <= c)
timesMonotone2' = Sub axiom

flipLT :: forall m n. (CmpNat m n ~ LT):-(CmpNat n m ~ GT)
flipLT = Sub axiom

flipGT :: forall m n. (CmpNat m n ~ GT):-(CmpNat n m ~ LT)
flipGT = Sub axiom

ltIsSuccLe :: forall m n. (CmpNat m n ~ LT):-(m+1<=n)
ltIsSuccLe = Sub $ axiomLe @(m+1) @n

succLeIsLT :: forall m n. (m+1<=n):-(CmpNat m n ~ LT)
succLeIsLT = Sub axiom 

ltIsLE :: forall m n. (CmpNat m n ~ LT):-(m<=n)
ltIsLE = Sub axiom -- Sub $ Dict \\ leTrans @m @(m+1) @n \\ ltIsSuccLe @m @n \\ plusMonotone2 @m @0 @1

gtIsNotLE :: forall m n. (CmpNat m n ~ GT):-((m <=? n) ~ False)
gtIsNotLE = Sub axiom

notLeIsGT :: forall m n. ((m <=? n) ~ False):-(CmpNat m n ~ GT)
notLeIsGT = Sub axiom

-- A more strict version
modBound' :: forall m n. (1 <= n) :- (CmpNat  (Mod m n)  n ~ LT)
modBound' = Sub axiom

Axioms for the minus operator:

minusNat :: forall n m. (KnownNat n, KnownNat m, m<=n) :- KnownNat (n - m)
minusNat = Sub $ case magic @n @m (-) of Sub r -> r

plusMinus :: forall m n. Dict (((m+n)-n) ~ m)
plusMinus = axiom

minusPlus :: forall n m. (n<=m):-(((m-n)+n) ~ m)
minusPlus = Sub axiom

minusIsCancellative1 :: forall m n o. ((m-n) ~ (o-n),n<=m):-(m~o)
minusIsCancellative1 = Sub axiom

minusIsCancellative2 :: forall m n o. ((m-n) ~ (m-o),n<=m):-(n~o)
minusIsCancellative2 = Sub axiom

minusMonotone1 :: forall a b c. (a <= b,c<=a):-(a - c <= b - c)
minusMonotone1 = Sub axiom

minusMonotone1' :: forall a b c. (a - c <= b - c,c<=a):-(a <= b)
minusMonotone1' = Sub axiom

minusMonotone2 :: forall a b c. (a <= b,b <= c):-(c - b <= c - a)
minusMonotone2 = Sub axiom

minusMonotone2' :: forall a b c. (c - b <= c - a,b<=c):-(a <= b)
minusMonotone2' = Sub axiom

The current tools can do a lot of things. For instance:

class c => IdC c
instance c => IdC c

class ForallT IdC p => Forall2 (p :: k1 -> k2 -> Constraint)
instance ForallT IdC p => Forall2 p

inst2 :: forall (p :: k1 -> k2 -> Constraint) . (a :: k1) (b :: k2)  . Forall2 p :- p a b
inst2 = Sub $ case instT :: ForallT IdC p :- IdC (p a b) of Sub Dict -> Dict

Forall can also do other fancy things:

class con c (s c) => What con s c
instance con c (s c) => What con s c

Now Forall (What con s) means that for all c, the constraint con c (s c) holds. This can be used to express that a class like

class C elem container | container -> elem where
  insert :: elem -> container -> container

is a "superclass" of a corresponding constructor class:

class Forall (What C f) => D f where
  mapIt :: (a -> b) -> f a -> f b
insert1 :: D f => a -> f a -> f a
insert1 = -- something using `inst`

Unfortunately, each such case must currently be constructed entirely by hand. Is there some way we can do this "generically", letting the user provide some representation of the structure of a constraint expression, where the holes should be, and (ugh) which holes should be tied together?

Hi Edward, Ryan,

I'm looking at Edward's comments on this libraries thread, and SPJ's follow-up in January linking to the QuantifiedConstraints work/Trac #2893 just Phab'd.

I have a possible use case in mind for implication constraints, so I came here to look at the package. But I'm finding no helpful documentation about it. I've tried reading the commets in the source. Do I need to understand Category Theory and what is a Heyting Algebra to use this? Then I won't bother.

To give a hint of my use case: I'm wondering if constraint implication can help express the logic in an anonymous/extensible records system. If I have a base constraint Has r l a expressing record r has label l at type a, can I express the constraint on record append :: r1 -> r2 -> r3 such that

(forall l1 a1 . Has r1 l1 a1 => Has r3 l1 a1, forall l2 a2 . Has r2 l2 a2 => Has r3 l2 a2) => ...

Ideally record append should go beyond that to say that if Has r3 l a then either Has r1 l a or Has r2 l a. Then perhaps I need to understand Edward's comment

3.) Constraint also admits a sum type, (\/) but it acts more like a least upper bound than an either.

I suggest derive KnownNat and KnownSymbol without magic, using the method from the package singletons in the module Data.Singletons.Prelude.Num.
This one allows us to derive without the unsafe coercion of the kind * to * -> *.
This method is used in the instance declaration SNum Nat.
Pull request #59 was added.

Currently:

dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ a)
timesDiv :: forall a b. Dict ((a * Div b a) <= a)

a*floor(b/a) = b, not a, if a divides b.
a*floor(b/a) <= b, not a.

The following snippet used to type check with constraints 0.4.1.3 but now it doesn't as of 0.6:

import Control.Concurrent.Async.Lifted.Safe -- lifted-async >= 0.7
import Control.Monad.Reader
import Control.Monad.Trans.Control -- monad-control >= 1

foo :: (MonadBaseControl IO m, Forall (Pure m)) => ReaderT () m a -> ReaderT () m a
foo act = withAsync act wait

{-
Ideally we could write:

withAsync
  :: forall m a b. (MonadBaseControl IO m, forall a. StM m a ~ a)
  => m a -> (Async a -> m b) -> m b

but GHC doesn't support quantified constraints. So instead we do this in lifted-async:

class StM m a ~ a => Pure m a
withAsync
  :: forall m a b. (MonadBaseControl IO m, Forall (Pure m))
  => m a -> (Async a -> m b) -> m b
-}

With constraints >= 0.6, GHC complains

    Could not deduce (StM
                        m (Data.Constraint.Forall.Skolem (Pure (ReaderT () m)))
                      ~ Data.Constraint.Forall.Skolem (Pure (ReaderT () m)))
    from the context (MonadBaseControl IO m, Forall (Pure m))
      bound by the type signature for
                 bar :: (MonadBaseControl IO m, Forall (Pure m)) =>
                        ReaderT () m a -> ReaderT () m a

This is because

Forall (Pure m)
~ Forall_ (Pure m)
~ Pure m (Skolem (Pure m))
~ (StM m (Skolem (Pure m)) ~ (Skolem (Pure m)))

and if m ~ ReaderT () n, GHC can't deduce the constraints.

In contrast with constraints == 0.4.1.3:

Forall (Pure m)
~ (Pure m A, Pure m B)
~ (StM m A ~ A, StM m B ~ B)

so if m ~ ReaderT () n, the constraints become

(StM (ReaderT n) A ~ A, StM (ReaderT n) B ~ B)

which are true.

In order to work around this issue, I have to change the constraints of foo to contain ReaderT ():

foo :: (MonadBaseControl IO m, Forall (Pure (ReaderT () m)) => ReaderT () m a -> ReaderT () m a

Was this use-site change intentional? Could we somehow restore the previous behavior (in constraints or lifted-async) without sacrificing the better definitions of Forall and Skolem etc?

Now that Forall is poly-kinded, I think we can define ForallF to use it:

class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)
instance p (f a) => ComposeC p f a

class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)
instance Forall (ComposeC p f) => ForallF p f

instF :: forall p f a . ForallF p f :- p (f a)
instF = Sub $
  case inst :: Forall (ComposeC p f) :- ComposeC p f a of
   Sub Dict -> Dict

Unfortunately, I haven't been able to find a way to write functions converting between this ForallF and the standard ForallF without mentioning the names of skolems. The essential difficulty seems to be moving foralls around. I conjecture, however, that they are fundamentally equivalent, and that anything in the wild that satisfies one will also satisfy the other.

Is there any way to give a common name to Sub Dict?

The closest I got was

subdict :: forall a b. a => a :- b
subdict = Sub @a @b (Dict @a)

but I couldn't write refl in terms of it without a constraint..

refl :: a => a :- a
refl = subdict

Can the kind of ForallT be generalised

-- ForallT :: (k4 -> Constraint) -> ((k1 -> k2) -> k3 -> k4) -> Constraint
ForallT :: (k3 -> Constraint) -> (k1 -> k2 -> k3)

I need this to model PipeKit from Faster Coroutine Pipelines

class ForallT Monad pipe => PipeKit pipe where
  input :: pipe i o i
  output :: o -> pipe i o ()
  -- ...

Works by removing kind annotations

class    p (t a b)        => R p t a b
instance p (t a b)        => R p t a b

class    Forall (R p t a) => Q p t a
instance Forall (R p t a) => Q p t a

class    Forall (Q p t)   => ForallT p t
instance Forall (Q p t)   => ForallT p t

instT :: forall p t f a. ForallT p t :- p (t f a)
instT = Sub $
  case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->
  case inst :: Forall (R p t f) :- R p t f a of
    Sub Dict -> Dict }

Just wanted to report that constraints 0.3.4 compile fails with ghc 7.6.3 when we
tried to bump it in the gentoo haskell overlay, thanks.

-- mode: compilation; default-directory: "/var/tmp/portage/dev-haskell/constraints-0.3.4/work/constraints-0.3.4/" --
Compilation started at Sat Oct 12 23:40:10

./setup build
Building constraints-0.3.4...
Preprocessing library constraints-0.3.4...
[1 of 3] Compiling Data.Constraint ( Data/Constraint.hs, dist/build/Data/Constraint.o )

Data/Constraint.hs:133:43: parse error on input `::'

Compilation exited abnormally with code 1 at Sat Oct 12 23:40:10

Forall p won't work as expected if there are multiple occurence of a in the rhs of p a.
A trivial example:

{-# LANGUAGE ConstraintKinds, LiberalTypeSynonyms, TypeOperators, TypeFamilies #-}
module Main where
import Data.Constraint
import Data.Constraint.Forall

type Reflex a = a ~ a

reflexDic :: Forall Reflex :- Reflex a
reflexDic = inst

This code won't compile in constraints-0.4 plus ghc-7.8.3. The compilation error is as follows:

    Couldn't match type ‘Data.Constraint.Forall.A’
                  with ‘Data.Constraint.Forall.B’
    Expected type: Forall Reflex :- Reflex a
      Actual type: Forall ((~) Data.Constraint.Forall.A)
                   :- (Data.Constraint.Forall.A ~ a)
    In the expression: inst
    In an equation for ‘myDic’: myDic = inst

Instead of:

It could be:

dividesTimes :: Divides a b :- Divides a (b * c) 

The version where a divides c is recoverable via commutativity of the multiplication.

These might be useful for Data.Constraint.Deferrable

deferWithDefault_ :: forall c. Deferrable c => forall r. r -> (c => r) -> r
deferWithDefault_ def r =
  case deferEither_ @c r of
    Left  err -> def
    Right a   -> a

deferWithDefault :: Deferrable c => proxy c -> r -> (c => r) -> r
deferWithDefault proxy def r =
  case deferEither proxy r of
    Left  err -> def
    Right a   -> a

Since 7.10 Typeable is derived for everything. This means Forall Typeable = (Typeable A, Typeable B) is satisfied so you can write

import Data.Constraint
import Data.Constraint.Forall

typeable :: a -> Dict (Typeable a)
typeable _ = case inst of Sub d -> d

> case typeable 'a' of Dict -> typeOf 'a'
A

which allows you to write an unsafeCoerce without any extensions:

import Data.Typeable

unsafeCoerce :: a -> b
unsafeCoerce a = b
  where
    Just b = case typeable a of
      Dict -> case typeable b of
        Dict -> cast a

> unsafeCoerce 'a'
97