|
|
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 #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/QuantifiedConstraints
which in turn contains a link to the GHC Proposal where the change
is specified.
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
[W] (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
* Define a type TcRnTypes.QCInst, which holds a given
quantified constraint in the inert set
* TcSMonad.InertCans gets an extra field, inert_insts :: [QCInst],
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.)
* topReactionsStage calls doTopReactOther for CIrredCan and
CTyEqCan, so they can try to react with any given
quantified constraints (TcInteract.matchLocalInst)
* 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
Some other related refactoring
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* Move SCC on evidence bindings to post-desugaring, which fixed
#14735, and is generally nicer anyway because we can use
existing CoreSyn free-var functions. (Quantified constraints
made the free-vars of an ev-term a bit more complicated.)
* In LookupInstResult, replace GenInst with OneInst and NotSure,
using the latter for multiple matches and/or one or more
unifiers
|
