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.

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:

Incompleteness of type inference: must quantify over implication constraints
Implement "Quantified constraints" proposal
Add (->) representation and the Invariant class to GHC.Generics
Need for higher kinded roles
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 don't kick in when used in TypeApplications
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

Closed Tickets:

A type-level "implies" constraint on Constraints
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: 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

Last modified 3 months ago Last modified on Feb 23, 2018 8:48:26 AM