[GHC] #5927: A type-level "implies" constraint on Constraints

[GHC]

#5927: A type-level "implies" constraint on Constraints
-------------------------------------+-------------------------------------
        Reporter:  illissius         |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.4.1
  checker)                           |             Keywords:
      Resolution:  duplicate         |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #2893             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Ben Gamari <ben@…>):

 In [changeset:"7df589608abb178efd6499ee705ba4eebd0cf0d1/ghc" 7df5896/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="7df589608abb178efd6499ee705ba4eebd0cf0d1"
 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/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
  [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

   * 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
   #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
 }}}

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