[commit: ghc] wip/T2893: Implement QuantifiedConstraints (dbcf8d0)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/T2893
Link       : http://ghc.haskell.org/trac/ghc/changeset/dbcf8d0b9076ae32b9138623eb84f67c18ed3dab/ghc

>---------------------------------------------------------------

commit dbcf8d0b9076ae32b9138623eb84f67c18ed3dab
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Sat Jan 27 14:32:34 2018 +0000

    Implement QuantifiedConstraints
    
    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/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
     [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
    
      * 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


>---------------------------------------------------------------

dbcf8d0b9076ae32b9138623eb84f67c18ed3dab
 compiler/deSugar/DsBinds.hs                        |   7 +
 compiler/main/DynFlags.hs                          |   2 +
 compiler/typecheck/TcCanonical.hs                  | 166 ++++++++++++++++++---
 compiler/typecheck/TcEvidence.hs                   |  27 +++-
 compiler/typecheck/TcHsSyn.hs                      |  16 +-
 compiler/typecheck/TcInteract.hs                   |   4 +
 compiler/typecheck/TcMType.hs                      |   5 +-
 compiler/typecheck/TcRnTypes.hs                    |   5 +
 compiler/typecheck/TcSMonad.hs                     | 162 ++++++++++++++++----
 compiler/typecheck/TcValidity.hs                   |  23 ++-
 compiler/types/InstEnv.hs                          |  75 +++++++---
 compiler/types/Type.hs                             |  27 +++-
 .../ghc-boot-th/GHC/LanguageExtensions/Type.hs     |   1 +
 testsuite/tests/typecheck/should_compile/T2893.hs  |  18 +++
 testsuite/tests/typecheck/should_compile/T2893a.hs |  27 ++++
 testsuite/tests/typecheck/should_compile/all.T     |   2 +
 16 files changed, 470 insertions(+), 97 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc dbcf8d0b9076ae32b9138623eb84f67c18ed3dab