diff options
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 154 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.hs | 66 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 129 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.hs | 304 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T12593.hs | 14 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T12593.stderr | 31 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/tc141.stderr | 10 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/T9605.stderr | 6 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/tcfail122.stderr | 2 |
10 files changed, 370 insertions, 347 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index b6a76c762b..3f121bd898 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -10,6 +10,7 @@ module TcCanonical( #include "HsVersions.h" import TcRnTypes +import TcUnify( swapOverTyVars ) import TcType import Type import TcFlatten @@ -22,7 +23,6 @@ import Coercion import FamInstEnv ( FamInstEnvs ) import FamInst ( tcTopNormaliseNewTypeTF_maybe ) import Var -import Name( isSystemName ) import Outputable import DynFlags( DynFlags ) import VarSet @@ -654,13 +654,13 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 `andWhenContinue` \ new_ev -> can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } --- Type variable on LHS or RHS are last. We want only flat types sent --- to canEqTyVar. +-- Type variable on LHS or RHS are last. +-- NB: pattern match on True: we want only flat types sent to canEqTyVar. -- See also Note [No top-level newtypes on RHS of representational equalities] -can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) _ _ ps_ty2 - = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty2 -can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 (TyVarTy tv2) _ - = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty1 +can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2 + = canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2 +can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2 + = canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1 -- We've flattened and the types don't match. Give up. can_eq_nc' True _rdr_env _envs ev _eq_rel _ ps_ty1 _ ps_ty2 @@ -1335,18 +1335,26 @@ canCFunEqCan ev fn tys fsk , cc_tyargs = tys', cc_fsk = fsk }) } } --------------------- -canEqTyVar :: CtEvidence -> EqRel -> SwapFlag - -> TcTyVar -- already flat - -> TcType -- already flat +canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs + -> EqRel -> SwapFlag + -> TcTyVar -> TcType -- lhs: already flat, not a cast + -> TcType -> TcType -- rhs: already flat, not a cast -> TcS (StopOrContinue Ct) --- A TyVar on LHS, but so far un-zonked -canEqTyVar ev eq_rel swapped tv1 ps_ty2 -- ev :: tv ~ s2 - = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ps_ty2 $$ ppr swapped) +canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _ + | tv1 == tv2 + = canEqReflexive ev eq_rel ps_ty1 + + | swapOverTyVars tv1 tv2 + = do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr tv2 $$ ppr swapped) -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True } -- Flatten the RHS less vigorously, to avoid gratuitous flattening -- True <=> xi2 should not itself be a type-function application ; dflags <- getDynFlags + ; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 } + +canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2 + = do { dflags <- getDynFlags ; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 } canEqTyVar2 :: DynFlags @@ -1361,21 +1369,17 @@ canEqTyVar2 :: DynFlags -- preserved as much as possible canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 - | Just (tv2, kco2) <- getCastedTyVar_maybe xi2 - = canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2 - | OC_OK xi2' <- occurCheckExpand dflags tv1 xi2 -- No occurs check - -- We use xi2' on the RHS of the new CTyEqCan, a ~ xi2' - -- to establish the invariant that a does not appear in the - -- rhs of the CTyEqCan. This is guaranteed by occurCheckExpand; - -- see Note [Occurs check expansion] in TcType - = rewriteEqEvidence ev swapped xi1 xi2' co1 (mkTcReflCo role xi2') + -- Must do the occurs check even on tyvar/tyvar + -- equalities, in case have x ~ (y :: ..x...) + -- Trac #12593 + = rewriteEqEvidence ev swapped xi1 xi2' co1 co2 `andWhenContinue` \ new_ev -> homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' -> CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1 , cc_rhs = xi2'', cc_eq_rel = eq_rel } - | otherwise -- Occurs check error + | otherwise -- Occurs check error (or a forall) = do { traceTcS "canEqTyVar2 occurs check error" (ppr tv1 $$ ppr xi2) ; rewriteEqEvidence ev swapped xi1 xi2 co1 co2 `andWhenContinue` \ new_ev -> @@ -1394,117 +1398,13 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2 -- canonical, and we might loop if we were to use it in rewriting. else do { traceTcS "Occurs-check in representational equality" (ppr xi1 $$ ppr xi2) - ; continueWith (CIrredEvCan { cc_ev = new_ev }) } } + ; continueWith (CIrredEvCan { cc_ev = new_ev }) } } where role = eqRelRole eq_rel xi1 = mkTyVarTy tv1 co1 = mkTcReflCo role xi1 co2 = mkTcReflCo role xi2 -canEqTyVarTyVar :: CtEvidence -- tv1 ~ rhs (or rhs ~ tv1, if swapped) - -> EqRel - -> SwapFlag - -> TcTyVar -> TcTyVar -- tv1, tv2 - -> Coercion -- the co in (rhs = tv2 |> co) - -> TcS (StopOrContinue Ct) --- Both LHS and RHS rewrote to a type variable --- See Note [Canonical orientation for tyvar/tyvar equality constraints] -canEqTyVarTyVar ev eq_rel swapped tv1 tv2 kco2 - | tv1 == tv2 - = do { let mk_coh = case swapped of IsSwapped -> mkTcCoherenceLeftCo - NotSwapped -> mkTcCoherenceRightCo - ; setEvBindIfWanted ev (EvCoercion $ mkTcReflCo role xi1 `mk_coh` kco2) - ; stopWith ev "Equal tyvars" } - --- We don't do this any more --- See Note [Orientation of equalities with fmvs] in TcFlatten --- | isFmvTyVar tv1 = do_fmv swapped tv1 xi1 xi2 co1 co2 --- | isFmvTyVar tv2 = do_fmv (flipSwap swapped) tv2 xi2 xi1 co2 co1 - - | swap_over = do_swap - | otherwise = no_swap - where - role = eqRelRole eq_rel - xi1 = mkTyVarTy tv1 - co1 = mkTcReflCo role xi1 - xi2 = mkTyVarTy tv2 - co2 = mkTcReflCo role xi2 `mkTcCoherenceRightCo` kco2 - - no_swap = canon_eq swapped tv1 xi1 xi2 co1 co2 - do_swap = canon_eq (flipSwap swapped) tv2 xi2 xi1 co2 co1 - - canon_eq swapped tv1 ty1 ty2 co1 co2 - -- ev : tv1 ~ orhs (not swapped) or orhs ~ tv1 (swapped) - -- co1 : xi1 ~ tv1 - -- co2 : xi2 ~ tv2 - = do { traceTcS "canEqTyVarTyVar" - (vcat [ ppr swapped - , ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) - , ppr ty1 <+> dcolon <+> ppr (typeKind ty1) - , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) - , ppr co1 <+> dcolon <+> ppr (tcCoercionKind co1) - , ppr co2 <+> dcolon <+> ppr (tcCoercionKind co2) ]) - ; rewriteEqEvidence ev swapped ty1 ty2 co1 co2 - `andWhenContinue` \ new_ev -> - homogeniseRhsKind new_ev eq_rel ty1 ty2 $ \new_new_ev ty2' -> - CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1 - , cc_rhs = ty2', cc_eq_rel = eq_rel } } - -{- We don't do this any more - See Note [Orientation of equalities with fmvs] in TcFlatten - -- tv1 is the flatten meta-var - do_fmv swapped tv1 xi1 xi2 co1 co2 - | same_kind - = canon_eq swapped tv1 xi1 xi2 co1 co2 - | otherwise -- Presumably tv1 :: *, since it is a flatten meta-var, - -- at a kind that has some interesting sub-kind structure. - -- Since the two kinds are not the same, we must have - -- tv1 `subKind` tv2, which is the wrong way round - -- e.g. (fmv::*) ~ (a::OpenKind) - -- So make a new meta-var and use that: - -- fmv ~ (beta::*) - -- (a::OpenKind) ~ (beta::*) - = ASSERT2( k1_sub_k2, - ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) $$ - ppr xi2 <+> dcolon <+> ppr (typeKind xi2) ) - ASSERT2( isWanted ev, ppr ev ) -- Only wanteds have flatten meta-vars - do { tv_ty <- newFlexiTcSTy (tyVarKind tv1) - ; new_ev <- newWantedEvVarNC (ctEvLoc ev) - (mkPrimEqPredRole (eqRelRole eq_rel) - g tv_ty xi2) - ; emitWorkNC [new_ev] - ; canon_eq swapped tv1 xi1 tv_ty co1 (ctEvCoercion new_ev) } --} - - swap_over - -- If tv1 is touchable, swap only if tv2 is also - -- touchable and it's strictly better to update the latter - -- But see Note [Avoid unnecessary swaps] - | Just lvl1 <- metaTyVarTcLevel_maybe tv1 - = case metaTyVarTcLevel_maybe tv2 of - Nothing -> False - Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True - | lvl1 `strictlyDeeperThan` lvl2 -> False - | otherwise -> nicer_to_update_tv2 - - -- So tv1 is not a meta tyvar - -- If only one is a meta tyvar, put it on the left - -- This is not because it'll be solved; but because - -- the floating step looks for meta tyvars on the left - | isMetaTyVar tv2 = True - - -- So neither is a meta tyvar (including FlatMetaTv) - - -- If only one is a flatten skolem, put it on the left - -- See Note [Eliminate flat-skols] - | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True - - | otherwise = False - - nicer_to_update_tv2 - = (isSigTyVar tv1 && not (isSigTyVar tv2)) - || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1))) - -- | Solve a reflexive equality constraint canEqReflexive :: CtEvidence -- ty ~ ty -> EqRel diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index 583ca622f9..75224d8001 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -13,6 +13,7 @@ import BasicTypes ( infinity, IntWithInf, intGtLimit ) import HsTypes ( HsIPName(..) ) import TcCanonical import TcFlatten +import TcUnify( canSolveByUnification ) import VarSet import Type import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId ) @@ -1124,56 +1125,33 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv ; stopWith ev "Solved from inert (r)" } + | ReprEq <- eq_rel -- We never solve representational + = unsolved_inert -- equalities by unification + + | isGiven ev -- See Note [Touchables and givens] + = unsolved_inert + | otherwise = do { tclvl <- getTcLevel - ; if canSolveByUnification tclvl ev eq_rel tv rhs + ; if canSolveByUnification tclvl tv rhs then do { solveByUnification ev tv rhs ; n_kicked <- kickOutAfterUnification tv ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) } - else do { traceTcS "Can't solve tyvar equality" - (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv) - , ppWhen (isMetaTyVar tv) $ - nest 4 (text "TcLevel of" <+> ppr tv - <+> text "is" <+> ppr (metaTyVarTcLevel tv)) - , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) - , text "TcLevel =" <+> ppr tclvl ]) - ; addInertEq workItem - ; return (Stop ev (text "Kept as inert")) } } - -interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi) + else unsolved_inert } --- @trySpontaneousSolve wi@ solves equalities where one side is a --- touchable unification variable. --- Returns True <=> spontaneous solve happened -canSolveByUnification :: TcLevel -> CtEvidence -> EqRel - -> TcTyVar -> Xi -> Bool -canSolveByUnification tclvl gw eq_rel tv xi - | ReprEq <- eq_rel -- we never solve representational equalities this way. - = False - - | isGiven gw -- See Note [Touchables and givens] - = False - - | isTouchableMetaTyVar tclvl tv - = case metaTyVarInfo tv of - SigTv -> is_tyvar xi - _ -> True - - | otherwise -- Untouchable - = False where - is_tyvar xi - = case tcGetTyVar_maybe xi of - Nothing -> False - Just tv -> case tcTyVarDetails tv of - MetaTv { mtv_info = info } - -> case info of - SigTv -> True - _ -> False - SkolemTv {} -> True - FlatSkol {} -> False - RuntimeUnk -> True + unsolved_inert + = do { traceTcS "Can't solve tyvar equality" + (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv) + , ppWhen (isMetaTyVar tv) $ + nest 4 (text "TcLevel of" <+> ppr tv + <+> text "is" <+> ppr (metaTyVarTcLevel tv)) + , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ]) + ; addInertEq workItem + ; return (Stop ev (text "Kept as inert")) } + +interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi) solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () -- Solve with the identity coercion @@ -1449,7 +1427,9 @@ reduce_top_fun_eq old_ev fsk ax_co rhs_ty ; dischargeFmv old_ev fsk final_co alpha_ty ; traceTcS "doTopReactFunEq (occurs)" $ vcat [ text "old_ev:" <+> ppr old_ev - , nest 2 (text ":=") <+> ppr final_co + , nest 2 (text ":=") <+> + if isDerived old_ev then text "(derived)" + else ppr final_co , text "new_ev:" <+> ppr new_ev ] ; stopWith old_ev "Fun/Top (wanted)" } where diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index e4d6a4b05e..bd64f541ac 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -83,6 +83,7 @@ module TcType ( --------------------------------- -- Misc type manipulators deNoteType, occurCheckExpand, OccCheckResult(..), + occCheckExpand, orphNamesOfType, orphNamesOfCo, orphNamesOfTypes, orphNamesOfCoCon, getDFunTyKey, @@ -1564,7 +1565,49 @@ The two variants of the function are to support TcUnify.checkTauTvUpdate, which wants to prevent unification with type families. For more on this point, see Note [Prevent unification with type families] in TcUnify. -See also Note [occurCheckExpand] in TcCanonical +Note [Occurrence checking: look inside kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are considering unifying + (alpha :: *) ~ Int -> (beta :: alpha -> alpha) +This may be an error (what is that alpha doing inside beta's kind?), +but we must not make the mistake of actuallyy unifying or we'll +build an infinite data structure. So when looking for occurrences +of alpha in the rhs, we must look in the kinds of type variables +that occur there. + +NB: we may be able to remove the problem via expansion; see + Note [Occurs check expansion]. So we have to try that. + +Note [Checking for foralls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Unless we have -XImpredicativeTypes (which is a totally unsupported +feature), we do not want to unify + alpha ~ (forall a. a->a) -> Int +So we look for foralls hidden inside the type, and it's convenient +to do that at the same time as the occurs check (which looks for +occurrences of alpha). + +However, it's not just a question of looking for foralls /anywhere/! +Consider + (alpha :: forall k. k->*) ~ (beta :: forall k. k->*) +This is legal; e.g. dependent/should_compile/T11635. + +We don't want to reject it because of the forall in beta's kind, +but (see Note [Occurrence checking: look inside kinds]) we do +need to look in beta's kind. So we carry a flag saying if a 'forall' +is OK, and sitch the flag on when stepping inside a kind. + +Why is it OK? Why does it not count as impredicative polymorphism? +The reason foralls are bad is because we reply on "seeing" foralls +when doing implicit instantiation. But the forall inside the kind is +fine. We'll generate a kind equality constraint + (forall k. k->*) ~ (forall k. k->*) +to check that the kinds of lhs and rhs are compatible. If alpha's +kind had instead been + (alpha :: kappa) +then this kind equality would rightly complain about unifying kappa +with (forall k. k->*) + -} data OccCheckResult a @@ -1602,39 +1645,63 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type -- - TcUnify.checkTauTvUpdate (on-the-fly unifier) -- - TcInteract.canSolveByUnification (main constraint solver) occurCheckExpand dflags tv ty - | fast_check ty = return ty - | otherwise = go emptyVarEnv ty + = case fast_check impredicative ty of + OC_OK _ -> OC_OK ty + OC_Forall -> OC_Forall + OC_Occurs -> case occCheckExpand tv ty of + Nothing -> OC_Occurs + Just ty' -> OC_OK ty' where - details = tcTyVarDetails tv - + details = tcTyVarDetails tv impredicative = canUnifyWithPolyType dflags details - -- True => fine - fast_check (LitTy {}) = True - fast_check (TyVarTy tv') = tv /= tv' && fast_check (tyVarKind tv') - fast_check (TyConApp tc tys) = all fast_check tys - && (isTauTyCon tc || impredicative) - fast_check (FunTy a r) = fast_check a && fast_check r - fast_check (AppTy fun arg) = fast_check fun && fast_check arg - fast_check (ForAllTy (TvBndr tv' _) ty) - = impredicative - && fast_check (tyVarKind tv') - && (tv == tv' || fast_check ty) - fast_check (CastTy ty co) = fast_check ty && fast_check_co co - fast_check (CoercionTy co) = fast_check_co co + ok :: OccCheckResult () + ok = OC_OK () + + fast_check :: Bool -> TcType -> OccCheckResult () + -- True <=> Foralls are ok; otherwise stop with OC_Forall + -- See Note [Checking for foralls] + + fast_check _ (TyVarTy tv') + | tv == tv' = OC_Occurs + | otherwise = fast_check True (tyVarKind tv') + -- See Note [Occurrence checking: look inside kinds] + + fast_check b (TyConApp tc tys) + | not (b || isTauTyCon tc) = OC_Forall + | otherwise = mapM (fast_check b) tys >> ok + fast_check _ (LitTy {}) = ok + fast_check b (FunTy a r) = fast_check b a >> fast_check b r + fast_check b (AppTy fun arg) = fast_check b fun >> fast_check b arg + fast_check b (CastTy ty co) = fast_check b ty >> fast_check_co co + fast_check _ (CoercionTy co) = fast_check_co co + fast_check b (ForAllTy (TvBndr tv' _) ty) + | not b = OC_Forall + | tv == tv' = ok + | otherwise = do { fast_check True (tyVarKind tv') + ; fast_check b ty } -- we really are only doing an occurs check here; no bother about -- impredicativity in coercions, as they're inferred - fast_check_co co = not (tv `elemVarSet` tyCoVarsOfCo co) + fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs + | otherwise = ok - go :: VarEnv TyVar -- carries mappings necessary because of kind expansion - -> Type -> OccCheckResult Type + +occCheckExpand :: TcTyVar -> TcType -> Maybe TcType +occCheckExpand tv ty + = go emptyVarEnv ty + where + go :: VarEnv TyVar -> Type -> Maybe Type + -- The Varenv carries mappings necessary + -- because of kind expansion go env (TyVarTy tv') - | tv == tv' = OC_Occurs + | tv == tv' = Nothing | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'') | otherwise = do { k' <- go env (tyVarKind tv') ; return (mkTyVarTy $ setTyVarKind tv' k') } + -- See Note [Occurrence checking: look inside kinds] + go _ ty@(LitTy {}) = return ty go env (AppTy ty1 ty2) = do { ty1' <- go env ty1 ; ty2' <- go env ty2 @@ -1643,29 +1710,22 @@ occurCheckExpand dflags tv ty ; ty2' <- go env ty2 ; return (mkFunTy ty1' ty2') } go env ty@(ForAllTy (TvBndr tv' vis) body_ty) - | not impredicative = OC_Forall | tv == tv' = return ty - | otherwise = do { ki' <- go env ki + | otherwise = do { ki' <- go env (tyVarKind tv') ; let tv'' = setTyVarKind tv' ki' env' = extendVarEnv env tv' tv'' ; body' <- go env' body_ty ; return (ForAllTy (TvBndr tv'' vis) body') } - where ki = tyVarKind tv' -- For a type constructor application, first try expanding away the -- offending variable from the arguments. If that doesn't work, next -- see if the type constructor is a type synonym, and if so, expand -- it and try again. go env ty@(TyConApp tc tys) - = case do { tys <- mapM (go env) tys - ; return (mkTyConApp tc tys) } of - OC_OK ty - | impredicative || isTauTyCon tc - -> return ty -- First try to eliminate the tyvar from the args - | otherwise - -> OC_Forall -- A type synonym with a forall on the RHS - bad | Just ty' <- coreView ty -> go env ty' - | otherwise -> bad + = case mapM (go env) tys of + Just tys' -> return (mkTyConApp tc tys') + Nothing | Just ty' <- coreView ty -> go env ty' + | otherwise -> Nothing -- Failing that, try to expand a synonym go env (CastTy ty co) = do { ty' <- go env ty @@ -1683,7 +1743,6 @@ occurCheckExpand dflags tv ty ; arg' <- go_co env arg ; return (mkAppCo co' arg') } go_co env co@(ForAllCo tv' kind_co body_co) - | not impredicative = OC_Forall | tv == tv' = return co | otherwise = do { kind_co' <- go_co env kind_co ; let tv'' = setTyVarKind tv' $ diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index ca3347861b..b564f9fd9a 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -18,6 +18,7 @@ module TcUnify ( -- Various unifications unifyType, unifyTheta, unifyKind, noThing, uType, unifyExpType, + swapOverTyVars, canSolveByUnification, -------------------------------- -- Holes @@ -1116,13 +1117,13 @@ uType origin t_or_k orig_ty1 orig_ty2 ; case lookup_res of Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) ; go ty1 ty2 } - Unfilled ds1 -> uUnfilledVar origin t_or_k NotSwapped tv1 ds1 ty2 } + Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } go ty1 (TyVarTy tv2) = do { lookup_res <- lookupTcTyVar tv2 ; case lookup_res of Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) ; go ty1 ty2 } - Unfilled ds2 -> uUnfilledVar origin t_or_k IsSwapped tv2 ds2 ty1 } + Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) @@ -1304,87 +1305,77 @@ of the substitution; rather, notice that @uVar@ (defined below) nips back into @uTys@ if it turns out that the variable is already bound. -} +---------- uUnfilledVar :: CtOrigin -> TypeOrKind -> SwapFlag - -> TcTyVar -> TcTyVarDetails -- Tyvar 1 - -> TcTauType -- Type 2 + -> TcTyVar -- Tyvar 1 + -> TcTauType -- Type 2 -> TcM Coercion -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar -- It might be a skolem, or untouchable, or meta -uUnfilledVar origin t_or_k swapped tv1 details1 (TyVarTy tv2) - | tv1 == tv2 -- Same type variable => no-op - = return (mkNomReflCo (mkTyVarTy tv1)) - - | otherwise -- Distinct type variables - = do { lookup2 <- lookupTcTyVar tv2 - ; case lookup2 of - Filled ty2' - -> uUnfilledVar origin t_or_k swapped tv1 details1 ty2' - Unfilled details2 - -> uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2 - } - -uUnfilledVar origin t_or_k swapped tv1 details1 non_var_ty2 --- ty2 is not a type variable - = case details1 of - MetaTv { mtv_ref = ref1 } - -> do { dflags <- getDynFlags - ; mb_ty2' <- checkTauTvUpdate dflags origin t_or_k tv1 non_var_ty2 - ; case mb_ty2' of - Just (ty2', co_k) -> maybe_sym swapped <$> - updateMeta tv1 ref1 ty2' co_k - Nothing -> do { traceTc "Occ/type-family defer" - (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) - $$ ppr non_var_ty2 $$ ppr (typeKind non_var_ty2)) - ; defer } - } - - _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts +uUnfilledVar origin t_or_k swapped tv1 ty2 + = do { ty2 <- zonkTcType ty2 + -- Zonk to expose things to the + -- occurs check, and so that if ty2 + -- looks like a type variable then it + -- is a type variable + ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 } + +---------- +uUnfilledVar1 :: CtOrigin + -> TypeOrKind + -> SwapFlag + -> TcTyVar -- Tyvar 1 + -> TcTauType -- Type 2, zonked + -> TcM Coercion +uUnfilledVar1 origin t_or_k swapped tv1 ty2 + | Just tv2 <- tcGetTyVar_maybe ty2 + = go tv2 + + | otherwise + = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + where - defer = unSwap swapped (uType_defer origin t_or_k) (mkTyVarTy tv1) non_var_ty2 - -- Occurs check or an untouchable: just defer - -- NB: occurs check isn't necessarily fatal: - -- eg tv1 occured in type family parameter + -- 'go' handles the case where both are + -- tyvars so we might want to swap + go tv2 | tv1 == tv2 -- Same type variable => no-op + = return (mkNomReflCo (mkTyVarTy tv1)) ----------------- -uUnfilledVars :: CtOrigin + | swapOverTyVars tv1 tv2 -- Distinct type variables + = uUnfilledVar2 origin t_or_k (flipSwap swapped) + tv2 (mkTyVarTy tv1) + + | otherwise + = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + +---------- +uUnfilledVar2 :: CtOrigin -> TypeOrKind -> SwapFlag - -> TcTyVar -> TcTyVarDetails -- Tyvar 1 - -> TcTyVar -> TcTyVarDetails -- Tyvar 2 + -> TcTyVar -- Tyvar 1 + -> TcTauType -- Type 2, zonked -> TcM Coercion --- Invarant: The type variables are distinct, --- Neither is filled in yet - -uUnfilledVars origin t_or_k swapped tv1 details1 tv2 details2 - = do { traceTc "uUnfilledVars for" (ppr tv1 <+> text "and" <+> ppr tv2) - ; traceTc "uUnfilledVars" ( text "trying to unify" <+> ppr k1 - <+> text "with" <+> ppr k2) - ; co_k <- uType kind_origin KindLevel k1 k2 - ; let no_swap ref = maybe_sym swapped <$> - updateMeta tv1 ref ty2 (mkSymCo co_k) - do_swap ref = maybe_sym (flipSwap swapped) <$> - updateMeta tv2 ref ty1 co_k - ; case (details1, details2) of - { ( MetaTv { mtv_info = i1, mtv_ref = ref1 } - , MetaTv { mtv_info = i2, mtv_ref = ref2 } ) - | nicer_to_update_tv1 tv1 i1 i2 -> no_swap ref1 - | otherwise -> do_swap ref2 - ; (MetaTv { mtv_ref = ref1 }, _) -> no_swap ref1 - ; (_, MetaTv { mtv_ref = ref2 }) -> do_swap ref2 - - -- Can't do it in-place, so defer - -- This happens for skolems of all sorts - ; _ -> do { traceTc "deferring because I can't find a meta-tyvar:" - (pprTcTyVarDetails details1 <+> pprTcTyVarDetails details2) - ; unSwap swapped (uType_defer origin t_or_k) ty1 ty2 } } } +uUnfilledVar2 origin t_or_k swapped tv1 ty2 + = do { dflags <- getDynFlags + ; cur_lvl <- getTcLevel + ; go dflags cur_lvl } where - k1 = tyVarKind tv1 - k2 = tyVarKind tv2 + go dflags cur_lvl + | canSolveByUnification cur_lvl tv1 ty2 + , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2 + = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1) + ; co <- updateMeta tv1 ty2' co_k + ; return (maybe_sym swapped co) } + + | otherwise + = unSwap swapped (uType_defer origin t_or_k) ty1 ty2 + -- Occurs check or an untouchable: just defer + -- NB: occurs check isn't necessarily fatal: + -- eg tv1 occured in type family parameter + ty1 = mkTyVarTy tv1 - ty2 = mkTyVarTy tv2 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k) -- | apply sym iff swapped @@ -1392,27 +1383,16 @@ maybe_sym :: SwapFlag -> Coercion -> Coercion maybe_sym IsSwapped = mkSymCo maybe_sym NotSwapped = id -nicer_to_update_tv1 :: TcTyVar -> MetaInfo -> MetaInfo -> Bool -nicer_to_update_tv1 _ _ SigTv = True -nicer_to_update_tv1 _ SigTv _ = False - -- Try not to update SigTvs; and try to update sys-y type - -- variables in preference to ones gotten (say) by - -- instantiating a polymorphic function with a user-written - -- type sig -nicer_to_update_tv1 tv1 _ _ = isSystemName (Var.varName tv1) - ---------------- -checkTauTvUpdate :: DynFlags - -> CtOrigin - -> TypeOrKind - -> TcTyVar -- tv :: k1 - -> TcType -- ty :: k2 - -> TcM (Maybe ( TcType -- possibly-expanded ty - , Coercion )) -- :: k2 ~N k1 --- (checkTauTvUpdate tv ty) --- We are about to update the TauTv tv with ty. +metaTyVarUpdateOK :: DynFlags + -> TcTyVar -- tv :: k1 + -> TcType -- ty :: k2 + -> Maybe TcType -- possibly-expanded ty +-- (metaTyFVarUpdateOK tv ty) +-- We are about to update the meta-tyvar tv with ty. -- Check (a) that tv doesn't occur in ty (occurs check) --- (b) that kind(ty) matches kind(tv) +-- (b) that ty does not have any foralls +-- (in the impredicative case), or type functions -- -- We have two possible outcomes: -- (1) Return the type to update the type variable with, @@ -1429,48 +1409,106 @@ checkTauTvUpdate :: DynFlags -- we return Nothing, leaving it to the later constraint simplifier to -- sort matters out. -checkTauTvUpdate dflags origin t_or_k tv ty - | SigTv <- info - = ASSERT( not (isTyVarTy ty) ) - return Nothing - | 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)) } - +metaTyVarUpdateOK dflags tv ty + = case defer_me impredicative ty of + OC_OK _ -> Just ty + OC_Forall -> Nothing -- forall or type function + OC_Occurs -> occCheckExpand tv ty 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 + defer_me :: Bool -- True <=> foralls are ok + -> TcType + -> OccCheckResult () -- Checks for (a) occurrence of tv -- (b) type family applications - -- (c) foralls + -- (c) foralls if the Bool is false -- See Note [Prevent unification with type families] -- See Note [Refactoring hazard: checkTauTvUpdate] - defer_me (LitTy {}) = False - defer_me (TyVarTy tv') = tv == tv' || defer_me (tyVarKind tv') - defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys - || not (impredicative || isTauTyCon tc) - defer_me (ForAllTy bndr t) = defer_me (binderKind bndr) || defer_me t - || not impredicative - defer_me (FunTy fun arg) = defer_me fun || defer_me arg - 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 + -- See Note [Checking for foralls] in TcType + + defer_me _ (TyVarTy tv') + | tv == tv' = OC_Occurs + | otherwise = defer_me True (tyVarKind tv') + defer_me b (TyConApp tc tys) + | isTypeFamilyTyCon tc = OC_Forall -- We use OC_Forall to signal + -- forall /or/ type function + | not (isTauTyCon tc) = OC_Forall + | otherwise = mapM (defer_me b) tys >> OC_OK () + + defer_me b (ForAllTy (TvBndr tv' _) t) + | not b = OC_Forall + | tv == tv' = OC_OK () + | otherwise = do { defer_me True (tyVarKind tv'); defer_me b t } + + defer_me _ (LitTy {}) = OC_OK () + defer_me b (FunTy fun arg) = defer_me b fun >> defer_me b arg + defer_me b (AppTy fun arg) = defer_me b fun >> defer_me b arg + defer_me b (CastTy ty co) = defer_me b 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 + defer_me_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs + | otherwise = OC_OK () + +swapOverTyVars :: TcTyVar -> TcTyVar -> Bool +-- See Note [Canonical orientation for tyvar/tyvar equality constraints] +swapOverTyVars tv1 tv2 + | Just lvl1 <- metaTyVarTcLevel_maybe tv1 + -- If tv1 is touchable, swap only if tv2 is also + -- touchable and it's strictly better to update the latter + -- But see Note [Avoid unnecessary swaps] + = case metaTyVarTcLevel_maybe tv2 of + Nothing -> False + Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True + | lvl1 `strictlyDeeperThan` lvl2 -> False + | otherwise -> nicer_to_update tv2 + + -- So tv1 is not a meta tyvar + -- If only one is a meta tyvar, put it on the left + -- This is not because it'll be solved; but because + -- the floating step looks for meta tyvars on the left + | isMetaTyVar tv2 = True + + -- So neither is a meta tyvar (including FlatMetaTv) + + -- If only one is a flatten skolem, put it on the left + -- See Note [Eliminate flat-skols] + | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True + + | otherwise = False + + where + nicer_to_update tv2 + = (isSigTyVar tv1 && not (isSigTyVar tv2)) + || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1))) + +-- @trySpontaneousSolve wi@ solves equalities where one side is a +-- touchable unification variable. +-- Returns True <=> spontaneous solve happened +canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool +canSolveByUnification tclvl tv xi + | isTouchableMetaTyVar tclvl tv + = case metaTyVarInfo tv of + SigTv -> is_tyvar xi + _ -> True + + | otherwise -- Untouchable + = False + where + is_tyvar xi + = case tcGetTyVar_maybe xi of + Nothing -> False + Just tv -> case tcTyVarDetails tv of + MetaTv { mtv_info = info } + -> case info of + SigTv -> True + _ -> False + SkolemTv {} -> True + FlatSkol {} -> False + RuntimeUnk -> True {- Note [Prevent unification with type families] @@ -1508,14 +1546,15 @@ with type families].) So I checked the result of occurCheckExpand for any type family occurrences and deferred if there were any. This was done in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 . -This approach turned out not to be performant, because the expanded type -was bigger than the original type, and tyConsOfType looks through type -synonyms. So it then struck me that we could dispense with the defer_me -check entirely. This simplified the code nicely, and it cut the allocations -in T5030 by half. But, as documented in Note [Prevent unification with -type families], this destroyed performance in T3064. Regardless, I missed this -regression and the change was committed as -3f5d1a13f112f34d992f6b74656d64d95a3f506d . +This approach turned out not to be performant, because the expanded +type was bigger than the original type, and tyConsOfType (needed to +see if there are any type family occurrences) looks through type +synonyms. So it then struck me that we could dispense with the +defer_me check entirely. This simplified the code nicely, and it cut +the allocations in T5030 by half. But, as documented in Note [Prevent +unification with type families], this destroyed performance in +T3064. Regardless, I missed this regression and the change was +committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d . Bottom lines: * defer_me is back, but now fixed w.r.t. #11407. @@ -1598,15 +1637,14 @@ lookupTcTyVar tyvar -- | Fill in a meta-tyvar updateMeta :: TcTyVar -- ^ tv to fill in, tv :: k1 - -> TcRef MetaDetails -- ^ ref to tv's metadetails -> TcType -- ^ ty2 :: k2 -> Coercion -- ^ kind_co :: k2 ~N k1 -> TcM Coercion -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2) -updateMeta tv1 ref1 ty2 kind_co - = do { let ty2_refl = mkNomReflCo ty2 - (ty2', co) = ( ty2 `mkCastTy` kind_co - , mkCoherenceLeftCo ty2_refl kind_co ) - ; writeMetaTyVarRef tv1 ref1 ty2' +updateMeta tv1 ty2 kind_co + = do { let ty2' = ty2 `mkCastTy` kind_co + ty2_refl = mkNomReflCo ty2 + co = mkCoherenceLeftCo ty2_refl kind_co + ; writeMetaTyVar tv1 ty2' ; return co } {- diff --git a/testsuite/tests/polykinds/T12593.hs b/testsuite/tests/polykinds/T12593.hs new file mode 100644 index 0000000000..867fb89284 --- /dev/null +++ b/testsuite/tests/polykinds/T12593.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTs, ConstraintKinds, PolyKinds, TypeInType, KindSignatures, RankNTypes #-} + +module T12593 where + +import Data.Kind + +newtype Free k p a b where + Free :: (forall q. k q => (forall c d. p c d -> q c d) -> q a b) + -> Free k p a b + +run :: k2 q => Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) + -> q a b +run (Free cat) = cat diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr new file mode 100644 index 0000000000..4b551558a1 --- /dev/null +++ b/testsuite/tests/polykinds/T12593.stderr @@ -0,0 +1,31 @@ + +T12593.hs:11:16: error: + • Expecting two fewer arguments to ‘Free k k4 k5 p’ + Expected kind ‘k0 -> k1 -> *’, but ‘Free k k4 k5 p’ has kind ‘*’ + • In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:31: error: + • Expecting one more argument to ‘k’ + Expected a type, but + ‘k’ has kind + ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *) + -> Constraint’ + • In the kind ‘k’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b + +T12593.hs:12:40: error: + • Expecting two more arguments to ‘k4’ + Expected a type, but + ‘k4’ has kind + ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’ + • In the kind ‘k1’ + In the type signature: + run :: k2 q => + Free k k1 k2 p a b + -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 1c27dfd82e..6da6ae4439 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -151,3 +151,4 @@ test('T11640', normal, compile, ['']) test('T11554', normal, compile_fail, ['']) test('T12055', normal, compile, ['']) test('T12055a', normal, compile_fail, ['']) +test('T12593', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr index cf206a11ae..d205fa9ced 100644 --- a/testsuite/tests/typecheck/should_compile/tc141.stderr +++ b/testsuite/tests/typecheck/should_compile/tc141.stderr @@ -35,11 +35,11 @@ tc141.hs:13:13: error: in v tc141.hs:15:18: error: - • Couldn't match expected type ‘a1’ with actual type ‘t’ - because type variable ‘a1’ would escape its scope + • Couldn't match expected type ‘a2’ with actual type ‘t’ + because type variable ‘a2’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - v :: a1 + v :: a2 at tc141.hs:14:14-19 • In the expression: b In an equation for ‘v’: v = b @@ -49,6 +49,6 @@ tc141.hs:15:18: error: v = b in v • Relevant bindings include - v :: a1 (bound at tc141.hs:15:14) + v :: a2 (bound at tc141.hs:15:14) b :: t (bound at tc141.hs:13:5) - g :: t1 -> t -> forall a. a (bound at tc141.hs:13:1) + g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1) diff --git a/testsuite/tests/typecheck/should_fail/T9605.stderr b/testsuite/tests/typecheck/should_fail/T9605.stderr index 38da1c46a3..db65629fba 100644 --- a/testsuite/tests/typecheck/should_fail/T9605.stderr +++ b/testsuite/tests/typecheck/should_fail/T9605.stderr @@ -1,11 +1,11 @@ T9605.hs:7:6: error: • Couldn't match type ‘Bool’ with ‘m Bool’ - Expected type: t1 -> m Bool - Actual type: t1 -> Bool + Expected type: t0 -> m Bool + Actual type: t0 -> Bool • The function ‘f1’ is applied to one argument, its type is ‘m0 Bool’, - it is specialized to ‘t1 -> Bool’ + it is specialized to ‘t0 -> Bool’ In the expression: f1 undefined In an equation for ‘f2’: f2 = f1 undefined • Relevant bindings include f2 :: m Bool (bound at T9605.hs:7:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr index ab743441f9..a6fbc86c49 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr @@ -1,6 +1,6 @@ tcfail122.hs:8:9: error: - • Couldn't match kind ‘* -> *’ with ‘*’ + • Couldn't match kind ‘*’ with ‘* -> *’ When matching the kind of ‘a’ • In the expression: undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d |