From: simonpj@microsoft.com Date: Fri, 15 Oct 2010 13:08:18 +0000 (+0000) Subject: Fix Trac #4401: meta-tyvars allocated by the constraint solver are always touchable X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=commitdiff_plain;h=27225b0c9f799a251c96242f502e8cfd6bf76d7c;ds=sidebyside Fix Trac #4401: meta-tyvars allocated by the constraint solver are always touchable See Note [Touchable meta type variables] in TcSMonad --- diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 950d733..65330ac 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -35,7 +35,7 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstSigTyVars, - tcInstType, tcInstSigType, + tcInstType, tcInstSigType, instMetaTyVar, tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -305,6 +305,7 @@ newMetaTyVar meta_info kind ; let name = mkSysTvName uniq fs fs = case meta_info of TauTv -> fsLit "t" + TcsTv -> fsLit "u" SigTv _ -> fsLit "a" ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 93c795d..3c1961b 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -566,40 +566,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 +818,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) } diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index b49dbff..b20d32e 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -302,6 +302,11 @@ data MetaInfo -- The Name is the name of the function from whose -- type signature we got this skolem + | TcsTv -- A MetaTv allocated by the constraint solver + -- Its particular property is that it is always "touchable" + -- Nevertheless, the constraint solver has to try to guess + -- what type to instantiate it to + ---------------------------------- -- SkolemInfo describes a site where -- a) type variables are skolemised @@ -408,6 +413,7 @@ pprTcTyVarDetails :: TcTyVarDetails -> SDoc pprTcTyVarDetails (SkolemTv _) = ptext (sLit "sk") pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk") pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau") +pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs") pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig") pprUserTypeCtxt :: UserTypeCtxt -> SDoc @@ -433,8 +439,9 @@ pprSkolTvBinding tv where ppr_details (SkolemTv info) = ppr_skol info ppr_details (FlatSkol {}) = ptext (sLit "is a flattening type variable") - ppr_details (MetaTv TauTv _) = ptext (sLit "is a meta type variable") - ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") <+> quotes (ppr n) + ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for") + <+> quotes (ppr n) + ppr_details (MetaTv _ _) = ptext (sLit "is a meta type variable") ppr_skol UnkSkol = ptext (sLit "is an unknown type variable") -- Unhelpful ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type") @@ -615,8 +622,8 @@ isTyConableTyVar tv -- not a SigTv = ASSERT( isTcTyVar tv) case tcTyVarDetails tv of - MetaTv TauTv _ -> True - _ -> False + MetaTv (SigTv _) _ -> False + _ -> True isSkolemTyVar tv = ASSERT2( isTcTyVar tv, ppr tv )