Implement QuantifiedConstraints
AbandonedPublic

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

Details

Reviewers
goldfire
Trac Issues
#2893
Summary

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

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

Validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Lint WarningsExcuse: It's okay
SeverityLocationCodeMessage
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
Unit
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

compiler/typecheck/TcCanonical.hs
152

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)

compiler/typecheck/TcInteract.hs
2044

why's there a spurious newline change here?

compiler/typecheck/TcValidity.hs
2005

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

docs/users_guide/glasgow_exts.rst
9657

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

9670

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

int-index added inline comments.
compiler/typecheck/TcValidity.hs
445

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!

Simon

compiler/typecheck/TcCanonical.hs
152

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