Commit 7df58960 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

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
parent 36091ec9
......@@ -221,7 +221,7 @@ setIdInfo :: Id -> IdInfo -> Id
setIdInfo id info = info `seq` (lazySetIdInfo id info)
-- Try to avoid spack leaks by seq'ing
modifyIdInfo :: (IdInfo -> IdInfo) -> Id -> Id
modifyIdInfo :: HasDebugCallStack => (IdInfo -> IdInfo) -> Id -> Id
modifyIdInfo fn id = setIdInfo id (fn (idInfo id))
-- maybeModifyIdInfo tries to avoid unnecessary thrashing
......
......@@ -53,7 +53,7 @@ import Name
import VarSet
import Rules
import VarEnv
import Var( EvVar )
import Var( EvVar, varType )
import Outputable
import Module
import SrcLoc
......@@ -64,6 +64,7 @@ import BasicTypes
import DynFlags
import FastString
import Util
import UniqSet( nonDetEltsUniqSet )
import MonadUtils
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
......@@ -1144,15 +1145,39 @@ dsTcEvBinds (TcEvBinds {}) = panic "dsEvBinds" -- Zonker has got rid of this
dsTcEvBinds (EvBinds bs) = dsEvBinds bs
dsEvBinds :: Bag EvBind -> DsM [CoreBind]
dsEvBinds bs = mapM ds_scc (sccEvBinds bs)
dsEvBinds bs
= do { ds_bs <- mapBagM dsEvBind bs
; return (mk_ev_binds ds_bs) }
mk_ev_binds :: Bag (Id,CoreExpr) -> [CoreBind]
-- We do SCC analysis of the evidence bindings, /after/ desugaring
-- them. This is convenient: it means we can use the CoreSyn
-- free-variable functions rather than having to do accurate free vars
-- for EvTerm.
mk_ev_binds ds_binds
= map ds_scc (stronglyConnCompFromEdgedVerticesUniq edges)
where
ds_scc (AcyclicSCC (EvBind { eb_lhs = v, eb_rhs = r}))
= liftM (NonRec v) (dsEvTerm r)
ds_scc (CyclicSCC bs) = liftM Rec (mapM dsEvBind bs)
edges :: [ Node EvVar (EvVar,CoreExpr) ]
edges = foldrBag ((:) . mk_node) [] ds_binds
mk_node :: (Id, CoreExpr) -> Node EvVar (EvVar,CoreExpr)
mk_node b@(var, rhs)
= DigraphNode { node_payload = b
, node_key = var
, node_dependencies = nonDetEltsUniqSet $
exprFreeVars rhs `unionVarSet`
coVarsOfType (varType var) }
-- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
-- is still deterministic even if the edges are in nondeterministic order
-- as explained in Note [Deterministic SCC] in Digraph.
ds_scc (AcyclicSCC (v,r)) = NonRec v r
ds_scc (CyclicSCC prs) = Rec prs
dsEvBind :: EvBind -> DsM (Id, CoreExpr)
dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r)
{-**********************************************************************
* *
Desugaring EvTerms
......@@ -1162,6 +1187,13 @@ dsEvBind (EvBind { eb_lhs = v, eb_rhs = r}) = liftM ((,) v) (dsEvTerm r)
dsEvTerm :: EvTerm -> DsM CoreExpr
dsEvTerm (EvExpr e) = return e
dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev
dsEvTerm (EvFun { et_tvs = tvs, et_given = given
, et_binds = ev_binds, et_body = wanted_id })
= do { ds_ev_binds <- dsTcEvBinds ev_binds
; return $ (mkLams (tvs ++ given) $
mkCoreLets ds_ev_binds $
Var wanted_id) }
{-**********************************************************************
* *
......
......@@ -4186,6 +4186,7 @@ xFlagsDeps = [
flagSpec "PatternSynonyms" LangExt.PatternSynonyms,
flagSpec "PolyKinds" LangExt.PolyKinds,
flagSpec "PolymorphicComponents" LangExt.RankNTypes,
flagSpec "QuantifiedConstraints" LangExt.QuantifiedConstraints,
flagSpec "PostfixOperators" LangExt.PostfixOperators,
flagSpec "QuasiQuotes" LangExt.QuasiQuotes,
flagSpec "Rank2Types" LangExt.RankNTypes,
......@@ -4309,6 +4310,7 @@ impliedXFlags :: [(LangExt.Extension, TurnOnFlag, LangExt.Extension)]
impliedXFlags
-- See Note [Updating flag description in the User's Guide]
= [ (LangExt.RankNTypes, turnOn, LangExt.ExplicitForAll)
, (LangExt.QuantifiedConstraints, turnOn, LangExt.ExplicitForAll)
, (LangExt.ScopedTypeVariables, turnOn, LangExt.ExplicitForAll)
, (LangExt.LiberalTypeSynonyms, turnOn, LangExt.ExplicitForAll)
, (LangExt.ExistentialQuantification, turnOn, LangExt.ExplicitForAll)
......
......@@ -2011,6 +2011,7 @@ mkCallUDs' env f args
EqPred {} -> True
IrredPred {} -> True -- Things like (D []) where D is a
-- Constraint-ranged family; Trac #7785
ForAllPred {} -> True
{-
Note [Type determines value]
......
......@@ -55,6 +55,7 @@ import TcType
import HscTypes
import Class( Class )
import MkId( mkDictFunId )
import CoreSyn( Expr(..) ) -- For the Coercion constructor
import Id
import Name
import Var ( EvVar, mkTyVar, tyVarName, TyVarBndr(..) )
......@@ -352,6 +353,7 @@ instCallConstraints orig preds
; traceTc "instCallConstraints" (ppr evs)
; return (mkWpEvApps evs) }
where
go :: TcPredType -> TcM EvTerm
go pred
| Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
= do { co <- unifyType Nothing ty1 ty2
......@@ -361,7 +363,7 @@ instCallConstraints orig preds
| Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
, tc `hasKey` heqTyConKey
= do { co <- unifyType Nothing ty1 ty2
; return (evDFunApp (dataConWrapId heqDataCon) args [evCoercion co]) }
; return (evDFunApp (dataConWrapId heqDataCon) args [Coercion co]) }
| otherwise
= emitWanted orig pred
......@@ -371,10 +373,14 @@ instDFunType :: DFunId -> [DFunInstType]
, TcThetaType ) -- instantiated constraint
-- See Note [DFunInstType: instantiating types] in InstEnv
instDFunType dfun_id dfun_inst_tys
= do { (subst, inst_tys) <- go emptyTCvSubst dfun_tvs dfun_inst_tys
= do { (subst, inst_tys) <- go empty_subst dfun_tvs dfun_inst_tys
; return (inst_tys, substTheta subst dfun_theta) }
where
(dfun_tvs, dfun_theta, _) = tcSplitSigmaTy (idType dfun_id)
dfun_ty = idType dfun_id
(dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
-- With quantified constraints, the
-- type of a dfun may not be closed
go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
go subst [] [] = return (subst, [])
......
......@@ -24,10 +24,13 @@ import Class
import TyCon
import TyCoRep -- cleverly decomposes types, good for completeness checking
import Coercion
import CoreSyn
import Id( idType, mkTemplateLocals )
import FamInstEnv ( FamInstEnvs )
import FamInst ( tcTopNormaliseNewTypeTF_maybe )
import Var
import VarEnv( mkInScopeSet )
import VarSet( delVarSetList )
import Outputable
import DynFlags( DynFlags )
import NameSet
......@@ -81,15 +84,31 @@ last time through, so we can skip the classification step.
canonicalize :: Ct -> TcS (StopOrContinue Ct)
canonicalize (CNonCanonical { cc_ev = ev })
= {-# SCC "canNC" #-}
case classifyPredType (ctEvPred ev) of
case classifyPredType pred of
ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
canClassNC ev cls tys
EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
canEqNC ev eq_rel ty1 ty2
IrredPred {} -> do traceTcS "canEvNC:irred" (ppr (ctEvPred ev))
IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
canIrred ev
ForAllPred _ _ pred -> do traceTcS "canEvNC:forall" (ppr pred)
canForAll ev (isClassPred pred)
where
pred = ctEvPred ev
canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
= canForAll ev pend_sc
canonicalize (CIrredCan { cc_ev = ev })
| EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
= -- For insolubles (all of which are equalities, do /not/ flatten the arguments
-- In Trac #14350 doing so led entire-unnecessary and ridiculously large
-- type function expansion. Instead, canEqNC just applies
-- the substitution to the predicate, and may do decomposition;
-- e.g. a ~ [a], where [G] a ~ [Int], can decompose
canEqNC ev eq_rel ty1 ty2
| otherwise
= canIrred ev
canonicalize (CDictCan { cc_ev = ev, cc_class = cls
......@@ -130,7 +149,7 @@ canClassNC :: CtEvidence -> Class -> [Type] -> TcS (StopOrContinue Ct)
-- Precondition: EvVar is class evidence
canClassNC ev cls tys
| isGiven ev -- See Note [Eagerly expand given superclasses]
= do { sc_cts <- mkStrictSuperClasses ev cls tys
= do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
; emitWork sc_cts
; canClass ev cls tys False }
......@@ -174,7 +193,7 @@ solveCallStack ev ev_cs = do
-- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
cs_tm <- evCallStack ev_cs
let ev_tm = mkEvCast cs_tm (wrapIP (ctEvPred ev))
setWantedEvBind (ctEvEvId ev) (EvExpr ev_tm)
setEvBindIfWanted ev ev_tm
canClass :: CtEvidence
-> Class -> [Type]
......@@ -424,67 +443,52 @@ makeSuperClasses :: [Ct] -> TcS [Ct]
makeSuperClasses cts = concatMapM go cts
where
go (CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
= mkStrictSuperClasses ev cls tys
= mkStrictSuperClasses ev [] [] cls tys
go (CQuantCan (QCI { qci_pred = pred, qci_ev = ev }))
= ASSERT2( isClassPred pred, ppr pred ) -- The cts should all have
-- class pred heads
mkStrictSuperClasses ev tvs theta cls tys
where
(tvs, theta, cls, tys) = tcSplitDFunTy (ctEvPred ev)
go ct = pprPanic "makeSuperClasses" (ppr ct)
mkStrictSuperClasses :: CtEvidence -> Class -> [Type] -> TcS [Ct]
-- Return constraints for the strict superclasses of (c tys)
mkStrictSuperClasses ev cls tys
= mk_strict_superclasses (unitNameSet (className cls)) ev cls tys
mk_superclasses :: NameSet -> CtEvidence -> TcS [Ct]
-- Return this constraint, plus its superclasses, if any
mk_superclasses rec_clss ev
| ClassPred cls tys <- classifyPredType (ctEvPred ev)
= mk_superclasses_of rec_clss ev cls tys
| otherwise -- Superclass is not a class predicate
= return [mkNonCanonical ev]
mk_superclasses_of :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
-- Always return this class constraint,
-- and expand its superclasses
mk_superclasses_of rec_clss ev cls tys
| loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
; return [this_ct] } -- cc_pend_sc of this_ct = True
| otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
, ppr (isCTupleClass cls)
, ppr rec_clss
])
; sc_cts <- mk_strict_superclasses rec_clss' ev cls tys
; return (this_ct : sc_cts) }
-- cc_pend_sc of this_ct = False
where
cls_nm = className cls
loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
-- Tuples never contribute to recursion, and can be nested
rec_clss' = rec_clss `extendNameSet` cls_nm
this_ct = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
, cc_pend_sc = loop_found }
-- NB: If there is a loop, we cut off, so we have not
-- added the superclasses, hence cc_pend_sc = True
mk_strict_superclasses :: NameSet -> CtEvidence -> Class -> [Type] -> TcS [Ct]
mkStrictSuperClasses
:: CtEvidence
-> [TyVar] -> ThetaType -- These two args are non-empty only when taking
-- superclasses of a /quantified/ constraint
-> Class -> [Type] -> TcS [Ct]
-- Return constraints for the strict superclasses of
-- ev :: forall as. theta => cls tys
mkStrictSuperClasses ev tvs theta cls tys
= mk_strict_superclasses (unitNameSet (className cls))
ev tvs theta cls tys
mk_strict_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType
-> Class -> [Type] -> TcS [Ct]
-- Always return the immediate superclasses of (cls tys);
-- and expand their superclasses, provided none of them are in rec_clss
-- nor are repeated
mk_strict_superclasses rec_clss ev cls tys
mk_strict_superclasses rec_clss ev tvs theta cls tys
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
= do { sc_evs <- newGivenEvVars (mk_given_loc loc)
(mkEvScSelectors (evId evar) cls tys)
; concatMapM (mk_superclasses rec_clss) sc_evs }
= concatMapM (do_one_given evar (mk_given_loc loc)) $
classSCSelIds cls
where
dict_ids = mkTemplateLocals theta
size = sizeTypes tys
| all noFreeVarsOfType tys
= return [] -- Wanteds with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds]
do_one_given evar given_loc sel_id
= do { let sc_pred = funResultTy (piResultTys (idType sel_id) tys)
given_ty = mkInfSigmaTy tvs theta sc_pred
; given_ev <- newGivenEvVar given_loc $
(given_ty, mk_sc_sel evar sel_id)
; mk_superclasses rec_clss given_ev tvs theta sc_pred }
mk_sc_sel evar sel_id
= EvExpr $ mkLams tvs $ mkLams dict_ids $
Var sel_id `mkTyApps` tys `App`
(evId evar `mkTyApps` mkTyVarTys tvs `mkVarApps` dict_ids)
| otherwise -- Wanted/Derived case, just add Derived superclasses
-- that can lead to improvement.
= do { let loc = ctEvLoc ev
; sc_evs <- mapM (newDerivedNC loc) (immSuperClasses cls tys)
; concatMapM (mk_superclasses rec_clss) sc_evs }
where
size = sizeTypes tys
mk_given_loc loc
| isCTupleClass cls
= loc -- For tuple predicates, just take them apart, without
......@@ -503,6 +507,63 @@ mk_strict_superclasses rec_clss ev cls tys
| otherwise -- Probably doesn't happen, since this function
= loc -- is only used for Givens, but does no harm
mk_strict_superclasses rec_clss ev tvs theta cls tys
| all noFreeVarsOfType tys
= return [] -- Wanteds with no variables yield no deriveds.
-- See Note [Improvement from Ground Wanteds]
| otherwise -- Wanted/Derived case, just add Derived superclasses
-- that can lead to improvement.
= ASSERT2( null tvs && null theta, ppr tvs $$ ppr theta )
concatMapM do_one_derived (immSuperClasses cls tys)
where
loc = ctEvLoc ev
do_one_derived sc_pred
= do { sc_ev <- newDerivedNC loc sc_pred
; mk_superclasses rec_clss sc_ev [] [] sc_pred }
mk_superclasses :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> PredType -> TcS [Ct]
-- Return this constraint, plus its superclasses, if any
mk_superclasses rec_clss ev tvs theta pred
| ClassPred cls tys <- classifyPredType pred
= mk_superclasses_of rec_clss ev tvs theta cls tys
| otherwise -- Superclass is not a class predicate
= return [mkNonCanonical ev]
mk_superclasses_of :: NameSet -> CtEvidence
-> [TyVar] -> ThetaType -> Class -> [Type]
-> TcS [Ct]
-- Always return this class constraint,
-- and expand its superclasses
mk_superclasses_of rec_clss ev tvs theta cls tys
| loop_found = do { traceTcS "mk_superclasses_of: loop" (ppr cls <+> ppr tys)
; return [this_ct] } -- cc_pend_sc of this_ct = True
| otherwise = do { traceTcS "mk_superclasses_of" (vcat [ ppr cls <+> ppr tys
, ppr (isCTupleClass cls)
, ppr rec_clss
])
; sc_cts <- mk_strict_superclasses rec_clss' ev tvs theta cls tys
; return (this_ct : sc_cts) }
-- cc_pend_sc of this_ct = False
where
cls_nm = className cls
loop_found = not (isCTupleClass cls) && cls_nm `elemNameSet` rec_clss
-- Tuples never contribute to recursion, and can be nested
rec_clss' = rec_clss `extendNameSet` cls_nm
this_ct | null tvs, null theta
= CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
, cc_pend_sc = loop_found }
-- NB: If there is a loop, we cut off, so we have not
-- added the superclasses, hence cc_pend_sc = True
| otherwise
= CQuantCan (QCI { qci_tvs = tvs, qci_pred = mkClassPred cls tys
, qci_ev = ev
, qci_pend_sc = loop_found })
{-
************************************************************************
......@@ -515,16 +576,8 @@ mk_strict_superclasses rec_clss ev cls tys
canIrred :: CtEvidence -> TcS (StopOrContinue Ct)
-- Precondition: ty not a tuple and no other evidence form
canIrred ev
| EqPred eq_rel ty1 ty2 <- classifyPredType pred
= -- For insolubles (all of which are equalities, do /not/ flatten the arguments
-- In Trac #14350 doing so led entire-unnecessary and ridiculously large
-- type function expansion. Instead, canEqNC just applies
-- the substitution to the predicate, and may do decomposition;
-- e.g. a ~ [a], where [G] a ~ [Int], can decompose
canEqNC ev eq_rel ty1 ty2
| otherwise
= do { traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
= do { let pred = ctEvPred ev
; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred)
; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { -- Re-classify, in case flattening has improved its shape
......@@ -533,19 +586,172 @@ canIrred ev
EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2
_ -> continueWith $
mkIrredCt new_ev } }
where
pred = ctEvPred ev
canHole :: CtEvidence -> Hole -> TcS (StopOrContinue Ct)
canHole ev hole
= do { let ty = ctEvPred ev
; (xi,co) <- flatten FM_SubstOnly ev ty -- co :: xi ~ ty
= do { let pred = ctEvPred ev
; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
, cc_hole = hole }))
; stopWith new_ev "Emit insoluble hole" } }
{-
{- *********************************************************************
* *
* Quantified predicates
* *
********************************************************************* -}
{- 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.
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, and a Haskell Symposium paper about it.
We implement two main extensions to the design in the paper:
1. We allow a variable in the instance head, e.g.
f :: forall m a. (forall b. m b) => D (m a)
Notice the 'm' in the head of the quantified constraint, not
a class.
2. We suport superclasses to quantified constraints.
For example (contrived):
f :: (Ord b, forall b. Ord b => Ord (m b)) => m a -> m a -> Bool
f x y = x==y
Here we need (Eq (m a)); but the quantifed constraint deals only
with Ord. But we can make it work by using its superclass.
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
Note that a quantified constraint is never /inferred/
(by TcSimplify.simplifyInfer). A function can only have a
quantified constraint in its type if it is given an explicit
type signature.
Note that we implement
-}
canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct)
-- We have a constraint (forall as. blah => C tys)
canForAll ev pend_sc
= do { -- First rewrite it to apply the current substitution
-- Do not bother with type-family reductions; we can't
-- do them under a forall anyway (c.f. Flatten.flatten_one
-- on a forall type)
let pred = ctEvPred ev
; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
do { -- Now decompose into its pieces and solve it
-- (It takes a lot less code to flatten before decomposing.)
; case classifyPredType (ctEvPred new_ev) of
ForAllPred tv_bndrs theta pred
-> solveForAll new_ev tv_bndrs theta pred pend_sc
_ -> pprPanic "canForAll" (ppr new_ev)
} }
solveForAll :: CtEvidence -> [TyVarBinder] -> TcThetaType -> PredType -> Bool
-> TcS (StopOrContinue Ct)
solveForAll ev tv_bndrs theta pred pend_sc
| CtWanted { ctev_dest = dest } <- ev
= -- See Note [Solving a Wanted forall-constraint]
do { let skol_info = QuantCtxtSkol
empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs
; given_ev_vars <- mapM newEvVar (substTheta subst theta)
; (w_id, ev_binds)
<- checkConstraintsTcS skol_info skol_tvs given_ev_vars $
do { wanted_ev <- newWantedEvVarNC loc $
substTy subst pred
; return ( ctEvEvId wanted_ev
, unitBag (mkNonCanonical wanted_ev)) }
; setWantedEvTerm dest $
EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
, et_binds = ev_binds, et_body = w_id }
; stopWith ev "Wanted forall-constraint" }
| isGiven ev -- See Note [Solving a Given forall-constraint]
= do { addInertForAll qci
; stopWith ev "Given forall-constraint" }
| otherwise
= stopWith ev "Derived forall-constraint"
where
loc = ctEvLoc ev
tvs = binderVars tv_bndrs
qci = QCI { qci_ev = ev, qci_tvs = tvs
, qci_pred = pred, qci_pend_sc = pend_sc }
{- Note [Solving a Wanted forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Solving a wanted forall (quantified) constraint
[W] df :: forall ab. (Eq a, Ord b) => C x a b
is delightfully easy. Just build an implication constraint
forall ab. (g1::Eq a, g2::Ord b) => [W] d :: C x a
and discharge df thus:
df = /\ab. \g1 g2. let <binds> in d
where <binds> is filled in by solving the implication constraint.
All the machinery is to hand; there is little to do.
Note [Solving a Given forall-constraint]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For a Given constraint
[G] df :: forall ab. (Eq a, Ord b) => C x a b
we just add it to TcS's local InstEnv of known instances,
via addInertForall. Then, if we look up (C x Int Bool), say,
we'll find a match in the InstEnv.
************************************************************************
* *
* Equalities
......@@ -630,11 +836,14 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
= canEqReflexive ev ReprEq ty1
-- When working with ReprEq, unwrap newtypes.
can_eq_nc' _flat rdr_env envs ev ReprEq ty1 _ ty2 ps_ty2
| Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
-- See Note [Unwrap newtypes first]
can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2