diff options
| -rw-r--r-- | compiler/typecheck/TcExpr.lhs | 32 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.lhs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.lhs | 47 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.lhs | 25 | ||||
| -rw-r--r-- | compiler/utils/MonadUtils.hs | 6 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T7220.hs (renamed from testsuite/tests/typecheck/should_fail/T7220.hs) | 0 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 5 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T7220.stderr | 9 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
9 files changed, 79 insertions, 61 deletions
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index deda6137d0..a242ed77d2 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -124,16 +124,9 @@ tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr) tcInferRhoNC (L loc expr) = setSrcSpan loc $ - do { (expr', rho) <- tcInfExpr expr + do { (expr', rho) <- tcInfer (tcExpr expr) ; return (L loc expr', rho) } -tcInfExpr :: HsExpr Name -> TcM (HsExpr TcId, TcRhoType) -tcInfExpr (HsVar f) = tcInferId f -tcInfExpr (HsPar e) = do { (e', ty) <- tcInferRhoNC e - ; return (HsPar e', ty) } -tcInfExpr (HsApp e1 e2) = tcInferApp e1 [e2] -tcInfExpr e = tcInfer (tcExpr e) - tcHole :: OccName -> TcRhoType -> TcM (HsExpr TcId) tcHole occ res_ty = do { ty <- newFlexiTyVarTy liftedTypeKind @@ -326,13 +319,15 @@ tcExpr (OpApp arg1 op fix arg2) res_ty -- Eg we do not want to allow (D# $ 4.0#) Trac #5570 -- (which gives a seg fault) -- We do this by unifying with a MetaTv; but of course - -- it must allow foralls in the type it unifies with (hence PolyTv)! + -- it must allow foralls in the type it unifies with (hence ReturnTv)! -- -- The result type can have any kind (Trac #8739), -- so we can just use res_ty -- ($) :: forall (a:*) (b:Open). (a->b) -> a -> b - ; a_ty <- newPolyFlexiTyVarTy + ; a_tv <- newReturnTyVar liftedTypeKind + ; let a_ty = mkTyVarTy a_tv + ; arg2' <- tcArg op (arg2, arg2_ty, 2) ; co_a <- unifyType arg2_ty a_ty -- arg2 ~ a @@ -937,23 +932,6 @@ mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun) , ptext (sLit "is applied to")] ---------------- -tcInferApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args - -> TcM (HsExpr TcId, TcRhoType) -- Translated fun and args - -tcInferApp (L _ (HsPar e)) args = tcInferApp e args -tcInferApp (L _ (HsApp e1 e2)) args = tcInferApp e1 (e2:args) -tcInferApp fun args - = -- Very like the tcApp version, except that there is - -- no expected result type passed in - do { (fun1, fun_tau) <- tcInferFun fun - ; (co_fun, expected_arg_tys, actual_res_ty) - <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau - ; args1 <- tcArgs fun args expected_arg_tys - ; let fun2 = mkLHsWrapCo co_fun fun1 - app = foldl mkHsApp fun2 args1 - ; return (unLoc app, actual_res_ty) } - ----------------- tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) -- Infer and instantiate the type of a function tcInferFun (L loc (HsVar name)) diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index d6f37c8f96..c78c125bf1 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -19,12 +19,12 @@ module TcMType ( newFlexiTyVar, newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] - newPolyFlexiTyVarTy, + newReturnTyVar, newMetaKindVar, newMetaKindVars, mkTcTyVarName, cloneMetaTyVar, newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, - newMetaDetails, isFilledMetaTyVar, isFlexiMetaTyVar, + newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- -- Creating new evidence variables @@ -311,7 +311,7 @@ newMetaTyVar meta_info kind = do { uniq <- newUnique ; let name = mkTcTyVarName uniq s s = case meta_info of - PolyTv -> fsLit "s" + ReturnTv -> fsLit "r" TauTv -> fsLit "t" FlatMetaTv -> fsLit "fmv" SigTv -> fsLit "a" @@ -363,9 +363,9 @@ isFilledMetaTyVar tv ; return (isIndirect details) } | otherwise = return False -isFlexiMetaTyVar :: TyVar -> TcM Bool +isUnfilledMetaTyVar :: TyVar -> TcM Bool -- True of a un-filled-in (Flexi) meta type variable -isFlexiMetaTyVar tv +isUnfilledMetaTyVar tv | not (isTcTyVar tv) = return False | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv = do { details <- readMutVar ref @@ -448,9 +448,8 @@ newFlexiTyVarTy kind = do newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) -newPolyFlexiTyVarTy :: TcM TcType -newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind - ; return (TyVarTy tv) } +newReturnTyVar :: Kind -> TcM TcTyVar +newReturnTyVar kind = newMetaTyVar ReturnTv kind tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar]) -- Instantiate with META type variables diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs index a4a646c8e9..dba1be8964 100644 --- a/compiler/typecheck/TcType.lhs +++ b/compiler/typecheck/TcType.lhs @@ -269,6 +269,35 @@ Similarly consider When doing kind inference on {S,T} we don't want *skolems* for k1,k2, because they end up unifying; we want those SigTvs again. +Note [ReturnTv] +~~~~~~~~~~~~~~~ +We sometimes want to convert a checking algorithm into an inference +algorithm. An easy way to do this is to "check" that a term has a +metavariable as a type. But, we must be careful to allow that metavariable +to unify with *anything*. (Well, anything that doesn't fail an occurs-check.) +This is what ReturnTv means. + +For example, if we have + + (undefined :: (forall a. TF1 a ~ TF2 a => a)) x + +we'll call (tcInfer . tcExpr) on the function expression. tcInfer will +create a ReturnTv to represent the expression's type. We really need this +ReturnTv to become set to (forall a. TF1 a ~ TF2 a => a) despite the fact +that this type mentions type families and is a polytype. + +However, we must also be careful to make sure that the ReturnTvs really +always do get unified with something -- we don't want these floating +around in the solver. So, we check after running the checker to make +sure the ReturnTv is filled. If it's not, we set it to a TauTv. + +We can't ASSERT that no ReturnTvs hit the solver, because they +can if there's, say, a kind error that stops checkTauTvUpdate from +working. This happens in test case typecheck/should_fail/T5570, for +example. + +See also the commentary on #9404. + \begin{code} -- A TyVarDetails is inside a TyVar data TcTyVarDetails @@ -307,7 +336,9 @@ data MetaInfo -- A TauTv is always filled in with a tau-type, which -- never contains any ForAlls - | PolyTv -- Like TauTv, but can unify with a sigma-type + | ReturnTv -- Can unify with *anything*. Used to convert a + -- type "checking" algorithm into a type inference algorithm. + -- See Note [ReturnTv] | SigTv -- A variant of TauTv, except that it should not be -- unified with a type, only with a type variable @@ -481,7 +512,7 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_untch = untch }) = pp_info <> colon <> ppr untch where pp_info = case info of - PolyTv -> ptext (sLit "poly") + ReturnTv -> ptext (sLit "return") TauTv -> ptext (sLit "tau") SigTv -> ptext (sLit "sig") FlatMetaTv -> ptext (sLit "fuv") @@ -1133,7 +1164,7 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type -- Check whether -- a) the given variable occurs in the given type. -- b) there is a forall in the type (unless we have -XImpredicativeTypes --- or it's a PolyTv +-- or it's a ReturnTv -- c) if it's a SigTv, ty should be a tyvar -- -- We may have needed to do some type synonym unfolding in order to @@ -1152,13 +1183,13 @@ occurCheckExpand dflags tv ty impredicative = case details of - MetaTv { mtv_info = PolyTv } -> True - MetaTv { mtv_info = SigTv } -> False - MetaTv { mtv_info = TauTv } -> xopt Opt_ImpredicativeTypes dflags - || isOpenTypeKind (tyVarKind tv) + MetaTv { mtv_info = ReturnTv } -> True + MetaTv { mtv_info = SigTv } -> False + MetaTv { mtv_info = TauTv } -> xopt Opt_ImpredicativeTypes dflags + || isOpenTypeKind (tyVarKind tv) -- Note [OpenTypeKind accepts foralls] -- in TcUnify - _other -> True + _other -> True -- We can have non-meta tyvars in given constraints -- Check 'ty' is a tyvar, or can be expanded into one diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index f5033ee08a..421d076dbf 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -46,6 +46,7 @@ import TyCon import TysWiredIn import Var import VarEnv +import VarSet import ErrUtils import DynFlags import BasicTypes @@ -338,10 +339,19 @@ tcSubType origin ctxt ty_actual ty_expected PatSigOrigin -> TypeEqOrigin { uo_actual = ty2, uo_expected = ty1 } _other -> TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 } +-- | Infer a type using a type "checking" function by passing in a ReturnTv, +-- which can unify with *anything*. See also Note [ReturnTv] in TcType tcInfer :: (TcType -> TcM a) -> TcM (a, TcType) -tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind - ; res <- tc_infer ty - ; return (res, ty) } +tcInfer tc_check + = do { tv <- newReturnTyVar openTypeKind + ; let ty = mkTyVarTy tv + ; res <- tc_check ty + ; whenM (isUnfilledMetaTyVar tv) $ -- checking was uninformative + do { traceTc "Defaulting an un-filled ReturnTv to a TauTv" empty + ; tau_ty <- newFlexiTyVarTy openTypeKind + ; writeMetaTyVar tv tau_ty } + ; return (res, ty) } + where ----------------- tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId) @@ -844,7 +854,7 @@ nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1) ---------------- checkTauTvUpdate :: DynFlags -> TcTyVar -> TcType -> TcM (Maybe TcType) -- (checkTauTvUpdate tv ty) --- We are about to update the TauTv/PolyTv tv with ty. +-- We are about to update the TauTv/ReturnTv tv with ty. -- Check (a) that tv doesn't occur in ty (occurs check) -- (b) that kind(ty) is a sub-kind of kind(tv) -- @@ -873,6 +883,9 @@ checkTauTvUpdate dflags tv ty ; case sub_k of Nothing -> return Nothing Just LT -> return Nothing + _ | is_return_tv -> if tv `elemVarSet` tyVarsOfType ty + then return Nothing + else return (Just ty1) _ | defer_me ty1 -- Quick test -> -- Failed quick test so try harder case occurCheckExpand dflags tv ty1 of @@ -882,11 +895,12 @@ checkTauTvUpdate dflags tv ty | otherwise -> return (Just ty1) } where info = ASSERT2( isMetaTyVar tv, ppr tv ) metaTyVarInfo tv + -- See Note [ReturnTv] in TcType + is_return_tv = case info of { ReturnTv -> True; _ -> False } impredicative = xopt Opt_ImpredicativeTypes dflags || isOpenTypeKind (tyVarKind tv) -- Note [OpenTypeKind accepts foralls] - || case info of { PolyTv -> True; _ -> False } defer_me :: TcType -> Bool -- Checks for (a) occurrence of tv @@ -917,7 +931,6 @@ we can instantiate it with Int#. So we also allow such type variables to be instantiate with foralls. It's a bit of a hack, but seems straightforward. - Note [Conservative unification check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When unifying (tv ~ rhs), w try to avoid creating deferred constraints diff --git a/compiler/utils/MonadUtils.hs b/compiler/utils/MonadUtils.hs index 60748ead29..b066b404a1 100644 --- a/compiler/utils/MonadUtils.hs +++ b/compiler/utils/MonadUtils.hs @@ -21,6 +21,7 @@ module MonadUtils , anyM, allM , foldlM, foldlM_, foldrM , maybeMapM + , whenM ) where ------------------------------------------------------------------------------- @@ -149,3 +150,8 @@ foldrM k z (x:xs) = do { r <- foldrM k z xs; k x r } maybeMapM :: Monad m => (a -> m b) -> (Maybe a -> m (Maybe b)) maybeMapM _ Nothing = return Nothing maybeMapM m (Just x) = liftM Just $ m x + +-- | Monadic version of @when@, taking the condition in the monad +whenM :: Monad m => m Bool -> m () -> m () +whenM mb thing = do { b <- mb + ; when b thing } diff --git a/testsuite/tests/typecheck/should_fail/T7220.hs b/testsuite/tests/typecheck/should_compile/T7220.hs index 36ae54a61d..36ae54a61d 100644 --- a/testsuite/tests/typecheck/should_fail/T7220.hs +++ b/testsuite/tests/typecheck/should_compile/T7220.hs diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 8448411d7c..ef830d14d5 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -422,5 +422,6 @@ test('T8856', normal, compile, ['']) test('T9117', normal, compile, ['']) test('T9117_2', expect_broken('9117'), compile, ['']) test('T9708', normal, compile_fail, ['']) -test('T9404', expect_broken(9404), compile, ['']) -test('T9404b', expect_broken(9404), compile, ['']) +test('T9404', normal, compile, ['']) +test('T9404b', normal, compile, ['']) +test('T7220', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T7220.stderr b/testsuite/tests/typecheck/should_fail/T7220.stderr deleted file mode 100644 index 86c4c5f1cb..0000000000 --- a/testsuite/tests/typecheck/should_fail/T7220.stderr +++ /dev/null @@ -1,9 +0,0 @@ - -T7220.hs:24:6: - Cannot instantiate unification variable ‘b0’ - with a type involving foralls: forall b. (C A b, TF b ~ Y) => b - Perhaps you want ImpredicativeTypes - In the expression: f :: (forall b. (C A b, TF b ~ Y) => b) -> X - In the expression: (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u - In an equation for ‘v’: - v = (f :: (forall b. (C A b, TF b ~ Y) => b) -> X) u diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index f30bbb2481..2b128dc004 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -291,7 +291,6 @@ test('T6161', normal, compile_fail, ['']) test('T7368', normal, compile_fail, ['']) test('T7264', normal, compile_fail, ['']) test('T6069', normal, compile_fail, ['']) -test('T7220', normal, compile_fail, ['']) test('T7410', normal, compile_fail, ['']) test('T7453', normal, compile_fail, ['']) test('T7525', normal, compile_fail, ['']) |