Opened 11 years ago

Closed 16 months ago

#2893 closed feature request (fixed)

Implement "Quantified constraints" proposal

Reported by: porges Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 6.10.1
Keywords: QuantifiedConstraints, GHCProposal Cc: id@…, reiner.pope@…, illissius@…, sjoerd@…, shane@…, ggreif@…, maoe, RyanGlScott, Iceland_jack, baramoglo
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: quantified-constraints/T2893{,a,c}
Blocked By: Blocking:
Related Tickets: #5927 Differential Rev(s): Phab:D4724
Wiki Page:

Change History (41)

comment:1 Changed 11 years ago by guest

Cc: id@… added

My initial sense is this is a nice proposal.

I wonder a little bit how this would interact with other typeclass needs.

What's an example of a function that would need to be typed

:: (Monad m, forall a. Monoid (m a)) => (something or other)

? And would the compiler be able to infer the signature if it wasn't written?

(and is this even the right forum to be asking these questions in? Who wrote the proposal, and when?)

-Isaac Dupree

comment:2 Changed 11 years ago by porges

Well here's an example: today I was trying to write an instance of Applicative for things that are Monoids and Foldable (started by generalizing from [a]):

This is currently not possible because Applicative & Foldable are both (* -> *) and Monoids are (*). As far as I can tell, the proposal would allow something like this:

instance (Foldable l, forall a. Monoid (l a)) => Applicative l where
	fs <*> xs = foldMap (<$> xs) fs

I may be horribly wrong, however :)

(Also I can't implement pure :P)

comment:3 Changed 11 years ago by simonpj

difficulty: Unknown
Milestone: _|_

I had trouble following the proposal. I didn't see how Section 3 addressed the issues raised in Sections 1 and 2. For example, to avoid the cascade of Typeable2, Typeable3 etc classes the solution is presumably polymorphism at the kind level. (Tim Sheard's language Omega has this.)

Still, I recognise the merit of quantification in contexts. Indeed, Ralf Hinze and I suggested it back in 2000 in Section 7 of Derivable type classes. (This section is rather independent of the rest of the paper.)

