• 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
      #9123 (especially!  higher kinded roles)
    The wiki page is
    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
      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
TcInstDcls.hs 79.4 KB