From e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Mon, 22 Feb 2016 12:54:56 -0500 Subject: Fix #11407. This removes the `defer_me` check that was in checkTauTvUpdate and uses only a type family check instead. The old defer_me check repeated work done by fast_check in occurCheckExpand. There is also some error message improvement, necessitated by the terrible error message that the test case produced, even when it didn't consume all of memory. test case: dependent/should_fail/T11407 [skip ci] --- compiler/typecheck/TcErrors.hs | 15 +++++++- compiler/typecheck/TcUnify.hs | 45 +++++----------------- compiler/types/TyCoRep.hs | 25 ++++++------ compiler/types/Type.hs | 9 ++++- compiler/types/Type.hs-boot | 5 +++ testsuite/tests/dependent/should_fail/T11407.hs | 10 +++++ .../tests/dependent/should_fail/T11407.stderr | 8 ++++ testsuite/tests/dependent/should_fail/all.T | 1 + 8 files changed, 70 insertions(+), 48 deletions(-) create mode 100644 testsuite/tests/dependent/should_fail/T11407.hs create mode 100644 testsuite/tests/dependent/should_fail/T11407.stderr diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 48c036117f..0b0dae4e71 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -1179,7 +1179,20 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 hang (text "Occurs check: cannot construct the infinite" <+> what <> colon) 2 (sep [ppr ty1, char '~', ppr ty2]) extra2 = important $ mkEqInfoMsg ct ty1 ty2 - ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, report] } + + interesting_tyvars + = filter (not . isEmptyVarSet . tyCoVarsOfType . tyVarKind) $ + filter isTyVar $ + varSetElems $ + tyCoVarsOfType ty1 `unionVarSet` tyCoVarsOfType ty2 + extra3 = relevant_bindings $ + ppWhen (not (null interesting_tyvars)) $ + hang (text "Type variable kinds:") 2 $ + vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt)) + interesting_tyvars) + + tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) + ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, extra3, report] } | OC_Forall <- occ_check_expand = do { let msg = vcat [ text "Cannot instantiate unification variable" diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 77651c8568..a87f30479e 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -50,7 +50,7 @@ import TyCon import TysWiredIn import Var import VarEnv -import VarSet +import NameEnv import ErrUtils import DynFlags import BasicTypes @@ -1449,53 +1449,28 @@ checkTauTvUpdate dflags origin t_or_k tv ty | otherwise = do { ty <- zonkTcType ty ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv) - ; if | defer_me ty -> -- Quick test - -- Failed quick test so try harder - case occurCheckExpand dflags tv ty of - OC_OK ty2 | defer_me ty2 -> return Nothing - | otherwise -> return (Just (ty2, co_k)) - _ -> return Nothing - | otherwise -> return (Just (ty, co_k)) } + ; return $ case occurCheckExpand dflags tv ty of + OC_OK ty2 | type_fam_free ty2 -> Just (ty2, co_k) + _ -> Nothing } + where kind_origin = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k) details = tcTyVarDetails tv info = mtv_info details - impredicative = canUnifyWithPolyType dflags details - defer_me :: TcType -> Bool - -- Checks for (a) occurrence of tv - -- (b) type family applications - -- (c) foralls -- See Note [Conservative unification check] - defer_me (LitTy {}) = False - defer_me (TyVarTy tv') = tv == tv' - defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys - || not (impredicative || isTauTyCon tc) - defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t - || (isNamedBinder bndr && not impredicative) - defer_me (AppTy fun arg) = defer_me fun || defer_me arg - defer_me (CastTy ty co) = defer_me ty || defer_me_co co - defer_me (CoercionTy co) = defer_me_co co - - -- We don't really care if there are type families in a coercion, - -- but we still can't have an occurs-check failure - defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co + type_fam_free :: TcType -> Bool + type_fam_free = not . any isTypeFamilyTyCon . nameEnvElts . tyConsOfType {- Note [Conservative unification check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When unifying (tv ~ rhs), w try to avoid creating deferred constraints -only for efficiency. However, we do not unify (the defer_me check) if - a) There's an occurs check (tv is in fvs(rhs)) +only for efficiency. However, we do not unify if + a) There's an occurs check (tv is in fvs(rhs)) (established by occurCheckExpand) + (see Note [Type synonyms and the occur check]) b) There's a type-function call in 'rhs' -If we fail defer_me we use occurCheckExpand to try to make it pass, -(see Note [Type synonyms and the occur check]) and then use defer_me -again to check. Example: Trac #4917) - a ~ Const a b -where type Const a b = a. We can solve this immediately, even when -'a' is a skolem, just by expanding the synonym. - We always defer type-function calls, even if it's be perfectly safe to unify, eg (a ~ F [b]). Reason: this ensures that the constraint solver gets to see, and hence simplify the type-function call, which diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 4c60b6e54f..78adcd2901 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -126,6 +126,7 @@ module TyCoRep ( import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig , DataCon, eqSpecTyVar ) import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy + , tyCoVarsOfTypesWellScoped, varSetElemsWellScoped , partitionInvisibles, coreView, typeKind ) -- Transitively pulls in a LOT of stuff, better to break the loop @@ -2867,7 +2868,7 @@ tidyFreeTyCoVars :: TidyEnv -> TyCoVarSet -> TidyEnv -- ^ Add the free 'TyVar's to the env in tidy form, -- so that we can tidy the type they are free in tidyFreeTyCoVars (full_occ_env, var_env) tyvars - = fst (tidyOpenTyCoVars (full_occ_env, var_env) (varSetElems tyvars)) + = fst (tidyOpenTyCoVars (full_occ_env, var_env) (varSetElemsWellScoped tyvars)) --------------- tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar]) @@ -2885,9 +2886,9 @@ tidyOpenTyCoVar env@(_, subst) tyvar --------------- tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar -tidyTyVarOcc (_, subst) tv +tidyTyVarOcc env@(_, subst) tv = case lookupVarEnv subst tv of - Nothing -> tv + Nothing -> updateTyVarKind (tidyType env) tv Just tv' -> tv' --------------- @@ -2913,19 +2914,21 @@ tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co) --------------- -- | Grabs the free type variables, tidies them -- and then uses 'tidyType' to work over the type itself -tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type) -tidyOpenType env ty - = (env', tidyType (trimmed_occ_env, var_env) ty) +tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type]) +tidyOpenTypes env tys + = (env', tidyTypes (trimmed_occ_env, var_env) tys) where - (env'@(_, var_env), tvs') = tidyOpenTyCoVars env (tyCoVarsOfTypeList ty) + (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $ + tyCoVarsOfTypesWellScoped tys trimmed_occ_env = initTidyOccEnv (map getOccName tvs') -- The idea here was that we restrict the new TidyEnv to the - -- _free_ vars of the type, so that we don't gratuitously rename - -- the _bound_ variables of the type. + -- _free_ vars of the types, so that we don't gratuitously rename + -- the _bound_ variables of the types. --------------- -tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type]) -tidyOpenTypes env tys = mapAccumL tidyOpenType env tys +tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type) +tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in + (env', ty') --------------- -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment) diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index b71bba315d..a3efac0250 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -127,6 +127,7 @@ module Type ( -- * Well-scoped lists of variables varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped, + tyCoVarsOfTypesWellScoped, -- * Type comparison eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc, @@ -1872,6 +1873,10 @@ varSetElemsWellScoped = toposortTyVars . varSetElems tyCoVarsOfTypeWellScoped :: Type -> [TyVar] tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList +-- | Get the free vars of types in scoped order +tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] +tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList + {- ************************************************************************ * * @@ -2271,7 +2276,9 @@ tyConsOfType ty go_prov (PhantomProv co) = go_co co go_prov (ProofIrrelProv co) = go_co co go_prov (PluginProv _) = emptyNameEnv - go_prov (HoleProv h) = pprPanic "tyConsOfType hit a hole" (ppr h) + go_prov (HoleProv _) = emptyNameEnv + -- this last case can happen from the tyConsOfType used from + -- checkTauTvUpdate go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys go_cos cos = foldr (plusNameEnv . go_co) emptyNameEnv cos diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot index abddc24b25..aecfc7fa22 100644 --- a/compiler/types/Type.hs-boot +++ b/compiler/types/Type.hs-boot @@ -1,5 +1,7 @@ module Type where import TyCon +import Var ( TyVar, TyCoVar ) +import VarSet ( TyCoVarSet ) import {-# SOURCE #-} TyCoRep( Type, Kind ) isPredTy :: Type -> Bool @@ -16,3 +18,6 @@ coreViewOneStarKind :: Type -> Maybe Type partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a]) coreView :: Type -> Maybe Type + +tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] +varSetElemsWellScoped :: TyCoVarSet -> [TyCoVar] diff --git a/testsuite/tests/dependent/should_fail/T11407.hs b/testsuite/tests/dependent/should_fail/T11407.hs new file mode 100644 index 0000000000..533870f94b --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T11407.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +module T11407 where + +import Data.Kind + +type Const a b = a + +data family UhOh (f :: k1) (a :: k2) (b :: k3) +data instance UhOh (f :: * -> * -> *) (a :: x a) (b :: Const * a) = UhOh diff --git a/testsuite/tests/dependent/should_fail/T11407.stderr b/testsuite/tests/dependent/should_fail/T11407.stderr new file mode 100644 index 0000000000..b5d95bf2a1 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T11407.stderr @@ -0,0 +1,8 @@ + +T11407.hs:10:40: error: + • Occurs check: cannot construct the infinite kind: k0 ~ x a + • In the second argument of ‘UhOh’, namely ‘(a :: x a)’ + In the data instance declaration for ‘UhOh’ + • Type variable kinds: + a :: k0 + x :: k0 -> * diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 8f9c9d0016..08f6cf653d 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -8,3 +8,4 @@ test('PromotedClass', normal, compile_fail, ['']) test('SelfDep', normal, compile_fail, ['']) test('BadTelescope4', normal, compile_fail, ['']) test('RenamingStar', normal, compile_fail, ['']) +test('T11407', normal, compile_fail, ['']) -- cgit v1.2.1