Skip to content
  • Simon Peyton Jones's avatar
    Implement QuantifiedConstraints · 7df58960
    Simon Peyton Jones authored
    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
    7df58960