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 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

- (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

This is Simon's patch, part of his `wip/T2893` branch.