[GHC] #2893: Implement "Quantified contexts" proposal

[GHC]

#2893: Implement "Quantified contexts" proposal
-------------------------------------+-------------------------------------
        Reporter:  porges            |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  ⊥
       Component:  Compiler          |              Version:  6.10.1
      Resolution:                    |             Keywords:
                                     |  QuantifiedContexts
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I've build an implementation of `QuantifiedConstraints`, held on
 `wip/T2893`.  Here's the commit message
 {{{
 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
 }}}
 I'll try to get it up on Phabricator on Monday, unless someone would care
 to beat me to it.

 Please give it a try!

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/2893#comment:28>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler