Implement QuantifiedConstraints

Authored by bgamari on May 23 2018, 11:24 AM.


Trac Issues

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

#9123 (especially!  higher kinded roles)

The wiki page is

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

  • (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 Trac #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
Test Plan


Diff Detail

rGHC Glasgow Haskell Compiler
Lint WarningsExcuse: It's okay
Warningcompiler/deSugar/DsBinds.hs:1170TXT3Line Too Long
Warningcompiler/typecheck/TcCanonical.hs:104TXT3Line Too Long
Warningcompiler/typecheck/TcCanonical.hs:542TXT3Line Too Long
Warningcompiler/typecheck/TcCanonical.hs:545TXT3Line Too Long
Warningcompiler/typecheck/TcCanonical.hs:940TXT3Line Too Long
Warningcompiler/typecheck/TcCanonical.hs:941TXT3Line Too Long
Warningcompiler/typecheck/TcEvidence.hs:774TXT3Line Too Long
Warningcompiler/typecheck/TcEvidence.hs:904TXT3Line Too Long
Warningcompiler/typecheck/TcEvidence.hs:905TXT3Line Too Long
Warningcompiler/typecheck/TcInteract.hs:1817TXT3Line Too Long
Warningcompiler/typecheck/TcInteract.hs:2630TXT3Line Too Long
Warningcompiler/typecheck/TcInteract.hs:2634TXT3Line Too Long
Warningcompiler/typecheck/TcValidity.hs:445TXT3Line Too Long
Warningcompiler/typecheck/TcValidity.hs:1411TXT3Line Too Long
Warningcompiler/typecheck/TcValidity.hs:1420TXT3Line Too Long
Warningcompiler/types/Class.hs:20TXT3Line Too Long
Warningcompiler/types/Class.hs:242TXT3Line Too Long
Warningcompiler/types/Class.hs:248TXT3Line Too Long
Warningcompiler/types/Class.hs:256TXT3Line Too Long
Warningtestsuite/tests/quantified-constraints/T9123.hs:20TXT3Line Too Long
No Unit Test Coverage
Build Status
Buildable 20820
Build 46186: [GHC] Linux/amd64: Continuous Integration
Build 46185: [GHC] OSX/amd64: Continuous Integration
Build 46184: [GHC] Windows/amd64: Continuous Integration
Build 46183: arc lint + arc unit
bgamari created this revision.May 23 2018, 11:24 AM
bgamari updated this revision to Diff 16512.May 23 2018, 11:37 AM

Fix wibbles

I'm pretty unfamiliar with the type checker sub system, but i think i spotted 1-2 possible typos/spurious edits/places that might need additional clarity

overall from a 1000 mile perspective looks lovely


is it clear from context why the theta and tvs (type variables?) arguments are empty here?

(i'm largely unfamiliar with ghc's type checking code base so this may be a naive ask)


why's there a spurious newline change here?


might be helpful to explain what these example type expressions are about


meta question: do we have a way to make sure we have stable / permanent links to all these resource?


possibly fuzzy question: how does / might decidable superclasses interact with this extension?

int-index added inline comments.

There's a typo here, s/Perhpas/Perhaps/.

simonpj added a subscriber: simonpj.Jun 1 2018, 9:55 AM

Thanks for comments. I have made minor changes -- to comments, plus fixing the spelling error in the error message, and pushed to the wip/ branch.

I think we are done!

Ben: could you squash the minor patch into the big patch, rebase, validate, and commit to HEAD? Thanks!



Those two args are used only for quantified constraints. I'll add a coment