wiki:QuantifiedConstraints

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

Status

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

Open Tickets:

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

Closed Tickets:

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

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