diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs
index bf48bad7b9f62b7dca4c8e4f7731a6ad496b0f6c..e38769a14fcab09e2bba9a6b9c97acf0ee2904ba 100644
--- a/compiler/basicTypes/Id.hs
+++ b/compiler/basicTypes/Id.hs
@@ -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
diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs
index 4684d436a466e6313a3530e8a975ffe883144815..ba904c1122fdb5e593c0f73a0d6d372b948f026d 100644
--- a/compiler/deSugar/DsBinds.hs
+++ b/compiler/deSugar/DsBinds.hs
@@ -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) }
+
{-**********************************************************************
* *
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index b2c82fa2ee1423f074e92123d5fdb6972d8e9082..306a15a15b35e8ccade0a03702ab7b42e2abd508 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -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)
diff --git a/compiler/specialise/Specialise.hs b/compiler/specialise/Specialise.hs
index c4fe042b1fb8f55e2ed032e8b491fadcc270f770..bc3e27f6748262502fc2af1d4034f385c036c7ed 100644
--- a/compiler/specialise/Specialise.hs
+++ b/compiler/specialise/Specialise.hs
@@ -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]
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 7b27dfa3b45564a6a4f7113f99e12128db8dadf2..bcd511b982fa93dc97feaacba6acd69b614af313 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -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, [])
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index d540272a5356b3dcd689c25ed727d8d5bcdbc466..b0ff962e5c719a40f6ca67ddd044ff756afd6a7b 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -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
+ | ReprEq <- eq_rel
+ , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
= can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
-can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
- | Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
+
+ | ReprEq <- eq_rel
+ , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
= can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
-- Then, get rid of casts
@@ -657,7 +866,7 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
-- Literals
can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
| l1 == l2
- = do { setEqIfWanted ev (mkReflCo (eqRelRole eq_rel) ty1)
+ = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
-- Try to decompose type constructor applications
@@ -727,27 +936,28 @@ can_eq_nc_forall ev eq_rel s1 s2
phi1' = substTy subst1 phi1
-- Unify the kinds, extend the substitution
+ go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
+ -> TcS (TcCoercion, Cts)
go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
= do { let tv2 = binderVar bndr2
- ; kind_co <- unifyWanted loc Nominal
- (tyVarKind skol_tv)
- (substTy subst (tyVarKind tv2))
+ ; (kind_co, wanteds1) <- unify loc Nominal (tyVarKind skol_tv)
+ (substTy subst (tyVarKind tv2))
; let subst' = extendTvSubst subst tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
- ; co <- go skol_tvs subst' bndrs2
- ; return (mkForAllCo skol_tv kind_co co) }
+ ; (co, wanteds2) <- go skol_tvs subst' bndrs2
+ ; return ( mkTcForAllCo skol_tv kind_co co
+ , wanteds1 `unionBags` wanteds2 ) }
-- Done: unify phi1 ~ phi2
go [] subst bndrs2
= ASSERT( null bndrs2 )
- unifyWanted loc (eqRelRole eq_rel)
- phi1' (substTy subst phi2)
+ unify loc (eqRelRole eq_rel) phi1' (substTy subst phi2)
go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
- ; all_co <- checkConstraintsTcS skol_info skol_tvs $
+ ; all_co <- checkTvConstraintsTcS skol_info skol_tvs $
go skol_tvs empty_subst2 bndrs2
; setWantedEq orig_dest all_co
@@ -758,6 +968,17 @@ can_eq_nc_forall ev eq_rel s1 s2
pprEq s1 s2 -- See Note [Do not decompose given polytype equalities]
; stopWith ev "Discard given polytype equality" }
+ where
+ unify :: CtLoc -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
+ -- This version returns the wanted constraint rather
+ -- than putting it in the work list
+ unify loc role ty1 ty2
+ | ty1 `tcEqType` ty2
+ = return (mkTcReflCo role ty1, emptyBag)
+ | otherwise
+ = do { (wanted, co) <- newWantedEq loc role ty1 ty2
+ ; return (co, unitBag (mkNonCanonical wanted)) }
+
---------------------------------
-- | Compare types for equality, while zonking as necessary. Gives up
-- as soon as it finds that two types are not equal.
@@ -895,7 +1116,26 @@ zonk_eq_types = go
combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
combine_rev f (Right tys) (Right ty) = Right (f ty tys)
-{-
+{- See Note [Unwrap newtypes first]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ newtype N m a = MkN (m a)
+Then N will get a conservative, Nominal role for its second paramter 'a',
+because it appears as an argument to the unknown 'm'. Now consider
+ [W] N Maybe a ~R# N Maybe b
+
+If we decompose, we'll get
+ [W] a ~N# b
+
+But if instead we unwrap we'll get
+ [W] Maybe a ~R# Maybe b
+which in turn gives us
+ [W] a ~R# b
+which is easier to satisfy.
+
+Bottom line: unwrap newtypes before decomposing them!
+c.f. Trac #9123 comment:52,53 for a compelling example.
+
Note [Newtypes can blow the stack]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
@@ -1962,8 +2202,8 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest
= do { mb_new_ev <- newWanted loc new_pred
; MASSERT( tcCoercionRole co == ctEvRole ev )
; setWantedEvTerm dest
- (EvExpr $ mkEvCast (getEvExpr mb_new_ev)
- (tcDowngradeRole Representational (ctEvRole ev) co))
+ (mkEvCast (getEvExpr mb_new_ev)
+ (tcDowngradeRole Representational (ctEvRole ev) co))
; case mb_new_ev of
Fresh new_ev -> continueWith new_ev
Cached _ -> stopWith ev "Cached wanted" }
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index fb60ba350bca78d5dc983b0bb01fe87f22835488..897ed963297e309c040ce9206fe11e87d7e42dd8 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -864,11 +864,11 @@ addDeferredBinding ctxt err ct
; case dest of
EvVarDest evar
- -> addTcEvBind ev_binds_var $ mkWantedEvBind evar (EvExpr err_tm)
+ -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
HoleDest hole
-> do { -- See Note [Deferred errors for coercion holes]
let co_var = coHoleCoVar hole
- ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var (EvExpr err_tm)
+ ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
; fillCoercionHole hole (mkTcCoVarCo co_var) }}
| otherwise -- Do not set any evidence for Given/Derived
diff --git a/compiler/typecheck/TcEvTerm.hs b/compiler/typecheck/TcEvTerm.hs
index 4c3961964c3eb1b3a78c53dc61557228a5aedbc8..8d8aa9bb10d727514fc48684ee709a1c90dcff2f 100644
--- a/compiler/typecheck/TcEvTerm.hs
+++ b/compiler/typecheck/TcEvTerm.hs
@@ -23,9 +23,10 @@ import SrcLoc
-- Used with Opt_DeferTypeErrors
-- See Note [Deferring coercion errors to runtime]
-- in TcSimplify
-evDelayedError :: Type -> FastString -> EvExpr
+evDelayedError :: Type -> FastString -> EvTerm
evDelayedError ty msg
- = Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
+ = EvExpr $
+ Var errorId `mkTyApps` [getRuntimeRep ty, ty] `mkApps` [litMsg]
where
errorId = tYPE_ERROR_ID
litMsg = Lit (MachStr (fastStringToByteString msg))
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 8abfc90f0474b3aa4be94348e4c98c23c2b8b54f..66fcb7a5897a0427fac274a35ed8792c4518a0d3 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -16,14 +16,14 @@ module TcEvidence (
lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
isEmptyEvBindMap,
EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
- sccEvBinds, evBindVar, isNoEvBindsVar,
+ evBindVar, isNoEvBindsVar,
-- EvTerm (already a CoreExpr)
EvTerm(..), EvExpr,
evId, evCoercion, evCast, evDFunApp, evSelector,
mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
- evTermCoercion,
+ evTermCoercion, evTermCoercion_maybe,
EvCallStack(..),
EvTypeable(..),
@@ -69,7 +69,6 @@ import CoreFVs ( exprSomeFreeVars )
import Util
import Bag
-import Digraph
import qualified Data.Data as Data
import Outputable
import SrcLoc
@@ -315,8 +314,8 @@ mkWpCastN co
mkWpTyApps :: [Type] -> HsWrapper
mkWpTyApps tys = mk_co_app_fn WpTyApp tys
-mkWpEvApps :: [EvExpr] -> HsWrapper
-mkWpEvApps args = mk_co_app_fn WpEvApp (map EvExpr args)
+mkWpEvApps :: [EvTerm] -> HsWrapper
+mkWpEvApps args = mk_co_app_fn WpEvApp args
mkWpEvVarApps :: [EvVar] -> HsWrapper
mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
@@ -416,7 +415,6 @@ instance Data.Data TcEvBinds where
{- Note [No evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
Class constraints etc give rise to /term/ bindings for evidence, and
we have nowhere to put term bindings in /types/. So in some places we
use NoEvBindsVar (see newNoTcEvBinds) to signal that no term-level
@@ -501,8 +499,8 @@ mkWantedEvBind :: EvVar -> EvTerm -> EvBind
mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
-- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
-mkGivenEvBind :: EvVar -> EvExpr -> EvBind
-mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr tm }
+mkGivenEvBind :: EvVar -> EvTerm -> EvBind
+mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
-- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
@@ -510,8 +508,17 @@ mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr
-- type EvTerm = CoreExpr
-- Because of staging problems issues around EvTypeable
data EvTerm
- = EvExpr EvExpr
- | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
+ = EvExpr EvExpr
+
+ | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
+
+ | EvFun -- /\as \ds. let binds in v
+ { et_tvs :: [TyVar]
+ , et_given :: [EvVar]
+ , et_binds :: TcEvBinds -- This field is why we need an EvFun
+ -- constructor, and can't just use EvExpr
+ , et_body :: EvVar }
+
deriving Data.Data
type EvExpr = CoreExpr
@@ -525,17 +532,17 @@ evId = Var
-- coercion bindings
-- See Note [Coercion evidence terms]
-evCoercion :: TcCoercion -> EvExpr
-evCoercion = Coercion
+evCoercion :: TcCoercion -> EvTerm
+evCoercion co = EvExpr (Coercion co)
-- | d |> co
-evCast :: EvExpr -> TcCoercion -> EvExpr
-evCast et tc | isReflCo tc = et
- | otherwise = Cast et tc
+evCast :: EvExpr -> TcCoercion -> EvTerm
+evCast et tc | isReflCo tc = EvExpr et
+ | otherwise = EvExpr (Cast et tc)
-- Dictionary instance application
-evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
-evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
+evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
+evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
-- Selector id plus the types at which it
-- should be instantiated, used for HasField
@@ -544,7 +551,6 @@ evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
-
-- Dictionary for (Typeable ty)
evTypeable :: Type -> EvTypeable -> EvTerm
evTypeable = EvTypeable
@@ -762,17 +768,23 @@ Important Details:
-}
-mkEvCast :: EvExpr -> TcCoercion -> EvExpr
+mkEvCast :: EvExpr -> TcCoercion -> EvTerm
mkEvCast ev lco
- | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
- isTcReflCo lco = ev
+ | ASSERT2( tcCoercionRole lco == Representational
+ , (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
+ isTcReflCo lco = EvExpr ev
| otherwise = evCast ev lco
-mkEvScSelectors :: EvExpr -> Class -> [TcType] -> [(TcPredType, EvExpr)]
-mkEvScSelectors ev cls tys
+
+mkEvScSelectors -- Assume class (..., D ty, ...) => C a b
+ :: Class -> [TcType] -- C ty1 ty2
+ -> [(TcPredType, -- D ty[ty1/a,ty2/b]
+ EvExpr) -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
+ ]
+mkEvScSelectors cls tys
= zipWith mk_pr (immSuperClasses cls tys) [0..]
where
- mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys `App` ev)
+ mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys)
where
sc_sel_id = classSCSelId cls i -- Zero-indexed
@@ -783,17 +795,31 @@ isEmptyTcEvBinds :: TcEvBinds -> Bool
isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
-evTermCoercion :: EvTerm -> TcCoercion
+evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
-- Applied only to EvTerms of type (s~t)
-- See Note [Coercion evidence terms]
+evTermCoercion_maybe ev_term
+ | EvExpr e <- ev_term = go e
+ | otherwise = Nothing
+ where
+ go :: EvExpr -> Maybe TcCoercion
+ go (Var v) = return (mkCoVarCo v)
+ go (Coercion co) = return co
+ go (Cast tm co) = do { co' <- go tm
+ ; return (mkCoCast co' co) }
+ go _ = Nothing
-{-
-************************************************************************
+evTermCoercion :: EvTerm -> TcCoercion
+evTermCoercion tm = case evTermCoercion_maybe tm of
+ Just co -> co
+ Nothing -> pprPanic "evTermCoercion" (ppr tm)
+
+
+{- *********************************************************************
* *
Free variables
* *
-************************************************************************
--}
+********************************************************************* -}
findNeededEvVars :: EvBindMap -> VarSet -> VarSet
findNeededEvVars ev_binds seeds
@@ -813,14 +839,10 @@ findNeededEvVars ev_binds seeds
| otherwise
= needs
-evTermCoercion (EvExpr (Var v)) = mkCoVarCo v
-evTermCoercion (EvExpr (Coercion co)) = co
-evTermCoercion (EvExpr (Cast tm co)) = mkCoCast (evTermCoercion (EvExpr tm)) co
-evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
-
evVarsOfTerm :: EvTerm -> VarSet
evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
+evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun]
evVarsOfTerms :: [EvTerm] -> VarSet
evVarsOfTerms = mapUnionVarSet evVarsOfTerm
@@ -833,22 +855,20 @@ evVarsOfTypeable ev =
EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
EvTypeableTyLit e -> evVarsOfTerm e
--- | Do SCC analysis on a bag of 'EvBind's.
-sccEvBinds :: Bag EvBind -> [SCC EvBind]
-sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
- where
- edges :: [ Node EvVar EvBind ]
- edges = foldrBag ((:) . mk_node) [] bs
- mk_node :: EvBind -> Node EvVar EvBind
- mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
- = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `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.
+{- Note [Free vars of EvFun]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Finding the free vars of an EvFun is made tricky by the fact the
+bindings et_binds may be a mutable variable. Fortunately, we
+can just squeeze by. Here's how.
+
+* evVarsOfTerm is used only by TcSimplify.neededEvVars.
+* Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
+ ic_binds field of an Implication
+* So we can track usage via the processing for that implication,
+ (see Note [Tracking redundant constraints] in TcSimplify).
+ We can ignore usage from the EvFun altogether.
-{-
************************************************************************
* *
Pretty printing
@@ -881,11 +901,12 @@ pprHsWrapper wrap pp_thing_inside
<+> pprParendCo co)]
help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
- help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
- help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
+ help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False]
+ help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False]
help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
- pp_bndr v = pprBndr LambdaBind v <> dot
+pprLamBndr :: Id -> SDoc
+pprLamBndr v = pprBndr LambdaBind v
add_parens, no_parens :: SDoc -> Bool -> SDoc
add_parens d True = parens d
@@ -916,6 +937,9 @@ instance Outputable EvBind where
instance Outputable EvTerm where
ppr (EvExpr e) = ppr e
ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
+ ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
+ = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
+ 2 (ppr bs $$ ppr w) -- Not very pretty
instance Outputable EvCallStack where
ppr EvCsEmpty
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 0bc5c9c81e1a8fce5469018ceec71f78f74b1867..8cabd0ca0924365a0e9ea7fc6f4ecd0ec283d7bf 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -346,6 +346,15 @@ zonkEvVarOcc env v
= return (EvId $ zonkIdOcc env v)
-}
+zonkCoreBndrX :: ZonkEnv -> Var -> TcM (ZonkEnv, Var)
+zonkCoreBndrX env v
+ | isId v = do { v' <- zonkIdBndr env v
+ ; return (extendIdZonkEnv1 env v', v') }
+ | otherwise = zonkTyBndrX env v
+
+zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
+zonkCoreBndrsX = mapAccumLM zonkCoreBndrX
+
zonkTyBndrsX :: ZonkEnv -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
zonkTyBndrsX = mapAccumLM zonkTyBndrX
@@ -1437,10 +1446,18 @@ zonkRule _ (XRuleDecl _) = panic "zonkRule"
-}
zonkEvTerm :: ZonkEnv -> EvTerm -> TcM EvTerm
-zonkEvTerm env (EvExpr e) =
- EvExpr <$> zonkCoreExpr env e
-zonkEvTerm env (EvTypeable ty ev) =
- EvTypeable <$> zonkTcTypeToType env ty <*> zonkEvTypeable env ev
+zonkEvTerm env (EvExpr e)
+ = EvExpr <$> zonkCoreExpr env e
+zonkEvTerm env (EvTypeable ty ev)
+ = EvTypeable <$> zonkTcTypeToType env ty <*> zonkEvTypeable env ev
+zonkEvTerm env (EvFun { et_tvs = tvs, et_given = evs
+ , et_binds = ev_binds, et_body = body_id })
+ = do { (env0, new_tvs) <- zonkTyBndrsX env tvs
+ ; (env1, new_evs) <- zonkEvBndrsX env0 evs
+ ; (env2, new_ev_binds) <- zonkTcEvBinds env1 ev_binds
+ ; let new_body_id = zonkIdOcc env2 body_id
+ ; return (EvFun { et_tvs = new_tvs, et_given = new_evs
+ , et_binds = new_ev_binds, et_body = new_body_id }) }
zonkCoreExpr :: ZonkEnv -> CoreExpr -> TcM CoreExpr
zonkCoreExpr env (Var v)
@@ -1463,9 +1480,8 @@ zonkCoreExpr env (Tick t e)
zonkCoreExpr env (App e1 e2)
= App <$> zonkCoreExpr env e1 <*> zonkCoreExpr env e2
zonkCoreExpr env (Lam v e)
- = do v' <- zonkIdBndr env v
- let env1 = extendIdZonkEnv1 env v'
- Lam v' <$> zonkCoreExpr env1 e
+ = do { (env1, v') <- zonkCoreBndrX env v
+ ; Lam v' <$> zonkCoreExpr env1 e }
zonkCoreExpr env (Let bind e)
= do (env1, bind') <- zonkCoreBind env bind
Let bind'<$> zonkCoreExpr env1 e
@@ -1478,11 +1494,10 @@ zonkCoreExpr env (Case scrut b ty alts)
return $ Case scrut' b' ty' alts'
zonkCoreAlt :: ZonkEnv -> CoreAlt -> TcM CoreAlt
-zonkCoreAlt env (dc, pats, rhs)
- = do pats' <- mapM (zonkIdBndr env) pats
- let env1 = extendZonkEnv env pats'
+zonkCoreAlt env (dc, bndrs, rhs)
+ = do (env1, bndrs') <- zonkCoreBndrsX env bndrs
rhs' <- zonkCoreExpr env1 rhs
- return $ (dc, pats', rhs')
+ return $ (dc, bndrs', rhs')
zonkCoreBind :: ZonkEnv -> CoreBind -> TcM (ZonkEnv, CoreBind)
zonkCoreBind env (NonRec v e)
@@ -1558,7 +1573,7 @@ zonkEvBind env bind@(EvBind { eb_lhs = var, eb_rhs = term })
; term' <- case getEqPredTys_maybe (idType var') of
Just (r, ty1, ty2) | ty1 `eqType` ty2
- -> return (EvExpr (evCoercion (mkTcReflCo r ty1)))
+ -> return (evCoercion (mkTcReflCo r ty1))
_other -> zonkEvTerm env term
; return (bind { eb_lhs = var', eb_rhs = term' }) }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 21a8209b5ee68c3c343bc3c6a835af5909343b67..d09675778d85d68c1d4004f4de3709d957672120 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -1052,7 +1052,7 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds sc_theta
; sc_top_name <- newName (mkSuperDictAuxOcc n (getOccName cls))
; sc_ev_id <- newEvVar sc_pred
- ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id (EvExpr sc_ev_tm)
+ ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm
; let sc_top_ty = mkInvForAllTys tyvars (mkLamTypes dfun_evs sc_pred)
sc_top_id = mkLocalId sc_top_name sc_top_ty
export = ABE { abe_ext = noExt
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index b2be509b698a8569087cb83fc4380777353f7f2b..3e41c61264963163f01018d9d7fd08ccf20292a7 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -44,7 +44,7 @@ import FieldLabel
import FunDeps
import FamInst
import FamInstEnv
-import Unify ( tcUnifyTyWithTFs )
+import Unify ( tcUnifyTyWithTFs, ruleMatchTyKiX )
import TcEvidence
import MkCore ( mkStringExprFS, mkNaturalExpr )
@@ -720,11 +720,11 @@ interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_insol = insoluble })
= continueWith workItem
where
- swap_me :: SwapFlag -> CtEvidence -> EvExpr
+ swap_me :: SwapFlag -> CtEvidence -> EvTerm
swap_me swap ev
= case swap of
- NotSwapped -> ctEvExpr ev
- IsSwapped -> evCoercion (mkTcSymCo (evTermCoercion (EvExpr (ctEvExpr ev))))
+ NotSwapped -> ctEvTerm ev
+ IsSwapped -> evCoercion (mkTcSymCo (evTermCoercion (ctEvTerm ev)))
interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
@@ -1055,14 +1055,14 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
then stopWith ev_w "interactDict/solved from instance"
else
- do { -- We were unable to solve the [W] constraint from in-scope
- -- instances so we solve it from the matching inert we found
+ do { -- Ths short-cut solver didn't fire, so we
+ -- solve ev_w from the matching inert ev_i we found
what_next <- solveOneFromTheOther ev_i ev_w
; traceTcS "lookupInertDict" (ppr what_next)
; case what_next of
- KeepInert -> do { setEvBindIfWanted ev_w (ctEvExpr ev_i)
+ KeepInert -> do { setEvBindIfWanted ev_w (ctEvTerm ev_i)
; return $ Stop ev_w (text "Dict equal" <+> parens (ppr what_next)) }
- KeepWork -> do { setEvBindIfWanted ev_i (ctEvExpr ev_w)
+ KeepWork -> do { setEvBindIfWanted ev_i (ctEvTerm ev_w)
; updInertDicts $ \ ds -> delDict ds cls tys
; continueWith workItem } } }
@@ -1127,9 +1127,9 @@ shortCutSolver dflags ev_w ev_i
try_solve_from_instance loc (ev_binds, solved_dicts) ev
| let pred = ctEvPred ev
, ClassPred cls tys <- classifyPredType pred
- = do { inst_res <- lift $ match_class_inst dflags True cls tys loc_w
+ = do { inst_res <- lift $ matchGlobalInst dflags True cls tys loc_w
; case inst_res of
- GenInst { lir_new_theta = preds
+ OneInst { lir_new_theta = preds
, lir_mk_ev = mk_ev
, lir_safe_over = safeOverlap }
| safeOverlap
@@ -1625,10 +1625,10 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
; stopWith ev "Solved from inert" }
| ReprEq <- eq_rel -- See Note [Do not unify representational equalities]
- = unsolved_inert
+ = continueWith workItem
| isGiven ev -- See Note [Touchables and givens]
- = unsolved_inert
+ = continueWith workItem
| otherwise
= do { tclvl <- getTcLevel
@@ -1637,18 +1637,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
; n_kicked <- kickOutAfterUnification tv
; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
- else unsolved_inert }
-
- where
- unsolved_inert
- = do { traceTcS "Can't solve tyvar equality"
- (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
- , ppWhen (isMetaTyVar tv) $
- nest 4 (text "TcLevel of" <+> ppr tv
- <+> text "is" <+> ppr (metaTyVarTcLevel tv))
- , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
- ; addInertEq workItem
- ; stopWith ev "Kept as inert" }
+ else continueWith workItem }
interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
@@ -1814,7 +1803,7 @@ emitFunDepDeriveds fd_eqns
= do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
; mapM_ (unifyDerived loc Nominal) eqs }
| otherwise
- = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr eqs)
+ = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
; subst <- instFlexi tvs -- Takes account of kind substitution
; mapM_ (do_one_eq loc subst) eqs }
@@ -1831,30 +1820,32 @@ emitFunDepDeriveds fd_eqns
-}
topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
-topReactionsStage wi
- = do { tir <- doTopReact wi
- ; case tir of
- ContinueWith wi -> continueWith wi
- Stop ev s -> return (Stop ev (text "Top react:" <+> s)) }
-
-doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
--- The work item does not react with the inert set, so try interaction with top-level
--- instances. Note:
---
--- (a) The place to add superclasses in not here in doTopReact stage.
--- Instead superclasses are added in the worklist as part of the
--- canonicalization process. See Note [Adding superclasses].
-
-doTopReact work_item
+-- The work item does not react with the inert set,
+-- so try interaction with top-level instances. Note:
+topReactionsStage work_item
= do { traceTcS "doTopReact" (ppr work_item)
; case work_item of
CDictCan {} -> do { inerts <- getTcSInerts
; doTopReactDict inerts work_item }
CFunEqCan {} -> doTopReactFunEq work_item
+ CIrredCan {} -> doTopReactOther work_item
+ CTyEqCan {} -> doTopReactOther work_item
_ -> -- Any other work item does not react with any top-level equations
continueWith work_item }
+--------------------
+doTopReactOther :: Ct -> TcS (StopOrContinue Ct)
+doTopReactOther work_item
+ = do { -- Try local quantified constraints
+ res <- matchLocalInst pred (ctEvLoc ev)
+ ; case res of
+ OneInst {} -> chooseInstance ev pred res
+ _ -> continueWith work_item }
+ where
+ ev = ctEvidence work_item
+ pred = ctEvPred ev
+
--------------------
doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
@@ -2227,41 +2218,69 @@ Another example is indexed-types/should_compile/T10634
doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
-- Try to use type-class instance declarations to simplify the constraint
-doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
+doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
, cc_tyargs = xis })
- | isGiven fl -- Never use instances for Given constraints
+ | isGiven ev -- Never use instances for Given constraints
= do { try_fundep_improvement
; continueWith work_item }
- | Just ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
- = do { setEvBindIfWanted fl (ctEvExpr ev)
- ; stopWith fl "Dict/Top (cached)" }
+ | Just solved_ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
+ = do { setEvBindIfWanted ev (ctEvTerm solved_ev)
+ ; stopWith ev "Dict/Top (cached)" }
| otherwise -- Wanted or Derived, but not cached
= do { dflags <- getDynFlags
- ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
- ; case lkup_inst_res of
- GenInst { lir_new_theta = theta
- , lir_mk_ev = mk_ev
- , lir_safe_over = s } ->
- do { traceTcS "doTopReact/found instance for" $ ppr fl
- ; checkReductionDepth deeper_loc dict_pred
- ; unless s $ insertSafeOverlapFailureTcS work_item
- ; if isDerived fl then finish_derived theta
- else finish_wanted theta mk_ev }
- NoInstance ->
- do { when (isImprovable fl) $
- try_fundep_improvement
- ; continueWith work_item } }
+ ; lkup_res <- matchClassInst dflags inerts cls xis dict_loc
+ ; case lkup_res of
+ OneInst { lir_safe_over = s }
+ -> do { unless s $ insertSafeOverlapFailureTcS work_item
+ ; when (isWanted ev) $ addSolvedDict ev cls xis
+ ; chooseInstance ev dict_pred lkup_res }
+ _ -> -- NoInstance or NotSure
+ do { when (isImprovable ev) $
+ try_fundep_improvement
+ ; continueWith work_item } }
where
dict_pred = mkClassPred cls xis
- dict_loc = ctEvLoc fl
+ dict_loc = ctEvLoc ev
dict_origin = ctLocOrigin dict_loc
- deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
+
+ -- We didn't solve it; so try functional dependencies with
+ -- the instance environment, and return
+ -- See also Note [Weird fundeps]
+ try_fundep_improvement
+ = do { traceTcS "try_fundeps" (ppr work_item)
+ ; instEnvs <- getInstEnvs
+ ; emitFunDepDeriveds $
+ improveFromInstEnv instEnvs mk_ct_loc dict_pred }
+
+ mk_ct_loc :: PredType -- From instance decl
+ -> SrcSpan -- also from instance deol
+ -> CtLoc
+ mk_ct_loc inst_pred inst_loc
+ = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
+ inst_pred inst_loc }
+
+doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+
+
+chooseInstance :: CtEvidence -> TcPredType -> LookupInstResult
+ -> TcS (StopOrContinue Ct)
+chooseInstance ev pred
+ (OneInst { lir_new_theta = theta
+ , lir_mk_ev = mk_ev })
+ = do { traceTcS "doTopReact/found instance for" $ ppr ev
+ ; checkReductionDepth deeper_loc pred
+ ; if isDerived ev then finish_derived theta
+ else finish_wanted theta mk_ev }
+ where
+ loc = ctEvLoc ev
+ deeper_loc = zap_origin (bumpCtLocDepth loc)
+ origin = ctLocOrigin loc
zap_origin loc -- After applying an instance we can set ScOrigin to
-- infinity, so that prohibitedSuperClassSolve never fires
- | ScOrigin {} <- dict_origin
+ | ScOrigin {} <- origin
= setCtLocOrigin loc (ScOrigin infinity)
| otherwise
= loc
@@ -2270,11 +2289,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
-> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
-- Precondition: evidence term matches the predicate workItem
finish_wanted theta mk_ev
- = do { addSolvedDict fl cls xis
- ; evc_vars <- mapM (newWanted deeper_loc) theta
- ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvExpr evc_vars))
+ = do { evc_vars <- mapM (newWanted deeper_loc) theta
+ ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars))
; emitWorkNC (freshGoals evc_vars)
- ; stopWith fl "Dict/Top (solved wanted)" }
+ ; stopWith ev "Dict/Top (solved wanted)" }
finish_derived theta -- Use type-class instances for Deriveds, in the hope
= -- of generating some improvements
@@ -2282,26 +2300,10 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
-- It's easy because no evidence is involved
do { emitNewDeriveds deeper_loc theta
; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
- ; stopWith fl "Dict/Top (solved derived)" }
-
- -- We didn't solve it; so try functional dependencies with
- -- the instance environment, and return
- -- See also Note [Weird fundeps]
- try_fundep_improvement
- = do { traceTcS "try_fundeps" (ppr work_item)
- ; instEnvs <- getInstEnvs
- ; emitFunDepDeriveds $
- improveFromInstEnv instEnvs mk_ct_loc dict_pred }
-
- mk_ct_loc :: PredType -- From instance decl
- -> SrcSpan -- also from instance deol
- -> CtLoc
- mk_ct_loc inst_pred inst_loc
- = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
- inst_pred inst_loc }
-
-doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
+ ; stopWith ev "Dict/Top (solved derived)" }
+chooseInstance ev _ lookup_res
+ = pprPanic "chooseInstance" (ppr ev $$ ppr lookup_res)
{- *******************************************************************
* *
@@ -2317,20 +2319,26 @@ doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
type SafeOverlapping = Bool
data LookupInstResult
- = NoInstance
- | GenInst { lir_new_theta :: [TcPredType]
+ = NoInstance -- Definitely no instance
+
+ | OneInst { lir_new_theta :: [TcPredType]
, lir_mk_ev :: [EvExpr] -> EvTerm
, lir_safe_over :: SafeOverlapping }
+ | NotSure -- Multiple matches and/or one or more unifiers
+
instance Outputable LookupInstResult where
ppr NoInstance = text "NoInstance"
- ppr (GenInst { lir_new_theta = ev
+ ppr NotSure = text "NotSure"
+ ppr (OneInst { lir_new_theta = ev
, lir_safe_over = s })
- = text "GenInst" <+> vcat [ppr ev, ss]
+ = text "OneInst" <+> vcat [ppr ev, ss]
where ss = text $ if s then "[safe]" else "[unsafe]"
-matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchClassInst :: DynFlags -> InertSet
+ -> Class -> [Type]
+ -> CtLoc -> TcS LookupInstResult
matchClassInst dflags inerts clas tys loc
-- First check whether there is an in-scope Given that could
-- match this constraint. In that case, do not use top-level
@@ -2342,21 +2350,33 @@ matchClassInst dflags inerts clas tys loc
= do { traceTcS "Delaying instance application" $
vcat [ text "Work item=" <+> pprClassPred clas tys
, text "Potential matching givens:" <+> ppr matchable_givens ]
- ; return NoInstance }
+ ; return NotSure }
+
+ | otherwise
+ = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr pred <+> char '{'
+ ; local_res <- matchLocalInst pred loc
+ ; case local_res of
+ OneInst {} ->
+ do { traceTcS "} matchClassInst local match" $ ppr local_res
+ ; return local_res }
+
+ NotSure -> -- In the NotSure case for local instances
+ -- we don't want to try global instances
+ do { traceTcS "} matchClassInst local not sure" empty
+ ; return local_res }
+
+ NoInstance -- No local instances, so try global ones
+ -> do { global_res <- matchGlobalInst dflags False clas tys loc
+ ; traceTcS "} matchClassInst global result" $ ppr global_res
+ ; return global_res } }
where
- pred = mkClassPred clas tys
+ pred = mkClassPred clas tys
-matchClassInst dflags _ clas tys loc
- = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr (mkClassPred clas tys) <+> char '{'
- ; res <- match_class_inst dflags False clas tys loc
- ; traceTcS "} matchClassInst result" $ ppr res
- ; return res }
-
-match_class_inst :: DynFlags
- -> Bool -- True <=> caller is the short-cut solver
- -- See Note [Shortcut solving: overlap]
- -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
-match_class_inst dflags short_cut clas tys loc
+matchGlobalInst :: DynFlags
+ -> Bool -- True <=> caller is the short-cut solver
+ -- See Note [Shortcut solving: overlap]
+ -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
+matchGlobalInst dflags short_cut clas tys loc
| cls_name == knownNatClassName = matchKnownNat clas tys
| cls_name == knownSymbolClassName = matchKnownSymbol clas tys
| isCTupleClass clas = matchCTuple clas tys
@@ -2507,12 +2527,42 @@ PS: the term "naturally coherent" doesn't really seem helpful.
Perhaps "invertible" or something? I left it for now though.
-}
+matchLocalInst :: TcPredType -> CtLoc -> TcS LookupInstResult
+matchLocalInst pred loc
+ = do { ics <- getInertCans
+ ; case match_local_inst (inert_insts ics) of
+ ([], False) -> return NoInstance
+ ([(dfun_ev, inst_tys)], unifs)
+ | not unifs
+ -> match_one pred loc True (ctEvEvId dfun_ev) inst_tys
+ _ -> return NotSure }
+ where
+ pred_tv_set = tyCoVarsOfType pred
+
+ match_local_inst :: [QCInst]
+ -> ( [(CtEvidence, [DFunInstType])]
+ , Bool ) -- True <=> Some unify but do not match
+ match_local_inst []
+ = ([], False)
+ match_local_inst (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
+ , qci_ev = ev })
+ : qcis)
+ | let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
+ , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
+ emptyTvSubstEnv qpred pred
+ , let match = (ev, map (lookupVarEnv tv_subst) qtvs)
+ = (match:matches, unif)
-{- *******************************************************************
-* *
- Class lookup in the instance environment
-* *
-**********************************************************************-}
+ | otherwise
+ = ASSERT2( disjointVarSet qtv_set (tyCoVarsOfType pred)
+ , ppr qci $$ ppr pred )
+ -- ASSERT: unification relies on the
+ -- quantified variables being fresh
+ (matches, unif || this_unif)
+ where
+ qtv_set = mkVarSet qtvs
+ this_unif = mightMatchLater qpred (ctEvLoc ev) pred loc
+ (matches, unif) = match_local_inst qcis
matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
matchInstEnv dflags short_cut_solver clas tys loc
@@ -2520,51 +2570,57 @@ matchInstEnv dflags short_cut_solver clas tys loc
; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
(matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
+ ; traceTcS "matchInstEnv" $
+ vcat [ text "goal:" <+> ppr clas <+> ppr tys
+ , text "matches:" <+> ppr matches
+ , text "unify:" <+> ppr unify ]
; case (matches, unify, safeHaskFail) of
-- Nothing matches
- ([], _, _)
+ ([], [], _)
-> do { traceTcS "matchClass not matching" (ppr pred)
; return NoInstance }
-- A single match (& no safe haskell failure)
([(ispec, inst_tys)], [], False)
- | short_cut_solver
+ | short_cut_solver -- Called from the short-cut solver
, isOverlappable ispec
-- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
-- then don't let the short-cut solver choose it, because a
-- later instance might overlap it. Trac #14434 is an example
-- See Note [Shortcut solving: overlap]
- -> do { traceTcS "matchClass: ingnoring overlappable" (ppr pred)
- ; return NoInstance }
+ -> do { traceTcS "matchClass: ignoring overlappable" (ppr pred)
+ ; return NotSure }
| otherwise
- -> do { let dfun_id = instanceDFunId ispec
- ; traceTcS "matchClass success" $
- vcat [text "dict" <+> ppr pred,
- text "witness" <+> ppr dfun_id
- <+> ppr (idType dfun_id) ]
- -- Record that this dfun is needed
- ; match_one (null unsafeOverlaps) dfun_id inst_tys }
+ -> do { let dfun_id = instanceDFunId ispec
+ ; traceTcS "matchClass success" $
+ vcat [text "dict" <+> ppr pred,
+ text "witness" <+> ppr dfun_id
+ <+> ppr (idType dfun_id) ]
+ -- Record that this dfun is needed
+ ; match_one pred loc (null unsafeOverlaps) dfun_id inst_tys }
-- More than one matches (or Safe Haskell fail!). Defer any
-- reactions of a multitude until we learn more about the reagent
- (matches, _, _)
- -> do { traceTcS "matchClass multiple matches, deferring choice" $
- vcat [text "dict" <+> ppr pred,
- text "matches" <+> ppr matches]
- ; return NoInstance } }
+ _ -> do { traceTcS "matchClass multiple matches, deferring choice" $
+ vcat [text "dict" <+> ppr pred,
+ text "matches" <+> ppr matches]
+ ; return NotSure } }
where
pred = mkClassPred clas tys
- match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
- -- See Note [DFunInstType: instantiating types] in InstEnv
- match_one so dfun_id mb_inst_tys
- = do { checkWellStagedDFun pred dfun_id loc
- ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
- ; return $ GenInst { lir_new_theta = theta
- , lir_mk_ev = EvExpr . evDFunApp dfun_id tys
- , lir_safe_over = so } }
+match_one :: TcPredType -> CtLoc -> SafeOverlapping
+ -> DFunId -> [DFunInstType] -> TcS LookupInstResult
+ -- See Note [DFunInstType: instantiating types] in InstEnv
+match_one pred loc so dfun_id mb_inst_tys
+ = do { traceTcS "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
+ ; checkWellStagedDFun pred dfun_id loc
+ ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
+ ; traceTcS "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
+ ; return $ OneInst { lir_new_theta = theta
+ , lir_mk_ev = evDFunApp dfun_id tys
+ , lir_safe_over = so } }
{- ********************************************************************
@@ -2575,13 +2631,13 @@ matchInstEnv dflags short_cut_solver clas tys loc
matchCTuple :: Class -> [Type] -> TcS LookupInstResult
matchCTuple clas tys -- (isCTupleClass clas) holds
- = return (GenInst { lir_new_theta = tys
+ = return (OneInst { lir_new_theta = tys
, lir_mk_ev = tuple_ev
, lir_safe_over = True })
-- The dfun *is* the data constructor!
where
data_con = tyConSingleDataCon (classTyCon clas)
- tuple_ev = EvExpr . evDFunApp (dataConWrapId data_con) tys
+ tuple_ev = evDFunApp (dataConWrapId data_con) tys
{- ********************************************************************
* *
@@ -2673,8 +2729,8 @@ makeLitDict clas ty et
$ idType meth -- forall n. KnownNat n => SNat n
, Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
-- SNat n ~ Integer
- , let ev_tm = EvExpr $ mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
- = return $ GenInst { lir_new_theta = []
+ , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
+ = return $ OneInst { lir_new_theta = []
, lir_mk_ev = \_ -> ev_tm
, lir_safe_over = True }
@@ -2710,12 +2766,15 @@ matchTypeable _ _ = return NoInstance
-- | Representation for a type @ty@ of the form @arg -> ret@.
doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
doFunTy clas ty arg_ty ret_ty
- = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
- build_ev [arg_ev, ret_ev] =
- evTypeable ty $ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
- build_ev _ = panic "TcInteract.doFunTy"
- ; return $ GenInst preds build_ev True
- }
+ = return $ OneInst { lir_new_theta = preds
+ , lir_mk_ev = mk_ev
+ , lir_safe_over = True }
+ where
+ preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
+ mk_ev [arg_ev, ret_ev] = evTypeable ty $
+ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
+ mk_ev _ = panic "TcInteract.doFunTy"
+
-- | Representation for type constructor applied to some kinds.
-- 'onlyNamedBndrsApplied' has ensured that this application results in a type
@@ -2723,11 +2782,13 @@ doFunTy clas ty arg_ty ret_ty
doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
doTyConApp clas ty tc kind_args
| Just _ <- tyConRepName_maybe tc
- = return $ GenInst (map (mk_typeable_pred clas) kind_args)
- (\kinds -> evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds))
- True
+ = return $ OneInst { lir_new_theta = (map (mk_typeable_pred clas) kind_args)
+ , lir_mk_ev = mk_ev
+ , lir_safe_over = True }
| otherwise
= return NoInstance
+ where
+ mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
-- | Representation for TyCon applications of a concrete kind. We just use the
-- kind itself, but first we must make sure that we've instantiated all kind-
@@ -2752,9 +2813,13 @@ doTyApp clas ty f tk
| isForAllTy (typeKind f)
= return NoInstance -- We can't solve until we know the ctr.
| otherwise
- = return $ GenInst (map (mk_typeable_pred clas) [f, tk])
- (\[t1,t2] -> evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2))
- True
+ = return $ OneInst { lir_new_theta = map (mk_typeable_pred clas) [f, tk]
+ , lir_mk_ev = mk_ev
+ , lir_safe_over = True }
+ where
+ mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
+ mk_ev _ = panic "doTyApp"
+
-- Emit a `Typeable` constraint for the given type.
mk_typeable_pred :: Class -> Type -> PredType
@@ -2768,7 +2833,9 @@ doTyLit kc t = do { kc_clas <- tcLookupClass kc
; let kc_pred = mkClassPred kc_clas [ t ]
mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
mk_ev _ = panic "doTyLit"
- ; return (GenInst [kc_pred] mk_ev True) }
+ ; return (OneInst { lir_new_theta = [kc_pred]
+ , lir_mk_ev = mk_ev
+ , lir_safe_over = True }) }
{- Note [Typeable (T a b c)]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2818,15 +2885,15 @@ a TypeRep for them. For qualified but not polymorphic types, like
-- See also Note [The equality types story] in TysPrim
matchLiftedEquality :: [Type] -> TcS LookupInstResult
matchLiftedEquality args
- = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
- , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId heqDataCon) args
+ = return (OneInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
+ , lir_mk_ev = evDFunApp (dataConWrapId heqDataCon) args
, lir_safe_over = True })
-- See also Note [The equality types story] in TysPrim
matchLiftedCoercible :: [Type] -> TcS LookupInstResult
matchLiftedCoercible args@[k, t1, t2]
- = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
- , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId coercibleDataCon)
+ = return (OneInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
+ , lir_mk_ev = evDFunApp (dataConWrapId coercibleDataCon)
args
, lir_safe_over = True })
where
@@ -2928,7 +2995,7 @@ matchHasField dflags short_cut clas tys loc
-- Use the equality proof to cast the selector Id to
-- type (r -> a), then use the newtype coercion to cast
-- it to a HasField dictionary.
- mk_ev (ev1:evs) = EvExpr $ evSelector sel_id tvs evs `evCast` co
+ mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
where
co = mkTcSubCo (evTermCoercion (EvExpr ev1))
`mkTcTransCo` mkTcSymCo co2
@@ -2944,7 +3011,7 @@ matchHasField dflags short_cut clas tys loc
-- it must not be higher-rank.
; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
then do { addUsedGRE True gre
- ; return GenInst { lir_new_theta = theta
+ ; return OneInst { lir_new_theta = theta
, lir_mk_ev = mk_ev
, lir_safe_over = True
} }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 89741d2c4bd926f5a4c1c6ca84aa8c39da9f2307..87a9fa395dee1ef2b86a1444bae1cd54c935602e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -205,11 +205,11 @@ cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
; return (implic { ic_wanted = inner_wanted' }) }
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
-emitWanted :: CtOrigin -> TcPredType -> TcM EvExpr
+emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted origin pty
= do { ev <- newWanted origin Nothing pty
; emitSimple $ mkNonCanonical ev
- ; return $ ctEvExpr ev }
+ ; return $ ctEvTerm ev }
-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
@@ -247,8 +247,9 @@ newDict cls tys
predTypeOccName :: PredType -> OccName
predTypeOccName ty = case classifyPredType ty of
ClassPred cls _ -> mkDictOcc (getOccName cls)
- EqPred _ _ _ -> mkVarOccFS (fsLit "co")
- IrredPred _ -> mkVarOccFS (fsLit "irred")
+ EqPred {} -> mkVarOccFS (fsLit "co")
+ IrredPred {} -> mkVarOccFS (fsLit "irred")
+ ForAllPred {} -> mkVarOccFS (fsLit "df")
{-
************************************************************************
@@ -1477,7 +1478,7 @@ zonkCt ct
= ASSERT( not (isCFunEqCan ct) )
-- We do not expect to see any CFunEqCans, because zonkCt is only called on
-- unflattened constraints.
- do { fl' <- zonkCtEvidence (cc_ev ct)
+ do { fl' <- zonkCtEvidence (ctEvidence ct)
; return (mkNonCanonical fl') }
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index fcea649d01539955e40183fbb9894c157be8cb1c..f43072f59b3153f1dc04e7d3c2aaf873b87fcaec 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -116,7 +116,8 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
(mkTyVarBinders Inferred univ_tvs
, req_theta, ev_binds, req_dicts)
(mkTyVarBinders Inferred ex_tvs
- , mkTyVarTys ex_tvs, prov_theta, map evId filtered_prov_dicts)
+ , mkTyVarTys ex_tvs, prov_theta
+ , map (EvExpr . evId) filtered_prov_dicts)
(map nlHsVar args, map idType args)
pat_ty rec_fields }
tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
@@ -539,7 +540,7 @@ tc_patsyn_finish :: Located Name -- ^ PatSyn Name
-> Bool -- ^ Whether infix
-> LPat GhcTc -- ^ Pattern of the PatSyn
-> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
- -> ([TcTyVarBinder], [TcType], [PredType], [EvExpr])
+ -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
-> ([LHsExpr GhcTcId], [TcType]) -- ^ Pattern arguments and
-- types
-> TcType -- ^ Pattern type
@@ -625,7 +626,7 @@ tc_patsyn_finish lname dir is_infix lpat'
tcPatSynMatcher :: Located Name
-> LPat GhcTc
-> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
- -> ([TcTyVar], [TcType], ThetaType, [EvExpr])
+ -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
-> ([LHsExpr GhcTcId], [TcType])
-> TcType
-> TcM ((Id, Bool), LHsBinds GhcTc)
diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs
index b84e5ad83265e69fed93873a7c76601d46ca8a1f..a112003ef924fdb5e142023b87dce5ac445c6120 100644
--- a/compiler/typecheck/TcPluginM.hs
+++ b/compiler/typecheck/TcPluginM.hs
@@ -69,7 +69,7 @@ import TcRnMonad ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM
, liftIO, traceTc )
import TcMType ( TcTyVar, TcType )
import TcEnv ( TcTyThing )
-import TcEvidence ( TcCoercion, CoercionHole
+import TcEvidence ( TcCoercion, CoercionHole, EvTerm(..)
, EvExpr, EvBind, mkGivenEvBind )
import TcRnTypes ( CtEvidence(..) )
import Var ( EvVar )
@@ -173,7 +173,7 @@ newDerived loc pty = return CtDerived { ctev_pred = pty, ctev_loc = loc }
newGiven :: CtLoc -> PredType -> EvExpr -> TcPluginM CtEvidence
newGiven loc pty evtm = do
new_ev <- newEvVar pty
- setEvBind $ mkGivenEvBind new_ev evtm
+ setEvBind $ mkGivenEvBind new_ev (EvExpr evtm)
return CtGiven { ctev_pred = pty, ctev_evar = new_ev, ctev_loc = loc }
-- | Create a fresh evidence variable.
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index fb09fdd9234f96b59cabfcbb9fc6b9aaa079f063..73b15a525277315a5486ea48a451c0f83cf6de45 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -64,6 +64,9 @@ module TcRnTypes(
TcIdSigInst(..), TcPatSynInfo(..),
isPartialSig, hasCompleteSig,
+ -- QCInst
+ QCInst(..), isPendingScInst,
+
-- Canonical constraints
Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
@@ -78,7 +81,7 @@ module TcRnTypes(
mkNonCanonical, mkNonCanonicalCt, mkGivens,
mkIrredCt, mkInsolubleCt,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
- ctEvExpr, ctEvCoercion, ctEvEvId,
+ ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
@@ -1699,6 +1702,26 @@ data Ct
cc_hole :: Hole
}
+ | CQuantCan QCInst -- A quantified constraint
+ -- NB: I expect to make more of the cases in Ct
+ -- look like this, with the payload in an
+ -- auxiliary type
+
+------------
+data QCInst -- A much simplified version of ClsInst
+ -- See Note [Quantified constraints] in TcCanonical
+ = QCI { qci_ev :: CtEvidence -- Always of type forall tvs. context => ty
+ -- Always Given
+ , qci_tvs :: [TcTyVar] -- The tvs
+ , qci_pred :: TcPredType -- The ty
+ , qci_pend_sc :: Bool -- Same as cc_pend_sc flag in CDictCan
+ -- Invariant: True => qci_pred is a ClassPred
+ }
+
+instance Outputable QCInst where
+ ppr (QCI { qci_ev = ev }) = ppr ev
+
+------------
-- | An expression or type hole
data Hole = ExprHole UnboundVar
-- ^ Either an out-of-scope variable or a "true" hole in an
@@ -1785,7 +1808,8 @@ mkGivens loc ev_ids
, ctev_loc = loc })
ctEvidence :: Ct -> CtEvidence
-ctEvidence = cc_ev
+ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev
+ctEvidence ct = cc_ev ct
ctLoc :: Ct -> CtLoc
ctLoc = ctEvLoc . ctEvidence
@@ -1798,7 +1822,7 @@ ctOrigin = ctLocOrigin . ctLoc
ctPred :: Ct -> PredType
-- See Note [Ct/evidence invariant]
-ctPred ct = ctEvPred (cc_ev ct)
+ctPred ct = ctEvPred (ctEvidence ct)
ctEvId :: Ct -> EvVar
-- The evidence Id for this Ct
@@ -1823,7 +1847,7 @@ ctEqRel :: Ct -> EqRel
ctEqRel = ctEvEqRel . ctEvidence
instance Outputable Ct where
- ppr ct = ppr (cc_ev ct) <+> parens pp_sort
+ ppr ct = ppr (ctEvidence ct) <+> parens pp_sort
where
pp_sort = case ct of
CTyEqCan {} -> text "CTyEqCan"
@@ -1836,6 +1860,9 @@ instance Outputable Ct where
| insol -> text "CIrredCan(insol)"
| otherwise -> text "CIrredCan(sol)"
CHoleCan { cc_hole = hole } -> text "CHoleCan:" <+> ppr hole
+ CQuantCan (QCI { qci_pend_sc = pend_sc })
+ | pend_sc -> text "CQuantCan(psc)"
+ | otherwise -> text "CQuantCan"
{-
************************************************************************
@@ -1866,9 +1893,7 @@ tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk })
= tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk
`unionFV` tyCoFVsOfType (tyVarKind fsk)
tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys
-tyCoFVsOfCt (CIrredCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
-tyCoFVsOfCt (CHoleCan { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
-tyCoFVsOfCt (CNonCanonical { cc_ev = ev }) = tyCoFVsOfType (ctEvPred ev)
+tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct)
-- | Returns free variables of a bag of constraints as a non-deterministic
-- set. See Note [Deterministic FV] in FV.
@@ -2069,13 +2094,13 @@ NB: we keep *all* derived insolubles under some circumstances:
-}
isWantedCt :: Ct -> Bool
-isWantedCt = isWanted . cc_ev
+isWantedCt = isWanted . ctEvidence
isGivenCt :: Ct -> Bool
-isGivenCt = isGiven . cc_ev
+isGivenCt = isGiven . ctEvidence
isDerivedCt :: Ct -> Bool
-isDerivedCt = isDerived . cc_ev
+isDerivedCt = isDerived . ctEvidence
isCTyEqCan :: Ct -> Bool
isCTyEqCan (CTyEqCan {}) = True
@@ -2170,11 +2195,18 @@ isUserTypeErrorCt ct = case getUserTypeErrorMsg ct of
_ -> False
isPendingScDict :: Ct -> Maybe Ct
--- Says whether cc_pend_sc is True, AND if so flips the flag
+-- Says whether this is a CDictCan with cc_pend_sc is True,
+-- AND if so flips the flag
isPendingScDict ct@(CDictCan { cc_pend_sc = True })
= Just (ct { cc_pend_sc = False })
isPendingScDict _ = Nothing
+isPendingScInst :: QCInst -> Maybe QCInst
+-- Same as isPrendinScDict, but for QCInsts
+isPendingScInst qci@(QCI { qci_pend_sc = True })
+ = Just (qci { qci_pend_sc = False })
+isPendingScInst _ = Nothing
+
setPendingScDict :: Ct -> Ct
-- Set the cc_pend_sc flag to True
setPendingScDict ct@(CDictCan { cc_pend_sc = False })
@@ -2722,8 +2754,12 @@ ctEvEqRel = predTypeEqRel . ctEvPred
ctEvRole :: CtEvidence -> Role
ctEvRole = eqRelRole . ctEvEqRel
+ctEvTerm :: CtEvidence -> EvTerm
+ctEvTerm ev = EvExpr (ctEvExpr ev)
+
ctEvExpr :: CtEvidence -> EvExpr
-ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
+ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ })
+ = Coercion $ ctEvCoercion ev
ctEvExpr ev = evId (ctEvEvId ev)
ctEvCoercion :: CtEvidence -> Coercion
@@ -2856,7 +2892,7 @@ ctFlavourRole (CFunEqCan { cc_ev = ev })
ctFlavourRole (CHoleCan { cc_ev = ev })
= (ctEvFlavour ev, NomEq)
ctFlavourRole ct
- = ctEvFlavourRole (cc_ev ct)
+ = ctEvFlavourRole (ctEvidence ct)
{- Note [eqCanRewrite]
~~~~~~~~~~~~~~~~~~~~~~
@@ -3224,6 +3260,9 @@ data SkolemInfo
| ReifySkol -- Bound during Template Haskell reification
+ | QuantCtxtSkol -- Quantified context, e.g.
+ -- f :: forall c. (forall a. c a => c [a]) => blah
+
| UnkSkol -- Unhelpful info (until I improve it)
instance Outputable SkolemInfo where
@@ -3253,6 +3292,8 @@ pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaratio
pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name)
pprSkolInfo ReifySkol = text "the type being reified"
+pprSkolInfo (QuantCtxtSkol {}) = text "a quantified context"
+
-- UnkSkol
-- For type variables the others are dealt with by pprSkolTvBinding.
-- For Insts, these cases should not happen
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index d26275b83976665508df20fc1cd06b49540ece29..9814358c7430218dbcb68748cbad226b01bf9747 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -16,10 +16,13 @@ module TcSMonad (
TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds,
failTcS, warnTcS, addErrTcS,
runTcSEqualities,
- nestTcS, nestImplicTcS, setEvBindsTcS, checkConstraintsTcS,
+ nestTcS, nestImplicTcS, setEvBindsTcS,
+ checkConstraintsTcS, checkTvConstraintsTcS,
runTcPluginTcS, addUsedGRE, addUsedGREs,
+ QCInst(..),
+
-- Tracing etc
panicTcS, traceTcS,
traceFireTcS, bumpStepCountTcS, csTraceTcS,
@@ -33,8 +36,8 @@ module TcSMonad (
newWanted, newWantedEvVar, newWantedNC, newWantedEvVarNC, newDerivedNC,
newBoundEvVarId,
unifyTyVar, unflattenFmv, reportUnifications,
- setEvBind, setWantedEq, setEqIfWanted,
- setWantedEvTerm, setWantedEvBind, setEvBindIfWanted,
+ setEvBind, setWantedEq,
+ setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars,
emitNewDeriveds, emitNewDerivedEq,
checkReductionDepth,
@@ -53,10 +56,10 @@ module TcSMonad (
getInertEqs, getInertCans, getInertGivens,
getInertInsols,
getTcSInerts, setTcSInerts,
- matchableGivens, prohibitedSuperClassSolve,
+ matchableGivens, prohibitedSuperClassSolve, mightMatchLater,
getUnsolvedInerts,
removeInertCts, getPendingScDicts,
- addInertCan, addInertEq, insertFunEq,
+ addInertCan, insertFunEq, addInertForAll,
emitWorkNC, emitWork,
isImprovable,
@@ -137,6 +140,7 @@ import Kind
import TcType
import DynFlags
import Type
+import TyCoRep( coHoleCoVar )
import Coercion
import Unify
@@ -168,7 +172,7 @@ import Control.Monad
import qualified Control.Monad.Fail as MonadFail
import MonadUtils
import Data.IORef
-import Data.List ( foldl', partition )
+import Data.List ( foldl', partition, mapAccumL )
#if defined(DEBUG)
import Digraph
@@ -438,17 +442,22 @@ instance Outputable InertSet where
where
dicts = bagToList (dictsToBag solved_dicts)
+emptyInertCans :: InertCans
+emptyInertCans
+ = IC { inert_count = 0
+ , inert_eqs = emptyDVarEnv
+ , inert_dicts = emptyDicts
+ , inert_safehask = emptyDicts
+ , inert_funeqs = emptyFunEqs
+ , inert_insts = []
+ , inert_irreds = emptyCts }
+
emptyInert :: InertSet
emptyInert
- = IS { inert_cans = IC { inert_count = 0
- , inert_eqs = emptyDVarEnv
- , inert_dicts = emptyDicts
- , inert_safehask = emptyDicts
- , inert_funeqs = emptyFunEqs
- , inert_irreds = emptyCts }
- , inert_flat_cache = emptyExactFunEqs
- , inert_fsks = []
- , inert_solved_dicts = emptyDictMap }
+ = IS { inert_cans = emptyInertCans
+ , inert_fsks = []
+ , inert_flat_cache = emptyExactFunEqs
+ , inert_solved_dicts = emptyDictMap }
{- Note [Solved dictionaries]
@@ -480,6 +489,12 @@ Other notes about solved dictionaries
* THe inert_solved_dicts are all Wanteds, never givens
+* We only cache dictionaries from top-level instances, not from
+ local quantified constraints. Reason: if we cached the latter
+ we'd need to purge the cache when bringing new quantified
+ constraints into scope, because quantified constraints "shadow"
+ top-level instances.
+
Note [Do not add superclasses of solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Every member of inert_solved_dicts is the result of applying a dictionary
@@ -639,6 +654,8 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- All fully rewritten (modulo flavour constraints)
-- wrt inert_eqs
+ , inert_insts :: [QCInst]
+
, inert_safehask :: DictMap Ct
-- Failed dictionary resolution due to Safe Haskell overlapping
-- instances restriction. We keep this separate from inert_dicts
@@ -995,6 +1012,7 @@ instance Outputable InertCans where
ppr (IC { inert_eqs = eqs
, inert_funeqs = funeqs, inert_dicts = dicts
, inert_safehask = safehask, inert_irreds = irreds
+ , inert_insts = insts
, inert_count = count })
= braces $ vcat
[ ppUnless (isEmptyDVarEnv eqs) $
@@ -1008,6 +1026,8 @@ instance Outputable InertCans where
text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
, ppUnless (isEmptyCts irreds) $
text "Irreds =" <+> pprCts irreds
+ , ppUnless (null insts) $
+ text "Given instances =" <+> vcat (map ppr insts)
, text "Unsolved goals =" <+> int count
]
@@ -1455,6 +1475,45 @@ equalities arising from injectivity.
-}
+{- *********************************************************************
+* *
+ Inert instances: inert_insts
+* *
+********************************************************************* -}
+
+addInertForAll :: QCInst -> TcS ()
+-- Add a local Given instance, typically arising from a type signature
+addInertForAll qci
+ = updInertCans $ \ics ->
+ ics { inert_insts = qci : inert_insts ics }
+
+{- Note [Local instances and incoherence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f :: forall b c. (Eq b, forall a. Eq a => Eq (c a))
+ => c b -> Bool
+ f x = x==x
+
+We get [W] Eq (c b), and we must use the local instance to solve it.
+
+BUT that wanted also unifies with the top-level Eq [a] instance,
+and Eq (Maybe a) etc. We want the local instance to "win", otherwise
+we can't solve the wanted at all. So we mark it as Incohherent.
+According to Note [Rules for instance lookup] in InstEnv, that'll
+make it win even if there are other instances that unify.
+
+Moreover this is not a hack! The evidence for this local instance
+will be constructed by GHC at a call site... from the very instances
+that unify with it here. It is not like an incoherent user-written
+instance which might have utterly different behaviour.
+
+Consdider f :: Eq a => blah. If we have [W] Eq a, we certainly
+get it from the Eq a context, without worrying that there are
+lots of top-level instances that unify with [W] Eq a! We'll use
+those instances to build evidence to pass to f. That's just the
+nullary case of what's happening here.
+-}
+
{- *********************************************************************
* *
Adding an inert
@@ -1495,43 +1554,37 @@ So in kickOutRewritable we look at all the tyvars of the
CFunEqCan, including the fsk.
-}
-addInertEq :: Ct -> TcS ()
--- This is a key function, because of the kick-out stuff
+addInertCan :: Ct -> TcS () -- Constraints *other than* equalities
-- Precondition: item /is/ canonical
-- See Note [Adding an equality to the InertCans]
-addInertEq ct
- = do { traceTcS "addInertEq {" $
- text "Adding new inert equality:" <+> ppr ct
-
- ; ics <- getInertCans
-
- ; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel })
- <- maybeEmitShadow ics ct
-
- ; (_, ics1) <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
-
- ; let ics2 = ics1 { inert_eqs = addTyEq (inert_eqs ics1) tv ct
- , inert_count = bumpUnsolvedCount ev (inert_count ics1) }
- ; setInertCans ics2
-
- ; traceTcS "addInertEq }" $ empty }
-
---------------
-addInertCan :: Ct -> TcS () -- Constraints *other than* equalities
addInertCan ct
= do { traceTcS "insertInertCan {" $
- text "Trying to insert new non-eq inert item:" <+> ppr ct
+ text "Trying to insert new inert item:" <+> ppr ct
; ics <- getInertCans
- ; ct <- maybeEmitShadow ics ct
+ ; ct <- maybeEmitShadow ics ct
+ ; ics <- maybeKickOut ics ct
; setInertCans (add_item ics ct)
; traceTcS "addInertCan }" $ empty }
+maybeKickOut :: InertCans -> Ct -> TcS InertCans
+-- For a CTyEqCan, kick out any inert that can be rewritten by the CTyEqCan
+maybeKickOut ics ct
+ | CTyEqCan { cc_tyvar = tv, cc_ev = ev, cc_eq_rel = eq_rel } <- ct
+ = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) tv ics
+ ; return ics' }
+ | otherwise
+ = return ics
+
add_item :: InertCans -> Ct -> InertCans
add_item ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys })
= ics { inert_funeqs = insertFunEq (inert_funeqs ics) tc tys item }
+add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev })
+ = ics { inert_eqs = addTyEq (inert_eqs ics) tv item
+ , inert_count = bumpUnsolvedCount ev (inert_count ics) }
+
add_item ics@(IC { inert_irreds = irreds, inert_count = count })
item@(CIrredCan { cc_ev = ev, cc_insol = insoluble })
= ics { inert_irreds = irreds `Bag.snocBag` item
@@ -1545,8 +1598,7 @@ add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
add_item _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
- ppr item -- CTyEqCan is dealt with by addInertEq
- -- Can't be CNonCanonical, CHoleCan,
+ ppr item -- Can't be CNonCanonical, CHoleCan,
-- because they only land in inert_irreds
bumpUnsolvedCount :: CtEvidence -> Int -> Int
@@ -1580,12 +1632,14 @@ kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that
-> InertCans
-> (WorkList, InertCans)
-- See Note [kickOutRewritable]
-kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
- , inert_dicts = dictmap
- , inert_safehask = safehask
- , inert_funeqs = funeqmap
- , inert_irreds = irreds
- , inert_count = n })
+kick_out_rewritable new_fr new_tv
+ ics@(IC { inert_eqs = tv_eqs
+ , inert_dicts = dictmap
+ , inert_safehask = safehask
+ , inert_funeqs = funeqmap
+ , inert_irreds = irreds
+ , inert_insts = old_insts
+ , inert_count = n })
| not (new_fr `eqMayRewriteFR` new_fr)
= (emptyWorkList, ics)
-- If new_fr can't rewrite itself, it can't rewrite
@@ -1601,6 +1655,7 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
, inert_safehask = safehask -- ??
, inert_funeqs = feqs_in
, inert_irreds = irs_in
+ , inert_insts = insts_in
, inert_count = n - workListWantedCount kicked_out }
kicked_out :: WorkList
@@ -1613,7 +1668,8 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
kicked_out = foldrBag extendWorkListCt
(emptyWorkList { wl_eqs = tv_eqs_out
, wl_funeqs = feqs_out })
- (dicts_out `andCts` irs_out)
+ ((dicts_out `andCts` irs_out)
+ `extendCtsList` insts_out)
(tv_eqs_out, tv_eqs_in) = foldDVarEnv kick_out_eqs ([], emptyDVarEnv) tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
@@ -1624,6 +1680,22 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs = tv_eqs
-- Of course we must kick out irreducibles like (c a), in case
-- we can rewrite 'c' to something more useful
+ -- Kick-out for inert instances
+ -- See Note [Quantified constraints] in TcCanonical
+ insts_out :: [Ct]
+ insts_in :: [QCInst]
+ (insts_out, insts_in)
+ | fr_may_rewrite (Given, NomEq) -- All the insts are Givens
+ = partitionWith kick_out_qci old_insts
+ | otherwise
+ = ([], old_insts)
+ kick_out_qci qci
+ | let ev = qci_ev qci
+ , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
+ = Left (mkNonCanonical ev)
+ | otherwise
+ = Right qci
+
(_, new_role) = new_fr
fr_can_rewrite_ty :: EqRel -> Type -> Bool
@@ -1868,14 +1940,17 @@ getPendingScDicts :: TcS [Ct]
-- Set the flag to False in the inert set, and return that Ct
getPendingScDicts = updRetInertCans get_sc_dicts
where
- get_sc_dicts ic@(IC { inert_dicts = dicts })
- = (sc_pend_dicts, ic')
+ get_sc_dicts ic@(IC { inert_dicts = dicts, inert_insts = insts })
+ = (sc_pend_insts ++ sc_pend_dicts, ic')
where
- ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts }
+ ic' = ic { inert_dicts = foldr add dicts sc_pend_dicts
+ , inert_insts = insts' }
sc_pend_dicts :: [Ct]
sc_pend_dicts = foldDicts get_pending dicts []
+ (sc_pend_insts, insts') = mapAccumL get_pending_inst [] insts
+
get_pending :: Ct -> [Ct] -> [Ct] -- Get dicts with cc_pend_sc = True
-- but flipping the flag
get_pending dict dicts
@@ -1887,6 +1962,13 @@ getPendingScDicts = updRetInertCans get_sc_dicts
= addDict dicts cls tys ct
add ct _ = pprPanic "getPendingScDicts" (ppr ct)
+ get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst)
+ get_pending_inst cts qci
+ | Just qci' <- isPendingScInst qci
+ = (CQuantCan qci' : cts, qci')
+ | otherwise
+ = (cts, qci)
+
getUnsolvedInerts :: TcS ( Bag Implication
, Cts -- Tyvar eqs: a ~ ty
, Cts -- Fun eqs: F a ~ ty
@@ -1995,7 +2077,7 @@ getNoGivenEqs tclvl skol_tvs
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in TcInteract.
matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred (IS { inert_cans = inert_cans })
+matchableGivens loc_w pred_w (IS { inert_cans = inert_cans })
= filterBag matchable_given all_relevant_givens
where
-- just look in class constraints and irreds. matchableGivens does get called
@@ -2004,7 +2086,7 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
-- non-canonical -- that is, irreducible -- equalities.
all_relevant_givens :: Cts
all_relevant_givens
- | Just (clas, _) <- getClassPredTys_maybe pred
+ | Just (clas, _) <- getClassPredTys_maybe pred_w
= findDictsByClass (inert_dicts inert_cans) clas
`unionBags` inert_irreds inert_cans
| otherwise
@@ -2012,16 +2094,17 @@ matchableGivens loc_w pred (IS { inert_cans = inert_cans })
matchable_given :: Ct -> Bool
matchable_given ct
- | CtGiven { ctev_loc = loc_g } <- ctev
- , Just _ <- tcUnifyTys bind_meta_tv [ctEvPred ctev] [pred]
- , not (prohibitedSuperClassSolve loc_g loc_w)
- = True
+ | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
+ = mightMatchLater pred_g loc_g pred_w loc_w
| otherwise
= False
- where
- ctev = cc_ev ct
+mightMatchLater :: TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+mightMatchLater given_pred given_loc wanted_pred wanted_loc
+ = not (prohibitedSuperClassSolve given_loc wanted_loc)
+ && isJust (tcUnifyTys bind_meta_tv [given_pred] [wanted_pred])
+ where
bind_meta_tv :: TcTyVar -> BindFlag
-- Any meta tyvar may be unified later, so we treat it as
-- bindable when unifying with givens. That ensures that we
@@ -2134,6 +2217,7 @@ removeInertCt is ct =
CTyEqCan { cc_tyvar = x, cc_rhs = ty } ->
is { inert_eqs = delTyEq (inert_eqs is) x ty }
+ CQuantCan {} -> panic "removeInertCt: CQuantCan"
CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
CHoleCan {} -> panic "removeInertCt: CHoleCan"
@@ -2662,9 +2746,10 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside)
, tcs_count = count
} ->
do { inerts <- TcM.readTcRef old_inert_var
- ; let nest_inert = emptyInert { inert_cans = inert_cans inerts
- , inert_solved_dicts = inert_solved_dicts inerts }
- -- See Note [Do not inherit the flat cache]
+ ; let nest_inert = emptyInert
+ { inert_cans = inert_cans inerts
+ , inert_solved_dicts = inert_solved_dicts inerts }
+ -- See Note [Do not inherit the flat cache]
; new_inert_var <- TcM.newTcRef nest_inert
; new_wl_var <- TcM.newTcRef emptyWorkList
; let nest_env = TcSEnv { tcs_ev_binds = ref
@@ -2724,28 +2809,30 @@ nestTcS (TcS thing_inside)
; return res }
-checkConstraintsTcS :: SkolemInfo
- -> [TcTyVar] -- Skolems
- -> TcS result
- -> TcS result
--- Just like TcUnify.checkTvConstraints, but in the TcS monnad,
--- using the work-list to gather the constraints
-checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
+checkTvConstraintsTcS :: SkolemInfo
+ -> [TcTyVar] -- Skolems
+ -> TcS (result, Cts)
+ -> TcS result
+-- Just like TcUnify.checkTvConstraints, but
+-- - In the TcS monnad
+-- - The thing-inside should not put things in the work-list
+-- Instead, it returns the Wanted constraints it needs
+-- - No 'givens', and no TcEvBinds; this is type-level constraints only
+checkTvConstraintsTcS skol_info skol_tvs (TcS thing_inside)
= TcS $ \ tcs_env ->
- do { new_wl_var <- TcM.newTcRef emptyWorkList
- ; let new_tcs_env = tcs_env { tcs_worklist = new_wl_var }
+ do { let wl_panic = pprPanic "TcSMonad.buildImplication" $
+ ppr skol_info $$ ppr skol_tvs
+ -- This panic checks that the thing-inside
+ -- does not emit any work-list constraints
+ new_tcs_env = tcs_env { tcs_worklist = wl_panic }
- ; (res, new_tclvl) <- TcM.pushTcLevelM $
- thing_inside new_tcs_env
+ ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $
+ thing_inside new_tcs_env
- ; wl@WL { wl_eqs = eqs } <- TcM.readTcRef new_wl_var
- ; ASSERT2( null (wl_funeqs wl) && null (wl_rest wl) &&
- null (wl_implics wl), ppr wl )
- unless (null eqs) $
+ ; unless (null wanteds) $
do { tcl_env <- TcM.getLclEnv
; ev_binds_var <- TcM.newNoTcEvBinds
- ; let wc = WC { wc_simple = listToCts eqs
- , wc_impl = emptyBag }
+ ; let wc = emptyWC { wc_simple = wanteds }
imp = newImplication { ic_tclvl = new_tclvl
, ic_skols = skol_tvs
, ic_wanted = wc
@@ -2759,6 +2846,47 @@ checkConstraintsTcS skol_info skol_tvs (TcS thing_inside)
; return res }
+checkConstraintsTcS :: SkolemInfo
+ -> [TcTyVar] -- Skolems
+ -> [EvVar] -- Givens
+ -> TcS (result, Cts)
+ -> TcS (result, TcEvBinds)
+-- Just like checkConstraintsTcS, but
+-- - In the TcS monnad
+-- - The thing-inside should not put things in the work-list
+-- Instead, it returns the Wanted constraints it needs
+-- - I did not bother to put in the fast-path for
+-- empty-skols/empty-givens, or for empty-wanteds, because
+-- this function is used only for "quantified constraints" in
+-- with both tests are pretty much guaranteed to fail
+checkConstraintsTcS skol_info skol_tvs given (TcS thing_inside)
+ = TcS $ \ tcs_env ->
+ do { let wl_panic = pprPanic "TcSMonad.buildImplication" $
+ ppr skol_info $$ ppr skol_tvs
+ -- This panic checks that the thing-inside
+ -- does not emit any work-list constraints
+ new_tcs_env = tcs_env { tcs_worklist = wl_panic }
+
+ ; ((res, wanteds), new_tclvl) <- TcM.pushTcLevelM $
+ thing_inside new_tcs_env
+
+ ; tcl_env <- TcM.getLclEnv
+ ; ev_binds_var <- TcM.newTcEvBinds
+ ; let wc = emptyWC { wc_simple = wanteds }
+ imp = newImplication { ic_tclvl = new_tclvl
+ , ic_skols = skol_tvs
+ , ic_given = given
+ , ic_wanted = wc
+ , ic_binds = ev_binds_var
+ , ic_env = tcl_env
+ , ic_info = skol_info }
+
+ -- Add the implication to the work-list
+ ; TcM.updTcRef (tcs_worklist tcs_env)
+ (extendWorkListImplic (unitBag imp))
+
+ ; return (res, TcEvBinds ev_binds_var) }
+
{-
Note [Propagate the solved dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3076,7 +3204,7 @@ dischargeFunEq (CtGiven { ctev_evar = old_evar, ctev_loc = loc }) fsk co xi
dischargeFunEq ev@(CtWanted { ctev_dest = dest }) fmv co xi
= ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
- do { setWantedEvTerm dest (EvExpr (evCoercion co))
+ do { setWantedEvTerm dest (evCoercion co)
; unflattenFmv fmv xi
; n_kicked <- kickOutAfterUnification fmv
; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
@@ -3173,28 +3301,25 @@ setWantedEq (HoleDest hole) co
; wrapTcS $ TcM.fillCoercionHole hole co }
setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev)
--- | Equalities only
-setEqIfWanted :: CtEvidence -> Coercion -> TcS ()
-setEqIfWanted (CtWanted { ctev_dest = dest }) co = setWantedEq dest co
-setEqIfWanted _ _ = return ()
-
--- | Good for equalities and non-equalities
+-- | Good for both equalities and non-equalities
setWantedEvTerm :: TcEvDest -> EvTerm -> TcS ()
setWantedEvTerm (HoleDest hole) tm
- = do { let co = evTermCoercion tm
- ; useVars (coVarsOfCo co)
+ | Just co <- evTermCoercion_maybe tm
+ = do { useVars (coVarsOfCo co)
; wrapTcS $ TcM.fillCoercionHole hole co }
-setWantedEvTerm (EvVarDest ev) tm = setWantedEvBind ev tm
+ | otherwise
+ = do { let co_var = coHoleCoVar hole
+ ; setEvBind (mkWantedEvBind co_var tm)
+ ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) }
-setWantedEvBind :: EvVar -> EvTerm -> TcS ()
-setWantedEvBind ev_id tm = setEvBind (mkWantedEvBind ev_id tm)
+setWantedEvTerm (EvVarDest ev_id) tm
+ = setEvBind (mkWantedEvBind ev_id tm)
-setEvBindIfWanted :: CtEvidence -> EvExpr -> TcS ()
+setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS ()
setEvBindIfWanted ev tm
= case ev of
- CtWanted { ctev_dest = dest }
- -> setWantedEvTerm dest (EvExpr tm)
- _ -> return ()
+ CtWanted { ctev_dest = dest } -> setWantedEvTerm dest tm
+ _ -> return ()
newTcEvBinds :: TcS EvBindsVar
newTcEvBinds = wrapTcS TcM.newTcEvBinds
@@ -3205,7 +3330,7 @@ newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds
newEvVar :: TcPredType -> TcS EvVar
newEvVar pred = wrapTcS (TcM.newEvVar pred)
-newGivenEvVar :: CtLoc -> (TcPredType, EvExpr) -> TcS CtEvidence
+newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS CtEvidence
-- Make a new variable of the given PredType,
-- immediately bind it to the given term
-- and return its CtEvidence
@@ -3216,13 +3341,13 @@ newGivenEvVar loc (pred, rhs)
-- | Make a new 'Id' of the given type, bound (in the monad's EvBinds) to the
-- given term
-newBoundEvVarId :: TcPredType -> EvExpr -> TcS EvVar
+newBoundEvVarId :: TcPredType -> EvTerm -> TcS EvVar
newBoundEvVarId pred rhs
= do { new_ev <- newEvVar pred
; setEvBind (mkGivenEvBind new_ev rhs)
; return new_ev }
-newGivenEvVars :: CtLoc -> [(TcPredType, EvExpr)] -> TcS [CtEvidence]
+newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence]
newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index e6c00aea4a5d392631522febb3dd70d49b3fa34d..bd04fd5b9c4d493a81332c1f1c9ea30372a815a9 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -254,7 +254,7 @@ defaultCallStacks wanteds
defaultCallStack ct
| ClassPred cls tys <- classifyPredType (ctPred ct)
, Just {} <- isCallStackPred cls tys
- = do { solveCallStack (cc_ev ct) EvCsEmpty
+ = do { solveCallStack (ctEvidence ct) EvCsEmpty
; return Nothing }
defaultCallStack ct
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index f5f7532075389c7dd3fa1d61533edd7ea3ff292a..21d030c060ada862bd39e617c718ec2c8753c6a7 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1718,7 +1718,7 @@ tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
-- df :: forall m. (forall b. Eq b => Eq (m b)) -> C m
--
-- Also NB splitFunTys, not tcSplitFunTys;
--- the latter specifically stops at PredTy arguments,
+-- the latter specifically stops at PredTy arguments,
-- and we don't want to do that here
tcSplitDFunTy ty
= case tcSplitForAllTys ty of { (tvs, rho) ->
@@ -1990,6 +1990,7 @@ pickQuantifiablePreds qtvs theta
EqPred NomEq ty1 ty2 -> quant_fun ty1 || quant_fun ty2
IrredPred ty -> tyCoVarsOfType ty `intersectsVarSet` qtvs
+ ForAllPred {} -> False
pick_cls_pred flex_ctxt cls tys
= tyCoVarsOfTypes tys `intersectsVarSet` qtvs
@@ -2094,6 +2095,7 @@ isImprovementPred ty
EqPred ReprEq _ _ -> False
ClassPred cls _ -> classHasFds cls
IrredPred {} -> True -- Might have equalities after reduction?
+ ForAllPred {} -> False
{- Note [Expanding superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index ab31e2ef7f55d6f5a9ba29b601dc4dd86f8b78b9..1e15f658bdd79df8740f658758574b512d9e3a6e 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -10,7 +10,7 @@ module TcValidity (
ContextKind(..), expectedKindInCtxt,
checkValidTheta, checkValidFamPats,
checkValidInstance, checkValidInstHead, validDerivPred,
- checkInstTermination, checkTySynRhs,
+ checkTySynRhs,
ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
checkValidTyFamEqn,
arityErr, badATErr,
@@ -441,7 +441,8 @@ rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank
rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes or Rank2Types")
tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism")
synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms")
-constraintMonoType = MonoType (text "A constraint must be a monotype")
+constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype"
+ , text "Perhaps you intended to use QuantifiedConstraints" ])
funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result
funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank)
@@ -727,8 +728,13 @@ check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
-- Check the validity of a predicate in a signature
-- See Note [Validity checking for constraints]
check_pred_ty env dflags ctxt pred
- = do { check_type env SigmaCtxt constraintMonoType pred
+ = do { check_type env SigmaCtxt rank pred
; check_pred_help False env dflags ctxt pred }
+ where
+ rank | xopt LangExt.QuantifiedConstraints dflags
+ = ArbitraryRank
+ | otherwise
+ = constraintMonoType
check_pred_help :: Bool -- True <=> under a type synonym
-> TidyEnv
@@ -1334,7 +1340,7 @@ checkValidInstance ctxt hs_type ty
; undecidable_ok <- xoptM LangExt.UndecidableInstances
; if undecidable_ok
then checkAmbiguity ctxt ty
- else checkInstTermination inst_tys theta
+ else checkInstTermination theta tau
; traceTc "cvi 2" (ppr ty)
@@ -1376,42 +1382,50 @@ The underlying idea is that
context has fewer type constructors than the head.
-}
-checkInstTermination :: [TcType] -> ThetaType -> TcM ()
+checkInstTermination :: ThetaType -> TcPredType -> TcM ()
-- See Note [Paterson conditions]
-checkInstTermination tys theta
- = check_preds theta
+checkInstTermination theta head_pred
+ = check_preds emptyVarSet theta
where
- head_fvs = fvTypes tys
- head_size = sizeTypes tys
+ head_fvs = fvType head_pred
+ head_size = sizeType head_pred
- check_preds :: [PredType] -> TcM ()
- check_preds preds = mapM_ check preds
+ check_preds :: VarSet -> [PredType] -> TcM ()
+ check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds
- check :: PredType -> TcM ()
- check pred
+ check :: VarSet -> PredType -> TcM ()
+ check foralld_tvs pred
= case classifyPredType pred of
EqPred {} -> return () -- See Trac #4200.
- IrredPred {} -> check2 pred (sizeType pred)
+ IrredPred {} -> check2 foralld_tvs pred (sizeType pred)
ClassPred cls tys
| isTerminatingClass cls
-> return ()
| isCTupleClass cls -- Look inside tuple predicates; Trac #8359
- -> check_preds tys
+ -> check_preds foralld_tvs tys
+
+ | otherwise -- Other ClassPreds
+ -> check2 foralld_tvs pred bogus_size
+ where
+ bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys)
+ -- See Note [Invisible arguments and termination]
- | otherwise
- -> check2 pred (sizeTypes $ filterOutInvisibleTypes (classTyCon cls) tys)
- -- Other ClassPreds
+ ForAllPred tvs theta pred
+ -> do { check (foralld_tvs `extendVarSetList` binderVars tvs) pred
+ ; checkInstTermination theta pred }
- check2 pred pred_size
+ check2 foralld_tvs pred pred_size
| not (null bad_tvs) = addErrTc (noMoreMsg bad_tvs what)
| not (isTyFamFree pred) = addErrTc (nestedMsg what)
- | pred_size >= head_size = addErrTc (smallerMsg what)
+ | pred_size >= head_size = traceTc "check2" (ppr pred $$ ppr pred_size $$ ppr head_pred $$ ppr head_size)
+ >> addErrTc (smallerMsg what)
| otherwise = return ()
-- isTyFamFree: see Note [Type families in instance contexts]
where
what = text "constraint" <+> quotes (ppr pred)
- bad_tvs = fvType pred \\ head_fvs
+ bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred)
+ \\ head_fvs
smallerMsg :: SDoc -> SDoc
smallerMsg what
@@ -1557,6 +1571,20 @@ Here the instance is kind-indexed and really looks like
type F (k->k) (b::k->k) = Int
But if the 'b' didn't scope, we would make F's instance too
poly-kinded.
+
+Note [Invisible arguments and termination]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When checking the ​Paterson conditions for termination an instance
+declaration, we check for the number of "constructors and variables"
+in the instance head and constraints. Question: Do we look at
+
+ * All the arguments, visible or invisible?
+ * Just the visible arguments?
+
+I think both will ensure termination, provided we are consistent.
+Currently we are /not/ consistent, which is really a bug. It's
+described in Trac #15177, which contains a number of examples.
+The suspicious bits are the calls to filterOutInvisibleTypes.
-}
-- | Extra information about the parent instance declaration, needed
@@ -1753,30 +1781,33 @@ checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs pp_lhs loc
-- We have a decidable instance unless otherwise permitted
; undecidable_ok <- xoptM LangExt.UndecidableInstances
+ ; traceTc "checkVTFE" (pp_lhs $$ ppr rhs $$ ppr (tcTyFamInsts rhs))
; unless undecidable_ok $
- mapM_ addErrTc (checkFamInstRhs typats (tcTyFamInsts rhs)) }
+ mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) }
-- Make sure that each type family application is
-- (1) strictly smaller than the lhs,
-- (2) mentions no type variable more often than the lhs, and
-- (3) does not contain any further type family instances.
--
-checkFamInstRhs :: [Type] -- lhs
- -> [(TyCon, [Type])] -- type family instances
+checkFamInstRhs :: TyCon -> [Type] -- LHS
+ -> [(TyCon, [Type])] -- type family calls in RHS
-> [MsgDoc]
-checkFamInstRhs lhsTys famInsts
+checkFamInstRhs tc lhsTys famInsts
= mapMaybe check famInsts
where
- size = sizeTypes lhsTys
- fvs = fvTypes lhsTys
+ lhs_size = sizeTyConAppArgs tc lhsTys
+ fvs = fvTypes lhsTys
check (tc, tys)
| not (all isTyFamFree tys) = Just (nestedMsg what)
| not (null bad_tvs) = Just (noMoreMsg bad_tvs what)
- | size <= sizeTypes tys = Just (smallerMsg what)
+ | lhs_size <= fam_app_size = Just (smallerMsg what)
| otherwise = Nothing
where
- what = text "type family application" <+> quotes (pprType (TyConApp tc tys))
- bad_tvs = fvTypes tys \\ fvs
+ what = text "type family application"
+ <+> quotes (pprType (TyConApp tc tys))
+ bad_tvs = fvTypes tys \\ fvs
+ fam_app_size = sizeTyConAppArgs tc tys
checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
-> [Type] -- ^ patterns the user wrote
@@ -1974,7 +2005,7 @@ sizeType :: Type -> Int
-- Size of a type: the number of variables and constructors
sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
sizeType (TyVarTy {}) = 1
-sizeType (TyConApp _ tys) = sizeTypes tys + 1
+sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys
sizeType (LitTy {}) = 1
sizeType (AppTy fun arg) = sizeType fun + sizeType arg
sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
@@ -1983,16 +2014,17 @@ sizeType (CastTy ty _) = sizeType ty
sizeType (CoercionTy _) = 1
sizeTypes :: [Type] -> Int
-sizeTypes = sum . map sizeType
+sizeTypes = foldr ((+) . sizeType) 0
+
+sizeTyConAppArgs :: TyCon -> [Type] -> Int
+sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys)
+ -- See Note [Invisible arguments and termination]
-- Size of a predicate
--
-- We are considering whether class constraints terminate.
-- Equality constraints and constraints for the implicit
-- parameter class always terminate so it is safe to say "size 0".
--- (Implicit parameter constraints always terminate because
--- there are no instances for them---they are only solved by
--- "local instances" in expressions).
-- See Trac #4200.
sizePred :: PredType -> Int
sizePred ty = goClass ty
@@ -2002,14 +2034,19 @@ sizePred ty = goClass ty
go (ClassPred cls tys')
| isTerminatingClass cls = 0
| otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys')
- go (EqPred {}) = 0
- go (IrredPred ty) = sizeType ty
+ -- The filtering looks bogus
+ -- See Note [Invisible arguments and termination]
+ go (EqPred {}) = 0
+ go (IrredPred ty) = sizeType ty
+ go (ForAllPred _ _ pred) = goClass pred
-- | When this says "True", ignore this class constraint during
-- a termination check
isTerminatingClass :: Class -> Bool
isTerminatingClass cls
- = isIPClass cls
+ = isIPClass cls -- Implicit parameter constraints always terminate because
+ -- there are no instances for them --- they are only solved
+ -- by "local instances" in expressions
|| cls `hasKey` typeableClassKey
|| cls `hasKey` coercibleTyConKey
|| cls `hasKey` eqTyConKey
diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs
index aa95f13ac3a8b8accd0152ab8a0220548df3fd32..a50135bd7ba37c1413198e0692e0a11db1fd93f1 100644
--- a/compiler/types/Class.hs
+++ b/compiler/types/Class.hs
@@ -17,7 +17,7 @@ module Class (
mkClass, mkAbstractClass, classTyVars, classArity,
classKey, className, classATs, classATItems, classTyCon, classMethods,
classOpItems, classBigSig, classExtraBigSig, classTvsFds, classSCTheta,
- classAllSelIds, classSCSelId, classMinimalDef, classHasFds,
+ classAllSelIds, classSCSelId, classSCSelIds, classMinimalDef, classHasFds,
isAbstractClass,
) where
@@ -107,23 +107,23 @@ data ClassBody
-- Superclasses: eg: (F a ~ b, F b ~ G a, Eq a, Show b)
-- We need value-level selectors for both the dictionary
-- superclasses and the equality superclasses
- classSCThetaStuff :: [PredType], -- Immediate superclasses,
- classSCSels :: [Id], -- Selector functions to extract the
+ cls_sc_theta :: [PredType], -- Immediate superclasses,
+ cls_sc_sel_ids :: [Id], -- Selector functions to extract the
-- superclasses from a
-- dictionary of this class
-- Associated types
- classATStuff :: [ClassATItem], -- Associated type families
+ cls_ats :: [ClassATItem], -- Associated type families
-- Class operations (methods, not superclasses)
- classOpStuff :: [ClassOpItem], -- Ordered by tag
+ cls_ops :: [ClassOpItem], -- Ordered by tag
-- Minimal complete definition
- classMinimalDefStuff :: ClassMinimalDef
+ cls_min_def :: ClassMinimalDef
}
-- TODO: maybe super classes should be allowed in abstract class definitions
classMinimalDef :: Class -> ClassMinimalDef
-classMinimalDef Class{ classBody = ConcreteClass{ classMinimalDefStuff = d } } = d
+classMinimalDef Class{ classBody = ConcreteClass{ cls_min_def = d } } = d
classMinimalDef _ = mkTrue -- TODO: make sure this is the right direction
{-
@@ -181,11 +181,11 @@ mkClass cls_name tyvars fds super_classes superdict_sels at_stuff
classTyVars = tyvars,
classFunDeps = fds,
classBody = ConcreteClass {
- classSCThetaStuff = super_classes,
- classSCSels = superdict_sels,
- classATStuff = at_stuff,
- classOpStuff = op_stuff,
- classMinimalDefStuff = mindef
+ cls_sc_theta = super_classes,
+ cls_sc_sel_ids = superdict_sels,
+ cls_ats = at_stuff,
+ cls_ops = op_stuff,
+ cls_min_def = mindef
},
classTyCon = tycon }
@@ -239,41 +239,47 @@ classArity clas = length (classTyVars clas)
classAllSelIds :: Class -> [Id]
-- Both superclass-dictionary and method selectors
-classAllSelIds c@(Class { classBody = ConcreteClass { classSCSels = sc_sels }})
+classAllSelIds c@(Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels }})
= sc_sels ++ classMethods c
classAllSelIds c = ASSERT( null (classMethods c) ) []
+classSCSelIds :: Class -> [Id]
+-- Both superclass-dictionary and method selectors
+classSCSelIds (Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels }})
+ = sc_sels
+classSCSelIds c = ASSERT( null (classMethods c) ) []
+
classSCSelId :: Class -> Int -> Id
-- Get the n'th superclass selector Id
-- where n is 0-indexed, and counts
-- *all* superclasses including equalities
-classSCSelId (Class { classBody = ConcreteClass { classSCSels = sc_sels } }) n
+classSCSelId (Class { classBody = ConcreteClass { cls_sc_sel_ids = sc_sels } }) n
= ASSERT( n >= 0 && lengthExceeds sc_sels n )
sc_sels !! n
classSCSelId c n = pprPanic "classSCSelId" (ppr c <+> ppr n)
classMethods :: Class -> [Id]
-classMethods (Class { classBody = ConcreteClass { classOpStuff = op_stuff } })
+classMethods (Class { classBody = ConcreteClass { cls_ops = op_stuff } })
= [op_sel | (op_sel, _) <- op_stuff]
classMethods _ = []
classOpItems :: Class -> [ClassOpItem]
-classOpItems (Class { classBody = ConcreteClass { classOpStuff = op_stuff }})
+classOpItems (Class { classBody = ConcreteClass { cls_ops = op_stuff }})
= op_stuff
classOpItems _ = []
classATs :: Class -> [TyCon]
-classATs (Class { classBody = ConcreteClass { classATStuff = at_stuff } })
+classATs (Class { classBody = ConcreteClass { cls_ats = at_stuff } })
= [tc | ATI tc _ <- at_stuff]
classATs _ = []
classATItems :: Class -> [ClassATItem]
-classATItems (Class { classBody = ConcreteClass { classATStuff = at_stuff }})
+classATItems (Class { classBody = ConcreteClass { cls_ats = at_stuff }})
= at_stuff
classATItems _ = []
classSCTheta :: Class -> [PredType]
-classSCTheta (Class { classBody = ConcreteClass { classSCThetaStuff = theta_stuff }})
+classSCTheta (Class { classBody = ConcreteClass { cls_sc_theta = theta_stuff }})
= theta_stuff
classSCTheta _ = []
@@ -289,9 +295,9 @@ classBigSig (Class {classTyVars = tyvars,
= (tyvars, [], [], [])
classBigSig (Class {classTyVars = tyvars,
classBody = ConcreteClass {
- classSCThetaStuff = sc_theta,
- classSCSels = sc_sels,
- classOpStuff = op_stuff
+ cls_sc_theta = sc_theta,
+ cls_sc_sel_ids = sc_sels,
+ cls_ops = op_stuff
}})
= (tyvars, sc_theta, sc_sels, op_stuff)
@@ -301,8 +307,8 @@ classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
= (tyvars, fundeps, [], [], [], [])
classExtraBigSig (Class {classTyVars = tyvars, classFunDeps = fundeps,
classBody = ConcreteClass {
- classSCThetaStuff = sc_theta, classSCSels = sc_sels,
- classATStuff = ats, classOpStuff = op_stuff
+ cls_sc_theta = sc_theta, cls_sc_sel_ids = sc_sels,
+ cls_ats = ats, cls_ops = op_stuff
}})
= (tyvars, fundeps, sc_theta, sc_sels, ats, op_stuff)
diff --git a/compiler/types/InstEnv.hs b/compiler/types/InstEnv.hs
index 6f065e9ec520424694e12ec2c9a56d02f686a8df..d05294b197e04a948cb8a8be7b561afe8e9b29fc 100644
--- a/compiler/types/InstEnv.hs
+++ b/compiler/types/InstEnv.hs
@@ -18,9 +18,12 @@ module InstEnv (
fuzzyClsInstCmp, orphNamesOfClsInst,
InstEnvs(..), VisibleOrphanModules, InstEnv,
- emptyInstEnv, extendInstEnv, deleteFromInstEnv, identicalClsInstHead,
+ emptyInstEnv, extendInstEnv,
+ deleteFromInstEnv, deleteDFunFromInstEnv,
+ identicalClsInstHead,
extendInstEnvList, lookupUniqueInstEnv, lookupInstEnv, instEnvElts,
- memberInstEnv, instIsVisible,
+ memberInstEnv,
+ instIsVisible,
classInstances, instanceBindFun,
instanceCantMatch, roughMatchTcs,
isOverlappable, isOverlapping, isIncoherent
@@ -432,11 +435,11 @@ instIsVisible vis_mods ispec
-- NB: Instances from the interactive package always are visible. We can't
-- add interactive modules to the set since we keep creating new ones
-- as a GHCi session progresses.
- | isInteractiveModule mod = True
- | IsOrphan <- is_orphan ispec = mod `elemModuleSet` vis_mods
- | otherwise = True
- where
- mod = nameModule $ is_dfun_name ispec
+ = case nameModule_maybe (is_dfun_name ispec) of
+ Nothing -> True
+ Just mod | isInteractiveModule mod -> True
+ | IsOrphan <- is_orphan ispec -> mod `elemModuleSet` vis_mods
+ | otherwise -> True
classInstances :: InstEnvs -> Class -> [ClsInst]
classInstances (InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = vis_mods }) cls
@@ -471,6 +474,15 @@ deleteFromInstEnv inst_env ins_item@(ClsInst { is_cls_nm = cls_nm })
where
adjust (ClsIE items) = ClsIE (filterOut (identicalClsInstHead ins_item) items)
+deleteDFunFromInstEnv :: InstEnv -> DFunId -> InstEnv
+-- Delete a specific instance fron an InstEnv
+deleteDFunFromInstEnv inst_env dfun
+ = adjustUDFM adjust inst_env cls
+ where
+ (_, _, cls, _) = tcSplitDFunTy (idType dfun)
+ adjust (ClsIE items) = ClsIE (filterOut same_dfun items)
+ same_dfun (ClsInst { is_dfun = dfun' }) = dfun == dfun'
+
identicalClsInstHead :: ClsInst -> ClsInst -> Bool
-- ^ True when when the instance heads are the same
-- e.g. both are Eq [(a,b)]
@@ -549,23 +561,38 @@ instance declaration itself, controlled as follows:
Now suppose that, in some client module, we are searching for an instance
of the target constraint (C ty1 .. tyn). The search works like this.
- * Find all instances I that match the target constraint; that is, the
- target constraint is a substitution instance of I. These instance
- declarations are the candidates.
+* Find all instances `I` that *match* the target constraint; that is, the
+ target constraint is a substitution instance of `I`. These instance
+ declarations are the *candidates*.
+
+* Eliminate any candidate `IX` for which both of the following hold:
- * Find all non-candidate instances that unify with the target
- constraint. Such non-candidates instances might match when the
- target constraint is further instantiated. If all of them are
- incoherent, proceed; if not, the search fails.
+ - There is another candidate `IY` that is strictly more specific; that
+ is, `IY` is a substitution instance of `IX` but not vice versa.
- * Eliminate any candidate IX for which both of the following hold:
- * There is another candidate IY that is strictly more specific;
- that is, IY is a substitution instance of IX but not vice versa.
+ - Either `IX` is *overlappable*, or `IY` is *overlapping*. (This
+ "either/or" design, rather than a "both/and" design, allow a
+ client to deliberately override an instance from a library,
+ without requiring a change to the library.)
- * Either IX is overlappable or IY is overlapping.
+- If exactly one non-incoherent candidate remains, select it. If all
+ remaining candidates are incoherent, select an arbitrary one.
+ Otherwise the search fails (i.e. when more than one surviving
+ candidate is not incoherent).
- * If only one candidate remains, pick it. Otherwise if all remaining
- candidates are incoherent, pick an arbitrary candidate. Otherwise fail.
+- If the selected candidate (from the previous step) is incoherent, the
+ search succeeds, returning that candidate.
+
+- If not, find all instances that *unify* with the target constraint,
+ but do not *match* it. Such non-candidate instances might match when
+ the target constraint is further instantiated. If all of them are
+ incoherent, the search succeeds, returning the selected candidate; if
+ not, the search fails.
+
+Notice that these rules are not influenced by flag settings in the
+client module, where the instances are *used*. These rules make it
+possible for a library author to design a library that relies on
+overlapping instances without the client having to know.
Note [Overlapping instances] (NB: these notes are quite old)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -676,7 +703,7 @@ prematurely chosing a generic instance when a more specific one
exists.
--Jeff
-v
+
BUT NOTE [Nov 2001]: we must actually *unify* not reverse-match in
this test. Suppose the instance envt had
..., forall a b. C a a b, ..., forall a b c. C a b c, ...
@@ -741,7 +768,8 @@ lookupInstEnv' :: InstEnv -- InstEnv to look in
-> VisibleOrphanModules -- But filter against this
-> Class -> [Type] -- What we are looking for
-> ([InstMatch], -- Successful matches
- [ClsInst]) -- These don't match but do unify
+ [ClsInst]) -- These don't match but do unify
+ -- (no incoherent ones in here)
-- The second component of the result pair happens when we look up
-- Foo [a]
-- in an InstEnv that has entries for
@@ -778,7 +806,8 @@ lookupInstEnv' ie vis_mods cls tys
= find ((item, map (lookupTyVar subst) tpl_tvs) : ms) us rest
-- Does not match, so next check whether the things unify
- -- See Note [Overlapping instances] and Note [Incoherent instances]
+ -- See Note [Overlapping instances]
+ -- Ignore ones that are incoherent: Note [Incoherent instances]
| isIncoherent item
= find ms us rest
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index 88ed114fe638de93066c12f4a2bbe3bd63558bcc..58e38f267e0279149b5551913c8650a720838689 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -95,6 +95,8 @@ returnsConstraintKind = returnsTyCon constraintKindTyConKey
-- | Tests whether the given kind (which should look like @TYPE x@)
-- is something other than a constructor tree (that is, constructors at every node).
+-- E.g. True of TYPE k, TYPE (F Int)
+-- False of TYPE 'LiftedRep
isKindLevPoly :: Kind -> Bool
isKindLevPoly k = ASSERT2( isStarKind k || _is_type, ppr k )
-- the isStarKind check is necessary b/c of Constraint
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 99632088094d307838532b81eaacb1c997902bed..8450cd2f84bcfdf2eb067605e991cd40bf36983f 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1726,9 +1726,12 @@ eqRelRole :: EqRel -> Role
eqRelRole NomEq = Nominal
eqRelRole ReprEq = Representational
-data PredTree = ClassPred Class [Type]
- | EqPred EqRel Type Type
- | IrredPred PredType
+data PredTree
+ = ClassPred Class [Type]
+ | EqPred EqRel Type Type
+ | IrredPred PredType
+ | ForAllPred [TyVarBinder] [PredType] PredType
+ -- ForAllPred: see Note [Quantified constraints] in TcCanonical
-- NB: There is no TuplePred case
-- Tuple predicates like (Eq a, Ord b) are just treated
-- as ClassPred, as if we had a tuple class with two superclasses
@@ -1737,11 +1740,20 @@ data PredTree = ClassPred Class [Type]
classifyPredType :: PredType -> PredTree
classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
Just (tc, [_, _, ty1, ty2])
- | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
- | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
+ | tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
+ | tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
+
Just (tc, tys)
- | Just clas <- tyConClass_maybe tc -> ClassPred clas tys
- _ -> IrredPred ev_ty
+ | Just clas <- tyConClass_maybe tc
+ -> ClassPred clas tys
+
+ _ | (tvs, rho) <- splitForAllTyVarBndrs ev_ty
+ , (theta, pred) <- splitFunTys rho
+ , not (null tvs && null theta)
+ -> ForAllPred tvs theta pred
+
+ | otherwise
+ -> IrredPred ev_ty
getClassPredTys :: HasDebugCallStack => PredType -> (Class, [Type])
getClassPredTys ty = case getClassPredTys_maybe ty of
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 8b99d624e11ec5c877ad60f813fca8d7dfbcb65b..9395cbbe553ac817d6d20d0ce46d309c523913ba 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9407,8 +9407,8 @@ the type level:
GHC.TypeLits> natVal (lg (Proxy :: Proxy 2) (Proxy :: Proxy 8))
3
-Constraints in types
-====================
+Equality constraints, Coercible, and the kind Constraint
+========================================================
.. _equality-constraints:
@@ -9567,6 +9567,262 @@ contexts and superclasses, but to do so you must use
:extension:`UndecidableInstances` to signal that you don't mind if the type
checker fails to terminate.
+Quantified constraints
+======================
+
+The extension :extension:`QuantifiedConstraints` introduces **quantified constraints**,
+which give a new level of expressiveness in constraints. For example, consider ::
+
+ data Rose f a = Branch a (f (Rose f a))
+
+ instance (Eq a, ???) => Eq (Rose f a)
+ where
+ (Branch x1 c1) == (Branch x2 c2)
+ = x1==x1 && c1==c2
+
+From the ``x1==x2`` we need ``Eq a``, which is fine. From ``c1==c2`` we need ``Eq (f (Rose f a))`` which
+is *not* fine in Haskell today; we have no way to solve such a constraint.
+
+:extension:`QuantifiedConstraints` lets us write this ::
+
+ instance (Eq a, forall b. (Eq b) => Eq (f b))
+ => Eq (Rose f a)
+ where
+ (Branch x1 c1) == (Branch x2 c2)
+ = x1==x1 && c1==c2
+
+Here, the quantified constraint ``forall b. (Eq b) => Eq (f b)`` behaves
+a bit like a local instance declaration, and makes the instance typeable.
+
+The paper `Quantified class constraints <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_ (by Bottu, Karachalias, Schrijvers, Oliveira, Wadler, Haskell Symposium 2017) describes this feature in technical detail, with examples, and so is a primary reference source for this proposal.
+
+Motivation
+----------------
+Introducing quantified constraints offers two main benefits:
+
+- Firstly, they enable terminating resolution where this was not possible before. Consider for instance the following instance declaration for the general rose datatype ::
+
+ 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
+
+ This extension allows to write constraints of the form ``forall b. Eq b => Eq (f b)``,
+ which is needed to solve the ``Eq (f (Rose f x))`` constraint arising from the
+ second usage of the ``(==)`` method.
+
+- Secondly, quantified constraints allow for more concise and precise specifications. As an example, consider the MTL type class for monad transformers::
+
+ class Trans t where
+ lift :: Monad m => m a -> (t m) a
+
+ The developer knows that a monad transformer takes a monad ``m`` into a new monad ``t m``.
+ But this is property is not formally specified in the above declaration.
+ This omission becomes an issue when defining monad transformer composition::
+
+ newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
+
+ instance (Trans t1, Trans t2) => Trans (t1 * t2) where
+ lift = C . lift . lift
+
+ The goal here is to ``lift`` from monad ``m`` to ``t2 m`` and
+ then ``lift`` this again into ``t1 (t2 m)``.
+ However, this second ``lift`` can only be accepted when ``(t2 m)`` is a monad
+ and there is no way of establishing that this fact universally holds.
+
+ Quantified constraints enable this property to be made explicit in the ``Trans``
+ class declaration::
+
+ class (forall m. Monad m => Monad (t m)) => Trans t where
+ lift :: Monad m => m a -> (t m) a
+
+THe idea is very old; see Seciton 7 of `Derivable type classes <https://www.microsoft.com/en-us/research/publication/derivable-type-classes/>`_.
+
+Syntax changes
+----------------
+
+`Haskell 2010 <https://www.haskell.org/onlinereport/haskell2010/haskellch10.html#x17-18000010.5>`_ defines a ``context`` (the bit to the left of ``=>`` in a type) like this ::
+
+ context ::= class
+ | ( class1, ..., classn )
+
+ class ::= qtycls tyvar
+ | qtycls (tyvar atype1 ... atypen)
+
+We to extend ``class`` (warning: this is a rather confusingly named non-terminal symbol) with two extra forms, namely precisely what can appear in an instance declaration ::
+
+ class ::= ...
+ | context => qtycls inst
+ | context => tyvar inst
+
+The definition of ``inst`` is unchanged from the Haskell Report (roughly, just a type).
+That is the only syntactic change to the language.
+
+Notes:
+
+- Where GHC allows extensions instance declarations we allow exactly the same extensions to this new form of ``class``. Specifically, with ``ExplicitForAll`` and ``MultiParameterTypeClasses`` the syntax becomes ::
+
+ class ::= ...
+ | [forall tyavrs .] context => qtycls inst1 ... instn
+ | [forall tyavrs .] context => tyvar inst1 ... instn
+
+ Note that an explicit ``forall`` is often absolutely essential. Consider the rose-tree example ::
+
+ instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
+
+ Without the ``forall b``, the type variable ``b`` would be quantified over the whole instance declaration, which is not what is intended.
+
+- One of these new quantified constraints can appear anywhere that any other constraint can, not just in instance declarations. Notably, it can appear in a type signature for a value binding, data constructor, or expression. For example ::
+
+ f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a -> Rose f a -> Bool
+ f t1 t2 = not (t1 == t2)
+
+- The form with a type variable at the head allows this::
+
+ instance (forall xx. c (Free c xx)) => Monad (Free c) where
+ Free f >>= g = f g
+
+ See `Iceland Jack's summary <https://ghc.haskell.org/trac/ghc/ticket/14733#comment:6>`_. The key point is that the bit to the right of the `=>` may be headed by a type *variable* (`c` in this case), rather than a class. It should not be one of the forall'd variables, though.
+
+ (NB: this goes beyond what is described in `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but does not seem to introduce any new technical difficulties.)
+
+
+Typing changes
+----------------
+
+See `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_.
+
+Superclasses
+----------------
+
+Suppose we have::
+
+ f :: forall m. (forall a. Ord a => Ord (m a)) => m Int -> Bool
+ f x = x == x
+
+From the ``x==x`` we need an ``Eq (m Int)`` constraint, but the context only gives us a way to figure out ``Ord (m a)`` constraints. But from the given constraint ``forall a. Ord a => Ord (m a)`` we derive a second given constraint ``forall a. Ord a => Eq (m a)``, and from that we can readily solve ``Eq (m Int)``. This process is very similar to the way that superclasses already work: given an ``Ord a`` constraint we derive a second given ``Eq a`` constraint.
+
+NB: This treatment of superclasses goes beyond `the paper <http://i.cs.hku.hk/~bruno//papers/hs2017.pdf>`_, but is specifically desired by users.
+
+Overlap
+-------------
+
+Quantified constraints can potentially lead to overlapping local axioms.
+Consider for instance the following example::
+
+ class A a where {}
+ class B a where {}
+ class C a where {}
+ class (A a => C a) => D a where {}
+ class (B a => C a) => E a where {}
+
+ class C a => F a where {}
+ instance (B a, D a, E a) => F a where {}
+
+When type checking the instance declaration for ``F a``,
+we need to check that the superclass ``C`` of ``F`` holds.
+We thus try to entail the constraint ``C a`` under the theory containing:
+
+- The instance axioms : ``(B a, D a, E a) => F a``
+- The local axioms from the instance context : ``B a``, ``D a`` and ``E a``
+- The closure of the superclass relation over these local axioms : ``A a => C a`` and ``B a => C a``
+
+However, the ``A a => C a`` and ``B a => C a`` axioms both match the wanted constraint ``C a``.
+There are several possible approaches for handling these overlapping local axioms:
+
+- **Pick first**. We can simply select the **first matching axiom** we encounter.
+ In the above example, this would be ``A a => C a``.
+ We'd then need to entail ``A a``, for which we have no matching axioms available, causing the above program to be rejected.
+
+ But suppose we made a slight adjustment to the order of the instance context, putting ``E a`` before ``D a``::
+
+ instance (B a, E a, D a) => F a where {}
+
+ The first matching axiom we encounter while entailing ``C a``, is ``B a => C a``.
+ We have a local axiom ``B a`` available, so now the program is suddenly accepted.
+ This behaviour, where the ordering of an instance context determines
+ whether or not the program is accepted, seems rather confusing for the developer.
+
+- **Reject if in doubt**. An alternative approach would be to check for overlapping axioms,
+ when solving a constraint.
+ When multiple matching axioms are discovered, we **reject the program**.
+ This approach is a bit conservative, in that it may reject working programs.
+ But it seem much more transparent towards the developer, who
+ can be presented with a clear message, explaining why the program is rejected.
+
+- **Backtracking**. Lastly, a simple form of **backtracking** could be introduced.
+ We simply select the first matching axiom we encounter and when the entailment fails,
+ we backtrack and look for other axioms that might match the wanted constraint.
+
+ This seems the most intuitive and transparent approach towards the developer,
+ who no longer needs to concern himself with the fact that his code might contain
+ overlapping axioms or with the ordering of his instance contexts. But backtracking
+ would apply equally to ordinary instance selection (in the presence of overlapping
+ instances), so it is a much more pervasive change, with substantial consequences
+ for the type inference engine.
+
+GHC adoptst **Reject if in doubt** for now. We can see how painful it
+is in practice, and try something more ambitious if necessary.
+
+Instance lookup
+-------------------
+
+In the light of the overlap decision, instance lookup works like this, when
+trying to solve a class constraint ``C t``
+
+1. First see if there is a given un-quantified constraint ``C t``. If so, use it to solve the constraint.
+
+2. If not, look at all the available given quantified constraints; if exactly one one matches ``C t``, choose it; if more than one matches, report an error.
+
+3. If no quantified constraints match, look up in the global instances, as described in :ref:`instance-resolution` and :ref:`instance-overlap`.
+
+Termination
+---------------
+
+GHC uses the `Paterson Conditions <http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#instance-termination-rules>`_ to ensure that instance resolution terminates:
+
+The Paterson Conditions are these: for each class constraint ``(C t1 ... tn)``
+in the context
+
+1. No type variable has more occurrences in the constraint than in
+ the head
+
+2. The constraint has fewer constructors and variables (taken
+ together and counting repetitions) than the head
+
+3. The constraint mentions no type functions. A type function
+ application can in principle expand to a type of arbitrary size,
+ and so are rejected out of hand
+
+How are those rules modified for quantified constraints? In two ways.
+
+- Each quantified constraint, taken by itself, must satisfy the termination rules for an instance declaration.
+
+- After "for each class constraint ``(C t1 ... tn)``", add "or each quantified constraint ``(forall as. context => C t1 .. tn)``"
+
+Note that the second item only at the *head* of the quantified constraint, not its context. Reason: the head is the new goal that has to be solved if we use the instance declaration.
+
+Of course, ``UndecidableInstances`` lifts the Paterson Conditions, as now.
+
+Coherence
+-----------
+
+Although quantified constraints are a little like local instance declarations, they differ
+in one big way: the local instances are written by the compiler, not the user, and hence
+cannot introduce incoherence. Consider ::
+
+ f :: (forall a. Eq a => Eq (f a)) => f b -> f Bool
+ f x = ...rhs...
+
+In ``...rhs...`` there is, in effect a local instance for ``Eq (f a)`` for any ``a``. But
+at a call site for ``f`` the compiler itself produces evidence to pass to ``f``. For example,
+if we called ``f Nothing``, then ``f`` is ``Maybe`` and the compiler must prove (at the
+call site) that ``forall a. Eq a => Eq (Maybe a)`` holds. It can do this easily, by
+appealing to the existing instance declaration for ``Eq (Maybe a)``.
+
+In short, quantifed constraints do not introduce incoherence.
+
+
.. _extensions-to-type-signatures:
Extensions to type signatures
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index b3016e167d2a404786b28fe4326ac1ad5cb99f03..e98c871ce46f4cdec766410955a3db2c365a3508 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -135,4 +135,5 @@ data Extension
| MonadFailDesugaring
| EmptyDataDeriving
| NumericUnderscores
+ | QuantifiedConstraints
deriving (Eq, Enum, Show, Generic)
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 5ae423086acedd52423ea01325daa2955a47cf7b..5ea91b47d615776ac5553674af18fe56d0ffcbbb 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -40,7 +40,8 @@ expectedGhcOnlyExtensions = ["RelaxedLayout",
"AlternativeLayoutRule",
"AlternativeLayoutRuleTransitional",
"EmptyDataDeriving",
- "GeneralisedNewtypeDeriving"]
+ "GeneralisedNewtypeDeriving",
+ "QuantifiedConstraints"]
expectedCabalOnlyExtensions :: [String]
expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/quantified-constraints/Makefile b/testsuite/tests/quantified-constraints/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..9a36a1c5fee5849898f7c20c59672b9268409e4a
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/quantified-constraints/T14833.hs b/testsuite/tests/quantified-constraints/T14833.hs
new file mode 100644
index 0000000000000000000000000000000000000000..43b6491def75002e6152b2cb4ff4b845cf60fbd9
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14833.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14833 where
+
+data Dict c where
+ Dict :: c => Dict c
+
+class (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+-- Works ok
+iota1 :: (() => a) => Dict a
+iota1 = Dict
+
+iota2 :: Implies () a => Dict a
+iota2 = Dict
+
+{-
+[G] Implies () a
+[G] (() => a) -- By superclass
+
+[W] a
+-}
diff --git a/testsuite/tests/quantified-constraints/T14835.hs b/testsuite/tests/quantified-constraints/T14835.hs
new file mode 100644
index 0000000000000000000000000000000000000000..de9b450b7c21b5c9bba83e9a1516e413a6a54df9
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14835.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+data Dict c where
+ Dict :: c => Dict c
+
+class (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+curryC1 :: ((a, b) => c) => Dict (Implies a (Implies b c))
+curryC1 = Dict
+
+curryC2 :: Implies (a, b) c => Dict (Implies a (Implies b c))
+curryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14863.hs b/testsuite/tests/quantified-constraints/T14863.hs
new file mode 100644
index 0000000000000000000000000000000000000000..35e1a14b4298583ac6a97e9bd8e3efd7e003acbb
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14863.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T14863 where
+
+data Dict c where
+ Dict :: c => Dict c
+
+class (a => b) => Implies a b
+instance (a => b) => Implies a b
+
+uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c)
+uncurryCImpredic1 = Dict
+
+uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c)
+uncurryCImpredic2 = Dict
+
+uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c)
+uncurryC1 = Dict
+
+uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c)
+uncurryC2 = Dict
diff --git a/testsuite/tests/quantified-constraints/T14961.hs b/testsuite/tests/quantified-constraints/T14961.hs
new file mode 100644
index 0000000000000000000000000000000000000000..6f15ceb572b9a1ea8763f4fbbb017e3cb6f5cae4
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T14961.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T14961 where
+
+import Data.Kind
+
+import Control.Arrow (left, right, (&&&), (|||))
+import Control.Category
+import Prelude hiding (id, (.))
+
+import Data.Coerce
+
+class (forall x. f x => g x) => f ~=> g
+instance (forall x. f x => g x) => f ~=> g
+
+type family (#) (p :: Type -> Type -> Type) (ab :: (Type, Type))
+ = (r :: Type) | r -> p ab where
+ p # '(a, b) = p a b
+
+newtype Glass
+ :: ((Type -> Type -> Type) -> Constraint)
+ -> (Type, Type) -> (Type, Type) -> Type where
+ Glass :: (forall p. z p => p # ab -> p # st) -> Glass z st ab
+
+data A_Prism
+
+type family ConstraintOf (tag :: Type)
+ = (r :: (Type -> Type -> Type) -> Constraint) where
+ ConstraintOf A_Prism = Choice
+
+_Left0
+ :: Glass Choice
+ '(Either a x, Either b x)
+ '(a, b)
+_Left0 = Glass left'
+
+_Left1
+ :: c ~=> Choice
+ => Glass c '(Either a x, Either b x) '(a, b)
+_Left1 = Glass left'
+
+-- fails with
+-- • Could not deduce (Choice p)
+-- _Left2
+-- :: (forall p. c p => ConstraintOf A_Prism p)
+-- => Glass c '(Either a x, Either b x) '(a, b)
+-- _Left2 = Glass left'
+
+_Left3
+ :: d ~ ConstraintOf A_Prism
+ => (forall p . c p => d p)
+ => Glass c
+ '(Either a x, Either b x)
+ '(a, b)
+_Left3 = Glass left'
+
+-- fails to typecheck unless at least a partial type signature is provided
+-- l :: c ~=> Choice => Glass c _ _
+-- l = _Left1 . _Left1
+
+newtype Optic o st ab where
+ Optic
+ :: (forall c d. (d ~ ConstraintOf o, c ~=> d) => Glass c st ab)
+ -> Optic o st ab
+
+_Left
+ :: Optic A_Prism
+ '(Either a x, Either b x)
+ '(a, b)
+_Left = Optic _Left1
+
+instance Category (Glass z) where
+ id :: Glass z a a
+ id = Glass id
+
+ (.) :: Glass z uv ab -> Glass z st uv -> Glass z st ab
+ Glass abuv . Glass uvst = Glass (uvst . abuv)
+
+class Profunctor (p :: Type -> Type -> Type) where
+ dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
+ lmap :: (a -> b) -> p b c -> p a c
+ rmap :: (b -> c) -> p a b -> p a c
+
+class Profunctor p => Choice (p :: Type -> Type -> Type) where
+ left' :: p a b -> p (Either a c) (Either b c)
+ right' :: p a b -> p (Either c a) (Either c b)
diff --git a/testsuite/tests/quantified-constraints/T2893.hs b/testsuite/tests/quantified-constraints/T2893.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ffec2cf72d22bac1d73f45d77a397958ecc249fe
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+-- Two simple examples that should work
+
+module T2893 where
+
+f :: forall b c. (Eq b, forall a. Eq a => Eq (c a)) => c b -> Bool
+{-# NOINLINE f #-}
+f x = x==x
+
+g x = f [x]
+
+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
diff --git a/testsuite/tests/quantified-constraints/T2893a.hs b/testsuite/tests/quantified-constraints/T2893a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..187029fdd50e556e5ebd68bba76bd20b371d0969
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893a.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE
+ GADTs
+ , FlexibleContexts
+ , RankNTypes
+ , ScopedTypeVariables
+ , QuantifiedConstraints #-}
+
+module T2893a where
+
+import Control.Monad.ST
+import Data.Array.ST
+
+sortM
+ :: forall a s.
+ (Ord a, MArray (STUArray s) a (ST s))
+ => [a]
+ -> ST s [a]
+sortM xs = do
+ arr <- newListArray (1, length xs) xs
+ :: ST s (STUArray s Int a)
+ -- do some in-place sorting here
+ getElems arr
+
+sortP_3
+ :: (Ord a, forall s. MArray (STUArray s) a (ST s))
+ => [a] -> [a]
+sortP_3 xs = runST (sortM xs)
diff --git a/testsuite/tests/quantified-constraints/T2893c.hs b/testsuite/tests/quantified-constraints/T2893c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..832d0f8428df7200fd1d02e01fb850c9e0bff88f
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T2893c.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T2893c where
+
+data Rose f x = Rose x (f (Rose f x))
+
+instance Eq a => Eq (Rose f a) where
+ (Rose x1 _) == (Rose x2 _) = x1==x2
+
+-- Needs superclasses
+instance (Ord a, forall b. Ord b => Ord (f b))
+ => Ord (Rose f a) where
+ (Rose x1 rs1) >= (Rose x2 rs2)
+ = x1 >= x2 && rs1 == rs2
+ a <= b = False -- Just to suppress the warning
diff --git a/testsuite/tests/quantified-constraints/T9123.hs b/testsuite/tests/quantified-constraints/T9123.hs
new file mode 100644
index 0000000000000000000000000000000000000000..130312b150d2a73907f7cc9185ba1085df7cc652
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE InstanceSigs, RoleAnnotations #-}
+
+module T9123 where
+
+import Data.Coerce
+
+type role Wrap representational nominal
+newtype Wrap m a = Wrap (m a)
+
+class Monad' m where
+ join' :: forall a. m (m a) -> m a
+
+-- Tests the superclass stuff
+instance (forall p q. Coercible p q => Coercible (m p) (m q), Monad' m) => Monad' (Wrap m) where
+ join' :: forall a. Wrap m (Wrap m a) -> Wrap m a
+ join' = coerce @(m (m a) -> m a)
+ @(Wrap m (Wrap m a) -> Wrap m a)
+ join'
+
diff --git a/testsuite/tests/quantified-constraints/T9123a.hs b/testsuite/tests/quantified-constraints/T9123a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..76379b6c008d2e547f72c61b54c26b5e2ab002e8
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T9123a.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE QuantifiedConstraints, PolyKinds, ScopedTypeVariables
+ , StandaloneDeriving, RoleAnnotations, TypeApplications
+ , UndecidableInstances, InstanceSigs
+ , GeneralizedNewtypeDeriving #-}
+
+module T9123a where
+
+import Data.Coerce
+
+class MyMonad m where
+ join :: m (m a) -> m a
+
+newtype StateT s m a = StateT (s -> m (a, s))
+
+type role StateT nominal representational nominal -- as inferred
+
+instance MyMonad m => MyMonad (StateT s m) where
+ join = error "urk" -- A good impl exists, but is not
+ -- of interest for this test case
+
+newtype IntStateT m a = IntStateT (StateT Int m a)
+
+type role IntStateT representational nominal -- as inferred
+
+instance (MyMonad m, forall p q. Coercible p q => Coercible (m p) (m q))
+ => MyMonad (IntStateT m) where
+ join :: forall a. IntStateT m (IntStateT m a) -> IntStateT m a
+ join = coerce @(StateT Int m (StateT Int m a) -> StateT Int m a)
+ @(IntStateT m (IntStateT m a) -> IntStateT m a)
+ join
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
new file mode 100644
index 0000000000000000000000000000000000000000..71f5b9159af53f125f95f704d0b5e9af80b78e2b
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -0,0 +1,10 @@
+
+test('T14833', normal, compile, [''])
+test('T14835', normal, compile, [''])
+test('T2893', normal, compile, [''])
+test('T2893a', normal, compile, [''])
+test('T2893c', normal, compile, [''])
+test('T9123', normal, compile, [''])
+test('T14863', normal, compile, [''])
+test('T14961', normal, compile, [''])
+test('T9123a', normal, compile, [''])
diff --git a/testsuite/tests/rebindable/T5908.hs b/testsuite/tests/rebindable/T5908.hs
index 32a4d4e5e7722d4305d7bfa43b620e7848ae4a61..2666c3371a18bdd27bb68bc93e0656c8b9a46bfb 100644
--- a/testsuite/tests/rebindable/T5908.hs
+++ b/testsuite/tests/rebindable/T5908.hs
@@ -26,7 +26,7 @@ class Monad m where
(>>) :: forall e ex x a b . m e ex a -> m ex x b -> m e x b
return :: a -> m ex ex a
fail :: String -> m e x a
-
+
{-# INLINE (>>) #-}
m >> k = m >>= \ _ -> k
fail = error
diff --git a/testsuite/tests/typecheck/should_compile/T14735.hs b/testsuite/tests/typecheck/should_compile/T14735.hs
new file mode 100644
index 0000000000000000000000000000000000000000..c48231b7c2b0710fd4f20d518b1c83eda3b71787
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14735.hs
@@ -0,0 +1,30 @@
+{-# Language QuantifiedConstraints #-}
+{-# Language StandaloneDeriving #-}
+{-# Language DataKinds #-}
+{-# Language TypeOperators #-}
+{-# Language GADTs #-}
+{-# Language KindSignatures #-}
+{-# Language FlexibleInstances #-}
+{-# Language UndecidableInstances #-}
+{-# Language MultiParamTypeClasses #-}
+{-# Language RankNTypes #-}
+{-# Language ConstraintKinds #-}
+
+module T14735 where
+
+import Data.Kind
+
+data D c where
+ D :: c => D c
+
+newtype a :- b = S (a => D b)
+
+class C1 a b
+class C2 a b
+instance C1 a b => C2 a b
+
+class (forall xx. f xx) => Limit f
+instance (forall xx. f xx) => Limit f
+
+impl :: Limit (C1 a) :- Limit (C2 a)
+impl = S D
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d130a6995027d34b8128fb0c6be0e5577736dcea..43282341cc96a40e11c68a602b8831139f251544 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -620,3 +620,5 @@ test('SplitWD', normal, compile, [''])
# with -prof using -osuf to set a different object file suffix.
test('T14441', omit_ways(['profasm']), compile, [''])
test('T15050', [expect_broken(15050)], compile, [''])
+test('T14735', normal, compile, [''])
+
diff --git a/testsuite/tests/typecheck/should_fail/T7019.stderr b/testsuite/tests/typecheck/should_fail/T7019.stderr
index 2db5bbb90bc541d068bf64f07fa64bd1f632d3cd..09827e458bb50f489df18eaf2ac7454ae22731f3 100644
--- a/testsuite/tests/typecheck/should_fail/T7019.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019.stderr
@@ -2,4 +2,5 @@
T7019.hs:11:1: error:
• Illegal polymorphic type: forall a. c (Free c a)
A constraint must be a monotype
+ Perhaps you intended to use QuantifiedConstraints
• In the type synonym declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T7019a.stderr b/testsuite/tests/typecheck/should_fail/T7019a.stderr
index a50fbcf240c33c86e7e07879262e2427d172c637..e0e0342b617b4b94e8454f4f8bb9b5a2a2acbf1e 100644
--- a/testsuite/tests/typecheck/should_fail/T7019a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7019a.stderr
@@ -2,6 +2,7 @@
T7019a.hs:11:1: error:
• Illegal polymorphic type: forall b. Context (Associated a b)
A constraint must be a monotype
+ Perhaps you intended to use QuantifiedConstraints
• In the context: forall b. Context (Associated a b)
While checking the super-classes of class ‘Class’
In the class declaration for ‘Class’
diff --git a/testsuite/tests/typecheck/should_fail/T9196.stderr b/testsuite/tests/typecheck/should_fail/T9196.stderr
index f843c70929caf7c295fca753249d9ea61914e131..d6ca149f23e58e82a37e761d633a31b560d39106 100644
--- a/testsuite/tests/typecheck/should_fail/T9196.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9196.stderr
@@ -2,11 +2,11 @@
T9196.hs:4:6: error:
• Illegal polymorphic type: forall a1. Eq a1
A constraint must be a monotype
- • In the type signature:
- f :: (forall a. Eq a) => a -> a
+ Perhaps you intended to use QuantifiedConstraints
+ • In the type signature: f :: (forall a. Eq a) => a -> a
T9196.hs:7:6: error:
• Illegal qualified type: Eq a => Ord a
A constraint must be a monotype
- • In the type signature:
- g :: (Eq a => Ord a) => a -> a
+ Perhaps you intended to use QuantifiedConstraints
+ • In the type signature: g :: (Eq a => Ord a) => a -> a