Common name for ‘Sub Dict’ about constraints HOT 8 CLOSED

You would still need the unsafeCoercing to construct an a :- b from an a => Dict b then.

Here's one way (I think) to do the unsafeCoercing (using the old definition of (:-))

I vote for naming subdict implied:

implied :: forall a b. (a => b) => a :- b

from constraints.

I am also in favor of adding implied.

The change to (:-) proposed in #41 (comment) is interesting, but it would require constraints to cut off support for pre-8.6 versions of GHC. (Unless we were to employ some sort of CPP-based backwards-compatibility hack, which doesn't sound appealing.) Until then, adding implied should be uncontroversial.

from constraints.

Wait! Does it require implication constraints

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

Is it completely equivalent or is one more powerful than the other? I makes sense that entailment is a reified version of implication constraints like these are reified versions of coercion, constraints, equality, ...

Coercion :: Coercible a b => Coercion a b

Dict :: a => Dict a

Refl :: a ~ b => a :~: a

HRefl :: a ~~ b => a :~~: b

If so then there is no way to write subdict until we get implication constraints, feel free to close this.

from constraints.

There is no way to write this at present.

from constraints.

This is now possible with the WIP QuantifiedConstraints branch of GHC:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Foo where

data Dict c where
  Dict :: c => Dict c

newtype a :- b = Sub (a => Dict b)

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

from constraints.

This will probably have to wait until 8.6 or so before it can be added directly to the library. It seems like QuantifiedConstraints will miss the 8.4 branch at this point.

from constraints.

Can't wait for QC. Going the other way ((a :- b) -> Dict (a => b)) is not possible though

from constraints.

Building the other direction is a messy exercise in unsafeCoercing enough stuff to produce the right core. It is admissible.

But we could avoid that completely. In the presence of QuantifiedConstraints the encoding I use for (:-) is suboptimal. Switching from the existing Sub Dict encoding to

data a :- b where
   Sub :: (a => b) -> a :- b

or, equivalently,

newtype a :- b = Sub (Dict (a => b))

makes this easy though, giving a good reason to favor such an encoding over the current approach going forward.

from constraints.