Opened 7 years ago

Closed 18 months ago

Last modified 15 months ago

#5927 closed feature request (duplicate)

A type-level "implies" constraint on Constraints

Reported by: illissius Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.4.1
Keywords: QuantifiedConstraints Cc: heisenbug, dimitris@…, shane@…, tkn.akio@…, maoe, RyanGlScott, Artyom.Kazak, int-index, kosmikus, kcsongor
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #2893 Differential Rev(s):
Wiki Page:

Description

I have a datatype:

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

I have an instance for it:

instance Show (Exists Show) where
    show (Exists a) = show a

And that's alright, as far as it goes: any Exists Show can indeed itself be shown. But I want more. I want to be able to say:

instance (c `Implies` Show) => Show (Exists c) where
    show (Exists a) = show a

In other words, I want to be able to say that any (Exists c) where the constraint c implies Show can be shown. For example, if Num still had a Show constraint, I wouldn't want to have to write a separate instance Show (Exists Num) to be able to show an Exists Num; I would want to be able to write a single instance (along the lines of the above) which works for both.

GHC clearly has this information: it lets me use a function of type forall a. Eq a => a -> r as one of type forall a. Ord a => a -> r, but not vice versa, so it knows that Ord implies Eq, but not vice versa. I've attached a file which demonstrates this and a couple of other examples.

What's not completely clear to me is what would be the appropriate way to be able to ask it about this. An Implies constraint to parallel the (~) constraint would work, but with what syntax? (Just straightforwardly call it Implies?) And what semantics -- what would be the kind of Implies? It's notable that in the above example its arguments aren't of type Constraint, but rather * -> Constraint, and for (* -> *) -> Constraint it could similarly work, and with MPTCs * -> * -> Constraint and (* -> *) -> (* -> *) -> Constraint and * -> (* -> *) -> Constraint and so on probably also make sense... but I have no idea how to formalize this, where the boundaries lie, and whether it makes any kind of sense. I can try to think harder about it if that would help, but hopefully the outlines of the situation are more immediately obvious to someone on the GHC team.

Attachments (1)

implies.hs (816 bytes) - added by illissius 7 years ago.

Download all attachments as: .zip

Change History (36)

Changed 7 years ago by illissius

Attachment: implies.hs added

comment:1 Changed 7 years ago by simonpj

Cc: dimitris@… added
difficulty: Unknown
Milestone: 7.6.1

What you say makes sense, but I don't have any idea how to achieve it. One way to get what you want woudl be something like

instance (forall a. c a => Show a) => Show (Exists c) where ...

and that is close to the idea in Section 7.2 of Derivable Type Classes.

I have no idea how difficult this would to actually implement, but last time I thought about it, it seemed pretty hard. I'll milestone it at 7.6 for now, but it's much more than an incremental feature.

Simon

comment:2 Changed 7 years ago by illissius

If I'm understanding correctly, the problem could be decomposed into two parts?

  • On the one hand you would have an implication constraint between Constraints, c => d meaning that c implies d. GHC actually accepts this kind of syntax already, but it seems to mean something different (if I write foo :: (Ord Int => Eq Int) => Int, it seems to treat this as foo :: (Ord Int => Eq Int) -> Int and then expects an Ord Int => Eq Int, whatever that is, as a value-level argument?).
  • On the other hand you would have the quantified constraints feature from #2893. In the same way that you could write forall a. Monoid (m a), together with the previous feature you could write forall a. c a => Show a.

