diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 48c036117f79..0b0dae4e71c7 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 77651c8568ec..a87f30479ef2 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 4c60b6e54fa5..78adcd2901a0 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 b71bba315d6d..a3efac0250ae 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 abddc24b25b6..aecfc7fa2295 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 000000000000..533870f94b59 --- /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 000000000000..b5d95bf2a139 --- /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 8f9c9d0016d6..08f6cf653d0e 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, [''])