However, attractive as it is, it's quite a big step to add something akin to local instance declarations. Our ICFP'08 paper Type checking with open type functions relies rather crucially on not having such local instances. (We've managed to simplify the algorithm quite a bit since then, but it still relies on that assumption.)

So I'm not sure I see how to make quantified contexts compatible with type functions, and all the other stuff in Haskell. But their lack is clearly a wart, and one that may become more pressing.

Meanwhile, clarifying the proposal would be a good thing, even if it's not adopted right away.

Simon

comment:4 Changed 10 years ago by porges

A short version... we allow contexts of the form:

(forall a. Bar f a) => Foo f 

And more generally, these contexts can have contexts of their own:

(forall a. (Baz a) => Bar f a) => Foo f

I'm not sure if the 'more general' version adds extra difficulty in type-checking, as I am not very familiar with its intricacies.

Forgive my stupidity, I don't understand where the typechecking (at least in the first) becomes so difficult—the context means that there is an instance available which is free in the specified variable.

comment:5 Changed 9 years ago by lilac

Type of failure: None/Unknown

This blog post provides an excellent motivating example for this feature.

comment:6 Changed 9 years ago by reinerp

Cc: reiner.pope@… added

comment:7 Changed 8 years ago by illissius

Cc: illissius@… added

comment:8 Changed 8 years ago by batterseapower

As the blog post points out (and I recently rediscovered) GHC already supports this feature in a more elaborate form. This works:

{-# LANGUAGE GADTs, Rank2Types, FlexibleContexts #-}

class Foo a where
    foo :: a -> String

instance Foo [b] where
    foo = show . length

data FooDict a where
    FooDict :: Foo a => FooDict a

f :: (forall b. FooDict [b]) -> String
f FooDict = foo "Hello" ++ foo [1, 2, 3]

use_foo :: String
use_foo = f FooDict

But this is rejected:

g :: (forall b. Foo [b]) => String
g = foo "Hello" ++ foo [1, 2, 3]

use_foo' :: String
use_foo' = g

So there doesn't seem to be a fundamental difficulty here.

comment:9 Changed 7 years ago by sjoerd_visscher

Cc: sjoerd@… added

I don't see why this needs "local instances". The instances are not the problem, we can already do polymorphic instances, i.e. instance Monoid [a]. Even specifying the forall constraint now (accidentally) works in GHC 7.4.1.

As I see it, the problem is with matching the need for a constraint with the available constraints or instances. See #7019, the error is "Could not deduce (Monoid [b]) from the context (forall a. Monoid [a])".

Even g from the previous comment now compiles (with ConstraintKinds and UndecidableInstances), except when evaluating it, you get the error: "Could not deduce (forall b. Foo [b]) arising from a use of `g'".

So it seems that with implementing ConstraintKinds, there has been made a big step towards an implementation of quantified contexts.

comment:10 Changed 7 years ago by sjoerd_visscher

Edward Kmett created a workaround: Data.Constraint.Forall

It works like this: if you have p A and p B, for unexported A and B, then you must have forall a. p a. Then unsafeCoerce is used to coerce p A to p a.

comment:11 Changed 7 years ago by duairc

Cc: shane@… added

comment:12 Changed 5 years ago by heisenbug

Cc: ggreif@… added

Copying a use-case from #9196:

My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-* kind, that is an ADT.

See:

class Foo a where ...
data Bar (b :: Bool) x = ...
instance Foo (Bar True x) where ...
instance Foo (Bar False x) where ...

test :: (forall b. Foo (Bar b x)) =>...

Here the forall condition is satisfiable, as all Bool alternatives are covered with instance declarations.

comment:13 Changed 5 years ago by simonpj

The trouble is that I don't know how to do type inference in the presence of polymorphic constraints. It is not a small change.

It would be a useful feature. I've wanted it since at least 2000 (see Derivable Type Classes).

Simon

comment:14 Changed 4 years ago by maoe

Cc: maoe added

comment:15 Changed 3 years ago by RyanGlScott

Cc: RyanGlScott added

comment:16 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:17 Changed 3 years ago by Iceland_jack

Moved from #5927.

Use case from How to Twist Pointers without Breaking Them:

class Monoid m => Action m a where
 act :: m -> a -> a

[...]

We first formalise the action of monoids on functors. Intuitively, for a monoid m to act on the functor f, it should act in a uniform way on all the types f a. Therefore, we would like to assert a constraint something like forall a. Action m (f a). Unfortunately, Haskell does not allow the use of universally quantified constraints and hence we need a new type class.

class (Monoid m, Functor f) => ActionF m f where
  act' :: m -> f a -> f a

comment:18 Changed 3 years ago by Iceland_jack

This functionality does my head in so bear with me.

In the definition of Fmt, constraints of (p a, p b, p (a, b)) are assumed for :&

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

(p a, p b) often implies p (a, b), would this be captured by QuantifiedConstraints?

  (:&) :: (p a, p b, forall xx yy. (p xx, p yy) => p (xx, yy)) 
       => Fmt p r a 
       -> Fmt p r b 
       -> Fmt p r (a,b)

Does this even give us any additional power? Is this more or less powerful than the :=> class from constraints?

class b :=> h | h -> b where
  ins :: b :- h

instance (Eq      a, Eq      b) :=> Eq      (a, b) where ins = Sub Dict
instance (Ord     a, Ord     b) :=> Ord     (a, b) where ins = Sub Dict
instance (Show    a, Show    b) :=> Show    (a, b) where ins = Sub Dict
instance (Read    a, Read    b) :=> Read    (a, b) where ins = Sub Dict
instance (Bounded a, Bounded b) :=> Bounded (a, b) where ins = Sub Dict
instance (Monoid  a, Monoid  b) :=> Monoid  (a, b) where ins = Sub Dict
...

What if we assume that GHC generates instances of :=>?

comment:19 Changed 3 years ago by Iceland_jack

Has there been any discussion about GHC generating instances of :=> and Class

-- Given
--   class Foo a => Bar a
-- GHC should generate
--   instance Class (Foo a) (Bar a) where 
--     cls :: Bar a :- Foo a
--     cls = Sub Dict
class Class b h | h -> b where
  cls :: h :- b

or Lifting

class Lifting p f where
  lifting :: p a :- p (f a)

class Lifting2 p f where
  lifting2 :: p a :- Lifting p (f a)
Last edited 3 years ago by Iceland_jack (previous) (diff)

comment:20 Changed 3 years ago by RyanGlScott

Iceland_jack, there are two problems with using typeclasses like these to "solve" this problem:

  1. They're based on explicit Dict values. As a result, using them requires lots of pattern matching and type variable scoping hullabaloo, which gets annoying pretty quickly.
  2. What does it mean to automatically generate instances for (:=>)? Do we only generate instances that correspond to actual instance contexts? If so, then the following would typecheck, since there is an instance () :=> Eq ():
ins :: () :- Eq ()

But the following would not typecheck!

ins :: Eq () :- Eq ()

Because there is no instance Eq () => Eq () anywhere (and thus no instance Eq () :=> Eq ()), only instance Eq (). But the implication Eq () => Eq () should obviously hold. Does that mean we should also generate an instance Eq () :=> Eq () automatically? But what about (Eq (), Ord ()) => Eq ()? (Eq (), Ord (), Show ()) => Eq ()? There is an extremely high number of contexts in which Eq () holds, and generating every possible one of them would result in a combinatorial explosion.

While those classes are neat tricks that can get you some of the functionality of QuantifiedConstraints/ImplicationConstraints, they don't go all the way. I really feel that some compiler smarts would make these features manageable.

comment:21 in reply to:  20 Changed 3 years ago by Iceland_jack

Replying to RyanGlScott:

  1. What does it mean to automatically generate instances for (:=>)?

That is the question isn't it, I imagined it as Typeable or Coercible where the compiler creates instances on the fly but which instances I do not know.

While those classes are neat tricks that can get you some of the functionality of QuantifiedConstraints/ImplicationConstraints, they don't go all the way.

QuantifiedConstraints and ImplicationConstraints would certainly be preferable! Are there any plans to research / implement such features? They would enable a lot of awesome code that is currently beyond reach.

comment:22 Changed 3 years ago by goldfire

I have no specific, concrete plans to work on implication constraints, but I have a few enterprising students who may be looking for a project next semester. Implementation implication constraints is on the shortlist of projects to consider.

comment:23 Changed 3 years ago by Iceland_jack

I want to mention an example from 1997: Type classes: an exploration of the design space

What we really want is universal quantification:

class (forall s. Monad (m s))
   => StateMonad m where
    get :: m s s
    set :: s -> m s ()

which can be defined as

class ForallF Monad m => StateMonad m where
  get :: m s s
  set :: s -> m s ()

How does it compare to MonadState.

comment:24 in reply to:  12 Changed 2 years ago by dfeuer

Replying to heisenbug:

Copying a use-case from #9196:

My point is that I'd like to have polymorphic (multiparameter) constraints, where the param universally abstracted over is a non-* kind, that is an ADT.

See:

class Foo a where ...
data Bar (b :: Bool) x = ...
instance Foo (Bar True x) where ...
instance Foo (Bar False x) where ...

test :: (forall b. Foo (Bar b x)) =>...

Here the forall condition is satisfiable, as all Bool alternatives are covered with instance declarations.

Actually, the forall condition is not satisfiable. The smaller problem is that stuck type families like Any can inhabit Bool without being 'True or 'False. The bigger problem is that Haskell's "logic" is inherently constructive. The claim that for any type b :: Bool there exists some instance Foo b x does not translate to a way to actually get the dictionary representing that instance. So I think your beautiful dream is, sadly, almost certainly unrealizable.

comment:25 Changed 2 years ago by baramoglo

Cc: baramoglo added

comment:26 Changed 2 years ago by simonpj

Description: modified (diff)

comment:27 Changed 2 years ago by simonpj

Keywords: QuantifiedContexts added; proposal removed

comment:28 Changed 20 months ago by simonpj

I've build an implementation of QuantifiedConstraints, held on wip/T2893. Here's the commit message

commit dbcf8d0b9076ae32b9138623eb84f67c18ed3dab
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Sat Jan 27 14:32:34 2018 +0000

    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/QuantifiedContexts
    
    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
    
      * TcSMonad.InertCans gets an extra field, inert_insts,
        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.)
    
      * 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
    
    Still to come
      - User manual documentation
      - A GHC Proposal

I'll try to get it up on Phabricator on Monday, unless someone would care to beat me to it.

Please give it a try!

comment:29 Changed 20 months ago by simonpj

Differential Rev(s): Phab:D4353

You can review the code at Phab:D4353

comment:30 Changed 20 months ago by simonpj

Keywords: QuantifiedConstraints added; QuantifiedContexts removed

comment:31 Changed 20 months ago by simonpj

Description: modified (diff)
Summary: Implement "Quantified contexts" proposalImplement "Quantified constraints" proposal

comment:32 Changed 20 months ago by simonpj

Description: modified (diff)

comment:33 Changed 19 months ago by RyanGlScott

comment:34 Changed 19 months ago by simonpj

I've added the superclass stuff

commit 910dfcfeadc4f132e887bc4adf5ac2e17a29d99b
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Thu Mar 1 23:32:29 2018 +0000

    Add superclasses to quantified constraints
    
    This patch adds suppport for superclasses to quantified constraints.
    For example (contrived):
    
      f :: (forall a. Ord a => Ord (m a)) => m a -> m a -> Bool
      f x y = x==y
    
    Here we need (Eq (m a)); but the quantifed constraint deals only
    with Ord.  But we can make it work by using its superclass.
    
    This behaviour finally delivers on the promise of comment:30 of
    Trac #9123: we can write an implication constraint that solves
    the problem of higher-kinded roles.  Test
    quantified-constraints/T8123 demonstrates this in action.

 compiler/basicTypes/Id.hs                        |   2 +-
 compiler/typecheck/Inst.hs                       |   4 +-
 compiler/typecheck/TcCanonical.hs                | 180 ++++++++++++++---------
 compiler/typecheck/TcErrors.hs                   |   4 +-
 compiler/typecheck/TcEvTerm.hs                   |   5 +-
 compiler/typecheck/TcEvidence.hs                 |  74 ++++++----
 compiler/typecheck/TcHsSyn.hs                    |  23 ++-
 compiler/typecheck/TcInstDcls.hs                 |   2 +-
 compiler/typecheck/TcInteract.hs                 |  61 ++++----
 compiler/typecheck/TcMType.hs                    |   6 +-
 compiler/typecheck/TcPatSyn.hs                   |   7 +-
 compiler/typecheck/TcPluginM.hs                  |   2 +-
 compiler/typecheck/TcRnTypes.hs                  |  62 ++++++--
 compiler/typecheck/TcSMonad.hs                   | 119 +++++++--------
 compiler/typecheck/TcSimplify.hs                 |   2 +-
 compiler/typecheck/TcType.hs                     |   2 +-
 compiler/types/Class.hs                          |  54 ++++---
 compiler/types/Kind.hs                           |   2 +
 testsuite/tests/quantified-constraints/T2893b.hs |  24 ---
 testsuite/tests/quantified-constraints/T2893c.hs |  15 ++
 testsuite/tests/quantified-constraints/T9123.hs  |  24 +++
 testsuite/tests/quantified-constraints/T9123a.hs |  26 ++++
 testsuite/tests/quantified-constraints/all.T     |   5 +
 23 files changed, 426 insertions(+), 279 deletions(-)

So now all the features I was planning are implemented.

Give it a whirl!

comment:35 Changed 19 months ago by AntC

... superclass stufff ... Give it a whirl!

Terrific. I'd appreciate if someone could test my hypothesis of a use case [1]. Note this using QuantifiedConstraints purely as implications with nothing forall'd.:

Consider modelling the logic for somewhat-injective type functions. Take type-level Boolean And [5].

And is not fully injective but:

  • If the result is True, the two arguments must be True.
  • If the result is False and one argument is True, the other must be False.
class ( (b3 ~ True) => (b1 ~ True, b2 ~ True),
       (b3 ~ False, b1 ~ True) => b2 ~ False,
       (b3 ~ False, b2 ~ True) => b1 ~ False ) 
          => And (b1 :: Bool) (b2 :: Bool) (b3 :: Bool)  | b1 b2 -> b3
             where {}

instance And True  b2 b2
instance And False b2 False

x3 = undefined :: (And b1 b2 True) => (b1, b2)
-- should infer x3's type as :: (True, True)

[1]

[5] continued

comment:36 Changed 19 months ago by Iceland_jack

f should have an Ord a constraint right?

f :: (Ord a, forall x. Ord x => Ord (m x)) => m a -> m a -> Bool

comment:37 in reply to:  36 Changed 19 months ago by simonpj

Replying to Iceland_jack:

f should have an Ord a constraint right?

You mean in the commit message? Yes, you're right.

(Before putting this on master I'll squash all the commits and write a new message.)

comment:38 Changed 16 months ago by simonpj

Differential Rev(s): Phab:D4353Phab:D4724

OK, finally I have a single squashed commit, rebased on master, ready to push to HEAD.

It's in Phab:D4724. Please review!

Simon

comment:39 Changed 16 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

comment:40 Changed 16 months ago by RyanGlScott

Keywords: GHCProposal added

comment:41 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: quantified-constraints/T2893{,a,c}
Note: See TracTickets for help on using tickets.