Quantified constraints

This wiki page summarises the state of play on the idea of allowing quantification in class constraints. For example

data Rose f a = Branch a (f (Rose f a))

instance (Eq a, forall b. (Eq b) => Eq (f b))
       => Eq (Rose f a)
  where ...

The new bit is the forall in the context of the instance declaration. This is allowed in GHC 8.6 and later using the QuantifiedConstraints extension.

Here are some resources

  • #2893, a ticket about the idea


Use Keyword = QuantifiedConstraints to ensure that a ticket ends up on these lists.

Open Tickets:

Add (->) representation and the Invariant class to GHC.Generics
Several Traversable instances have an extra fmap
Solve Coercible constraints over type constructors
QuantifiedConstraints: Odd superclass constraint
QuantifiedConstraints: Adding to the context causes failure
QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'
QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias
QuantifiedConstraints: GHC does doesn't discharge constraints if they are quantified
QuantifiedConstraints: Reify implication constraints from terms lacking them
Make (=>) polykinded (:: k -> k -> Constraint)
QuantifiedConstraints: Doesn't apply implication for existential?
QuantifiedConstraints: Can't be RHS of type family instances
Have custom type errors imply Void
QuantifiedConstraints: Incorrect pretty printing
QuantifiedConstraints: Implication constraints with type families don't work
QuantifiedConstraints ignore FunctionalDependencies
Quantified constraints half-work with equality constraints
QuantifiedConstraints: trouble with type family
Implication introduction for quantified constraints
Surprising failure combining QuantifiedConstraints with Coercible

Closed Tickets:

Incompleteness of type inference: must quantify over implication constraints
Implement "Quantified constraints" proposal
A type-level "implies" constraint on Constraints
Emit quantified Coercible constraints in GeneralizedNewtypeDeriving
Deriving Data at higher kinds
Allow ‘unsafe’ deriving strategy, deriving code with ‘unsafeCoerce’
Won't use (forall xx. f xx) with -XQuantifiedConstraints
QuantifiedConstraints conflated with impredicative polymorphism?
GHC Panic with QuantifiedConstraints
Non-exhaustive patterns in case in GHCi with quantified class contexts
Infer context for Data instance of (data Foo f = Foo (f Bool) (f Int))
QuantifiedConstraints: Problems with Typeable
-XQuantifiedConstraints: Turn term-level entailments (:-) into constraints (=>)
QuantifiedConstraints: GHC can't deduce (() :: Constraint)?
QuantifiedConstraints: Can't deduce "(a, b)" from "a" and "b"
QuantifiedConstraints: Can't define class alias
QuantifiedConstraints: Can't quantify constraint involving type family
QuantifiedConstraints: Can't use forall'd variable in context
QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'
Can't witness transitivity ((.)) of isomorphism of Constraints
QuantifiedConstraints don't kick in when used in TypeApplications
QuantifiedConstraints: Can't print type of quantified constraint
QuantifiedConstraints: GHC can't infer
QuantifiedConstraints: introducing classes through equality constraints fails
QuantifiedConstraints and principal types
Type synonyms with hidden, determined type variables
UndecidableInstances validity checking is wrong in the presence of QuantifiedConstraints
Ambiguity checks in QuantifiedConstraints
QuantifiedConstraints: panic "addTcEvBind NoEvBindsVar"
Regarding coherence and implication loops in presence of QuantifiedConstraints
(forall x. c x, forall x. d x) is not equivalent to forall x. (c x, d x)
Quantified constraints do not work with equality constraints
Deriving with QuantifiedConstraints is unable to penetrate type families
GHC panic, with QuantifiedConstraints
Implication constraint priority breaks default class implementations

Last modified 4 months ago Last modified on Jun 8, 2018 1:11:38 PM