X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSMonad.lhs;h=23733446fbe338deddd286b076fc9dfd8439ba65;hb=2207ce8cdc4c33838f77f285c7dd4f7c75dbae1c;hp=b105f8de7267d0b7605e06f838ba1b1eaf27412a;hpb=debb7b80e707c343a3a7d8993ffab19b83e5c52b;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index b105f8d..2373344 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -9,8 +9,8 @@ module TcSMonad ( mkWantedConstraints, deCanonicaliseWanted, makeGivens, makeSolved, - CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, - joinFlavors, mkGivenFlavor, + CtFlavor (..), isWanted, isGiven, isDerived, canRewrite, canSolve, + combineCtLoc, mkGivenFlavor, TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0, -- Basic functionality tryTcS, nestImplicTcS, wrapErrTcS, wrapWarnTcS, @@ -100,7 +100,6 @@ import FunDeps import TcRnTypes -import Control.Monad import Data.IORef \end{code} @@ -142,8 +141,8 @@ data CanonicalCt | CTyEqCan { -- tv ~ xi (recall xi means function free) -- Invariant: -- * tv not in tvs(xi) (occurs check) - -- * If tv is a MetaTyVar, then typeKind xi <: typeKind tv - -- a skolem, then typeKind xi = typeKind tv + -- * If constraint is given then typeKind xi == typeKind tv + -- See Note [Spontaneous solving and kind compatibility] cc_id :: EvVar, cc_flavor :: CtFlavor, cc_tyvar :: TcTyVar, @@ -154,7 +153,8 @@ data CanonicalCt -- Invariant: * isSynFamilyTyCon cc_fun -- * cc_rhs is not a touchable unification variable -- See Note [No touchables as FunEq RHS] - -- * typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs + -- * If constraint is given then + -- typeKind (TyConApp cc_fun cc_tyargs) == typeKind cc_rhs cc_id :: EvVar, cc_flavor :: CtFlavor, cc_fun :: TyCon, -- A type function @@ -289,21 +289,61 @@ isDerived :: CtFlavor -> Bool isDerived (Derived {}) = True isDerived _ = False +canSolve :: CtFlavor -> CtFlavor -> Bool +-- canSolve ctid1 ctid2 +-- The constraint ctid1 can be used to solve ctid2 +-- "to solve" means a reaction where the active parts of the two constraints match. +-- active(F xis ~ xi) = F xis +-- active(tv ~ xi) = tv +-- active(D xis) = D xis +-- active(IP nm ty) = nm +----------------------------------------- +canSolve (Given {}) _ = True +canSolve (Derived {}) (Wanted {}) = True +canSolve (Derived {}) (Derived {}) = True +canSolve (Wanted {}) (Wanted {}) = True +canSolve _ _ = False + canRewrite :: CtFlavor -> CtFlavor -> Bool -- canRewrite ctid1 ctid2 --- The constraint ctid1 can be used to rewrite ctid2 +-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 canRewrite (Given {}) _ = True canRewrite (Derived {}) (Wanted {}) = True canRewrite (Derived {}) (Derived {}) = True -canRewrite (Wanted {}) (Wanted {}) = True + -- See note [Rewriting wanteds with wanteds] +canRewrite (Wanted {}) (Wanted {}) = False canRewrite _ _ = False -joinFlavors :: CtFlavor -> CtFlavor -> CtFlavor -joinFlavors (Wanted loc) _ = Wanted loc -joinFlavors _ (Wanted loc) = Wanted loc -joinFlavors (Derived loc) _ = Derived loc -joinFlavors _ (Derived loc) = Derived loc -joinFlavors (Given loc) _ = Given loc +\end{code} +Note [Rewriting wanteds with wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We will currently never use a wanted to rewrite any other +constraint (function @canRewrite@). If a rewriting was possible at all, +we simply wait until the wanted equality becomes given or derived and +then use it. This way we avoid rewriting by eventually insoluble wanteds, +such as in the following situation: + w1 : a ~ Int + w2 : F a ~ a + w3 : F Int ~ G Bool +where 'a' is a skolem variable. If we rewrite using w1 inside w2 we will +get the perhaps mystifying error at the end that we could not solve +(a ~ Int) and (G Bool ~ Int). But there is no point in rewriting with +a ~ Int as long as it is still wanted. + +Notice that on the other hand we often do solve one wanted from another, +(function @canSolve@) for instance in dictionary interactions, which is +a reaction that enables sharing both in the solver and in the final evidence +produced. + +\begin{code} + +combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc +-- Precondition: At least one of them should be wanted +combineCtLoc (Wanted loc) _ = loc +combineCtLoc _ (Wanted loc) = loc +combineCtLoc (Derived loc) _ = loc +combineCtLoc _ (Derived loc) = loc +combineCtLoc _ _ = panic "combineCtLoc: both given" mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor mkGivenFlavor (Wanted loc) sk = Given (setCtLocOrigin loc sk) @@ -566,40 +606,58 @@ pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2) isTouchableMetaTyVar :: TcTyVar -> TcS Bool --- is touchable variable! isTouchableMetaTyVar tv - | isMetaTyVar tv = do { untch <- getUntouchables - ; return (inTouchableRange untch tv) } - | otherwise = return False + = case tcTyVarDetails tv of + MetaTv TcsTv _ -> return True -- See Note [Touchable meta type variables] + MetaTv {} -> do { untch <- getUntouchables + ; return (inTouchableRange untch tv) } + _ -> return False +\end{code} +Note [Touchable meta type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Meta type variables allocated *by the constraint solver itself* are always +touchable. Example: + instance C a b => D [a] where... +if we use this instance declaration we "make up" a fresh meta type +variable for 'b', which we must later guess. (Perhaps C has a +functional dependency.) But since we aren't in the constraint *generator* +we can't allocate a Unique in the touchable range for this implication +constraint. Instead, we mark it as a "TcsTv", which makes it always-touchable. + +\begin{code} -- Flatten skolems -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ newFlattenSkolemTy :: TcType -> TcS TcType newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty - where newFlattenSkolemTyVar :: TcType -> TcS TcTyVar - newFlattenSkolemTyVar ty - = wrapTcS $ do { uniq <- TcM.newUnique - ; let name = mkSysTvName uniq (fsLit "f") - ; return $ - mkTcTyVar name (typeKind ty) (FlatSkol 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) } -- Instantiations -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] -instDFunTypes mb_inst_tys = - let inst_tv :: Either TyVar TcType -> TcS Type - inst_tv (Left tv) = wrapTcS $ TcM.tcInstTyVar tv >>= return . mkTyVarTy - inst_tv (Right ty) = return ty - in mapM inst_tv mb_inst_tys - +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 (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 -- Superclasses and recursive dictionaries -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -800,11 +858,13 @@ mkWantedFunDepEqns loc eqns where to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar] to_work_item ((qtvs, pairs), _, _) - = do { (_, _, tenv) <- wrapTcS $ TcM.tcInstTyVars (varSetElems qtvs) - ; mapM (do_one tenv) pairs } + = do { let tvs = varSetElems qtvs + ; tvs' <- mapM newFlexiTcS tvs + ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs') + ; mapM (do_one subst) pairs } - do_one tenv (ty1, ty2) = do { let sty1 = substTy tenv ty1 - sty2 = substTy tenv ty2 + do_one subst (ty1, ty2) = do { let sty1 = substTy subst ty1 + sty2 = substTy subst ty2 ; ev <- newWantedCoVar sty1 sty2 ; return (WantedEvVar ev loc) }