If that's the case then, seeing that quantified constraints already has a ticket, I'll clarify that this one is referring to the other half. It's also more useful by itself for my own use case because quantified constraints can be emulated to some extent with GADTs and evil hacks, but I don't see any way at all to express something like c => d (but correct me if I'm wrong!).

comment:3 Changed 7 years ago by simonpj

Yes, I was referring exclusively to #2893 (but I'd forgotten we have a ticket for it).

I'm afraid I don't understand the other part you describe.

comment:4 Changed 7 years ago by illissius

The canonical example of what #2893 lets you write is something like:

instance (Monad m, forall a. Monoid (m a)) => MonadPlus m where ...

The example from the paper is:

instance (Binary a, forall b. Binary b => Binary (f b)) => Binary (GRose f a) where ...

And the example here was:

instance (forall a. c a => Show a) => Show (Exists c) where ...

The way I have it in my head it's not clear to me that #2893 would, on its own, let you write the latter two examples. To put it simplistically it would you write the forall, but not the =>.

The way I'm reading the second example above is, "if (Binary a), and also (Binary (f b)) follows from (Binary b) for any b, then Binary (GRose f a)". The first example is saying, "if (Monad m), and also (Monoid (m a)) for any a, then (MonadPlus m)". The difference is that in the MonadPlus example and all existing Haskell there's noplace where you say "if b follows from a, then c", you only say "if b, then c". But the latter two examples do also have this "if b follows from a, then c" construct. And I think #2893 is what would let you say the "for any a" part of it, while the feature described by this ticket is what would let you say the "if b follows from a, then" part.

If we look at three simple examples:

instance forall a. C (A a) => D A where ...
instance (C a => C (A a)) => E (A a) where ...
instance (forall a. C a => C (A a)) => D A where ...

then #2893 (let's call it QuantifiedConstraints) would let you write the first example, this ticket (let's call it ImplicationConstraints) would let you write the second example, but only their combination would let you write the third example.

I'm imagining that, with ImplicationConstraints, (=>) would be a type level operator similar to (~):

(~)  :: forall k. k -> k -> Constraint
(=>) :: Constraint -> Constraint -> Constraint

and you would need QuantifiedConstraints to be able to use (=>) to also talk about k1...kN -> Constraints.

I hope this is clearer. Don't hesitate to holler at me if I'm talking nonsense.

comment:5 Changed 7 years ago by simonpj

OK well

  • Indeed I was thinking of the combination of QuantifiedConstraints and ImplicationConstraints; thanks for clarifying
  • The design and implementation would be a significant task.
  • I don't have a clear picture of the cost/benefit ratio

comment:6 Changed 7 years ago by illissius

Right; obviously it's up to you and the rest of the GHC team to figure out what it makes sense to spend time on. This is just to keep track of one of the things that would be nice. Thanks for your time!

comment:7 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:8 Changed 6 years ago by duairc

Cc: shane@… added

comment:9 Changed 6 years ago by goldfire

There's not really built-in compiler support for these ideas, but have you seen the constraints package? It allows you to manually enter and use implication relationships. This doesn't solve the fundamental problem here, but it may help with a workaround.

comment:10 Changed 6 years ago by illissius

I know about it (referenced it actually in an earlier comment), thanks! I don't think I have an actual practical problem to be worked around. I was just experimenting, exploring, and testing the limits of what's possible. As usual I hit them.

comment:11 Changed 6 years ago by akio

Cc: tkn.akio@… added

comment:12 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:13 Changed 5 years ago by thoughtpolice

Milestone: 7.10.17.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:14 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:15 Changed 4 years ago by thomie

Milestone: 8.0.1

comment:16 Changed 3 years ago by maoe

Cc: maoe added

comment:17 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

I do have a pratical use-case for this feature: I think it would help solve part of the story for being able to derive Generic instances for GADTs (see Trac issues #8560 and #10514). In particular, I think ImplicationConstraints would allow be to be polymorphic over any existentially quanitified constraint in a GADT. In particular, there are GADTs like this:

class GShow a where
  gshow :: a -> String

data T a where
  MkT :: GShow a => a -> T a

GHC generics currently lacks a facility for expressing the existential GShow constraint. I think we could add something like this:

data EC c f a where
  MkEC :: c => f a -> EC c f a

Then we could derive a Generic instance for T like so:

instance Generic (T a) where
  type Rep (T a) =
    D1 ('MetaData "T" "Ghci2" "interactive" 'False)
      (C1 ('MetaCons "MkT" 'PrefixI 'False)
        (EC (GShow a)
          (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rec0 a))))
  from (MkT x) = M1 (M1 (MkEC (M1 (K1 x))))
  to (M1 (M1 (MkEC (M1 (K1 x))))) = MkT x

So far, so good. Now I want to be able to define a generic GShow instance for T (where GShow comes from the generic-deriving library). We already have cases for all generic datatypes except EC. This is what I want to be able to write:

class GShow' f where
  gshow' :: f a -> String

instance (c => GShow' f) => GShow' (EC c f) where
  gshow' (MkEC x) = gshow' x

But for that, I need ImplicationConstraints. If I want to generalize this to Generic1 instances, I'd probably need QuantifiedConstraints too.

comment:18 Changed 3 years ago by Iceland_jack

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:19 Changed 3 years ago by Iceland_jack

Would this Show instance for Fmt work with ImplicationConstraints ((=>) :: (Type -> Constraints) -> (Type -> Constraints) -> Constraints):

data Fmt :: (* -> Constraint) -> (* -> *) -> * -> * where
  Int  :: p Int               => Fmt p r Int
  (:&) :: (p a, p b, p (a,b)) => Fmt p r a -> Fmt p r b -> Fmt p r (a,b)
  Lift :: p (r a)             => r a       -> Fmt p r a

instance (ctx `Implies` Show) => Show (Fmt ctx r a) where
  show t = case t of
             Int    -> "Int"
             l :& r -> show l ++ "&" ++ show r
             Lift r -> show r

A question on QuantifiedConstraints on this same example in ticket:2893#comment18.


Edit: If I understand correctly (=>) is the internal hom of constraints, Edward Kmett used the less ambiguous notation (|-) in private correspondence.

The combination of ImplicationConstraints + QuantifiedConstraints sounds very exciting.

Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:20 Changed 3 years ago by Iceland_jack

Are any of these variations of Exists useful

data Exists1 :: (Type -> Constraint) -> Type where
  Exists1 :: (ctx `Implies` c, c a) => a -> Exists1 ctx

data Exists2 :: (Type -> Constraint) -> Type where
  Exists2 :: (ctx `Implies` c, ctx a) => a -> Exists2 c

data Exists3 :: (Type -> Constraint) -> (Type -> Constraint) -> Type where
  Exists3 :: (ctx `Implies` c, ctx a) => a -> Exists3 ctx c 

data Exists4 :: (Type -> Constraint) -> Type where
  Exists4 :: (ctx `Implies` c, c a) => a -> Exists4 c

data Exists5 :: (Type -> Constraint) -> (Type -> Constraint) -> Type where
  Exists5 :: (ctx `Implies` c, c a) => a -> Exists5 ctx c 

-- ...

Edit: Will you be able to write

hestur :: (forall ctx. ctx `Implies` Show => Exists ctx -> IO ())
       -> ([Exists Show] -> [Exists (Show:&:Ord)] -> IO ())
hestur f xs ys = do
  traverse_ f xs
  traverse_ f ys

given combining constraints

class    (c a, d a) => (c :&: d) a
instance (c a, d a) => (c :&: d) a
infixl 7 :&:
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:21 Changed 3 years ago by Iceland_jack

http://yav.github.io/publications/improving-smt-types.pdf

3.1 Implication Constraints

During type inference, GHC uses implication constraints, which do not appear in Haskell source code directly. An implication constraint is, roughly, of the form G ⇒ W, where W is a collection of constraints that need to be discharged, and G are assumptions that may be used while discarding W. In the GHC source code, the constraints in G are referred to as given constraints, while the ones in W are known as wanted constraints. The intuition behind an implication constraint is that W contains the constraints that were collected while checking a program fragment, while G contains local assumptions that are available only in this particular piece of code.

comment:22 Changed 3 years ago by Iceland_jack

I believe MonadTrans should be

class forall m. Monad m `Implies` Monad (t m) => MonadTrans t where
  lift :: Monad m => m a -> (t m) a

comment:23 Changed 3 years ago by Iceland_jack

This has one of the best examples

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

newtype Free0 k p     = Free0 (forall q. k q => (p  -> q) -> q)
newtype Free1 k p a   = Free1 (forall q. k q => (p  ~> q) -> q a)
newtype Free2 k p a b = Free2 (forall q. k q => (p ~~> q) -> q a b)

class Semigroup m
class Semigroup m => Monoid m

class                   Semigroupoid c
class Semigroupoid c => Category c
class Category     c => Arrow    c

you can define

instance p `Implies` Semigroup => Semigroup (Free0 p a)
instance p `Implies` Monoid    => Monoid    (Free0 p a)

instance p `Implies` Semigroupoid => Semigroupoid (Free2 p a)
instance p `Implies` Category     => Category     (Free2 p a)
instance p `Implies` Arrow        => Arrow        (Free2 p a)
instance p `Implies` ArrowLoop    => ArrowLoop    (Free2 p a) -- (?)

instead of

instance Semigroup (Free0 Semigroup a)
instance Semigroup (Free0 Monoid    a)
instance Monoid    (Free0 Monoid    a)

instance Semigroupoid (Free2 Semigroupoid p)
instance Semigroupoid (Free2 Category     p)
instance Semigroupoid (Free2 Arrow        p)
instance Semigroupoid (Free2 ArrowLoop    p)
instance Category     (Free2 Category     p)
instance Category     (Free2 Arrow        p)
instance Category     (Free2 ArrowLoop    p)
instance Arrow        (Free2 Arrow        p)
instance Arrow        (Free2 ArrowLoop    p)
instance ArrowLoop    (Free2 ArrowLoop    p)

comment:24 Changed 2 years ago by Artyom.Kazak

Cc: Artyom.Kazak int-index added

comment:25 Changed 2 years ago by kosmikus

Cc: kosmikus added

comment:26 Changed 2 years ago by heisenbug

Cc: heisenbug added

comment:27 Changed 20 months ago by simonpj

Keywords: QuantifiedContexts added

comment:28 Changed 19 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:29 Changed 18 months ago by kcsongor

Cc: kcsongor added

comment:30 Changed 18 months ago by RyanGlScott

Resolution: duplicate
Status: newclosed

The "Implies" in (c `Implies` Show a) is the => in the quantified constraint (c => Show a). Quantified constraints also allow you to write forall a. Monoid a.

Or, to put things another way, this is a duplicate of #2893, which tracks the implementation of QuantifiedConstraints. I'll close this ticket in favor of that one.

Last edited 18 months ago by RyanGlScott (previous) (diff)

comment:31 Changed 18 months ago by simonpj

Are there any test cases from this ticket that we can add as regression tests for #2983?

comment:32 Changed 18 months ago by RyanGlScott

Hm. I suppose you could add the original program from this ticket:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module T5927 where

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

instance (forall a. c a => Show a) => Show (Exists c) where
  show (Exists a) = show a

But this actually fails!

Bug.hs:9:10: error:
    • Could not deduce: c (Exists c)
        arising from a use of ‘GHC.Show.$dmshowsPrec’
      from the context: forall a. c a => Show a
        bound by the instance declaration at Bug.hs:9:10-53
    • In the expression: GHC.Show.$dmshowsPrec @(Exists c)
      In an equation for ‘showsPrec’:
          showsPrec = GHC.Show.$dmshowsPrec @(Exists c)
      In the instance declaration for ‘Show (Exists c)’
    • Relevant bindings include
        showsPrec :: Int -> Exists c -> ShowS (bound at Bug.hs:9:10)
  |
9 | instance (forall a. c a => Show a) => Show (Exists c) where
  |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bug.hs:9:10: error:
    • Could not deduce: c (Exists c)
        arising from a use of ‘GHC.Show.$dmshowList’
      from the context: forall a. c a => Show a
        bound by the instance declaration at Bug.hs:9:10-53
    • In the expression: GHC.Show.$dmshowList @(Exists c)
      In an equation for ‘showList’:
          showList = GHC.Show.$dmshowList @(Exists c)
      In the instance declaration for ‘Show (Exists c)’
    • Relevant bindings include
        showList :: [Exists c] -> ShowS (bound at Bug.hs:9:10)
  |
9 | instance (forall a. c a => Show a) => Show (Exists c) where
  |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I'm not sure what to make of this. If you implement showsPrec and showList manually:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module T5927 where

import Text.Show

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

instance (forall a. c a => Show a) => Show (Exists c) where
  show (Exists a) = show a
  showsPrec p (Exists a) = showsPrec p a
  showList l = showListWith (\(Exists a) -> shows a) l

Then it typechecks.

comment:33 Changed 18 months ago by simonpj

Hmm. This is interesting. We have

$dmshowsPrec :: Show a => Int -> a -> ShowS

and the implied instance decl is

instance (forall a. c a => Show a) => Show (Exists c) where
  show (Exists a) = show a
  showsPrec = $dmshowsPrec

From the RHS of showsPred we get [W] Show (Exists c). And alas we try to solve that from the quantified constraint (which takes precedence over top-level instances), by instantiating a to (Exists c). So we get

  [W} c (Exists c)

which we can't solve.

This would happen on any recursive invocation of a method at the same type.

It's not clear what we want here. The quantified constraint claims to provide an instance for every type a which is jolly suspicious.

comment:34 Changed 18 months ago by RyanGlScott

Hm. That is not at all how I would have expected that instance to be solved. I agree that when typechecking $dmshowsPrec, we should start with:

  • [W] Show (Exists c)

But don't we get that immediately? In other words, this typechecks:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module T5927 where

import Text.Show

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

instance Show (Exists c) where
  show = show
  showsPrec = undefined
  showList = undefined

Because when typechecking the RHS of show, we need [W] Show (Exists c), but we already have that. It's only when we strengthen the context:

instance  (forall a. c a => Show a) => Show (Exists c) where
  show = show
  showsPrec = undefined
  showList = undefined

That GHC complains:

Bug.hs:12:10: error:
    • Could not deduce: c (Exists c) arising from a use of ‘show’
      from the context: forall a. c a => Show a
        bound by the instance declaration at Bug.hs:11:10-53
    • In the expression: show
      In an equation for ‘show’: show = show
      In the instance declaration for ‘Show (Exists c)’
    • Relevant bindings include
        show :: Exists c -> String (bound at Bug.hs:12:3)
   |
12 |   show = show
   |          ^^^^

comment:35 Changed 15 months ago by Ben Gamari <ben@…>

In 7df5896/ghc:

Implement QuantifiedConstraints

We have wanted quantified constraints for ages and, as I hoped,
they proved remarkably simple to implement.   All the machinery was
already in place.

The main ticket is Trac #2893, but also relevant are
  #5927
  #8516
  #9123 (especially!  higher kinded roles)
  #14070
  #14317

The wiki page is
  https://ghc.haskell.org/trac/ghc/wiki/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.

Here is the relevant Note:

Note [Quantified constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The -XQuantifiedConstraints extension allows type-class contexts like
this:

  data Rose f x = Rose x (f (Rose f x))

  instance (Eq a, forall b. Eq b => Eq (f b))
        => Eq (Rose f a)  where
    (Rose x1 rs1) == (Rose x2 rs2) = x1==x2 && rs1 >= rs2

Note the (forall b. Eq b => Eq (f b)) in the instance contexts.
This quantified constraint is needed to solve the
 [W] (Eq (f (Rose f x)))
constraint which arises form the (==) definition.

Here are the moving parts
  * Language extension {-# LANGUAGE QuantifiedConstraints #-}
    and add it to ghc-boot-th:GHC.LanguageExtensions.Type.Extension

  * A new form of evidence, EvDFun, that is used to discharge
    such wanted constraints

  * checkValidType gets some changes to accept forall-constraints
    only in the right places.

  * Type.PredTree gets a new constructor ForAllPred, and
    and classifyPredType analyses a PredType to decompose
    the new forall-constraints

  * Define a type TcRnTypes.QCInst, which holds a given
    quantified constraint in the inert set

  * TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
    which holds all the Given forall-constraints.  In effect,
    such Given constraints are like local instance decls.

  * When trying to solve a class constraint, via
    TcInteract.matchInstEnv, use the InstEnv from inert_insts
    so that we include the local Given forall-constraints
    in the lookup.  (See TcSMonad.getInstEnvs.)

  * topReactionsStage calls doTopReactOther for CIrredCan and
    CTyEqCan, so they can try to react with any given
    quantified constraints (TcInteract.matchLocalInst)

  * TcCanonical.canForAll deals with solving a
    forall-constraint.  See
       Note [Solving a Wanted forall-constraint]
       Note [Solving a Wanted forall-constraint]

  * We augment the kick-out code to kick out an inert
    forall constraint if it can be rewritten by a new
    type equality; see TcSMonad.kick_out_rewritable

Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

* Move SCC on evidence bindings to post-desugaring, which fixed
  #14735, and is generally nicer anyway because we can use
  existing CoreSyn free-var functions.  (Quantified constraints
  made the free-vars of an ev-term a bit more complicated.)

* In LookupInstResult, replace GenInst with OneInst and NotSure,
  using the latter for multiple matches and/or one or more
  unifiers
Note: See TracTickets for help on using tickets.