diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 73 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 66 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.hs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 2 | ||||
| -rw-r--r-- | compiler/types/Type.hs | 4 |
5 files changed, 92 insertions, 68 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 765abc7c47..2923dc53f7 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -541,12 +541,17 @@ mk_strict_superclasses rec_clss ev tvs theta cls tys mk_superclasses :: NameSet -> CtEvidence -> [TyVar] -> ThetaType -> PredType -> TcS [Ct] -- Return this constraint, plus its superclasses, if any +-- Precondition: ev :: forall tvs. theta => pred mk_superclasses rec_clss ev tvs theta pred - | ClassPred cls tys <- classifyPredType pred - = mk_superclasses_of rec_clss ev tvs theta cls tys + = case classifyPredType pred of + ClassPred cls tys -> mk_superclasses_of rec_clss ev tvs theta cls tys + ForAllPred tvs2 theta2 pred2 + -> do { given_ev <- newGivenEvVar (ctEvLoc ev) $ + (given_ty, mk_sc_sel evar sel_id) -- ***** workingf erhe *** - | otherwise -- Superclass is not a class predicate - = return [mkNonCanonical ev] + + _ -> -- Superclass is not a class predicate + return [mkNonCanonical ev] mk_superclasses_of :: NameSet -> CtEvidence -> [TyVar] -> ThetaType -> Class -> [Type] @@ -575,7 +580,8 @@ mk_superclasses_of rec_clss ev tvs theta cls tys -- 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 + = CQuantCan (QCI { qci_tvs = tvs + , qci_pred = mkClassPred cls tys , qci_ev = ev , qci_pend_sc = loop_found }) @@ -737,30 +743,20 @@ canForAll ev pend_sc let pred = ctEvPred ev ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + solveForAll new_ev pend_sc } - 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 +solveForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) -solveForAll ev tv_bndrs theta pred pend_sc +solveForAll ev 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) + do { let (tvs, theta, pred) = tcSplitSigmaTy (ctEvPred ev) + ; (skol_tvs, skol_theta, skol_pred) <- skolemiseQC tvs theta pred + ; given_ev_vars <- mapM newEvVar skol_theta ; (w_id, ev_binds) <- checkConstraintsTcS skol_info skol_tvs given_ev_vars $ - do { wanted_ev <- newWantedEvVarNC loc $ - substTy subst pred + do { wanted_ev <- newWantedEvVarNC loc skol_pred ; return ( ctEvEvId wanted_ev , unitBag (mkNonCanonical wanted_ev)) } @@ -771,16 +767,41 @@ solveForAll ev tv_bndrs theta pred pend_sc ; stopWith ev "Wanted forall-constraint" } | isGiven ev -- See Note [Solving a Given forall-constraint] - = do { addInertForAll qci + = do { qci <- mkQCI ev pend_sc + ; 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 } + +mkQCI :: CtEvidence -> Bool -> TcS Ct +-- Unwrap the predicate to expose the head +-- e.g. from (forall a. Eq a => forall b. Show b => C a b) +-- we expose the head (C a b) +mkQCI ev pend_sc + = go [] (ctEvPred ev) + where + go acc_tvs pred + | ForAllPred tvs theta body_pred <- classifyPredType pred + = do { (tvs', _, pred') <- skolemiseQC tvs theta body_pred + ; go (acc_tvs ++ tvs') pred' } + | otherwise + = return (QCI { qci_ev = ev + , qci_bndrs = acc_tvs + , qci_pred = pred + , qci_pend_sc = pend_sc } + +skolemiseQC :: [TcTyVar] -> TcThetaType -> TcPredType + -> TcS ([TcTyVar], ThetaType, TcPredType) +skolemiseQC tvs theta pred + = do { let skol_info = QuantCtxtSkol + empty_subst = mkEmptyTCvSubst $ mkInScopeSet $ + tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs + ; (subst, skol_tvs) <- tcInstSkolTyVarsX empty_subst tvs + ; return (skol_tvs, substTheta subst theta, substTy subst pred) } + {- Note [Solving a Wanted forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 3a80d5a62c..d9e717f48d 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -2280,46 +2280,44 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) +---------------------- chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct) -chooseInstance work_item - (OneInst { cir_new_theta = theta - , cir_what = what - , cir_mk_ev = mk_ev }) - = do { traceTcS "doTopReact/found instance for" $ ppr ev - ; deeper_loc <- checkInstanceOK loc what pred - ; if isDerived ev then finish_derived deeper_loc theta - else finish_wanted deeper_loc theta mk_ev } +-- Precondition: the ClsInstResult is always OneInst +chooseInstance work_item (OneInst { cir_new_theta = theta + , cir_what = what + , cir_mk_ev = mk_ev }) + | isDerived ev + = -- Use type-class instances for Deriveds, in the hope + -- of generating some improvements + -- C.f. Example 3 of Note [The improvement story] + -- It's easy because no evidence is involved + do { deeper_loc <- checkInstanceOK loc what pred + ; emitNewDeriveds deeper_loc theta + ; traceTcS "finish_derived" (ppr (ctl_depth loc) $$ ppr ev) + ; stopWith ev "Dict/Top (solved derived)" } + + | otherwise -- Wanted + = do { traceTcS "doTopReact/found wanted instance for" $ ppr ev + ; evb <- getTcEvBindsVar + ; if isCoEvBindsVar evb + then -- See Note [Instances in no-evidence implications] + continueWith work_item + else + do { deeper_loc <- checkInstanceOK loc what pred + ; evc_vars <- mapM (newWanted deeper_loc) theta + ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars)) + ; emitWorkNC (freshGoals evc_vars) + ; stopWith ev "Dict/Top (solved wanted)" } } + where - ev = ctEvidence work_item - pred = ctEvPred ev - loc = ctEvLoc ev - - finish_wanted :: CtLoc -> [TcPredType] - -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct) - -- Precondition: evidence term matches the predicate workItem - finish_wanted loc theta mk_ev - = do { evb <- getTcEvBindsVar - ; if isCoEvBindsVar evb - then -- See Note [Instances in no-evidence implications] - continueWith work_item - else - do { evc_vars <- mapM (newWanted loc) theta - ; setEvBindIfWanted ev (mk_ev (map getEvExpr evc_vars)) - ; emitWorkNC (freshGoals evc_vars) - ; stopWith ev "Dict/Top (solved wanted)" } } - - finish_derived loc theta - = -- Use type-class instances for Deriveds, in the hope - -- of generating some improvements - -- C.f. Example 3 of Note [The improvement story] - -- It's easy because no evidence is involved - do { emitNewDeriveds loc theta - ; traceTcS "finish_derived" (ppr (ctl_depth loc)) - ; stopWith ev "Dict/Top (solved derived)" } + ev = ctEvidence work_item + pred = ctEvPred ev + loc = ctEvLoc ev chooseInstance work_item lookup_res = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res) +---------------------- checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc -- Check that it's OK to use this insstance: -- (a) the use is well staged in the Template Haskell sense diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index bfedaf2ccc..bee1a8d13d 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1752,12 +1752,17 @@ data Ct ------------ 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 { qci_ev :: CtEvidence -- Always Given + -- Always of type forall tvs. ctxt => qci_pred + + , qci_bndrs :: [TcTcVar] -- Binders for tvs1, ctxt2, tvs2, etc + -- The tyvars among them scope over qci_pred + + , qci_pred :: TcPredType -- The predicate in the body + -- Can be ClassPred or IrredPred, but not ForAllPred + , qci_pend_sc :: Bool -- Same as cc_pend_sc flag in CDictCan - -- Invariant: True => qci_pred is a ClassPred + -- Invariant: True => qci_pred is a ClassPred } instance Outputable QCInst where diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index b267547dd7..01cd42e498 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1917,7 +1917,7 @@ checkInstTermination theta head_pred -- See Note [Invisible arguments and termination] ForAllPred tvs _ head_pred' - -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred' + -> check (foralld_tvs `extendVarSetList` tvs) head_pred' -- Termination of the quantified predicate itself is checked -- when the predicates are individually checked for validity diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 4426148967..bbd9b0ab08 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -1998,7 +1998,7 @@ data PredTree = ClassPred Class [Type] | EqPred EqRel Type Type | IrredPred PredType - | ForAllPred [TyCoVarBinder] [PredType] PredType + | ForAllPred [TyVar] [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 @@ -2015,7 +2015,7 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of | Just clas <- tyConClass_maybe tc -> ClassPred clas tys - _ | (tvs, rho) <- splitForAllVarBndrs ev_ty + _ | (tvs, rho) <- splitForAllTys ev_ty , (theta, pred) <- splitFunTys rho , not (null tvs && null theta) -> ForAllPred tvs theta pred |