
Simon Peyton Jones authored
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 typeclass 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 ghcbootth:GHC.LanguageExtensions.Type.Extension * A new form of evidence, EvDFun, that is used to discharge such wanted constraints * checkValidType gets some changes to accept forallconstraints only in the right places. * Type.PredTree gets a new constructor ForAllPred, and and classifyPredType analyses a PredType to decompose the new forallconstraints * 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 forallconstraints. 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 forallconstraints 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 forallconstraint. See Note [Solving a Wanted forallconstraint] Note [Solving a Wanted forallconstraint] * We augment the kickout 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 postdesugaring, which fixed #14735, and is generally nicer anyway because we can use existing CoreSyn freevar functions. (Quantified constraints made the freevars of an evterm a bit more complicated.) * In LookupInstResult, replace GenInst with OneInst and NotSure, using the latter for multiple matches and/or one or more unifiers
7df58960