From c80364f8e4681b34e974f5df36ecdacec7cd9cd8 Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Fri, 12 Nov 2010 13:00:11 +0000 Subject: [PATCH] A (final) re-engineering of the new typechecker Regression testing and user feedback for GHC 7.0 taught us a lot. This patch fixes numerous small bugs, and some major ones (eg Trac #4484, #4492), and improves type error messages. The main changes are: * Entirely remove the "skolem equivalance class" stuff; a very useful simplification * Instead, when flattening "wanted" constraints we generate unification variables (not flatten-skolems) for the flattened type function application * We then need a fixup pass at the end, TcSimplify.solveCTyFunEqs, which resolves any residual equalities of form F xi ~ alpha * When we come across a definite failure (e.g. Int ~ [a]), we now defer reporting the error until the end, in case we learn more about 'a'. That is particularly important for occurs-check errors. These are called "frozen" type errors. * Other improvements in error message generation. * Better tracing messages --- compiler/typecheck/Inst.lhs | 8 +- compiler/typecheck/TcCanonical.lhs | 382 ++++++++++++--------- compiler/typecheck/TcErrors.lhs | 259 ++++++++------ compiler/typecheck/TcInteract.lhs | 659 ++++++++++-------------------------- compiler/typecheck/TcRnTypes.lhs | 17 +- compiler/typecheck/TcSMonad.lhs | 247 +++++++++----- compiler/typecheck/TcSimplify.lhs | 331 +++++++++++++----- compiler/typecheck/TcType.lhs | 3 + compiler/types/Coercion.lhs | 4 +- 9 files changed, 1007 insertions(+), 903 deletions(-) diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs index 3a419be..e1f3fb7 100644 --- a/compiler/typecheck/Inst.lhs +++ b/compiler/typecheck/Inst.lhs @@ -473,11 +473,9 @@ hasEqualities :: [EvVar] -> Bool -- Has a bunch of canonical constraints (all givens) got any equalities in it? hasEqualities givens = any (has_eq . evVarPred) givens where - has_eq (EqPred {}) = True - has_eq (IParam {}) = False - has_eq (ClassP cls tys) = any has_eq (substTheta subst (classSCTheta cls)) - where - subst = zipOpenTvSubst (classTyVars cls) tys + has_eq (EqPred {}) = True + has_eq (IParam {}) = False + has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls) ---------------- tyVarsOfWanteds :: WantedConstraints -> TyVarSet diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index 8f25f7e..ffe0a7e 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -1,7 +1,6 @@ \begin{code} module TcCanonical( - mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, - canEq, canEqLeafTyVarLeft + mkCanonical, mkCanonicals, canWanteds, canGivens, canOccursCheck, canEq, ) where #include "HsVersions.h" @@ -26,6 +25,8 @@ import Control.Applicative ( (<|>) ) import VarSet import Bag +import HsBinds + import Control.Monad ( unless ) import TcSMonad -- The TcS Monad \end{code} @@ -77,15 +78,6 @@ NB: Flattening Skolems only occur in canonical constraints, which are never zonked, so we don't need to worry about zonking doing accidental unflattening. -NB: Note that (unlike the OutsideIn(X) draft of 7 May 2010) we are -actually doing the SAME thing here no matter whether we are flattening -a wanted or a given constraint. In both cases we simply generate some -flattening skolem variables and some extra given constraints; we never -generate actual unification variables or non-identity coercions. -Hopefully this will work, although SPJ had some vague worries about -unification variables from wanted constraints finding their way into -the generated given constraints...? - Note that we prefer to leave type synonyms unexpanded when possible, so when the flattener encounters one, it first asks whether its transitive expansion contains any type function applications. If so, @@ -99,104 +91,121 @@ multiple times. \begin{code} -- Flatten a bunch of types all at once. -flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], CanonicalCts) +flattenMany :: CtFlavor -> [Type] -> TcS ([Xi], [Coercion], CanonicalCts) +-- Coercions :: Xi ~ Type flattenMany ctxt tys - = do { (xis, cts_s) <- mapAndUnzipM (flatten ctxt) tys - ; return (xis, andCCans cts_s) } + = do { (xis, cos, cts_s) <- mapAndUnzip3M (flatten ctxt) tys + ; return (xis, cos, andCCans cts_s) } -- Flatten a type to get rid of type function applications, returning -- the new type-function-free type, and a collection of new equality --- constraints. See Note [Flattening] for more detail. This needs to --- be in the TcS monad so we can generate new flattening skolem --- variables. -flatten :: CtFlavor -> TcType -> TcS (Xi, CanonicalCts) - +-- constraints. See Note [Flattening] for more detail. +flatten :: CtFlavor -> TcType -> TcS (Xi, Coercion, CanonicalCts) +-- Postcondition: Coercion :: Xi ~ TcType flatten ctxt ty | Just ty' <- tcView ty - = do { (xi, ccs) <- flatten ctxt ty' + = do { (xi, co, ccs) <- flatten ctxt ty' -- Preserve type synonyms if possible - -- We can tell if t' is function-free by + -- We can tell if ty' is function-free by -- whether there are any floated constraints ; if isEmptyCCan ccs then - return (ty, emptyCCan) + return (ty, ty, emptyCCan) else - return (xi, ccs) } + return (xi, co, ccs) } flatten _ v@(TyVarTy _) - = return (v, emptyCCan) + = return (v, v, emptyCCan) flatten ctxt (AppTy ty1 ty2) - = do { (xi1,c1) <- flatten ctxt ty1 - ; (xi2,c2) <- flatten ctxt ty2 - ; return (mkAppTy xi1 xi2, c1 `andCCan` c2) } + = do { (xi1,co1,c1) <- flatten ctxt ty1 + ; (xi2,co2,c2) <- flatten ctxt ty2 + ; return (mkAppTy xi1 xi2, mkAppCoercion co1 co2, c1 `andCCan` c2) } flatten ctxt (FunTy ty1 ty2) - = do { (xi1,c1) <- flatten ctxt ty1 - ; (xi2,c2) <- flatten ctxt ty2 - ; return (mkFunTy xi1 xi2, c1 `andCCan` c2) } + = do { (xi1,co1,c1) <- flatten ctxt ty1 + ; (xi2,co2,c2) <- flatten ctxt ty2 + ; return (mkFunTy xi1 xi2, mkFunCoercion co1 co2, c1 `andCCan` c2) } flatten fl (TyConApp tc tys) -- For a normal type constructor or data family application, we just -- recursively flatten the arguments. | not (isSynFamilyTyCon tc) - = do { (xis,ccs) <- flattenMany fl tys - ; return (mkTyConApp tc xis, ccs) } + = do { (xis,cos,ccs) <- flattenMany fl tys + ; return (mkTyConApp tc xis, mkTyConCoercion tc cos, ccs) } -- Otherwise, it's a type function application, and we have to -- flatten it away as well, and generate a new given equality constraint -- between the application and a newly generated flattening skolem variable. - | otherwise - = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated - do { (xis, ccs) <- flattenMany fl tys - ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis + | otherwise + = ASSERT( tyConArity tc <= length tys ) -- Type functions are saturated + do { (xis, cos, ccs) <- flattenMany fl tys + ; let (xi_args, xi_rest) = splitAt (tyConArity tc) xis + (cos_args, cos_rest) = splitAt (tyConArity tc) cos -- The type function might be *over* saturated -- in which case the remaining arguments should -- be dealt with by AppTys fam_ty = mkTyConApp tc xi_args fam_co = fam_ty -- identity - ; xi_skol <- newFlattenSkolemTy fam_ty - ; cv <- newGivOrDerCoVar fam_ty xi_skol fam_co + ; (ret_co, rhs_var, ct) <- + if isGiven fl then + do { rhs_var <- newFlattenSkolemTy fam_ty + ; cv <- newGivOrDerCoVar fam_ty rhs_var fam_co + ; let ct = CFunEqCan { cc_id = cv + , cc_flavor = fl -- Given + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_var } + ; return $ (mkCoVarCoercion cv, rhs_var, ct) } + else -- Derived or Wanted: make a new *unification* flatten variable + do { rhs_var <- newFlexiTcSTy (typeKind fam_ty) + ; cv <- newWantedCoVar fam_ty rhs_var + ; let ct = CFunEqCan { cc_id = cv + , cc_flavor = mkWantedFlavor fl + -- Always Wanted, not Derived + , cc_fun = tc + , cc_tyargs = xi_args + , cc_rhs = rhs_var } + ; return $ (mkCoVarCoercion cv, rhs_var, ct) } + + ; return ( foldl AppTy rhs_var xi_rest + , foldl AppTy (mkSymCoercion ret_co + `mkTransCoercion` mkTyConCoercion tc cos_args) cos_rest + , ccs `extendCCans` ct) } - ; let ceq_given = CFunEqCan { cc_id = cv - , cc_flavor = mkGivenFlavor fl UnkSkol - , cc_fun = tc - , cc_tyargs = xi_args - , cc_rhs = xi_skol - } - -- ceq_given : F xi_args ~ xi_skol - - ; return ( foldl AppTy xi_skol xi_rest - , ccs `extendCCans` ceq_given) } flatten ctxt (PredTy pred) - = do { (pred',ccs) <- flattenPred ctxt pred - ; return (PredTy pred', ccs) } + = do { (pred', co, ccs) <- flattenPred ctxt pred + ; return (PredTy pred', co, ccs) } flatten ctxt ty@(ForAllTy {}) -- We allow for-alls when, but only when, no type function -- applications inside the forall involve the bound type variables +-- TODO: What if it is a (t1 ~ t2) => t3 +-- Must revisit when the New Coercion API is here! = do { let (tvs, rho) = splitForAllTys ty - ; (rho', ccs) <- flatten ctxt rho + ; (rho', co, ccs) <- flatten ctxt rho ; let bad_eqs = filterBag is_bad ccs is_bad c = tyVarsOfCanonical c `intersectsVarSet` tv_set tv_set = mkVarSet tvs ; unless (isEmptyBag bad_eqs) (flattenForAllErrorTcS ctxt ty bad_eqs) - ; return (mkForAllTys tvs rho', ccs) } + ; return (mkForAllTys tvs rho', mkForAllTys tvs co, ccs) } --------------- -flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, CanonicalCts) +flattenPred :: CtFlavor -> TcPredType -> TcS (TcPredType, Coercion, CanonicalCts) flattenPred ctxt (ClassP cls tys) - = do { (tys', ccs) <- flattenMany ctxt tys - ; return (ClassP cls tys', ccs) } + = do { (tys', cos, ccs) <- flattenMany ctxt tys + ; return (ClassP cls tys', mkClassPPredCo cls cos, ccs) } flattenPred ctxt (IParam nm ty) - = do { (ty', ccs) <- flatten ctxt ty - ; return (IParam nm ty', ccs) } + = do { (ty', co, ccs) <- flatten ctxt ty + ; return (IParam nm ty', mkIParamPredCo nm co, ccs) } +-- TODO: Handling of coercions between EqPreds must be revisited once the New Coercion API is ready! flattenPred ctxt (EqPred ty1 ty2) - = do { (ty1', ccs1) <- flatten ctxt ty1 - ; (ty2', ccs2) <- flatten ctxt ty2 - ; return (EqPred ty1' ty2', ccs1 `andCCan` ccs2) } + = do { (ty1', co1, ccs1) <- flatten ctxt ty1 + ; (ty2', co2, ccs2) <- flatten ctxt ty2 + ; return (EqPred ty1' ty2', mkEqPredCo co1 co2, ccs1 `andCCan` ccs2) } + \end{code} %************************************************************************ @@ -225,19 +234,33 @@ mkCanonical fl ev = case evVarPred ev of canClass :: CtFlavor -> EvVar -> Class -> [TcType] -> TcS CanonicalCts canClass fl v cn tys - = do { (xis,ccs) <- flattenMany fl tys - ; return $ ccs `extendCCans` CDictCan { cc_id = v - , cc_flavor = fl - , cc_class = cn - , cc_tyargs = xis } } -canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts + = do { (xis,cos,ccs) <- flattenMany fl tys -- cos :: xis ~ tys + ; let no_flattening_happened = isEmptyCCan ccs + dict_co = mkTyConCoercion (classTyCon cn) cos + ; v_new <- if no_flattening_happened then return v + else if isGiven fl then return v + -- The cos are all identities if fl=Given, + -- hence nothing to do + else do { v' <- newDictVar cn xis -- D xis + ; if isWanted fl + then setDictBind v (EvCast v' dict_co) + else setDictBind v' (EvCast v (mkSymCoercion dict_co)) + ; return v' } + + ; return (ccs `extendCCans` CDictCan { cc_id = v_new + , cc_flavor = fl + , cc_class = cn + , cc_tyargs = xis }) } + +canIP :: CtFlavor -> EvVar -> IPName Name -> TcType -> TcS CanonicalCts +-- See Note [Canonical implicit parameter constraints] to see why we don't +-- immediately canonicalize (flatten) IP constraints. canIP fl v nm ty = return $ singleCCan $ CIPCan { cc_id = v , cc_flavor = fl , cc_ip_nm = nm , cc_ip_ty = ty } - ----------------- canEq :: CtFlavor -> EvVar -> Type -> Type -> TcS CanonicalCts canEq fl cv ty1 ty2 @@ -308,36 +331,32 @@ canEq fl cv (FunTy s1 t1) (FunTy s2 t2) ; cc2 <- canEq fl resv t1 t2 ; return (cc1 `andCCan` cc2) } -canEq fl cv (PredTy p1) (PredTy p2) = canEqPred p1 p2 - where canEqPred (IParam n1 t1) (IParam n2 t2) - | n1 == n2 - = if isWanted fl then - do { v <- newWantedCoVar t1 t2 - ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) - ; canEq fl v t1 t2 } - else return emptyCCan -- DV: How to decompose given IP coercions? - - canEqPred (ClassP c1 tys1) (ClassP c2 tys2) - | c1 == c2 - = if isWanted fl then - do { vs <- zipWithM newWantedCoVar tys1 tys2 - ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) - ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 - } - else return emptyCCan - -- How to decompose given dictionary (and implicit parameter) coercions? - -- You may think that the following is right: - -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) - -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos - -- But this assumes that the coercion is a type constructor-based - -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose - -- to not decompose these coercions. We have to get back to this - -- when we clean up the Coercion API. - - canEqPred p1 p2 = misMatchErrorTcS fl (mkPredTy p1) (mkPredTy p2) - - -canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) +canEq fl cv (PredTy (IParam n1 t1)) (PredTy (IParam n2 t2)) + | n1 == n2 + = if isWanted fl then + do { v <- newWantedCoVar t1 t2 + ; setWantedCoBind cv $ mkIParamPredCo n1 (mkCoVarCoercion cv) + ; canEq fl v t1 t2 } + else return emptyCCan -- DV: How to decompose given IP coercions? + +canEq fl cv (PredTy (ClassP c1 tys1)) (PredTy (ClassP c2 tys2)) + | c1 == c2 + = if isWanted fl then + do { vs <- zipWithM newWantedCoVar tys1 tys2 + ; setWantedCoBind cv $ mkClassPPredCo c1 (map mkCoVarCoercion vs) + ; andCCans <$> zipWith3M (canEq fl) vs tys1 tys2 + } + else return emptyCCan + -- How to decompose given dictionary (and implicit parameter) coercions? + -- You may think that the following is right: + -- let cos = decomposeCo (length tys1) (mkCoVarCoercion cv) + -- in zipWith3M newGivOrDerCoVar tys1 tys2 cos + -- But this assumes that the coercion is a type constructor-based + -- coercion, and not a PredTy (ClassP cn cos) coercion. So we chose + -- to not decompose these coercions. We have to get back to this + -- when we clean up the Coercion API. + +canEq fl cv (TyConApp tc1 tys1) (TyConApp tc2 tys2) | isAlgTyCon tc1 && isAlgTyCon tc2 , tc1 == tc2 , length tys1 == length tys2 @@ -375,18 +394,20 @@ canEq fl cv ty1 ty2 canEq fl _ s1@(ForAllTy {}) s2@(ForAllTy {}) | tcIsForAllTy s1, tcIsForAllTy s2, Wanted {} <- fl - = misMatchErrorTcS fl s1 s2 - | otherwise + = canEqFailure fl s1 s2 + | otherwise = do { traceTcS "Ommitting decomposition of given polytype equality" (pprEq s1 s2) ; return emptyCCan } -- Finally expand any type synonym applications. canEq fl cv ty1 ty2 | Just ty1' <- tcView ty1 = canEq fl cv ty1' ty2 canEq fl cv ty1 ty2 | Just ty2' <- tcView ty2 = canEq fl cv ty1 ty2' -canEq fl _ ty1 ty2 - = misMatchErrorTcS fl ty1 ty2 - +canEq fl _ ty1 ty2 = canEqFailure fl ty1 ty2 +canEqFailure :: CtFlavor -> Type -> Type -> TcS CanonicalCts +canEqFailure fl ty1 ty2 + = do { addErrorTcS MisMatchError fl ty1 ty2 + ; return emptyCCan } \end{code} Note [Equality between type applications] @@ -536,24 +557,22 @@ reOrient _untch (OtherCls {}) (FskCls {}) = True reOrient _untch (OtherCls {}) (VarCls {}) = True reOrient _untch (OtherCls {}) (OtherCls {}) = panic "reOrient" -- One must be Var/Fun -reOrient _untch (FunCls {}) (VarCls tv2) = isMetaTyVar tv2 +reOrient _untch (FunCls {}) (VarCls {}) = False -- See Note [No touchables as FunEq RHS] in TcSMonad -reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs +reOrient _untch (FunCls {}) _ = False -- Fun/Other on rhs -reOrient _untch (VarCls tv1) (FunCls {}) = not $ isMetaTyVar tv1 - -- Put function on the left, *except* if the RHS becomes - -- a meta-tyvar; see invariant on CFunEqCan - -- and Note [No touchables as FunEq RHS] +reOrient _untch (VarCls {}) (FunCls {}) = True -reOrient _untch (VarCls tv1) (FskCls {}) = not $ isMetaTyVar tv1 - -- Put flatten-skolems on the left if possible: - -- see Note [Loopy Spontaneous Solving, Example 4] in TcInteract +reOrient _untch (VarCls {}) (FskCls {}) = False -reOrient _untch (VarCls {}) (OtherCls {}) = False -reOrient _untch (VarCls {}) (VarCls {}) = False +reOrient _untch (VarCls {}) (OtherCls {}) = False +reOrient _untch (VarCls tv1) (VarCls tv2) + | isMetaTyVar tv2 && not (isMetaTyVar tv1) = True + | otherwise = False + -- Just for efficiency, see CTyEqCan invariants -reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2 - -- See Note [Loopy Spontaneous Solving, Example 4] in TcInteract +reOrient _untch (FskCls {}) (VarCls tv2) = isMetaTyVar tv2 + -- Just for efficiency, see CTyEqCan invariants reOrient _untch (FskCls {}) (FskCls {}) = False reOrient _untch (FskCls {}) (FunCls {}) = True @@ -590,49 +609,83 @@ canEqLeaf untch fl cv cls1 cls2 canEqLeafOriented :: CtFlavor -> CoVar -> TypeClassifier -> TcType -> TcS CanonicalCts -- First argument is not OtherCls -canEqLeafOriented fl cv cls1@(FunCls fn tys) s2 - | let k1 = kindAppResult (tyConKind fn) tys, +canEqLeafOriented fl cv cls1@(FunCls fn tys1) s2 -- cv : F tys1 + | let k1 = kindAppResult (tyConKind fn) tys1, let k2 = typeKind s2, isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CFunEqCan - = kindErrorTcS fl (unClassify cls1) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract + = addErrorTcS KindError fl (unClassify cls1) s2 >> return emptyCCan + -- Eagerly fails, see Note [Kind errors] in TcInteract + | otherwise = ASSERT2( isSynFamilyTyCon fn, ppr (unClassify cls1) ) - do { (xis1,ccs1) <- flattenMany fl tys -- flatten type function arguments - ; (xi2,ccs2) <- flatten fl s2 -- flatten entire RHS - ; let final_cc = CFunEqCan { cc_id = cv - , cc_flavor = fl + do { (xis1,cos1,ccs1) <- flattenMany fl tys1 -- Flatten type function arguments + -- cos1 :: xis1 ~ tys1 + ; (xi2, co2, ccs2) <- flatten fl s2 -- Flatten entire RHS + -- co2 :: xi2 ~ s2 + ; let ccs = ccs1 `andCCan` ccs2 + no_flattening_happened = isEmptyCCan ccs + ; cv_new <- if no_flattening_happened then return cv + else if isGiven fl then return cv + else do { cv' <- newWantedCoVar (unClassify (FunCls fn xis1)) xi2 + -- cv' : F xis ~ xi2 + ; let -- fun_co :: F xis1 ~ F tys1 + fun_co = mkTyConCoercion fn cos1 + -- want_co :: F tys1 ~ s2 + want_co = mkSymCoercion fun_co + `mkTransCoercion` mkCoVarCoercion cv' + `mkTransCoercion` co2 + -- der_co :: F xis1 ~ xi2 + der_co = fun_co + `mkTransCoercion` mkCoVarCoercion cv + `mkTransCoercion` mkSymCoercion co2 + ; if isWanted fl + then setWantedCoBind cv want_co + else setWantedCoBind cv' der_co + ; return cv' } + + ; let final_cc = CFunEqCan { cc_id = cv_new + , cc_flavor = fl , cc_fun = fn , cc_tyargs = xis1 , cc_rhs = xi2 } - ; return $ ccs1 `andCCan` ccs2 `extendCCans` final_cc } + ; return $ ccs `extendCCans` final_cc } -- Otherwise, we have a variable on the left, so call canEqLeafTyVarLeft canEqLeafOriented fl cv (FskCls tv) s2 - = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2 - ; return $ ccs `extendCCans` cc } + = canEqLeafTyVarLeft fl cv tv s2 canEqLeafOriented fl cv (VarCls tv) s2 - = do { (cc,ccs) <- canEqLeafTyVarLeft fl cv tv s2 - ; return $ ccs `extendCCans` cc } + = canEqLeafTyVarLeft fl cv tv s2 canEqLeafOriented _ cv (OtherCls ty1) ty2 = pprPanic "canEqLeaf" (ppr cv $$ ppr ty1 $$ ppr ty2) -canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS (CanonicalCt, CanonicalCts) +canEqLeafTyVarLeft :: CtFlavor -> CoVar -> TcTyVar -> TcType -> TcS CanonicalCts -- Establish invariants of CTyEqCans -canEqLeafTyVarLeft fl cv tv s2 +canEqLeafTyVarLeft fl cv tv s2 -- cv : tv ~ s2 | isGiven fl && not (k1 `compatKind` k2) -- Establish the kind invariant for CTyEqCan - = kindErrorTcS fl (mkTyVarTy tv) s2 -- Eagerly fails, see Note [Kind errors] in TcInteract - + = addErrorTcS KindError fl (mkTyVarTy tv) s2 >> return emptyCCan + -- Eagerly fails, see Note [Kind errors] in TcInteract | otherwise - = do { (xi2,ccs2) <- flatten fl s2 -- flatten RHS - ; xi2' <- canOccursCheck fl tv xi2 -- do an occurs check, and return a possibly - -- unfolded version of the RHS, if we had to - -- unfold any type synonyms to get rid of tv. - ; let final_cc = CTyEqCan { cc_id = cv - , cc_flavor = fl - , cc_tyvar = tv - , cc_rhs = xi2' - } - ; return $ (final_cc, ccs2) } + = do { (xi2, co, ccs2) <- flatten fl s2 -- Flatten RHS co : xi2 ~ s2 + ; mxi2' <- canOccursCheck fl tv xi2 -- Do an occurs check, and return a possibly + -- unfolded version of the RHS, if we had to + -- unfold any type synonyms to get rid of tv. + ; case mxi2' of { + Nothing -> addErrorTcS OccCheckError fl (mkTyVarTy tv) xi2 >> return emptyCCan ; + Just xi2' -> + do { let no_flattening_happened = isEmptyCCan ccs2 + ; cv_new <- if no_flattening_happened then return cv + else if isGiven fl then return cv + else do { cv' <- newWantedCoVar (mkTyVarTy tv) xi2' -- cv' : tv ~ xi2 + ; if isWanted fl + then setWantedCoBind cv (mkCoVarCoercion cv' `mkTransCoercion` co) + else setWantedCoBind cv' (mkCoVarCoercion cv `mkTransCoercion` + mkSymCoercion co) + ; return cv' } + + ; return $ ccs2 `extendCCans` CTyEqCan { cc_id = cv_new + , cc_flavor = fl + , cc_tyvar = tv + , cc_rhs = xi2' } } } } where k1 = tyVarKind tv k2 = typeKind s2 @@ -646,10 +699,8 @@ canEqLeafTyVarLeft fl cv tv s2 -- variable, then the same type is returned. -- -- Precondition: the two types are not equal (looking though synonyms) -canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS Xi -canOccursCheck gw tv xi - | Just xi' <- expandAway tv xi = return xi' - | otherwise = occursCheckErrorTcS gw tv xi +canOccursCheck :: CtFlavor -> TcTyVar -> Xi -> TcS (Maybe Xi) +canOccursCheck _gw tv xi = return (expandAway tv xi) \end{code} @expandAway tv xi@ expands synonyms in xi just enough to get rid of @@ -678,18 +729,47 @@ expandAway tv t@(TyVarTy tv') expandAway tv xi | not (tv `elemVarSet` tyVarsOfType xi) = Just xi expandAway tv (AppTy ty1 ty2) - = mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2 + = do { ty1' <- expandAway tv ty1 + ; ty2' <- expandAway tv ty2 + ; return (mkAppTy ty1' ty2') } +-- mkAppTy <$> expandAway tv ty1 <*> expandAway tv ty2 expandAway tv (FunTy ty1 ty2) - = mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2 -expandAway _ (ForAllTy {}) = error "blorg" -- TODO -expandAway _ (PredTy {}) = error "flerg" -- TODO - + = do { ty1' <- expandAway tv ty1 + ; ty2' <- expandAway tv ty2 + ; return (mkFunTy ty1' ty2') } +-- mkFunTy <$> expandAway tv ty1 <*> expandAway tv ty2 +expandAway tv ty@(ForAllTy {}) + = let (tvs,rho) = splitForAllTys ty + tvs_knds = map tyVarKind tvs + in if tv `elemVarSet` tyVarsOfTypes tvs_knds then + -- Can't expand away the kinds unless we create + -- fresh variables which we don't want to do at this point. + Nothing + else do { rho' <- expandAway tv rho + ; return (mkForAllTys tvs rho') } +expandAway tv (PredTy pred) + = do { pred' <- expandAwayPred tv pred + ; return (PredTy pred') } -- For a type constructor application, first try expanding away the -- offending variable from the arguments. If that doesn't work, next -- see if the type constructor is a type synonym, and if so, expand -- it and try again. expandAway tv ty@(TyConApp tc tys) - = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv) + = (mkTyConApp tc <$> mapM (expandAway tv) tys) <|> (tcView ty >>= expandAway tv) + +expandAwayPred :: TcTyVar -> TcPredType -> Maybe TcPredType +expandAwayPred tv (ClassP cls tys) + = do { tys' <- mapM (expandAway tv) tys; return (ClassP cls tys') } +expandAwayPred tv (EqPred ty1 ty2) + = do { ty1' <- expandAway tv ty1 + ; ty2' <- expandAway tv ty2 + ; return (EqPred ty1' ty2') } +expandAwayPred tv (IParam nm ty) + = do { ty' <- expandAway tv ty + ; return (IParam nm ty') } + + + \end{code} Note [Type synonyms and canonicalization] diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index 5397527..932e5bc 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -3,8 +3,9 @@ module TcErrors( reportUnsolved, reportUnsolvedDeriv, reportUnsolvedWantedEvVars, warnDefaulting, unifyCtxt, typeExtraInfoMsg, - kindErrorTcS, misMatchErrorTcS, flattenForAllErrorTcS, - occursCheckErrorTcS, solverDepthErrorTcS + + flattenForAllErrorTcS, + solverDepthErrorTcS ) where #include "HsVersions.h" @@ -13,6 +14,8 @@ import TcRnMonad import TcMType import TcSMonad import TcType +import TypeRep + import Inst import InstEnv @@ -47,24 +50,126 @@ from the insts, or just whatever seems to be around in the monad just now? \begin{code} -reportUnsolved :: (CanonicalCts, Bag Implication) -> TcM () -reportUnsolved (unsolved_flats, unsolved_implics) - | isEmptyBag unsolved +reportUnsolved :: (Bag WantedEvVar, Bag Implication) -> Bag FrozenError -> TcM () +reportUnsolved (unsolved_flats, unsolved_implics) frozen_errors + | isEmptyBag unsolved && isEmptyBag frozen_errors = return () | otherwise - = do { unsolved <- mapBagM zonkWanted unsolved + = do { frozen_errors_zonked <- mapBagM zonk_frozen frozen_errors + ; let frozen_tvs = tyVarsOfFrozen frozen_errors_zonked + + ; unsolved <- mapBagM zonkWanted unsolved -- Zonk to un-flatten any flatten-skols ; env0 <- tcInitTidyEnv - ; let tidy_env = tidyFreeTyVars env0 (tyVarsOfWanteds unsolved) + ; let tidy_env = tidyFreeTyVars env0 $ + tyVarsOfWanteds unsolved `unionVarSet` frozen_tvs + tidy_unsolved = tidyWanteds tidy_env unsolved err_ctxt = CEC { cec_encl = [] , cec_extra = empty - , cec_tidy = tidy_env } - ; traceTc "reportUnsolved" (ppr unsolved) + , cec_tidy = tidy_env + } + + ; traceTc "reportUnsolved" (vcat [ + text "Unsolved constraints =" <+> ppr unsolved, + text "Frozen errors =" <+> ppr frozen_errors_zonked ]) + + ; let tidy_frozen_errors_zonked = tidyFrozen tidy_env frozen_errors_zonked + + ; reportTidyFrozens tidy_env tidy_frozen_errors_zonked ; reportTidyWanteds err_ctxt tidy_unsolved } where - unsolved = mkWantedConstraints unsolved_flats unsolved_implics + unsolved = Bag.mapBag WcEvVar unsolved_flats `unionBags` + Bag.mapBag WcImplic unsolved_implics + + zonk_frozen (FrozenError frknd fl ty1 ty2) + = do { ty1z <- zonkTcType ty1 + ; ty2z <- zonkTcType ty2 + ; return (FrozenError frknd fl ty1z ty2z) } + + tyVarsOfFrozen fr + = unionVarSets $ bagToList (mapBag tvs_of_frozen fr) + tvs_of_frozen (FrozenError _ _ ty1 ty2) = tyVarsOfTypes [ty1,ty2] + + tidyFrozen env fr = mapBag (tidy_frozen env) fr + tidy_frozen env (FrozenError frknd fl ty1 ty2) + = FrozenError frknd fl (tidyType env ty1) (tidyType env ty2) + +reportTidyFrozens :: TidyEnv -> Bag FrozenError -> TcM () +reportTidyFrozens tidy_env fr = mapBagM_ (reportTidyFrozen tidy_env) fr + +reportTidyFrozen :: TidyEnv -> FrozenError -> TcM () +reportTidyFrozen tidy_env err@(FrozenError _ fl _ty1 _ty2) + = do { let dec_errs = decompFrozenError err + init_err_ctxt = CEC { cec_encl = [] + , cec_extra = empty + , cec_tidy = tidy_env } + ; mapM_ (report_dec_err init_err_ctxt) dec_errs } + where + report_dec_err err_ctxt (ty1,ty2) + -- The only annoying thing here is that in the given case, + -- the ``Inaccessible code'' message will be printed once for + -- each decomposed equality. + = do { (tidy_env2,extra2) + <- if isGiven fl + then return (cec_tidy err_ctxt, inaccessible_msg) + else getWantedEqExtra emptyTvSubst (cec_tidy err_ctxt) loc_orig ty1 ty2 + ; let err_ctxt2 = err_ctxt { cec_tidy = tidy_env2 + , cec_extra = cec_extra err_ctxt $$ extra2 } + ; setCtFlavorLoc fl $ + reportEqErr err_ctxt2 ty1 ty2 + } + + loc_orig | Wanted loc <- fl = ctLocOrigin loc + | Derived loc _ <- fl = ctLocOrigin loc + | otherwise = pprPanic "loc_orig" empty + + inaccessible_msg + | Given loc <- fl + = hang (ptext (sLit "Inaccessible code in")) 2 (mk_what loc) + | otherwise = pprPanic "inaccessible_msg" empty + + mk_what loc + = case ctLocOrigin loc of + PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor") + <+> quotes (ppr dc) <> comma + , ptext (sLit "in") <+> pprMatchContext mc ] + other_skol -> pprSkolInfo other_skol + +decompFrozenError :: FrozenError -> [(TcType,TcType)] +-- Postcondition: will always return a non-empty list +decompFrozenError (FrozenError errk _fl ty1 ty2) + | OccCheckError <- errk + = dec_occ_check ty1 ty2 + | otherwise + = [(ty1,ty2)] + where dec_occ_check :: TcType -> TcType -> [(TcType,TcType)] + -- This error arises from an original: + -- a ~ Maybe a + -- But by now the a has been substituted away, eg: + -- Int ~ Maybe Int + -- Maybe b ~ Maybe (Maybe b) + dec_occ_check ty1 ty2 + | tcEqType ty1 ty2 = [] + dec_occ_check ty1@(TyVarTy {}) ty2 = [(ty1,ty2)] + dec_occ_check (FunTy s1 t1) (FunTy s2 t2) + = let errs1 = dec_occ_check s1 s2 + errs2 = dec_occ_check t1 t2 + in errs1 ++ errs2 + dec_occ_check ty1@(TyConApp fn1 tys1) ty2@(TyConApp fn2 tys2) + | fn1 == fn2 && length tys1 == length tys2 + , not (isSynFamilyTyCon fn1) + = concatMap (\(t1,t2) -> dec_occ_check t1 t2) (zip tys1 tys2) + | otherwise + = [(ty1,ty2)] + dec_occ_check ty1 ty2 + | Just (s1,t1) <- tcSplitAppTy_maybe ty1 + , Just (s2,t2) <- tcSplitAppTy_maybe ty2 + = let errs1 = dec_occ_check s1 s2 + errs2 = dec_occ_check t1 t2 + in errs1 ++ errs2 + dec_occ_check ty1 ty2 = [(ty1,ty2)] reportUnsolvedWantedEvVars :: Bag WantedEvVar -> TcM () reportUnsolvedWantedEvVars wanteds @@ -105,8 +210,8 @@ reportUnsolvedDeriv unsolved loc data ReportErrCtxt = CEC { cec_encl :: [Implication] -- Enclosing implications -- (innermost first) - , cec_tidy :: TidyEnv - , cec_extra :: SDoc -- Add this to each error message + , cec_tidy :: TidyEnv + , cec_extra :: SDoc -- Add this to each error message } reportTidyImplic :: ReportErrCtxt -> Implication -> TcM () @@ -123,6 +228,13 @@ reportTidyWanteds ctxt unsolved ; groupErrs (reportEqErrs ctxt) tv_eqs ; when (null tv_eqs) $ groupErrs (reportFlat ctxt) others + ; traceTc "rtw" (vcat [ + text "unsolved =" <+> ppr unsolved, + text "tveqs =" <+> ppr tv_eqs, + text "others =" <+> ppr others, + text "ambigs =" <+> ppr ambigs , + text "implics =" <+> ppr implics]) + ; when (null tv_eqs) $ mapBagM_ (reportTidyImplic ctxt) implics -- Only report ambiguity if no other errors (at all) happened @@ -273,8 +385,8 @@ reportEqErrs ctxt eqs orig env0 = cec_tidy ctxt report_one (EqPred ty1 ty2) = do { (env1, extra) <- getWantedEqExtra emptyTvSubst env0 orig ty1 ty2 - ; let ctxt' = ctxt { cec_tidy = env1 - , cec_extra = cec_extra ctxt $$ extra } + ; let ctxt' = ctxt { cec_tidy = env1 + , cec_extra = extra $$ cec_extra ctxt } ; reportEqErr ctxt' ty1 ty2 } report_one pred = pprPanic "reportEqErrs" (ppr pred) @@ -284,11 +396,13 @@ reportEqErr :: ReportErrCtxt -> TcType -> TcType -> TcM () reportEqErr ctxt ty1 ty2 | Just tv1 <- tcGetTyVar_maybe ty1 = reportTyVarEqErr ctxt tv1 ty2 | Just tv2 <- tcGetTyVar_maybe ty2 = reportTyVarEqErr ctxt tv2 ty1 + | otherwise -- Neither side is a type variable -- Since the unsolved constraint is canonical, -- it must therefore be of form (F tys ~ ty) = addErrorReport ctxt (misMatchOrCND ctxt ty1 ty2 $$ mkTyFunInfoMsg ty1 ty2) + reportTyVarEqErr :: ReportErrCtxt -> TcTyVar -> TcType -> TcM () -- tv1 and ty2 are already tidied reportTyVarEqErr ctxt tv1 ty2 @@ -300,14 +414,20 @@ reportTyVarEqErr ctxt tv1 ty2 | not is_meta1 = -- sk ~ ty, where ty isn't a meta-tyvar: mis-match - addErrTcM (addExtraInfo (misMatchOrCND ctxt ty1 ty2) - (cec_tidy ctxt) ty1 ty2) + addErrorReport (addExtraInfo ctxt ty1 ty2) + (misMatchOrCND ctxt ty1 ty2) -- So tv is a meta tyvar, and presumably it is -- an *untouchable* meta tyvar, else it'd have been unified | not (k2 `isSubKind` k1) -- Kind error = addErrorReport ctxt $ (kindErrorMsg (mkTyVarTy tv1) ty2) + -- Occurs check + | tv1 `elemVarSet` tyVarsOfType ty2 + = let occCheckMsg = hang (text "Occurs check: cannot construct the infinite type:") 2 + (sep [ppr ty1, char '=', ppr ty2]) + in addErrorReport ctxt occCheckMsg + -- Check for skolem escape | (implic:_) <- cec_encl ctxt -- Get the innermost context , let esc_skols = varSetElems (tyVarsOfType ty2 `intersectVarSet` ic_skols implic) @@ -334,15 +454,23 @@ reportTyVarEqErr ctxt tv1 ty2 , let implic_loc = ic_loc implic given = ic_given implic = setCtLoc (ic_loc implic) $ - do { let (env1, msg) = addExtraInfo (misMatchMsg ty1 ty2) (cec_tidy ctxt) ty1 ty2 - extra = vcat [ ptext (sLit "because") <+> ppr tv1 <+> ptext (sLit "is untouchable") - , ptext (sLit "inside the constraints") <+> pprEvVarTheta given - , nest 2 (ptext (sLit "bound at") - <+> pprSkolInfo (ctLocOrigin implic_loc)) ] - ; addErrTcM (env1, msg $$ extra) } - - | otherwise -- I'm not sure how this can happen! - = addErrTcM (addExtraInfo (misMatchMsg ty1 ty2) (cec_tidy ctxt) ty1 ty2) + do { let msg = misMatchMsg ty1 ty2 + extra = quotes (ppr tv1) + <+> sep [ ptext (sLit "is untouchable") + , ptext (sLit "inside the constraints") <+> pprEvVarTheta given + , ptext (sLit "bound at") <+> pprSkolInfo (ctLocOrigin implic_loc)] + ; addErrorReport (addExtraInfo ctxt ty1 ty2) (msg $$ nest 2 extra) } + + | otherwise -- This can happen, by a recursive decomposition of frozen + -- occurs check constraints + -- Example: alpha ~ T Int alpha has frozen. + -- Then alpha gets unified to T beta gamma + -- So now we have T beta gamma ~ T Int (T beta gamma) + -- Decompose to (beta ~ Int, gamma ~ T beta gamma) + -- The (gamma ~ T beta gamma) is the occurs check, but + -- the (beta ~ Int) isn't an error at all. So return () + = return () + where is_meta1 = isMetaTyVar tv1 k1 = tyVarKind tv1 @@ -374,15 +502,15 @@ couldNotDeduce givens wanteds , nest 2 $ ptext (sLit "from the context") <+> pprEvVarTheta givens] -addExtraInfo :: SDoc -> TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc) --- This version is used by TcSimplify too, which doesn't track the --- expected/acutal thing, so we just have ty1 ty2 here --- NB: The types are already tidied -addExtraInfo msg env ty1 ty2 - = (env2, msg $$ nest 2 (extra1 $$ extra2)) +addExtraInfo :: ReportErrCtxt -> TcType -> TcType -> ReportErrCtxt +-- Add on extra info about the types themselves +-- NB: The types themselves are already tidied +addExtraInfo ctxt ty1 ty2 + = ctxt { cec_tidy = env2 + , cec_extra = nest 2 (extra1 $$ extra2) $$ cec_extra ctxt } where - (env1, extra1) = typeExtraInfoMsg env ty1 - (env2, extra2) = typeExtraInfoMsg env1 ty2 + (env1, extra1) = typeExtraInfoMsg (cec_tidy ctxt) ty1 + (env2, extra2) = typeExtraInfoMsg env1 ty2 misMatchMsg :: TcType -> TcType -> SDoc -- Types are already tidy misMatchMsg ty1 ty2 = sep [ ptext (sLit "Couldn't match type") <+> quotes (ppr ty1) @@ -659,46 +787,6 @@ are created by in RtClosureInspect.zonkRTTIType. %************************************************************************ \begin{code} -kindErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a --- If there's a kind error, we don't want to blindly say "kind error" --- We might, say, be unifying a skolem 'a' with a type 'Int', --- in which case that's the error to report. So we set things --- up to call reportEqErr, which does the business properly -kindErrorTcS fl ty1 ty2 - = wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra -> - do { let ctxt = CEC { cec_encl = [] - , cec_extra = extra - , cec_tidy = env0 } - ; reportEqErr ctxt ty1 ty2 - ; failM - } - -misMatchErrorTcS :: CtFlavor -> TcType -> TcType -> TcS a -misMatchErrorTcS fl ty1 ty2 - = wrapEqErrTcS fl ty1 ty2 $ \ env0 ty1 ty2 extra -> - do { let msg = inaccessible_msg $$ misMatchMsg ty1 ty2 - (env1, msg1) = addExtraInfo msg env0 ty1 ty2 - ; failWithTcM (env1, msg1 $$ extra) } - where - inaccessible_msg - = case fl of - Given loc -> hang (ptext (sLit "Inaccessible code in")) - 2 (mk_what loc) - _ -> empty - mk_what loc - = case ctLocOrigin loc of - PatSkol dc mc -> sep [ ptext (sLit "a pattern with constructor") - <+> quotes (ppr dc) <> comma - , ptext (sLit "in") <+> pprMatchContext mc ] - other_skol -> pprSkolInfo other_skol - -occursCheckErrorTcS :: CtFlavor -> TcTyVar -> TcType -> TcS a -occursCheckErrorTcS fl tv ty - = wrapEqErrTcS fl (mkTyVarTy tv) ty $ \ env0 ty1 ty2 extra2 -> - do { let extra1 = sep [ppr ty1, char '=', ppr ty2] - ; failWithTcM (env0, hang msg 2 (extra1 $$ extra2)) } - where - msg = text $ "Occurs check: cannot construct the infinite type:" solverDepthErrorTcS :: Int -> [CanonicalCt] -> TcS a solverDepthErrorTcS depth stack @@ -741,31 +829,6 @@ setCtFlavorLoc (Wanted loc) thing = setCtLoc loc thing setCtFlavorLoc (Derived loc _) thing = setCtLoc loc thing setCtFlavorLoc (Given loc) thing = setCtLoc loc thing -wrapEqErrTcS :: CtFlavor -> TcType -> TcType - -> (TidyEnv -> TcType -> TcType -> SDoc -> TcM a) - -> TcS a -wrapEqErrTcS fl ty1 ty2 thing_inside - = do { ty_binds_var <- getTcSTyBinds - ; wrapErrTcS $ setCtFlavorLoc fl $ - do { -- Apply the current substitition - -- and zonk to get rid of flatten-skolems - ; ty_binds_map <- readTcRef ty_binds_var - ; let subst = mkOpenTvSubst (mapVarEnv snd ty_binds_map) - ; env0 <- tcInitTidyEnv - ; (env1, ty1) <- zonkSubstTidy env0 subst ty1 - ; (env2, ty2) <- zonkSubstTidy env1 subst ty2 - ; let do_wanted loc = do { (env3, extra) <- getWantedEqExtra subst env2 - (ctLocOrigin loc) ty1 ty2 - ; thing_inside env3 ty1 ty2 extra } - ; case fl of - Wanted loc -> do_wanted loc - Derived loc _ -> do_wanted loc - Given {} -> thing_inside env2 ty1 ty2 empty - -- We could print more info, but it - -- seems to be coming out already - } } - where - getWantedEqExtra :: TvSubst -> TidyEnv -> CtOrigin -> TcType -> TcType -> TcM (TidyEnv, SDoc) getWantedEqExtra subst env0 (TypeEqOrigin item) ty1 ty2 diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index b968d7b..44e8479 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -1,7 +1,7 @@ \begin{code} module TcInteract ( solveInteract, AtomicInert, - InertSet, emptyInert, updInertSet, extractUnsolved, solveOne + InertSet, emptyInert, updInertSet, extractUnsolved, solveOne, foldISEqCts ) where #include "HsVersions.h" @@ -11,18 +11,16 @@ import BasicTypes import TcCanonical import VarSet import Type -import TypeRep import Id -import VarEnv import Var import TcType -import HsBinds +import HsBinds -import InstEnv -import Class -import TyCon +import InstEnv +import Class +import TyCon import Name import FunDeps @@ -32,12 +30,11 @@ import Control.Monad ( when ) import Coercion import Outputable -import TcRnTypes +import TcRnTypes import TcErrors -import TcSMonad +import TcSMonad import Bag -import qualified Data.Map as Map -import Maybes +import qualified Data.Map as Map import Control.Monad( zipWithM, unless ) import FastString ( sLit ) @@ -46,7 +43,6 @@ import DynFlags Note [InertSet invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ - An InertSet is a bag of canonical constraints, with the following invariants: 1 No two constraints react with each other. @@ -60,15 +56,20 @@ An InertSet is a bag of canonical constraints, with the following invariants: given LHS's occur in any of the given RHS's or reactant parts] 3 Wanted equalities also form an idempotent substitution + 4 The entire set of equalities is acyclic. 5 Wanted dictionaries are inert with the top-level axiom set 6 Equalities of the form tv1 ~ tv2 always have a touchable variable on the left (if possible). - 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints + + 7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints will be marked as solved right before being pushed into the inert set. See note [Touchables and givens]. + + 8 No Given constraint mentions a touchable unification variable, + except if the Note that 6 and 7 are /not/ enforced by canonicalization but rather by insertion in the inert list, ie by TcInteract. @@ -81,31 +82,6 @@ now we do not distinguish between given and solved constraints. Note that we must switch wanted inert items to given when going under an implication constraint (when in top-level inference mode). -Note [InertSet FlattenSkolemEqClass] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The inert_fsks field of the inert set contains an "inverse map" of all the -flatten skolem equalities in the inert set. For instance, if inert_cts looks -like this: - - fsk1 ~ fsk2 - fsk3 ~ fsk2 - fsk4 ~ fsk5 - -Then, the inert_fsks fields holds the following map: - fsk2 |-> { fsk1, fsk3 } - fsk5 |-> { fsk4 } -Along with the necessary coercions to convert fsk1 and fsk3 back to fsk2 -and fsk4 back to fsk5. Hence, the invariants of the inert_fsks field are: - - (a) All TcTyVars in the domain and range of inert_fsks are flatten skolems - (b) All TcTyVars in the domain of inert_fsk occur naked as rhs in some - equalities of inert_cts - (c) For every mapping fsk1 |-> { (fsk2,co), ... } it must be: - co : fsk2 ~ fsk1 - -The role of the inert_fsks is to make it easy to maintain the equivalence -class of each flatten skolem, which is much needed to correctly do spontaneous -solving. See Note [Loopy Spontaneous Solving] \begin{code} data CCanMap a = CCanMap { cts_givder :: Map.Map a CanonicalCts @@ -156,8 +132,7 @@ data InertSet , inert_fds :: FDImprovements -- List of pairwise improvements that have kicked in already -- and reside either in the worklist or in the inerts - , inert_fsks :: Map.Map TcTyVar [(TcTyVar,Coercion)] } - -- See Note [InertSet FlattenSkolemEqClass] + } type FDImprovement = (PredType,PredType) type FDImprovements = [(PredType,PredType)] @@ -167,9 +142,6 @@ instance Outputable InertSet where , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is))) , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is))) - , vcat (map (\(v,rest) -> ppr v <+> text "|->" <+> hsep (map (ppr.fst) rest)) - (Map.toList $ inert_fsks is) - ) ] emptyInert :: InertSet @@ -177,21 +149,9 @@ emptyInert = IS { inert_eqs = Bag.emptyBag , inert_dicts = emptyCCanMap , inert_ips = emptyCCanMap , inert_funeqs = emptyCCanMap - , inert_fsks = Map.empty, inert_fds = [] } + , inert_fds = [] } updInertSet :: InertSet -> AtomicInert -> InertSet --- Introduces an element in the inert set for the first time -updInertSet is@(IS { inert_eqs = eqs, inert_fsks = fsks }) - item@(CTyEqCan { cc_id = cv - , cc_tyvar = tv1 - , cc_rhs = xi }) - | Just tv2 <- tcGetTyVar_maybe xi, - FlatSkol {} <- tcTyVarDetails tv1, - FlatSkol {} <- tcTyVarDetails tv2 - = let eqs' = eqs `Bag.snocBag` item - fsks' = Map.insertWith (++) tv2 [(tv1, mkCoVarCoercion cv)] fsks - -- See Note [InertSet FlattenSkolemEqClass] - in is { inert_eqs = eqs', inert_fsks = fsks' } updInertSet is item | isCTyEqCan item -- Other equality = let eqs' = inert_eqs is `Bag.snocBag` item @@ -214,14 +174,17 @@ foldISEqCtsM :: Monad m => (a -> AtomicInert -> m a) -> a -> InertSet -> m a foldISEqCtsM k z IS { inert_eqs = eqs } = Bag.foldlBagM k z eqs +foldISEqCts :: (a -> AtomicInert -> a) -> a -> InertSet -> a +foldISEqCts k z IS { inert_eqs = eqs } + = Bag.foldlBag k z eqs + extractUnsolved :: InertSet -> (InertSet, CanonicalCts) extractUnsolved is@(IS {inert_eqs = eqs}) - = let is_init = is { inert_eqs = emptyCCan - , inert_dicts = solved_dicts - , inert_ips = solved_ips - , inert_funeqs = solved_funeqs } - is_final = Bag.foldlBag updInertSet is_init solved_eqs -- Add equalities carefully - in (is_final, unsolved) + = let is_solved = is { inert_eqs = solved_eqs + , inert_dicts = solved_dicts + , inert_ips = solved_ips + , inert_funeqs = solved_funeqs } + in (is_solved, unsolved) where (unsolved_eqs, solved_eqs) = Bag.partitionBag isWantedCt eqs (unsolved_ips, solved_ips) = extractUnsolvedCMap (inert_ips is) @@ -231,23 +194,6 @@ extractUnsolved is@(IS {inert_eqs = eqs}) unsolved = unsolved_eqs `unionBags` unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs -getFskEqClass :: InertSet -> TcTyVar -> [(TcTyVar,Coercion)] --- Precondition: tv is a FlatSkol. See Note [InertSet FlattenSkolemEqClass] -getFskEqClass (IS { inert_eqs = cts, inert_fsks = fsks }) tv - = case lkpTyEqCanByLhs of - Nothing -> fromMaybe [] (Map.lookup tv fsks) - Just ceq -> - case tcGetTyVar_maybe (cc_rhs ceq) of - Just tv_rhs | FlatSkol {} <- tcTyVarDetails tv_rhs - -> let ceq_co = mkSymCoercion $ mkCoVarCoercion (cc_id ceq) - mk_co (v,c) = (v, mkTransCoercion c ceq_co) - in (tv_rhs, ceq_co): map mk_co (fromMaybe [] $ Map.lookup tv fsks) - _ -> [] - where lkpTyEqCanByLhs = Bag.foldlBag lkp Nothing cts - lkp :: Maybe CanonicalCt -> CanonicalCt -> Maybe CanonicalCt - lkp Nothing ct@(CTyEqCan {cc_tyvar = tv'}) | tv' == tv = Just ct - lkp other _ct = other - haveBeenImproved :: FDImprovements -> PredType -> PredType -> Bool haveBeenImproved [] _ _ = False haveBeenImproved ((pty1,pty2):fdimprs) pty1' pty2' @@ -264,6 +210,8 @@ getFDImprovements = inert_fds \end{code} +{-- DV: This note will go away! + Note [Touchables and givens] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Touchable variables will never show up in givens which are inputs to @@ -304,6 +252,10 @@ we may end up with something like which we should flip around to generate the solved constraint alpha ~s b. +-} + + + %********************************************************************* %* * * Main Interaction Solver * @@ -331,7 +283,6 @@ type WorkItem = CanonicalCt -- constraint pulled from WorkList -- A mixture of Given, Wanted, and Derived constraints. -- We split between equalities and the rest to process equalities first. type WorkList = CanonicalCts -type SWorkList = WorkList -- A worklist of solved unionWorkLists :: WorkList -> WorkList -> WorkList unionWorkLists = andCCan @@ -509,7 +460,7 @@ Note [Efficient Orientation] There are two cases where we have to be careful about orienting equalities to get better efficiency. -Case 2: In Rewriting Equalities (function rewriteEqLHS) +Case 1: In Rewriting Equalities (function rewriteEqLHS) When rewriting two equalities with the same LHS: (a) (tv ~ xi1) @@ -522,56 +473,24 @@ Case 2: In Rewriting Equalities (function rewriteEqLHS) This choice is implemented using the WhichComesFromInert flag. -Case 2: In Spontaneous Solving - Example 2a: - Inerts: [w1] : D alpha - [w2] : C beta - [w3] : F alpha ~ Int - [w4] : H beta ~ Int - Untouchables = [beta] - Then a wanted (beta ~ alpha) comes along. - 1) While interacting with the inerts it is going to kick w2,w4 - out of the inerts - 2) Then, it will spontaneoulsy be solved by (alpha := beta) - 3) Now (and here is the tricky part), to add him back as - solved (alpha ~ beta) is no good because, in the next - iteration, it will kick out w1,w3 as well so we will end up - with *all* the inert equalities back in the worklist! - - So it is tempting to just add (beta ~ alpha) instead, that is, - maintain the original orietnation of the constraint. - - But that does not work very well, because it may cause the - "double unification problem" (See Note [Avoid double unifications]). - For instance: - - Example 2b: - [w1] : fsk1 ~ alpha - [w2] : fsk2 ~ alpha - --- - At the end of the interaction suppose we spontaneously solve alpha := fsk1 - but keep [Given] fsk1 ~ alpha. Then, the second time around we see the - constraint (fsk2 ~ alpha), and we unify *again* alpha := fsk2, which is wrong. - - Our conclusion is that, while in some cases (Example 2a), it makes sense to - preserve the original orientation, it is hard to do this in a sound way. - So we *don't* do this for now, @solveWithIdentity@ outputs a constraint that - is oriented with the unified variable on the left. - -Case 3: Functional Dependencies and IP improvement work - TODO. Optimisation not yet implemented there. +Case 2: Functional Dependencies + Again, we should prefer, if possible, the inert variables on the RHS + +Case 3: IP improvement work + We must always rewrite so that the inert type is on the right. \begin{code} spontaneousSolveStage :: SimplifierStage spontaneousSolveStage workItem inerts - = do { mSolve <- trySpontaneousSolve workItem inerts + = do { mSolve <- trySpontaneousSolve workItem + ; case mSolve of - Nothing -> -- no spontaneous solution for him, keep going + SPCantSolve -> -- No spontaneous solution for him, keep going return $ SR { sr_new_work = emptyWorkList , sr_inerts = inerts , sr_stop = ContinueWith workItem } - Just (workItem', workList') + SPSolved workItem' | not (isGivenCt workItem) -- Original was wanted or derived but we have now made him -- given so we have to interact him with the inerts due to @@ -582,80 +501,86 @@ spontaneousSolveStage workItem inerts [ ("recursive interact with inert eqs", interactWithInertEqsStage) , ("recursive interact with inerts", interactWithInertsStage) ] inerts workItem' - ; return $ SR { sr_new_work = new_work `unionWorkLists` workList' - , sr_inerts = new_inert -- will include workItem' - , sr_stop = Stop } + ; return $ SR { sr_new_work = new_work + , sr_inerts = new_inert -- will include workItem' + , sr_stop = Stop } } | otherwise -> -- Original was given; he must then be inert all right, and -- workList' are all givens from flattening - return $ SR { sr_new_work = workList' + return $ SR { sr_new_work = emptyWorkList , sr_inerts = inerts `updInertSet` workItem' , sr_stop = Stop } + SPError -> -- Return with no new work + return $ SR { sr_new_work = emptyWorkList + , sr_inerts = inerts + , sr_stop = Stop } } +data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError +-- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable +-- SPSolved workItem' gives us a new *given* to go on +-- SPError means that it's completely impossible to solve this equality, eg due to a kind error + + -- @trySpontaneousSolve wi@ solves equalities where one side is a --- touchable unification variable. Returns: --- * Nothing if we were not able to solve it --- * Just wi' if we solved it, wi' (now a "given") should be put in the work list. +-- touchable unification variable. -- See Note [Touchables and givens] --- NB: just passing the inerts through for the skolem equivalence classes -trySpontaneousSolve :: WorkItem -> InertSet -> TcS (Maybe (WorkItem, SWorkList)) -trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) inerts +trySpontaneousSolve :: WorkItem -> TcS SPSolveResult +trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi }) | isGiven gw - = return Nothing + = return SPCantSolve | Just tv2 <- tcGetTyVar_maybe xi = do { tch1 <- isTouchableMetaTyVar tv1 ; tch2 <- isTouchableMetaTyVar tv2 ; case (tch1, tch2) of - (True, True) -> trySpontaneousEqTwoWay inerts cv gw tv1 tv2 - (True, False) -> trySpontaneousEqOneWay inerts cv gw tv1 xi - (False, True) -> trySpontaneousEqOneWay inerts cv gw tv2 (mkTyVarTy tv1) - _ -> return Nothing } + (True, True) -> trySpontaneousEqTwoWay cv gw tv1 tv2 + (True, False) -> trySpontaneousEqOneWay cv gw tv1 xi + (False, True) -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1) + _ -> return SPCantSolve } | otherwise = do { tch1 <- isTouchableMetaTyVar tv1 - ; if tch1 then trySpontaneousEqOneWay inerts cv gw tv1 xi + ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" (ppr workItem) - ; return Nothing } + ; return SPCantSolve } } -- No need for -- trySpontaneousSolve (CFunEqCan ...) = ... -- See Note [No touchables as FunEq RHS] in TcSMonad -trySpontaneousSolve _ _ = return Nothing +trySpontaneousSolve _ = return SPCantSolve ---------------- -trySpontaneousEqOneWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> Xi - -> TcS (Maybe (WorkItem,SWorkList)) +trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult -- tv is a MetaTyVar, not untouchable -trySpontaneousEqOneWay inerts cv gw tv xi +trySpontaneousEqOneWay cv gw tv xi | not (isSigTyVar tv) || isTyVarTy xi - = do { kxi <- zonkTcTypeTcS xi >>= return . typeKind -- Must look through the TcTyBinds - -- hence kxi and not typeKind xi - -- See Note [Kind Errors] + = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts + -- so we have its more specific kind in our hands ; if kxi `isSubKind` tyVarKind tv then - solveWithIdentity inerts cv gw tv xi + solveWithIdentity cv gw tv xi else if tyVarKind tv `isSubKind` kxi then - return Nothing -- kinds are compatible but we can't solveWithIdentity this way - -- This case covers the a_touchable :: * ~ b_untouchable :: ?? - -- which has to be deferred or floated out for someone else to solve - -- it in a scope where 'b' is no longer untouchable. - else kindErrorTcS gw (mkTyVarTy tv) xi -- See Note [Kind errors] + return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way + -- This case covers the a_touchable :: * ~ b_untouchable :: ?? + -- which has to be deferred or floated out for someone else to solve + -- it in a scope where 'b' is no longer untouchable. + else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors] + ; return SPError } } | otherwise -- Still can't solve, sig tyvar and non-variable rhs - = return Nothing + = return SPCantSolve ---------------- -trySpontaneousEqTwoWay :: InertSet -> CoVar -> CtFlavor -> TcTyVar -> TcTyVar - -> TcS (Maybe (WorkItem,SWorkList)) +trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here -trySpontaneousEqTwoWay inerts cv gw tv1 tv2 +trySpontaneousEqTwoWay cv gw tv1 tv2 | k1 `isSubKind` k2 - , nicer_to_update_tv2 = solveWithIdentity inerts cv gw tv2 (mkTyVarTy tv1) + , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1) | k2 `isSubKind` k1 - = solveWithIdentity inerts cv gw tv1 (mkTyVarTy tv2) + = solveWithIdentity cv gw tv1 (mkTyVarTy tv2) | otherwise -- None is a subkind of the other, but they are both touchable! - = kindErrorTcS gw (mkTyVarTy tv1) (mkTyVarTy tv2) -- See Note [Kind errors] + = do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2) + ; return SPError } where k1 = tyVarKind tv1 k2 = tyVarKind tv2 @@ -668,22 +593,20 @@ Consider the wanted problem: alpha ~ (# Int, Int #) where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' -simply returns @Nothing@ then that wanted constraint is going to propagate all the way and +simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and get quantified over in inference mode. That's bad because we do know at this point that the -constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails. +constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on. The same applies in canonicalization code in case of kind errors in the givens. However, when we canonicalize givens we only check for compatibility (@compatKind@). -If there were a kind error in the givens, this means some form of inconsistency or dead code. - -When we spontaneously solve wanteds we may have to look through the bindings, hence we -call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and -a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is -still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead -of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try -to detect whether spontaneous solving is possible. +If there were a kind error in the givens, this means some form of inconsistency or dead code. +You may think that when we spontaneously solve wanteds we may have to look through the +bindings to determine the right kind of the RHS type. E.g one may be worried that xi is +@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *). +But we orient our constraints so that spontaneously solved ones can rewrite all other constraint +so this situation can't happen. Note [Spontaneous solving and kind compatibility] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -714,106 +637,6 @@ Caveat: Whereas we would be able to apply the type instance, we would not be able to use the given (T Bool ~ (->)) in the body of 'flop' -Note [Loopy Spontaneous Solving] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Example 1: [The problem of loopy spontaneous solving] ----------- -Consider the original wanted: - wanted : Maybe (E alpha) ~ alpha -where E is a type family, such that E (T x) = x. After canonicalization, -as a result of flattening, we will get: - given : E alpha ~ fsk - wanted : alpha ~ Maybe fsk -where (fsk := E alpha, on the side). Now, if we spontaneously *solve* -(alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving -it and keep it as wanted. In inference mode we'll end up quantifying over - (alpha ~ Maybe (E alpha)) -Hence, 'solveWithIdentity' performs a small occurs check before -actually solving. But this occurs check *must look through* flatten skolems. - -However, it may be the case that the flatten skolem in hand is equal to some other -flatten skolem whith *does not* mention our unification variable. Here's a typical example: - -Example 2: [The need of keeping track of flatten skolem equivalence classes] ----------- -Original wanteds: - g: F alpha ~ F beta - w: alpha ~ F alpha -After canonicalization: - g: F beta ~ f1 - g: F alpha ~ f1 - w: alpha ~ f2 - g: F alpha ~ f2 -After some reactions: - g: f1 ~ f2 - g: F beta ~ f1 - w: alpha ~ f2 - g: F alpha ~ f2 -At this point, we will try to spontaneously solve (alpha ~ f2) which remains as yet unsolved. -We will look inside f2, which immediately mentions (F alpha), so it's not good to unify! However -by looking at the equivalence class of the flatten skolems, we can see that it is fine to -unify (alpha ~ f1) which solves our goals! - -Example 3: [The need of looking through TyBinds for already spontaneously solved variables] ----------- -A similar problem happens because of other spontaneous solving. Suppose we have the -following wanteds, arriving in this exact order: - (first) w: beta ~ alpha - (second) w: alpha ~ fsk - (third) g: F beta ~ fsk -Then, we first spontaneously solve the first constraint, making (beta := alpha), and having -(beta ~ alpha) as given. *Then* we encounter the second wanted (alpha ~ fsk). "fsk" does not -obviously mention alpha, so naively we can also spontaneously solve (alpha := fsk). But -that is wrong since fsk mentions beta, which has already secretly been unified to alpha! - -To avoid this problem, the same occurs check must unveil rewritings that can happen because -of spontaneously having solved other constraints. - -Example 4: [Orientation of (tv ~ xi) equalities] ----------- -We orient equalities (tv ~ xi) so that flatten skolems appear on the left, if possible. Here -is an example of why this is needed: - - [Wanted] w1: alpha ~ fsk - [Given] g1: F alpha ~ fsk - [Given] g2: b ~ fsk - Flatten skolem equivalence class = [] - -Assume that g2 is *not* oriented properly, as shown above. Then we would like to spontaneously -solve w1 but we can't set alpha := fsk, since fsk hides the type F alpha. However, by using -the equation g2 it would be possible to solve w1 by setting alpha := b. In other words, it is -not enough to look at a flatten skolem equivalence class to try to find alternatives to unify -with. We may have to go to other variables. - -By orienting the equalities so that flatten skolems are in the LHS we are eliminating them -as much as possible from the RHS of other wanted equalities, and hence it suffices to look -in their flatten skolem equivalence classes. - -NB: This situation appears in the IndTypesPerf test case, inside indexed-types/. - -Caveat: You may wonder if we should be doing this for unification variables as well. -However, Note [Efficient Orientation], Case 2, demonstrates that this is not possible -at least for touchable unification variables which we have to keep oriented with the -touchable on the LHS to be able to eliminate it. So then, what about untouchables? - -Example 4a: ------------ - Untouchable = beta, Touchable = alpha - - [Wanted] w1: alpha ~ fsk - [Given] g1: F alpha ~ fsk - [Given] g2: beta ~ fsk - Flatten skolem equivalence class = [] - -Should we be able to unify alpha := beta to solve the constraint? Arguably yes, but -that implies that an *untouchable* unification variable (beta) is in the same equivalence -class as a flatten skolem that mentions @alpha@. I.e. g2 means that: - beta ~ F alpha -But I do not think that there is any way to produce evidence for such a constraint from -the outside other than beta := F alpha, which violates the OutsideIn-ness. - - Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -825,7 +648,7 @@ We spontaneously solve the first wanted, without changing the order! Now the second wanted comes along, but he cannot rewrite the given, so we simply continue. At the end we spontaneously solve that guy, *reunifying* [alpha := Int] -We avoid this problem by orienting the given so that the unification +We avoid this problem by orienting the resulting given so that the unification variable is on the left. [Note that alternatively we could attempt to enforce this at canonicalization] @@ -835,153 +658,40 @@ unification variables as RHS of type family equations: F xis ~ alpha. \begin{code} ---------------- -solveWithIdentity :: InertSet - -> CoVar -> CtFlavor -> TcTyVar -> Xi - -> TcS (Maybe (WorkItem, SWorkList)) + +solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult -- Solve with the identity coercion -- Precondition: kind(xi) is a sub-kind of kind(tv) -- Precondition: CtFlavor is Wanted or Derived -- See [New Wanted Superclass Work] to see why solveWithIdentity -- must work for Derived as well as Wanted --- Returns: (workItem, workList) where +-- Returns: workItem where -- workItem = the new Given constraint --- workList = some additional work that may have been produced as a result of flattening --- in case we did some chasing through flatten skolem equivalence classes. -solveWithIdentity inerts cv gw tv xi - = do { tybnds <- getTcSTyBindsMap - ; case occurCheck tybnds inerts tv xi of - Nothing -> return Nothing - Just (xi_unflat,coi) -> solve_with xi_unflat coi } - where - solve_with xi_unflat coi -- coi : xi_unflat ~ xi - = do { traceTcS "Sneaky unification:" $ - vcat [text "Coercion variable: " <+> ppr gw, +solveWithIdentity cv wd tv xi + = do { traceTcS "Sneaky unification:" $ + vcat [text "Coercion variable: " <+> ppr wd, text "Coercion: " <+> pprEq (mkTyVarTy tv) xi, text "Left Kind is : " <+> ppr (typeKind (mkTyVarTy tv)), text "Right Kind is : " <+> ppr (typeKind xi) ] - ; setWantedTyBind tv xi_unflat -- Set tv := xi_unflat - ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat - ; let flav = mkGivenFlavor gw UnkSkol - ; (ct,cts, co) <- case coi of - ACo co -> do { (cc,ccs) <- canEqLeafTyVarLeft flav cv_given tv xi_unflat - ; return (cc, ccs, co) } - IdCo co -> return $ (CTyEqCan { cc_id = cv_given - , cc_flavor = mkGivenFlavor gw UnkSkol - , cc_tyvar = tv, cc_rhs = xi } - -- xi, *not* xi_unflat because - -- xi_unflat may require flattening! - , emptyWorkList, co) - ; case gw of - Wanted {} -> setWantedCoBind cv co - Derived {} -> setDerivedCoBind cv co - _ -> pprPanic "Can't spontaneously solve *given*" empty - -- See Note [Avoid double unifications] - ; return $ Just (ct,cts) - } - --- ; let flav = mkGivenFlavor gw UnkSkol --- ; (cts, co) <- case coi of --- -- TODO: Optimise this, along the way it used to be --- ACo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi_unflat xi_unflat --- ; setWantedTyBind tv xi_unflat --- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi_unflat --- ; return (can_eqs, co) } --- IdCo co -> do { cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi --- ; setWantedTyBind tv xi --- ; can_eqs <- canEq flav cv_given (mkTyVarTy tv) xi --- ; return (can_eqs, co) } --- ; case gw of --- Wanted {} -> setWantedCoBind cv co --- Derived {} -> setDerivedCoBind cv co --- _ -> pprPanic "Can't spontaneously solve *given*" empty --- -- See Note [Avoid double unifications] --- ; return $ Just cts } - -occurCheck :: VarEnv (TcTyVar, TcType) -> InertSet - -> TcTyVar -> TcType -> Maybe (TcType,CoercionI) --- Traverse @ty@ to make sure that @tv@ does not appear under some flatten skolem. --- If it appears under some flatten skolem look in that flatten skolem equivalence class --- (see Note [InertSet FlattenSkolemEqClass], [Loopy Spontaneous Solving]) to see if you --- can find a different flatten skolem to use, that is, one that does not mention @tv@. --- --- Postcondition: Just (ty', coi) = occurCheck binds inerts tv ty --- coi :: ty' ~ ty --- NB: The returned type ty' may not be flat! - -occurCheck ty_binds inerts the_tv the_ty - = ok emptyVarSet the_ty - where - -- If (fsk `elem` bad) then tv occurs in any rendering - -- of the type under the expansion of fsk - ok bad this_ty@(TyConApp tc tys) - | Just tys_cois <- allMaybes (map (ok bad) tys) - , (tys',cois') <- unzip tys_cois - = Just (TyConApp tc tys', mkTyConAppCoI tc cois') - | isSynTyCon tc, Just ty_expanded <- tcView this_ty - = ok bad ty_expanded -- See Note [Type synonyms and the occur check] in TcUnify - ok bad (PredTy sty) - | Just (sty',coi) <- ok_pred bad sty - = Just (PredTy sty', coi) - ok bad (FunTy arg res) - | Just (arg', coiarg) <- ok bad arg, Just (res', coires) <- ok bad res - = Just (FunTy arg' res', mkFunTyCoI coiarg coires) - ok bad (AppTy fun arg) - | Just (fun', coifun) <- ok bad fun, Just (arg', coiarg) <- ok bad arg - = Just (AppTy fun' arg', mkAppTyCoI coifun coiarg) - ok bad (ForAllTy tv1 ty1) - -- WARNING: What if it is a (t1 ~ t2) => t3? It's not handled properly at the moment. - | Just (ty1', coi) <- ok bad ty1 - = Just (ForAllTy tv1 ty1', mkForAllTyCoI tv1 coi) - - -- Variable cases - ok bad this_ty@(TyVarTy tv) - | tv == the_tv = Nothing -- Occurs check error - | not (isTcTyVar tv) = Just (this_ty, IdCo this_ty) -- Bound var - | FlatSkol zty <- tcTyVarDetails tv = ok_fsk bad tv zty - | Just (_,ty) <- lookupVarEnv ty_binds tv = ok bad ty - | otherwise = Just (this_ty, IdCo this_ty) - - -- Check if there exists a ty bind already, as a result of sneaky unification. - -- Fall through - ok _bad _ty = Nothing - - ----------- - ok_pred bad (ClassP cn tys) - | Just tys_cois <- allMaybes $ map (ok bad) tys - = let (tys', cois') = unzip tys_cois - in Just (ClassP cn tys', mkClassPPredCoI cn cois') - ok_pred bad (IParam nm ty) - | Just (ty',co') <- ok bad ty - = Just (IParam nm ty', mkIParamPredCoI nm co') - ok_pred bad (EqPred ty1 ty2) - | Just (ty1',coi1) <- ok bad ty1, Just (ty2',coi2) <- ok bad ty2 - = Just (EqPred ty1' ty2', mkEqPredCoI coi1 coi2) - ok_pred _ _ = Nothing - - ----------- - ok_fsk bad fsk zty - | fsk `elemVarSet` bad - -- We are already trying to find a rendering of fsk, - -- and to do that it seems we need a rendering, so fail - = Nothing - | otherwise - = firstJusts (ok new_bad zty : map (go_under_fsk new_bad) fsk_equivs) - where - fsk_equivs = getFskEqClass inerts fsk - new_bad = bad `extendVarSetList` (fsk : map fst fsk_equivs) - - ----------- - go_under_fsk bad_tvs (fsk,co) - | FlatSkol zty <- tcTyVarDetails fsk - = case ok bad_tvs zty of - Nothing -> Nothing - Just (ty,coi') -> Just (ty, mkTransCoI coi' (ACo co)) - | otherwise = pprPanic "go_down_equiv" (ppr fsk) + ; setWantedTyBind tv xi -- Set tv := xi_unflat + ; cv_given <- newGivOrDerCoVar (mkTyVarTy tv) xi xi + + ; case wd of Wanted {} -> setWantedCoBind cv xi + Derived {} -> setDerivedCoBind cv xi + _ -> pprPanic "Can't spontaneously solve given!" empty + + ; return $ SPSolved (CTyEqCan { cc_id = cv_given + , cc_flavor = mkGivenFlavor wd UnkSkol + , cc_tyvar = tv, cc_rhs = xi }) + } + \end{code} + + ********************************************************************************* * * The interact-with-inert Stage @@ -1009,8 +719,9 @@ data InteractResult } -- What to do with the inert reactant. -data InertAction = KeepInert | DropInert - deriving Eq +data InertAction = KeepInert + | DropInert + | KeepTransformedInert CanonicalCt -- Keep a slightly transformed inert mkIRContinue :: Monad m => WorkItem -> InertAction -> WorkList -> m InteractResult mkIRContinue wi keep newWork = return $ IR (ContinueWith wi) keep newWork Nothing @@ -1028,7 +739,7 @@ noInteraction :: Monad m => WorkItem -> m InteractResult noInteraction workItem = mkIRContinue workItem KeepInert emptyWorkList data WhichComesFromInert = LeftComesFromInert | RightComesFromInert - -- See Note [Efficient Orientation, Case 2] + -- See Note [Efficient Orientation] --------------------------------------------------- @@ -1039,8 +750,7 @@ data WhichComesFromInert = LeftComesFromInert | RightComesFromInert interactWithInertEqsStage :: SimplifierStage interactWithInertEqsStage workItem inert = foldISEqCtsM interactNext initITR inert - where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- We will fold over the equalities - , inert_fsks = Map.empty -- which will generate those two again + where initITR = SR { sr_inerts = IS { inert_eqs = emptyCCan -- Will fold over equalities , inert_dicts = inert_dicts inert , inert_ips = inert_ips inert , inert_funeqs = inert_funeqs inert @@ -1080,9 +790,9 @@ interactWithInertsStage workItem inert -- TODO: if we were caching variables, we'd know that only -- some are relevant. Experiment with this for now. = let cts = cCanMapToBag (inert_ips is) `unionBags` - cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is) - in (cts, is { inert_dicts = emptyCCanMap - , inert_ips = emptyCCanMap + cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is) + in (cts, is { inert_dicts = emptyCCanMap + , inert_ips = emptyCCanMap , inert_funeqs = emptyCCanMap }) interactNext :: StageResult -> AtomicInert -> TcS StageResult @@ -1093,11 +803,13 @@ interactNext it inert ; ir <- interactWithInert fdimprs_old inert workItem - -- New inerts depend on whether we KeepInert or not and must - -- be updated with FD improvement information from the interaction result (ir) - ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir) - upd_inert = if ir_inert_action ir == KeepInert - then inerts `updInertSet` inert else inerts + -- New inerts depend on whether we KeepInert or not and must + -- be updated with FD improvement information from the interaction result (ir) + ; let inerts_new = updInertSetFDImprs upd_inert (ir_improvement ir) + upd_inert = case ir_inert_action ir of + KeepInert -> inerts `updInertSet` inert + DropInert -> inerts + KeepTransformedInert inert' -> inerts `updInertSet` inert' ; return $ SR { sr_inerts = inerts_new , sr_new_work = sr_new_work it `unionWorkLists` ir_new_work ir @@ -1113,11 +825,11 @@ interactWithInert fdimprs inert workitem inert_ev = cc_id inert work_ev = cc_id workitem - -- Never interact a wanted and a derived where the derived's evidence - -- mentions the wanted evidence in an unguarded way. - -- See Note [Superclasses and recursive dictionaries] - -- and Note [New Wanted Superclass Work] - -- We don't have to do this for givens, as we fully know the evidence for them. + -- Never interact a wanted and a derived where the derived's evidence + -- mentions the wanted evidence in an unguarded way. + -- See Note [Superclasses and recursive dictionaries] + -- and Note [New Wanted Superclass Work] + -- We don't have to do this for givens, as we fully know the evidence for them. ; rec_ev_ok <- case (cc_flavor inert, cc_flavor workitem) of (Wanted loc, Derived {}) -> isGoodRecEv work_ev (WantedEvVar inert_ev loc) @@ -1142,18 +854,19 @@ doInteractWithInert :: FDImprovements -> CanonicalCt -> CanonicalCt -> TcS Inter doInteractWithInert fdimprs (CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) - workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) + workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 }) | cls1 == cls2 && (and $ zipWith tcEqType tys1 tys2) = solveOneFromTheOther (d1,fl1) workItem | cls1 == cls2 && (not (isGiven fl1 && isGiven fl2)) = -- See Note [When improvement happens] - do { let pty1 = ClassP cls1 tys1 - pty2 = ClassP cls2 tys2 - work_item_pred_loc = (pty2, ppr d2) - inert_pred_loc = (pty1, ppr d1) + do { let pty1 = ClassP cls1 tys1 + pty2 = ClassP cls2 tys2 + work_item_pred_loc = (pty2, pprFlavorArising fl2) + inert_pred_loc = (pty1, pprFlavorArising fl1) loc = combineCtLoc fl1 fl2 - eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc + eqn_pred_locs = improveFromAnother work_item_pred_loc inert_pred_loc + -- See Note [Efficient Orientation] ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs ; fd_work <- canWanteds wevvars @@ -1231,30 +944,28 @@ doInteractWithInert _fdimprs | nm1 == nm2 = -- See Note [When improvement happens] - do { co_var <- newWantedCoVar ty1 ty2 + do { co_var <- newWantedCoVar ty2 ty1 -- See Note [Efficient Orientation] ; let flav = Wanted (combineCtLoc ifl wfl) ; cans <- mkCanonical flav co_var ; mkIRContinue workItem KeepInert cans } --- Inert: equality, work item: function equality -- Never rewrite a given with a wanted equality, and a type function --- equality can never rewrite an equality. Note also that if we have --- F x1 ~ x2 and a ~ x3, and a occurs in x2, we don't rewrite it. We --- can wait until F x1 ~ x2 matches another F x1 ~ x4, and only then --- we will ``expose'' x2 and x4 to rewriting. +-- equality can never rewrite an equality. We rewrite LHS *and* RHS +-- of function equalities so that our inert set exposes everything that +-- we know about equalities. --- Otherwise, we can try rewriting the type function equality with the equality. +-- Inert: equality, work item: function equality doInteractWithInert _fdimprs (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 }) (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc , cc_tyargs = args, cc_rhs = xi2 }) | ifl `canRewrite` wfl - , tv `elemVarSet` tyVarsOfTypes args + , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2) ; mkIRStop KeepInert (workListFromCCan rewritten_funeq) } - -- must Stop here, because we may no longer be inert after the rewritting. + -- Must Stop here, because we may no longer be inert after the rewritting. -- Inert: function equality, work item: equality doInteractWithInert _fdimprs @@ -1262,9 +973,17 @@ doInteractWithInert _fdimprs , cc_tyargs = args, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 }) | wfl `canRewrite` ifl - , tv `elemVarSet` tyVarsOfTypes args + , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1) ; mkIRContinue workItem DropInert (workListFromCCan rewritten_funeq) } + -- One may think that we could (KeepTransformedInert rewritten_funeq) + -- but that is wrong, because it may end up not being inert with respect + -- to future inerts. Example: + -- Original inert = { F xis ~ [a], b ~ Maybe Int } + -- Work item comes along = a ~ [b] + -- If we keep { F xis ~ [b] } in the inert set we will end up with: + -- { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] } + -- At the end, which is *not* inert. So we should unfortunately DropInert here. doInteractWithInert _fdimprs (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1 @@ -1281,7 +1000,7 @@ doInteractWithInert _fdimprs lhss_match = tc1 == tc2 && and (zipWith tcEqType args1 args2) doInteractWithInert _fdimprs - inert@(CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) + (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 }) workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 }) -- Check for matching LHS | fl1 `canSolve` fl2 && tv1 == tv2 @@ -1290,8 +1009,7 @@ doInteractWithInert _fdimprs | fl2 `canSolve` fl1 && tv1 == tv2 = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCoercion cv2,xi2) (cv1,fl1,xi1) - ; mkIRContinue workItem DropInert cans } - + ; mkIRContinue workItem DropInert cans } -- Check for rewriting RHS | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2 = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2) @@ -1300,19 +1018,6 @@ doInteractWithInert _fdimprs = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1) ; mkIRContinue workItem DropInert rewritten_eq } --- Finally, if workitem is a Flatten Equivalence Class constraint and the --- inert is a wanted constraint, even when the workitem cannot rewrite the --- inert, drop the inert out because you may have to reconsider solving the --- inert *using* the equivalence class you created. See note [Loopy Spontaneous Solving] --- and [InertSet FlattenSkolemEqClass] - - | not $ isGiven fl1, -- The inert is wanted or derived - isMetaTyVar tv1, -- and has a unification variable lhs - FlatSkol {} <- tcTyVarDetails tv2, -- And workitem is a flatten skolem equality - Just tv2' <- tcGetTyVar_maybe xi2, FlatSkol {} <- tcTyVarDetails tv2' - = mkIRContinue workItem DropInert (workListFromCCan inert) - - -- Fall-through case for all other situations doInteractWithInert _fdimprs _ workItem = noInteraction workItem @@ -1347,22 +1052,27 @@ rewriteIP (cv,tv,xi) (ipid,gw,nm,ty) , cc_ip_ty = ty' }) } rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt -rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) +rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2) -- cv2 :: F args ~ xi2 = do { let arg_cos = substTysWith [tv] [mkCoVarCoercion cv1] args args' = substTysWith [tv] [xi1] args - fun_co = mkTyConCoercion tc arg_cos + fun_co = mkTyConCoercion tc arg_cos -- fun_co :: F args ~ F args' + + xi2' = substTyWith [tv] [xi1] xi2 + xi2_co = substTyWith [tv] [mkCoVarCoercion cv1] xi2 -- xi2_co :: xi2 ~ xi2' ; cv2' <- case gw of - Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2 + Wanted {} -> do { cv2' <- newWantedCoVar (mkTyConApp tc args') xi2' ; setWantedCoBind cv2 $ - mkTransCoercion fun_co (mkCoVarCoercion cv2') + fun_co `mkTransCoercion` + mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion xi2_co ; return cv2' } - _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2 $ - mkTransCoercion (mkSymCoercion fun_co) (mkCoVarCoercion cv2) + _giv_or_der -> newGivOrDerCoVar (mkTyConApp tc args') xi2' $ + mkSymCoercion fun_co `mkTransCoercion` + mkCoVarCoercion cv2 `mkTransCoercion` xi2_co ; return (CFunEqCan { cc_id = cv2' , cc_flavor = gw , cc_tyargs = args' , cc_fun = tc - , cc_rhs = xi2 }) } + , cc_rhs = xi2' }) } rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList @@ -1377,20 +1087,19 @@ rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2) , tv2 == tv2' -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2 = do { when (isWanted gw) (setWantedCoBind cv2 (mkSymCoercion co2')) ; return emptyCCan } - | otherwise - = do { cv2' <- - case gw of - Wanted {} - -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2' - ; setWantedCoBind cv2 $ + | otherwise + = do { cv2' <- + case gw of + Wanted {} + -> do { cv2' <- newWantedCoVar (mkTyVarTy tv2) xi2' + ; setWantedCoBind cv2 $ mkCoVarCoercion cv2' `mkTransCoercion` mkSymCoercion co2' - ; return cv2' } + ; return cv2' } _giv_or_der -> newGivOrDerCoVar (mkTyVarTy tv2) xi2' $ mkCoVarCoercion cv2 `mkTransCoercion` co2' - ; xi2'' <- canOccursCheck gw tv2 xi2' -- we know xi2' is *not* tv2 - ; canEq gw cv2' (mkTyVarTy tv2) xi2'' + ; canEq gw cv2' (mkTyVarTy tv2) xi2' } where xi2' = substTyWith [tv1] [xi1] xi2 @@ -1866,9 +1575,9 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Given loc -- Do not add any further derived superclasses; their -- full transitive closure has already been added. -- But do look for functional dependencies -doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Derived loc _ +doTopReact workItem@(CDictCan { cc_flavor = Derived loc _ , cc_class = cls, cc_tyargs = xis }) - = do { fd_work <- findClassFunDeps dv cls xis loc + = do { fd_work <- findClassFunDeps cls xis loc ; if isEmptyWorkList fd_work then return NoTopInt else return $ SomeTopInt { tir_new_work = fd_work @@ -1881,7 +1590,7 @@ doTopReact workItem@(CDictCan { cc_id = dv, cc_flavor = Wanted loc ; case lkp_inst_res of NoInstance -> do { traceTcS "doTopReact/ no class instance for" (ppr dv) - ; fd_work <- findClassFunDeps dv cls xis loc + ; fd_work <- findClassFunDeps cls xis loc ; if isEmptyWorkList fd_work then do { sc_work <- newDerivedSCWork dv loc cls xis -- See Note [Adding Derived Superclasses] @@ -1961,13 +1670,13 @@ doTopReact (CFunEqCan { cc_id = cv, cc_flavor = fl doTopReact _workItem = return NoTopInt ---------------------- -findClassFunDeps :: EvVar -> Class -> [Xi] -> WantedLoc -> TcS WorkList +findClassFunDeps :: Class -> [Xi] -> WantedLoc -> TcS WorkList -- Look for a fundep reaction beween the wanted item -- and a top-level instance declaration -findClassFunDeps dv cls xis loc +findClassFunDeps cls xis loc = do { instEnvs <- getInstEnvs ; let eqn_pred_locs = improveFromInstEnv (classInstances instEnvs) - (ClassP cls xis, ppr dv) + (ClassP cls xis, pprArisingAt loc) ; wevvars <- mkWantedFunDepEqns loc eqn_pred_locs -- NB: fundeps generate some wanted equalities, but -- we don't use their evidence for anything diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index 641319f..387961a 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -37,7 +37,7 @@ module TcRnTypes( Implication(..), CtLoc(..), ctLocSpan, ctLocOrigin, setCtLocOrigin, CtOrigin(..), EqOrigin(..), - WantedLoc, GivenLoc, + WantedLoc, GivenLoc, pushErrCtxt, SkolemInfo(..), @@ -879,12 +879,19 @@ ctLocOrigin (CtLoc o _ _) = o setCtLocOrigin :: CtLoc o -> o' -> CtLoc o' setCtLocOrigin (CtLoc _ s c) o = CtLoc o s c +pushErrCtxt :: orig -> ErrCtxt -> CtLoc orig -> CtLoc orig +pushErrCtxt o err (CtLoc _ s errs) = CtLoc o s (err:errs) + pprArising :: CtOrigin -> SDoc +-- Used for the main, top-level error message +-- We've done special processing for TypeEq and FunDep origins pprArising (TypeEqOrigin {}) = empty +pprArising FunDepOrigin = empty pprArising orig = text "arising from" <+> ppr orig -pprArisingAt :: CtLoc CtOrigin -> SDoc -pprArisingAt (CtLoc o s _) = sep [pprArising o, text "at" <+> ppr s] +pprArisingAt :: Outputable o => CtLoc o -> SDoc +pprArisingAt (CtLoc o s _) = sep [ text "arising from" <+> ppr o + , text "at" <+> ppr s] ------------------------------------------- -- CtOrigin gives the origin of *wanted* constraints @@ -916,9 +923,10 @@ data CtOrigin | StandAloneDerivOrigin -- Typechecking stand-alone deriving | DefaultOrigin -- Typechecking a default decl | DoOrigin -- Arising from a do expression - | IfOrigin -- Arising from an if statement + | IfOrigin -- Arising from an if statement | ProcOrigin -- Arising from a proc expression | AnnOrigin -- An annotation + | FunDepOrigin data EqOrigin = UnifyOrigin @@ -953,6 +961,7 @@ pprO DoOrigin = ptext (sLit "a do statement") pprO ProcOrigin = ptext (sLit "a proc expression") pprO (TypeEqOrigin eq) = ptext (sLit "an equality") <+> ppr eq pprO AnnOrigin = ptext (sLit "an annotation") +pprO FunDepOrigin = ptext (sLit "a functional dependency") instance Outputable EqOrigin where ppr (UnifyOrigin t1 t2) = ppr t1 <+> char '~' <+> ppr t2 diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 3d8163d..0a68650 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -12,11 +12,12 @@ module TcSMonad ( makeGivens, makeSolvedByInst, CtFlavor (..), isWanted, isGiven, isDerived, isDerivedSC, isDerivedByInst, - isGivenCt, isWantedCt, + isGivenCt, isWantedCt, pprFlavorArising, DerivedOrig (..), canRewrite, canSolve, - combineCtLoc, mkGivenFlavor, + combineCtLoc, mkGivenFlavor, mkWantedFlavor, + getWantedLoc, TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS, @@ -37,18 +38,20 @@ module TcSMonad ( getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getTcEvBinds, getUntouchables, - getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, - + getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors, + getTcSErrorsBag, FrozenError (..), + addErrorTcS, + ErrorKind(..), newFlattenSkolemTy, -- Flatten skolems instDFunTypes, -- Instantiation - instDFunConstraints, + instDFunConstraints, + newFlexiTcSTy, isGoodRecEv, - zonkTcTypeTcS, -- Zonk through the TyBinds of the Tcs Monad compatKind, @@ -111,6 +114,7 @@ import FunDeps import TcRnTypes +import Control.Monad import Data.IORef \end{code} @@ -154,11 +158,7 @@ data CanonicalCt -- * tv not in tvs(xi) (occurs check) -- * If constraint is given then typeKind xi `compatKind` typeKind tv -- See Note [Spontaneous solving and kind compatibility] - -- * If 'xi' is a flatten skolem then 'tv' can only be: - -- - a flatten skolem or a unification variable - -- i.e. equalities prefer flatten skolems in their LHS - -- See Note [Loopy Spontaneous Solving, Example 4] - -- Also related to [Flatten Skolem Equivalence Classes] + -- * We prefer unification variables on the left *JUST* for efficiency cc_id :: EvVar, cc_flavor :: CtFlavor, cc_tyvar :: TcTyVar, @@ -167,10 +167,8 @@ data CanonicalCt | CFunEqCan { -- F xis ~ xi -- Invariant: * isSynFamilyTyCon cc_fun - -- * cc_rhs is not a touchable unification variable - -- See Note [No touchables as FunEq RHS] -- * If constraint is given then - -- typeKind (TyConApp cc_fun cc_tyargs) `compatKind` typeKind cc_rhs + -- typeKind (F xis) `compatKind` typeKind xi cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -233,26 +231,6 @@ instance Outputable CanonicalCt where = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty) \end{code} - -Note [No touchables as FunEq RHS] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Notice that (F xis ~ beta), where beta is an touchable unification -variable, is not canonical. Why? - * If (F xis ~ beta) was the only wanted constraint, we'd - definitely want to spontaneously-unify it - - * But suppose we had an earlier wanted (beta ~ Int), and - have already spontaneously unified it. Then we have an - identity given (id : beta ~ Int) in the inert set. - - * But (F xis ~ beta) does not react with that given (because we - don't subsitute on the RHS of a function equality). So there's a - serious danger that we'd spontaneously unify it a second time. - -Hence the invariant. - -The invariant is - Note [Canonical implicit parameter constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The type in a canonical implicit parameter constraint doesn't need to @@ -348,6 +326,19 @@ isDerivedByInst :: CtFlavor -> Bool isDerivedByInst (Derived _ DerInst) = True isDerivedByInst _ = False +pprFlavorArising :: CtFlavor -> SDoc +pprFlavorArising (Derived wl _) = pprArisingAt wl +pprFlavorArising (Wanted wl) = pprArisingAt wl +pprFlavorArising (Given gl) = pprArisingAt gl + +getWantedLoc :: CanonicalCt -> WantedLoc +getWantedLoc ct + = ASSERT (isWanted (cc_flavor ct)) + case cc_flavor ct of + Wanted wl -> wl + _ -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty + + isWantedCt :: CanonicalCt -> Bool isWantedCt ct = isWanted (cc_flavor ct) isGivenCt :: CanonicalCt -> Bool @@ -385,6 +376,11 @@ mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk) mkGivenFlavor (Given loc) sk = Given (setCtLocOrigin loc sk) + +mkWantedFlavor :: CtFlavor -> CtFlavor +mkWantedFlavor (Wanted loc) = Wanted loc +mkWantedFlavor (Derived loc _) = Wanted loc +mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl) \end{code} @@ -417,10 +413,49 @@ data TcSEnv -- Global type bindings tcs_context :: SimplContext, + + tcs_errors :: IORef (Bag FrozenError), + -- Frozen errors that we defer reporting as much as possible, in order to + -- make them as informative as possible. See Note [Frozen Errors] tcs_untch :: Untouchables } +data FrozenError + = FrozenError ErrorKind CtFlavor TcType TcType + +data ErrorKind + = MisMatchError | OccCheckError | KindError + +instance Outputable FrozenError where + ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)" + +\end{code} + +Note [Frozen Errors] +~~~~~~~~~~~~~~~~~~~~ +Some of the errors that we get during canonicalization are best reported when all constraints +have been simplified as much as possible. For instance, assume that during simplification +the following constraints arise: + + [Wanted] F alpha ~ uf1 + [Wanted] beta ~ uf1 beta + +When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply +see a message: + 'Can't construct the infinite type beta ~ uf1 beta' +and the user has no idea what the uf1 variable is. + +Instead our plan is that we will NOT fail immediately, but: + (1) Record the "frozen" error in the tcs_errors field + (2) Isolate the offending constraint from the rest of the inerts + (3) Keep on simplifying/canonicalizing + +At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to +report a more informative error: + 'Can't construct the infinite type beta ~ F alpha beta' +\begin{code} + data SimplContext = SimplInfer -- Inferring type of a let-bound thing | SimplRuleLhs -- Inferring type of a RULE lhs @@ -492,37 +527,40 @@ traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc runTcS :: SimplContext -> Untouchables -- Untouchables -> TcS a -- What to run - -> TcM (a, Bag EvBind) + -> TcM (a, Bag FrozenError, Bag EvBind) runTcS context untouch tcs = do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds + ; err_ref <- TcM.newTcRef emptyBag ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_ty_binds = ty_binds_var - , tcs_context = context - , tcs_untch = untouch } + , tcs_context = context + , tcs_untch = untouch + , tcs_errors = err_ref + } -- Run the computation ; res <- unTcS tcs env - -- Perform the type unifications required ; ty_binds <- TcM.readTcRef ty_binds_var ; mapM_ do_unification (varEnvElts ty_binds) -- And return - ; ev_binds <- TcM.readTcRef evb_ref - ; return (res, evBindMapBinds ev_binds) } + ; frozen_errors <- TcM.readTcRef err_ref + ; ev_binds <- TcM.readTcRef evb_ref + ; return (res, frozen_errors, evBindMapBinds ev_binds) } where do_unification (tv,ty) = TcM.writeMetaTyVar tv ty - nestImplicTcS :: EvBindsVar -> Untouchables -> TcS a -> TcS a nestImplicTcS ref untch (TcS thing_inside) - = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt } -> + = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, tcs_context = ctxt, tcs_errors = err_ref } -> let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_ty_binds = ty_binds , tcs_untch = untch - , tcs_context = ctxtUnderImplic ctxt } + , tcs_context = ctxtUnderImplic ctxt + , tcs_errors = err_ref } in thing_inside nest_env @@ -536,14 +574,16 @@ ctxtUnderImplic :: SimplContext -> SimplContext ctxtUnderImplic SimplRuleLhs = SimplCheck ctxtUnderImplic ctxt = ctxt -tryTcS :: TcS a -> TcS a +tryTcS :: TcS a -> TcS a -- Like runTcS, but from within the TcS monad -- Ignore all the evidence generated, and do not affect caller's evidence! tryTcS tcs = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv ; ev_binds_var <- TcM.newTcEvBinds + ; err_ref <- TcM.newTcRef emptyBag ; let env1 = env { tcs_ev_binds = ev_binds_var - , tcs_ty_binds = ty_binds_var } + , tcs_ty_binds = ty_binds_var + , tcs_errors = err_ref } ; unTcS tcs env1 }) -- Update TcEvBinds @@ -564,6 +604,13 @@ getUntouchables = TcS (return . tcs_untch) getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType))) getTcSTyBinds = TcS (return . tcs_ty_binds) +getTcSErrors :: TcS (IORef (Bag FrozenError)) +getTcSErrors = TcS (return . tcs_errors) + +getTcSErrorsBag :: TcS (Bag FrozenError) +getTcSErrorsBag = do { err_ref <- getTcSErrors + ; wrapTcS $ TcM.readTcRef err_ref } + getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) @@ -584,10 +631,17 @@ setDerivedCoBind cv co setWantedTyBind :: TcTyVar -> TcType -> TcS () -- Add a type binding +-- We never do this twice! setWantedTyBind tv ty = do { ref <- getTcSTyBinds ; wrapTcS $ do { ty_binds <- TcM.readTcRef ref +#ifdef DEBUG + ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $ + vcat [ text "TERRIBLE ERROR: double set of meta type variable" + , ppr tv <+> text ":=" <+> ppr ty + , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)] +#endif ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } } setIPBind :: EvVar -> EvTerm -> TcS () @@ -616,6 +670,25 @@ getDefaultInfo ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt)) ; return (ctxt, tys, flags) } + + +-- Recording errors in the TcS monad +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS () +addErrorTcS frknd fl ty1 ty2 + = do { err_ref <- getTcSErrors + ; wrapTcS $ do + { TcM.updTcRef err_ref $ \ errs -> + consBag (FrozenError frknd fl ty1 ty2) errs + + -- If there's an error in the *given* constraints, + -- stop right now, to avoid a cascade of errors + -- in the wanteds + ; when (isGiven fl) TcM.failM + + ; return () } } + -- Just get some environments needed for instance looking up and matching -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -683,9 +756,12 @@ newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty newFlattenSkolemTyVar :: TcType -> TcS TcTyVar newFlattenSkolemTyVar ty - = wrapTcS $ do { uniq <- TcM.newUnique - ; let name = mkSysTvName uniq (fsLit "f") - ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } + = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique + ; let name = mkSysTvName uniq (fsLit "f") + ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } + ; traceTcS "New Flatten Skolem Born" $ + (ppr tv <+> text "[:= " <+> ppr ty <+> text "]") + ; return tv } -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -695,35 +771,37 @@ instDFunTypes mb_inst_tys = mapM inst_tv mb_inst_tys where inst_tv :: Either TyVar TcType -> TcS Type - inst_tv (Left tv) = mkTyVarTy <$> newFlexiTcS tv + inst_tv (Left tv) = mkTyVarTy <$> instFlexiTcS tv inst_tv (Right ty) = return ty instDFunConstraints :: TcThetaType -> TcS [EvVar] instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds --- newFlexiTcS :: TyVar -> TcS TcTyVar --- -- Make a TcsTv meta tyvar; it is always touchable, --- -- but we are supposed to guess its instantiation --- -- See Note [Touchable meta type variables] --- newFlexiTcS tv = wrapTcS $ TcM.instMetaTyVar TcsTv tv - -newFlexiTcS :: TyVar -> TcS TcTyVar +instFlexiTcS :: TyVar -> TcS TcTyVar -- Like TcM.instMetaTyVar but the variable that is created is always -- touchable; we are supposed to guess its instantiation. -- See Note [Touchable meta type variables] -newFlexiTcS tv = newFlexiTcSHelper (tyVarName tv) (tyVarKind tv) +instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) -newKindConstraint :: TcTyVar -> Kind -> TcS (CoVar, Type) +newFlexiTcSTy :: Kind -> TcS TcType +newFlexiTcSTy knd + = wrapTcS $ + do { uniq <- TcM.newUnique + ; ref <- TcM.newMutVar Flexi + ; let name = mkSysTvName uniq (fsLit "uf") + ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) } + +newKindConstraint :: TcTyVar -> Kind -> TcS CoVar -- Create new wanted CoVar that constrains the type to have the specified kind. newKindConstraint tv knd - = do { tv_k <- newFlexiTcSHelper (tyVarName tv) knd + = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd ; let ty_k = mkTyVarTy tv_k ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k - ; return (co_var, ty_k) } + ; return co_var } -newFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar -newFlexiTcSHelper tvname tvkind +instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar +instFlexiTcSHelper tvname tvkind = wrapTcS $ do { uniq <- TcM.newUnique ; ref <- TcM.newMutVar Flexi @@ -915,24 +993,11 @@ matchFam tycon args } -zonkTcTypeTcS :: TcType -> TcS TcType --- Zonk through the TyBinds of the Tcs Monad -zonkTcTypeTcS ty - = do { subst <- getTcSTyBindsMap >>= return . varEnvElts - ; let (dom,rng) = unzip subst - apply_once = substTyWith dom rng - ; let rng_idemp = [ substTyWith dom rng_idemp (apply_once t) | t <- rng ] - ; return (substTyWith dom rng_idemp ty) } - - - - - - -- Functional dependencies, instantiation of equations ------------------------------------------------------- -mkWantedFunDepEqns :: WantedLoc -> [(Equation, (PredType, SDoc), (PredType, SDoc))] +mkWantedFunDepEqns :: WantedLoc + -> [(Equation, (PredType, SDoc), (PredType, SDoc))] -> TcS [WantedEvVar] mkWantedFunDepEqns _ [] = return [] mkWantedFunDepEqns loc eqns @@ -941,18 +1006,32 @@ mkWantedFunDepEqns loc eqns ; return $ concat wevvars } where to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar] - to_work_item ((qtvs, pairs), _, _) + to_work_item ((qtvs, pairs), d1, d2) = do { let tvs = varSetElems qtvs - ; tvs' <- mapM newFlexiTcS tvs + ; tvs' <- mapM instFlexiTcS tvs ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') - ; mapM (do_one subst) pairs } + loc' = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc + ; mapM (do_one subst loc') pairs } - do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 - sty2 = substTy subst ty2 - ; ev <- newWantedCoVar sty1 sty2 - ; return (WantedEvVar ev loc) } + do_one subst loc' (ty1, ty2) + = do { let sty1 = substTy subst ty1 + sty2 = substTy subst ty2 + ; ev <- newWantedCoVar sty1 sty2 + ; return (WantedEvVar ev loc') } pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc pprEquationDoc (eqn, (p1, _), (p2, _)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)] + +mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv + -> TcM (TidyEnv, SDoc) +mkEqnMsg (pred1,from1) (pred2,from2) tidy_env + = do { pred1' <- TcM.zonkTcPredType pred1 + ; pred2' <- TcM.zonkTcPredType pred2 + ; let { pred1'' = tidyPred tidy_env pred1' + ; pred2'' = tidyPred tidy_env pred2' } + ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"), + nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), + nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])] + ; return (tidy_env, msg) } \end{code} diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index 853e2c4..a4bf30f 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -18,7 +18,8 @@ import TcInteract import Inst import Var import VarSet -import VarEnv ( varEnvElts ) +import VarEnv +import TypeRep import Name import NameEnv ( emptyNameEnv ) @@ -257,19 +258,18 @@ simplifyAsMuchAsPossible ctxt wanteds -- We allow ourselves to unify environment -- variables; hence *no untouchables* - ; ((unsolved_flats, unsolved_implics), ev_binds) + ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds) <- runTcS ctxt untch $ simplifyApproxLoop 0 wanteds -- Report any errors - ; reportUnsolved (emptyBag, unsolved_implics) + ; reportUnsolved (emptyBag, unsolved_implics) frozen_errors - ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats - ; return (final_wanted_evvars, ev_binds) } + ; return (unsolved_flats, ev_binds) } where simplifyApproxLoop :: Int -> WantedConstraints - -> TcS (CanonicalCts, Bag Implication) + -> TcS (Bag WantedEvVar, Bag Implication) simplifyApproxLoop n wanteds | n > 10 = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations") @@ -281,9 +281,10 @@ simplifyAsMuchAsPossible ctxt wanteds ; let (extra_flats, thiner_unsolved_implics) = approximateImplications unsolved_implics unsolved - = mkWantedConstraints unsolved_flats thiner_unsolved_implics + = Bag.mapBag WcEvVar unsolved_flats `unionBags` + Bag.mapBag WcImplic thiner_unsolved_implics - ;-- If no new work was produced then we are done with simplifyApproxLoop + ; -- If no new work was produced then we are done with simplifyApproxLoop if isEmptyBag extra_flats then do { traceTcS "simplifyApproxLoopRes" (vcat [ ptext (sLit "Wanted = ") <+> ppr wanteds @@ -469,7 +470,7 @@ simplifySuperClass :: EvVar -- The "self" dictionary simplifySuperClass self wanteds = do { wanteds <- mapBagM zonkWanted wanteds ; loc <- getCtLoc NoScSkol - ; (unsolved, ev_binds) + ; ((unsolved_flats,unsolved_impls), frozen_errors, ev_binds) <- runTcS SimplCheck NoUntouchables $ do { can_self <- canGivens loc [self] ; let inert = foldlBag updInertSet emptyInert can_self @@ -478,7 +479,7 @@ simplifySuperClass self wanteds ; solveWanteds inert wanteds } ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds ) - reportUnsolved unsolved } + reportUnsolved (unsolved_flats,unsolved_impls) frozen_errors } \end{code} @@ -623,21 +624,22 @@ simplifyCheck ctxt wanteds ; traceTc "simplifyCheck {" (vcat [ ptext (sLit "wanted =") <+> ppr wanteds ]) - ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $ - solveWanteds emptyInert wanteds + ; (unsolved, frozen_errors, ev_binds) + <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds ; traceTc "simplifyCheck }" $ ptext (sLit "unsolved =") <+> ppr unsolved - ; reportUnsolved unsolved + ; reportUnsolved unsolved frozen_errors ; return ev_binds } ---------------- -solveWanteds :: InertSet -- Given - -> WantedConstraints -- Wanted - -> TcS (CanonicalCts, -- Unsolved flats - Bag Implication) -- Unsolved implications +solveWanteds :: InertSet -- Given + -> WantedConstraints -- Wanted + -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why + -- they are WantedConstraints and not CanonicalCts + Bag Implication) -- Unsolved implications -- solveWanteds iterates when it is able to float equalities -- out of one or more of the implications solveWanteds inert wanteds @@ -647,63 +649,89 @@ solveWanteds inert wanteds vcat [ text "wanteds =" <+> ppr wanteds , text "inert =" <+> ppr inert ] ; (unsolved_flats, unsolved_implics) - <- simpl_loop 1 can_flats implic_wanteds - ; bb <- getTcEvBindsBag + <- simpl_loop 1 inert can_flats implic_wanteds + ; bb <- getTcEvBindsBag + ; tb <- getTcSTyBindsMap ; traceTcS "solveWanteds }" $ - vcat [ text "wanteds =" <+> ppr wanteds - , text "unsolved_flats =" <+> ppr unsolved_flats + vcat [ text "unsolved_flats =" <+> ppr unsolved_flats , text "unsolved_implics =" <+> ppr unsolved_implics - , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) - ] - ; return (unsolved_flats, unsolved_implics) } + , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb)) + , text "current tybinds =" <+> vcat (map ppr (varEnvElts tb)) + ] + + ; solveCTyFunEqs unsolved_flats unsolved_implics + -- See Note [Solving Family Equations] + } where simpl_loop :: Int + -> InertSet -> CanonicalCts -- May inlude givens (in the recursive call) -> Bag Implication -> TcS (CanonicalCts, Bag Implication) - simpl_loop n can_ws implics + simpl_loop n inert can_ws implics | n>10 = trace "solveWanteds: loop" $ -- Always bleat do { traceTcS "solveWanteds: loop" (ppr inert) -- Bleat more informatively ; return (can_ws, implics) } | otherwise - = do { inert1 <- solveInteract inert can_ws + = do { traceTcS "solveWanteds: simpl_loop start {" $ + vcat [ text "n =" <+> ppr n + , text "can_ws =" <+> ppr can_ws + , text "implics =" <+> ppr implics + , text "inert =" <+> ppr inert ] + ; inert1 <- solveInteract inert can_ws ; let (inert2, unsolved_flats) = extractUnsolved inert1 - ; traceTcS "solveWanteds/done flats" $ + -- NB: Importantly, inerts2 may contain *more* givens than inert + -- because of having solved equalities from can_ws + ; traceTcS "solveWanteds: done flats" $ vcat [ text "inerts =" <+> ppr inert2 , text "unsolved =" <+> ppr unsolved_flats ] -- See Note [Preparing inert set for implications] ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats) - ; (implic_eqs, unsolved_implics) + ; traceTcS "solveWanteds: doing nested implications {" $ + vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics + , text "implics =" <+> ppr implics ] + ; (implic_eqs, unsolved_implics) <- flatMapBagPairM (solveImplication inert_for_implics) implics - -- Apply defaulting rules if and only if there + ; traceTcS "solveWanteds: done nested implications }" $ + vcat [ text "implic_eqs =" <+> ppr implic_eqs + , text "unsolved_implics =" <+> ppr unsolved_implics ] + + -- Apply defaulting rules if and only if there -- no floated equalities. If there are, they may -- solve the remaining wanteds, so don't do defaulting. ; final_eqs <- if not (isEmptyBag implic_eqs) then return implic_eqs else applyDefaultingRules inert2 unsolved_flats + -- default_eqs are *givens*, so simpl_loop may -- recurse with givens in the argument + ; traceTcS "solveWanteds: simpl_loop end }" $ + vcat [ text "final_eqs =" <+> ppr final_eqs + , text "unsolved_flats =" <+> ppr unsolved_flats + , text "unsolved_implics =" <+> ppr unsolved_implics ] + ; if isEmptyBag final_eqs then return (unsolved_flats, unsolved_implics) else - do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat - [ text "floated_unsolved_eqs =" <+> ppr final_eqs - , text "unsolved_implics = " <+> ppr unsolved_implics ] - ; simpl_loop (n+1) - (unsolved_flats `unionBags` final_eqs) - unsolved_implics - } } - -solveImplication :: InertSet -- Given - -> Implication -- Wanted - -> TcS (CanonicalCts, -- Unsolved unification var = type - Bag Implication) -- Unsolved rest (always empty or singleton) + do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs) + -- final eqs is *just* a bunch of WantedEvVars + ; simpl_loop (n+1) inert2 + (can_final_eqs `andCCan` unsolved_flats) unsolved_implics + -- Important: reiterate with inert2, not plainly inert + -- because inert2 may contain more givens, as the result of solving + -- some wanteds in the incoming can_ws + } } + +solveImplication :: InertSet -- Given + -> Implication -- Wanted + -> TcS (Bag WantedEvVar, -- Unsolved unification var = type + Bag Implication) -- Unsolved rest (always empty or singleton) -- Returns: -- 1. A bag of floatable wanted constraints, not mentioning any skolems, -- that are of the form unification var = type @@ -734,7 +762,8 @@ solveImplication inert ; let (res_flat_free, res_flat_bound) = floatEqualities skols givens unsolved_flats - unsolved = mkWantedConstraints res_flat_bound unsolved_implics + unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags` + Bag.mapBag WcImplic unsolved_implics ; traceTcS "solveImplication end }" $ vcat [ text "res_flat_free =" <+> ppr res_flat_free @@ -746,19 +775,52 @@ solveImplication inert ; return (res_flat_free, res_bag) } -floatEqualities :: TcTyVarSet -> [EvVar] - -> CanonicalCts -> (CanonicalCts, CanonicalCts) +floatEqualities :: TcTyVarSet -> [EvVar] + -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar) + -- The CanonicalCts will be floated out to be used later, whereas + -- the remaining WantedEvVars will remain inside the implication. floatEqualities skols can_given wanteds | hasEqualities can_given = (emptyBag, wanteds) - | otherwise = partitionBag is_floatable wanteds - where - is_floatable :: CanonicalCt -> Bool - is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty }) - | isMetaTyVar tv || isMetaTyVarTy ty - = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv) - is_floatable _ = False + -- Note [Float Equalities out of Implications] + | otherwise = partitionBag is_floatable wanteds + where is_floatable :: WantedEvVar -> Bool + is_floatable (WantedEvVar cv _) + | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv) + is_floatable _wv = False + + tvs_under_fsks :: Type -> TyVarSet + -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym + tvs_under_fsks (TyVarTy tv) + | not (isTcTyVar tv) = unitVarSet tv + | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty + | otherwise = unitVarSet tv + tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys) + tvs_under_fsks (PredTy sty) = predTvs_under_fsks sty + tvs_under_fsks (FunTy arg res) = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res + tvs_under_fsks (AppTy fun arg) = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg + tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder + -- can mention type variables! + | isTyVar tv = inner_tvs `delVarSet` tv + | otherwise {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) ) + inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv) + where + inner_tvs = tvs_under_fsks ty + + predTvs_under_fsks :: PredType -> TyVarSet + predTvs_under_fsks (IParam _ ty) = tvs_under_fsks ty + predTvs_under_fsks (ClassP _ tys) = unionVarSets (map tvs_under_fsks tys) + predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2 + + + + \end{code} +Note [Float Equalities out of Implications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We want to float equalities out of vanilla existentials, but *not* out +of GADT pattern matches. + Note [Preparing inert set for implications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Before solving the nested implications, we convert any unsolved flat wanteds @@ -780,6 +842,111 @@ We were not able to solve (a ~w [beta]) but we can't just assume it as given because the resulting set is not inert. Hence we have to do a 'solveInteract' step first +\begin{code} + +solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication) +-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible +-- See Note [Solving Family Equations] +-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications +-- where the newly generated equalities (alpha := F xi) have been substituted through. +solveCTyFunEqs cts implics + = do { untch <- getUntouchables + ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts + ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:" + , ppr funeq_bnds + ]) + ; mapM_ solve_one funeq_bnds + + -- Apply the substitution through to eliminate the flatten + -- unification variables we substituted both in the unsolved flats and implics + ; let final_unsolved + = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts + final_implics + = Bag.mapBag (subst_impl funeq_bnds) implics + + ; return (final_unsolved, final_implics) } + + where solve_one (tv,(ty,cv,fl)) + | not (typeKind ty `isSubKind` tyVarKind tv) + = addErrorTcS KindError fl (mkTyVarTy tv) ty + -- Must do a small kind check since TcCanonical invariants + -- on family equations only impose compatibility, not subkinding + | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty + + subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint + subst_wanted funeq_bnds (WcEvVar wv) = WcEvVar (subst_wevar funeq_bnds wv) + subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl) + + subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar + subst_wevar funeq_bnds (WantedEvVar v loc) + = let orig_ty = varType v + new_ty = substFunEqBnds funeq_bnds orig_ty + in WantedEvVar (setVarType v new_ty) loc + + subst_impl :: FunEqBinds -> Implication -> Implication + subst_impl funeq_bnds impl@(Implic { ic_wanted = ws }) + = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws } + + +type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))] +-- Invariant: if it contains: +-- [... a -> (ta,...) ... b -> (tb,...) ... ] +-- then 'ta' cannot mention 'b' + +getSolvableCTyFunEqs :: Untouchables + -> CanonicalCts -- Precondition: all wanteds + -> (CanonicalCts, FunEqBinds) -- Postcondition: returns the unsolvables +getSolvableCTyFunEqs untch cts + = Bag.foldlBag dflt_funeq (emptyCCan, []) cts + where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv + , cc_flavor = fl + , cc_fun = tc + , cc_tyargs = xis + , cc_rhs = xi }) + | Just tv <- tcGetTyVar_maybe xi + , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable + , Nothing <- lookup tv extra_binds -- or in extra_binds + -- See Note [Solving Family Equations], Point 1 + = ASSERT ( isWanted fl ) + let ty_orig = mkTyConApp tc xis + ty_bind = substFunEqBnds extra_binds ty_orig + in if tv `elemVarSet` tyVarsOfType ty_bind + then (cts_in `extendCCans` ct, extra_binds) + -- See Note [Solving Family Equations], Point 2 + else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds) + -- Postcondition met because extra_binds is already applied to ty_bind + + dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds) + +substFunEqBnds :: FunEqBinds -> TcType -> TcType +substFunEqBnds bnds ty + = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds + -- foldr works because of the FunEqBinds invariant + + +\end{code} + +Note [Solving Family Equations] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +After we are done with simplification we may be left with constraints of the form: + [Wanted] F xis ~ beta +If 'beta' is a touchable unification variable not already bound in the TyBinds +then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'. + +When is it ok to do so? + 1) 'beta' must not already be defaulted to something. Example: + + [Wanted] F Int ~ beta <~ Will default [beta := F Int] + [Wanted] F Char ~ beta <~ Already defaulted, can't default again. We + have to report this as unsolved. + + 2) However, we must still do an occurs check when defaulting (F xis ~ beta), to + set [beta := F xis] only if beta is not among the free variables of xis. + + 3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS + of type family equations. See Inert Set invariants in TcInteract. + + ********************************************************************************* * * * Defaulting and disamgiguation * @@ -818,8 +985,8 @@ Basic plan behind applyDefaulting rules: \begin{code} applyDefaultingRules :: InertSet - -> CanonicalCts -- All wanteds - -> TcS CanonicalCts + -> CanonicalCts -- All wanteds + -> TcS (Bag WantedEvVar) -- All wanteds again! -- Return some *extra* givens, which express the -- type-class-default choice @@ -838,10 +1005,10 @@ applyDefaultingRules inert wanteds ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts , text "Type defaults =" <+> ppr deflt_cts]) - ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) } + ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) } ------------------ -defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts +defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar) -- defaultTyVar is used on any un-instantiated meta type variables to -- default the kind of ? and ?? etc to *. This is important to ensure -- that instance declarations match. For example consider @@ -859,17 +1026,11 @@ defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts defaultTyVar untch the_tv | isTouchableMetaTyVar_InRange untch the_tv , not (k `eqKind` default_k) - = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k + = do { ev <- TcSMonad.newKindConstraint the_tv default_k ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk - -- 'DefaultOrigin' is strictly the declaration, but it's convenient - wanted_eq = CTyEqCan { cc_id = ev - , cc_flavor = Wanted loc - , cc_tyvar = the_tv - , cc_rhs = better_ty } - ; return (unitBag wanted_eq) } - + ; return (unitBag (WantedEvVar ev loc)) } | otherwise - = return emptyCCan -- The common case + = return emptyBag -- The common case where k = tyVarKind the_tv default_k = defaultKind k @@ -932,39 +1093,41 @@ disambigGroup :: [Type] -- The default types -> InertSet -- Given inert -> [(CanonicalCt, TcTyVar)] -- All classes of the form (C a) -- sharing same type variable - -> TcS CanonicalCts + -> TcS (Bag WantedEvVar) disambigGroup [] _inert _grp = return emptyBag disambigGroup (default_ty:default_tys) inert group = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty) - ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl - -- We know this equality is canonical, - -- so we directly construct it as such - ; let given_eq = CTyEqCan { cc_id = ev - , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol - , cc_tyvar = the_tv - , cc_rhs = default_ty } - + ; let ct_loc = get_ct_loc (cc_flavor the_ct) + ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty + ; let wanted_eq = CTyEqCan { cc_id = ev + , cc_flavor = Wanted ct_loc + , cc_tyvar = the_tv + , cc_rhs = default_ty } ; success <- tryTcS $ - do { given_inert <- solveOne inert given_eq - ; final_inert <- solveInteract given_inert (listToBag wanteds) - ; let (_, unsolved) = extractUnsolved final_inert - ; return (isEmptyBag unsolved) } + do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds) + ; let (_, unsolved) = extractUnsolved final_inert + ; errs <- getTcSErrorsBag + ; return (isEmptyBag unsolved && isEmptyBag errs) } ; case success of - True -> -- Success: record the type variable binding, and return - do { setWantedTyBind the_tv default_ty - ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty - ; traceTcS "disambigGoup succeeded" (ppr default_ty) - ; return (unitBag given_eq) } + True -> -- Success: record the type variable binding, and return + do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty + ; traceTcS "disambigGroup succeeded" (ppr default_ty) + ; return (unitBag $ WantedEvVar ev ct_loc) } False -> -- Failure: try with the next type - do { traceTcS "disambigGoup succeeded" (ppr default_ty) + do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty) ; disambigGroup default_tys inert group } } where ((the_ct,the_tv):_) = group wanteds = map fst group wanted_ev_vars = map deCanonicaliseWanted wanteds + + get_ct_loc (Wanted l) = l + get_ct_loc _ = panic "Asked to disambiguate given or derived!" + + \end{code} Note [Avoiding spurious errors] @@ -979,5 +1142,3 @@ that g isn't polymorphic enough; but then we get another one when dealing with the (Num a) context arising from f's definition; we try to unify a with Int (to default it), but find that it's already been unified with the rigid variable from g's type sig - - diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index 47bb554..8a95b0f 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -451,6 +451,9 @@ pprSkolTvBinding tv sep [pprSkolInfo info, nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]] +instance Outputable SkolemInfo where + ppr = pprSkolInfo + pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol ctxt) = pprUserTypeCtxt ctxt diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index f7c48f4..faab463 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -45,7 +45,7 @@ module Coercion ( mkNewTypeCoercion, mkFamInstCoercion, mkAppsCoercion, mkCsel1Coercion, mkCsel2Coercion, mkCselRCoercion, - mkClassPPredCo, mkIParamPredCo, + mkClassPPredCo, mkIParamPredCo, mkEqPredCo, mkCoVarCoercion, mkCoPredCo, @@ -458,6 +458,8 @@ mkClassPPredCo cls = (PredTy . ClassP cls) mkIParamPredCo :: (IPName Name) -> Coercion -> Coercion mkIParamPredCo ipn = (PredTy . IParam ipn) +mkEqPredCo :: Coercion -> Coercion -> Coercion +mkEqPredCo co1 co2 = PredTy (EqPred co1 co2) \end{code} -- 1.7.10.4