# 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

- Derivable type classes, Section 7, where the idea was first proposed (I think).

- #2893, a ticket about the idea

- Quantified class constraints, a Haskell 2017 paper that works out the idea in some detail, and a Reddit thread about it.

## 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
- #14860
- QuantifiedConstraints: Can't quantify constraint involving type family
- #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
- #15639
- Surprising failure combining QuantifiedConstraints with Coercible
- #15888
- Quantified constraints can be loopy
- #16139
- GHC confused about type synonym kind with QuantifiedConstraints
- #16140
- Cannot create type synonym for quantified constraint without ImpredicativeTypes
- #16173
- Move `Data.Profunctor` from `profunctors` package to `base`
- #16245
- GHC panic (No skolem info) with QuantifiedConstraints and strange scoping
- #16365
- Inconsistency in quantified constraint solving

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
- #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
- #15593
- QuantifiedConstraints: trouble with type family
- #15625
- GHC panic, with QuantifiedConstraints
- #15635
- Implication introduction for quantified constraints
- #15636
- Implication constraint priority breaks default class implementations
- #15943
- "ASSERT failed" with quantified constraints
- #15974
- QuantifiedConstraints: Spurious error involving superclass constraints
- #16123
- QuantifiedConstraints fails to deduce trivial constraint

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