diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Concrete.hs | 33 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 8 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 172 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 184 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 116 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Zonk.hs | 28 |
6 files changed, 235 insertions, 306 deletions
diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index 0b20a1af9d..bee886a58f 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -15,8 +15,8 @@ import GHC.Core.Coercion import GHC.Core.TyCo.Rep import GHC.Tc.Utils.Monad -import GHC.Tc.Utils.TcType ( TcType, mkTyConApp ) -import GHC.Tc.Utils.TcMType ( newCoercionHole, newFlexiTyVarTy ) +import GHC.Tc.Utils.TcType ( mkTyConApp ) +import GHC.Tc.Utils.TcMType import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) ) @@ -402,11 +402,6 @@ There are, however, some interactions to take into account: Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2. -} --- | A coercion hole used to store evidence for `Concrete#` constraints. --- --- See Note [The Concrete mechanism]. -type ConcreteHole = CoercionHole - -- | Evidence for a `Concrete#` constraint: -- essentially a 'ConcreteHole' (a coercion hole) that will be filled later, -- except: @@ -458,42 +453,32 @@ hasFixedRuntimeRep frrOrig ty -- Create a new Wanted 'Concrete#' constraint and emit it. | otherwise -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel) - ; (hole, ct_ev) <- newConcretePrimWanted loc ki + ; (hole, _, ct_ev) <- newConcretePrimWanted loc ki ; emitSimple $ mkNonCanonical ct_ev ; return $ ConcreteHoleEvidence hole } } where ki :: Kind ki = typeKind ty --- | Create a new (initially unfilled) coercion hole, --- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint. -newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy') - -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep') - -> TcM ConcreteHole -newConcreteHole ki ty - = do { concrete_ty <- newFlexiTyVarTy ki - ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty - ; newCoercionHole co_ty } - -- | Create a new 'Concrete#' constraint. -newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, CtEvidence) +-- Returns the evidence, a metavariable which will be filled in with a +-- guaranteed-concrete type, and a Wanted CtEvidence +newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, TcType, CtEvidence) newConcretePrimWanted loc ty = do { let ki :: Kind ki = typeKind ty - ; hole <- newConcreteHole ki ty + ; (hole, concrete_ty) <- newConcreteHole ki ty ; let wantedCtEv :: CtEvidence wantedCtEv = CtWanted { ctev_dest = HoleDest hole , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] - , ctev_nosh = WOnly -- WOnly, because Derived Concrete# constraints - -- aren't useful: solving a Concrete# constraint - -- can't cause any unification to take place. + , ctev_rewriters = emptyRewriterSet , ctev_loc = loc } - ; return (hole, wantedCtEv) } + ; return (hole, concrete_ty, wantedCtEv) } {-*********************************************************************** * * diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 72670e6b06..a2720bc4e1 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -1261,10 +1261,10 @@ popErrCtxt = updLclEnv (\ env@(TcLclEnv { tcl_ctxt = ctxt }) -> getCtLocM :: CtOrigin -> Maybe TypeOrKind -> TcM CtLoc getCtLocM origin t_or_k = do { env <- getLclEnv - ; return (CtLoc { ctl_origin = origin - , ctl_env = env - , ctl_t_or_k = t_or_k - , ctl_depth = initialSubGoalDepth }) } + ; return (CtLoc { ctl_origin = origin + , ctl_env = env + , ctl_t_or_k = t_or_k + , ctl_depth = initialSubGoalDepth }) } setCtLocM :: CtLoc -> TcM a -> TcM a -- Set the SrcSpan and error context from the CtLoc diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 1ece974166..3c978b511c 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -37,9 +37,9 @@ module GHC.Tc.Utils.TcMType ( -------------------------------- -- Creating new evidence variables newEvVar, newEvVars, newDict, - newWantedWithLoc, newWanted, newWanteds, cloneWanted, cloneWC, + newWantedWithLoc, newWanted, newWanteds, cloneWanted, cloneWC, cloneWantedCtEv, emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars, - emitDerivedEqs, + emitWantedEqs, newTcEvBinds, newNoTcEvBinds, addTcEvBind, emitNewExprHole, @@ -47,6 +47,8 @@ module GHC.Tc.Utils.TcMType ( unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, + ConcreteHole, newConcreteHole, + newImplication, -------------------------------- @@ -97,6 +99,10 @@ module GHC.Tc.Utils.TcMType ( ------------------------------ -- Representation polymorphism checkTypeHasFixedRuntimeRep, + + ------------------------------ + -- Other + anyUnfilledCoercionHoles ) where import GHC.Prelude @@ -192,12 +198,15 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) -- | Create a new Wanted constraint with the given 'CtLoc'. newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty - = do d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole pty - else EvVarDest <$> newEvVar pty - return $ CtWanted { ctev_dest = d - , ctev_pred = pty - , ctev_nosh = WDeriv - , ctev_loc = loc } + = do d <- case classifyPredType pty of + EqPred {} -> HoleDest <$> newCoercionHole pty + SpecialPred ConcretePrimPred ty -> + HoleDest <$> (fst <$> newConcreteHole (typeKind ty) ty) + _ -> EvVarDest <$> newEvVar pty + return $ CtWanted { ctev_dest = d + , ctev_pred = pty + , ctev_loc = loc + , ctev_rewriters = emptyRewriterSet } -- | Create a new Wanted constraint with the given 'CtOrigin', and -- location information taken from the 'TcM' environment. @@ -216,13 +225,20 @@ newWanteds orig = mapM (newWanted orig Nothing) -- Cloning constraints ---------------------------------------------- -cloneWanted :: Ct -> TcM Ct -cloneWanted ct - | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct +cloneWantedCtEv :: CtEvidence -> TcM CtEvidence +cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) + | isEqPrimPred pty = do { co_hole <- newCoercionHole pty - ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) } + ; return (ctev { ctev_dest = HoleDest co_hole }) } + | SpecialPred ConcretePrimPred ty <- classifyPredType pty + = do { (co_hole, _) <- newConcreteHole (typeKind ty) ty + ; return (ctev { ctev_dest = HoleDest co_hole }) } | otherwise - = return ct + = pprPanic "cloneWantedCtEv" (ppr pty) +cloneWantedCtEv ctev = return ctev + +cloneWanted :: Ct -> TcM Ct +cloneWanted ct = mkNonCanonical <$> cloneWantedCtEv (ctEvidence ct) cloneWC :: WantedConstraints -> TcM WantedConstraints -- Clone all the evidence bindings in @@ -252,19 +268,13 @@ emitWanted origin pty ; emitSimple $ mkNonCanonical ev ; return $ ctEvTerm ev } -emitDerivedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM () --- Emit some new derived nominal equalities -emitDerivedEqs origin pairs +emitWantedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM () +-- Emit some new wanted nominal equalities +emitWantedEqs origin pairs | null pairs = return () | otherwise - = do { loc <- getCtLocM origin Nothing - ; emitSimples (listToBag (map (mk_one loc) pairs)) } - where - mk_one loc (ty1, ty2) - = mkNonCanonical $ - CtDerived { ctev_pred = mkPrimEqPred ty1 ty2 - , ctev_loc = loc } + = mapM_ (uncurry (emitWantedEq origin TypeLevel Nominal)) pairs -- | Emits a new equality constraint emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion @@ -272,8 +282,10 @@ emitWantedEq origin t_or_k role ty1 ty2 = do { hole <- newCoercionHole pty ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole - , ctev_nosh = WDeriv, ctev_loc = loc } + CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] } ; return (HoleCo hole) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -284,10 +296,10 @@ emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar emitWantedEvVar origin ty = do { new_cv <- newEvVar ty ; loc <- getCtLocM origin Nothing - ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv - , ctev_pred = ty - , ctev_nosh = WDeriv - , ctev_loc = loc } + ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv + , ctev_pred = ty + , ctev_loc = loc + , ctev_rewriters = emptyRewriterSet } ; emitSimple $ mkNonCanonical ctev ; return new_cv } @@ -302,7 +314,7 @@ emitNewExprHole occ ty ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u)) ; let her = HER ref ty u - ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel) + ; loc <- getCtLocM (ExprHoleOrigin (Just occ)) (Just TypeLevel) ; let hole = Hole { hole_sort = ExprHole her , hole_occ = occ @@ -353,7 +365,7 @@ newImplication newCoercionHole :: TcPredType -> TcM CoercionHole newCoercionHole pred_ty = do { co_var <- newEvVar pred_ty - ; traceTc "New coercion hole:" (ppr co_var) + ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) ; ref <- newMutVar Nothing ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } @@ -411,6 +423,24 @@ checkCoercionHole cv co | otherwise = False +-- | A coercion hole used to store evidence for `Concrete#` constraints. +-- +-- See Note [The Concrete mechanism]. +type ConcreteHole = CoercionHole + +-- | Create a new (initially unfilled) coercion hole, +-- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint. +newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy') + -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep') + -> TcM (ConcreteHole, TcType) + -- ^ where to put the evidence, and a metavariable to store + -- the concrete type +newConcreteHole ki ty + = do { concrete_ty <- newFlexiTyVarTy ki + ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty + ; hole <- newCoercionHole co_ty + ; return (hole, concrete_ty) } + {- ********************************************************************** * ExpType functions @@ -2465,14 +2495,11 @@ zonkSkolemInfoAnon (InferSkol ntys) = do { ntys' <- mapM do_one ntys zonkSkolemInfoAnon skol_info = return skol_info {- -%************************************************************************ -%* * -\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar} +************************************************************************ * * -* For internal use only! * + Zonking -- the main work-horses: zonkTcType, zonkTcTyVar * * ************************************************************************ - -} -- For unbound, mutable tyvars, zonkType uses the function given to it @@ -2620,13 +2647,21 @@ zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k) ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) } zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2) = do { (env1, p1') <- zonkTidyTcType env p1 - ; (env2, p2') <- zonkTidyTcType env1 p2 - ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) } + ; (env2, o1') <- zonkTidyOrigin env1 o1 + ; (env3, p2') <- zonkTidyTcType env2 p2 + ; (env4, o2') <- zonkTidyOrigin env3 o2 + ; return (env4, FunDepOrigin1 p1' o1' l1 p2' o2' l2) } zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2) = do { (env1, p1') <- zonkTidyTcType env p1 ; (env2, p2') <- zonkTidyTcType env1 p2 ; (env3, o1') <- zonkTidyOrigin env2 o1 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) } +zonkTidyOrigin env (InjTFOrigin1 pred1 orig1 loc1 pred2 orig2 loc2) + = do { (env1, pred1') <- zonkTidyTcType env pred1 + ; (env2, orig1') <- zonkTidyOrigin env1 orig1 + ; (env3, pred2') <- zonkTidyTcType env2 pred2 + ; (env4, orig2') <- zonkTidyOrigin env3 orig2 + ; return (env4, InjTFOrigin1 pred1' orig1' loc1 pred2' orig2' loc2) } zonkTidyOrigin env (CycleBreakerOrigin orig) = do { (env1, orig') <- zonkTidyOrigin env orig ; return (env1, CycleBreakerOrigin orig') } @@ -2636,6 +2671,10 @@ zonkTidyOrigin env (InstProvidedOrigin mod cls_inst) zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig) = do { (env1, ty') <- zonkTidyTcType env ty ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)} +zonkTidyOrigin env (WantedSuperclassOrigin pty orig) + = do { (env1, pty') <- zonkTidyTcType env pty + ; (env2, orig') <- zonkTidyOrigin env1 orig + ; return (env2, WantedSuperclassOrigin pty' orig') } zonkTidyOrigin env orig = return (env, orig) zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin]) @@ -2644,13 +2683,14 @@ zonkTidyOrigins = mapAccumLM zonkTidyOrigin ---------------- tidyCt :: TidyEnv -> Ct -> Ct -- Used only in error reporting -tidyCt env ct - = ct { cc_ev = tidy_ev (ctEvidence ct) } - where - tidy_ev :: CtEvidence -> CtEvidence +tidyCt env ct = ct { cc_ev = tidyCtEvidence env (ctEvidence ct) } + +tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence -- NB: we do not tidy the ctev_evar field because we don't -- show it in error messages - tidy_ev ctev = ctev { ctev_pred = tidyType env (ctev_pred ctev) } +tidyCtEvidence env ctev = ctev { ctev_pred = tidyType env ty } + where + ty = ctev_pred ctev tidyHole :: TidyEnv -> Hole -> Hole tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty } @@ -2728,3 +2768,49 @@ naughtyQuantification orig_ty tv escapees ] ; failWithTcM (env, msg) } + +{- +************************************************************************ +* * + Checking for coercion holes +* * +************************************************************************ +-} + +-- | Check whether any coercion hole in a RewriterSet is still unsolved. +-- Does this by recursively looking through filled coercion holes until +-- one is found that is not yet filled in, at which point this aborts. +anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool +anyUnfilledCoercionHoles (RewriterSet set) + = nonDetStrictFoldUniqSet go (return False) set + -- this does not introduce non-determinism, because the only + -- monadic action is to read, and the combining function is + -- commutative + where + go :: CoercionHole -> TcM Bool -> TcM Bool + go hole m_acc = m_acc <||> check_hole hole + + check_hole :: CoercionHole -> TcM Bool + check_hole hole = do { m_co <- unpackCoercionHole_maybe hole + ; case m_co of + Nothing -> return True -- unfilled hole + Just co -> unUCHM (check_co co) } + + check_ty :: Type -> UnfilledCoercionHoleMonoid + check_co :: Coercion -> UnfilledCoercionHoleMonoid + (check_ty, _, check_co, _) = foldTyCo folder () + + folder :: TyCoFolder () UnfilledCoercionHoleMonoid + folder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv) + , tcf_covar = \ _ cv -> check_ty (varType cv) + , tcf_hole = \ _ -> UCHM . check_hole + , tcf_tycobinder = \ _ _ _ -> () } + +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool } + +instance Semigroup UnfilledCoercionHoleMonoid where + UCHM l <> UCHM r = UCHM (l <||> r) + +instance Monoid UnfilledCoercionHoleMonoid where + mempty = UCHM (return False) diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index ae35cea3a2..807ad0ab56 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -92,11 +92,12 @@ module GHC.Tc.Utils.TcType ( orphNamesOfType, orphNamesOfCo, orphNamesOfTypes, orphNamesOfCoCon, getDFunTyKey, evVarPred, + ambigTkvsOfTy, --------------------------------- -- Predicate types mkMinimalBySCs, transSuperClasses, - pickQuantifiablePreds, pickCapturedPreds, + pickCapturedPreds, immSuperClasses, boxEqPred, isImprovementPred, @@ -105,7 +106,7 @@ module GHC.Tc.Utils.TcType ( -- * Finding "exact" (non-dead) type variables exactTyCoVarsOfType, exactTyCoVarsOfTypes, - anyRewritableTyVar, anyRewritableTyFamApp, anyRewritableCanEqLHS, + anyRewritableTyVar, anyRewritableTyFamApp, --------------------------------- -- Foreign import and export @@ -231,6 +232,7 @@ import qualified GHC.LanguageExtensions as LangExt import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) +import Data.List ( partition ) import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo ) @@ -847,15 +849,14 @@ isTyFamFree :: Type -> Bool -- ^ Check that a type does not contain any type family applications. isTyFamFree = null . tcTyFamInsts -any_rewritable :: Bool -- Ignore casts and coercions - -> EqRel -- Ambient role +any_rewritable :: EqRel -- Ambient role -> (EqRel -> TcTyVar -> Bool) -- check tyvar -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family -> (TyCon -> Bool) -- expand type synonym? -> TcType -> Bool -- Checks every tyvar and tyconapp (not including FunTys) within a type, -- ORing the results of the predicates above together --- Do not look inside casts and coercions if 'ignore_cos' is True +-- Do not look inside casts and coercions -- See Note [anyRewritableTyVar must be role-aware] -- -- This looks like it should use foldTyCo, but that function is @@ -864,7 +865,7 @@ any_rewritable :: Bool -- Ignore casts and coercions -- -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. {-# INLINE any_rewritable #-} -- this allows specialization of predicates -any_rewritable ignore_cos role tv_pred tc_pred should_expand +any_rewritable role tv_pred tc_pred should_expand = go role emptyVarSet where go_tv rl bvs tv | tv `elemVarSet` bvs = False @@ -890,8 +891,8 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand where arg_rep = getRuntimeRep arg -- forgetting these causes #17024 res_rep = getRuntimeRep res go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty - go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co - go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check + go rl bvs (CastTy ty _) = go rl bvs ty + go _ _ (CoercionTy _) = False go_tc NomEq bvs _ tys = any (go NomEq bvs) tys go_tc ReprEq bvs tc tys = any (go_arg bvs) @@ -901,19 +902,12 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand go_arg bvs (Representational, ty) = go ReprEq bvs ty go_arg _ (Phantom, _) = False -- We never rewrite with phantoms - go_co rl bvs co - | ignore_cos = False - | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co) - -- We don't have an equivalent of anyRewritableTyVar for coercions - -- (at least not yet) so take the free vars and test them - -anyRewritableTyVar :: Bool -- Ignore casts and coercions - -> EqRel -- Ambient role +anyRewritableTyVar :: EqRel -- Ambient role -> (EqRel -> TcTyVar -> Bool) -- check tyvar -> TcType -> Bool -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. -anyRewritableTyVar ignore_cos role pred - = any_rewritable ignore_cos role pred +anyRewritableTyVar role pred + = any_rewritable role pred (\ _ _ _ -> False) -- no special check for tyconapps -- (this False is ORed with other results, so it -- really means "do nothing special"; the arguments @@ -930,18 +924,7 @@ anyRewritableTyFamApp :: EqRel -- Ambient role -- always ignores casts & coercions -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. anyRewritableTyFamApp role check_tyconapp - = any_rewritable True role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon) - --- This version is used by shouldSplitWD. It *does* look in casts --- and coercions, and it always expands type synonyms whose RHSs mention --- type families. --- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. -anyRewritableCanEqLHS :: EqRel -- Ambient role - -> (EqRel -> TcTyVar -> Bool) -- check tyvar - -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family - -> TcType -> Bool -anyRewritableCanEqLHS role check_tyvar check_tyconapp - = any_rewritable False role check_tyvar check_tyconapp (not . isFamFreeTyCon) + = any_rewritable role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon) {- Note [anyRewritableTyVar must be role-aware] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1170,6 +1153,16 @@ findDupTyVarTvs prs eq_snd (_,tv1) (_,tv2) = tv1 == tv2 mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs +-- | Returns the (kind, type) variables in a type that are +-- as-yet-unknown: metavariables and RuntimeUnks +ambigTkvsOfTy :: TcType -> ([Var],[Var]) +ambigTkvsOfTy ty + = partition (`elemVarSet` dep_tkv_set) ambig_tkvs + where + tkvs = tyCoVarsOfTypeList ty + ambig_tkvs = filter isAmbiguousTyVar tkvs + dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs) + {- ************************************************************************ * * @@ -1774,71 +1767,7 @@ evVarPred var = varType var -- partial signatures, (isEvVarType kappa) will return False. But -- nothing is wrong. So I just removed the ASSERT. ------------------- --- | When inferring types, should we quantify over a given predicate? --- Generally true of classes; generally false of equality constraints. --- Equality constraints that mention quantified type variables and --- implicit variables complicate the story. See Notes --- [Inheriting implicit parameters] and [Quantifying over equality constraints] -pickQuantifiablePreds - :: TyVarSet -- Quantifying over these - -> TcThetaType -- Proposed constraints to quantify - -> TcThetaType -- A subset that we can actually quantify --- This function decides whether a particular constraint should be --- quantified over, given the type variables that are being quantified -pickQuantifiablePreds qtvs theta - = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without - -- -XFlexibleContexts: see #10608, #10351 - -- flex_ctxt <- xoptM Opt_FlexibleContexts - mapMaybe (pick_me flex_ctxt) theta - where - pick_me flex_ctxt pred - = case classifyPredType pred of - - ClassPred cls tys - | Just {} <- isCallStackPred cls tys - -- NEVER infer a CallStack constraint. Otherwise we let - -- the constraints bubble up to be solved from the outer - -- context, or be defaulted when we reach the top-level. - -- See Note [Overview of implicit CallStacks] - -> Nothing - - | isIPClass cls - -> Just pred -- See Note [Inheriting implicit parameters] - - | pick_cls_pred flex_ctxt cls tys - -> Just pred - - EqPred eq_rel ty1 ty2 - | quantify_equality eq_rel ty1 ty2 - , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2 - -- boxEqPred: See Note [Lift equality constraints when quantifying] - , pick_cls_pred flex_ctxt cls tys - -> Just (mkClassPred cls tys) - - IrredPred ty - | tyCoVarsOfType ty `intersectsVarSet` qtvs - -> Just pred - - _ -> Nothing - - - pick_cls_pred flex_ctxt cls tys - = tyCoVarsOfTypes tys `intersectsVarSet` qtvs - && (checkValidClsArgs flex_ctxt cls tys) - -- Only quantify over predicates that checkValidType - -- will pass! See #10351. - - -- See Note [Quantifying over equality constraints] - quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2 - quantify_equality ReprEq _ _ = True - - quant_fun ty - = case tcSplitTyConApp_maybe ty of - Just (tc, tys) | isTypeFamilyTyCon tc - -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs - _ -> False - +--------------------------- boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type]) -- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version -- (t1 ~ t2) or (t1 `Coercible` t2) @@ -2013,71 +1942,6 @@ Notice that See also GHC.Tc.TyCl.Utils.checkClassCycles. -Note [Lift equality constraints when quantifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can't quantify over a constraint (t1 ~# t2) because that isn't a -predicate type; see Note [Types for coercions, predicates, and evidence] -in GHC.Core.TyCo.Rep. - -So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted -to Coercible. - -This tiresome lifting is the reason that pick_me (in -pickQuantifiablePreds) returns a Maybe rather than a Bool. - -Note [Quantifying over equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should we quantify over an equality constraint (s ~ t)? In general, we don't. -Doing so may simply postpone a type error from the function definition site to -its call site. (At worst, imagine (Int ~ Bool)). - -However, consider this - forall a. (F [a] ~ Int) => blah -Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call -site we will know 'a', and perhaps we have instance F [Bool] = Int. -So we *do* quantify over a type-family equality where the arguments mention -the quantified variables. - -Note [Inheriting implicit parameters] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this: - - f x = (x::Int) + ?y - -where f is *not* a top-level binding. -From the RHS of f we'll get the constraint (?y::Int). -There are two types we might infer for f: - - f :: Int -> Int - -(so we get ?y from the context of f's definition), or - - f :: (?y::Int) => Int -> Int - -At first you might think the first was better, because then -?y behaves like a free variable of the definition, rather than -having to be passed at each call site. But of course, the WHOLE -IDEA is that ?y should be passed at each call site (that's what -dynamic binding means) so we'd better infer the second. - -BOTTOM LINE: when *inferring types* you must quantify over implicit -parameters, *even if* they don't mention the bound type variables. -Reason: because implicit parameters, uniquely, have local instance -declarations. See pickQuantifiablePreds. - -Note [Quantifying over equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should we quantify over an equality constraint (s ~ t)? In general, we don't. -Doing so may simply postpone a type error from the function definition site to -its call site. (At worst, imagine (Int ~ Bool)). - -However, consider this - forall a. (F [a] ~ Int) => blah -Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call -site we will know 'a', and perhaps we have instance F [Bool] = Int. -So we *do* quantify over a type-family equality where the arguments mention -the quantified variables. - ************************************************************************ * * Classifying types diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 1ff6c044dc..4a5ef151b7 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -556,8 +556,7 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt -- If wrap = tc_sub_type_et t1 t2 -- => wrap :: t1 ~> t2 tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected - = do { dflags <- getDynFlags - ; tc_sub_type dflags unifyTypeET inst_orig ctxt ty_actual ty_expected } + = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected tcSubTypePat _ _ (Infer inf_res) ty_expected = do { co <- fillInferResult ty_expected inf_res @@ -584,9 +583,8 @@ tcSubTypeNC :: CtOrigin -- ^ Used when instantiating -> TcM HsWrapper tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty = case res_ty of - Check ty_expected -> do { dflags <- getDynFlags - ; tc_sub_type dflags (unifyType m_thing) inst_orig ctxt - ty_actual ty_expected } + Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt + ty_actual ty_expected Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual -- See Note [Instantiation of InferResult] @@ -631,22 +629,18 @@ command. See Note [Implementing :type] in GHC.Tc.Module. -} --------------- -tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubTypeSigma :: CtOrigin -- where did the actual type arise / why are we + -- doing this subtype check? + -> UserTypeCtxt -- where did the expected type arise? + -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- External entry point, but no ExpTypes on either side -- Checks that actual <= expected -- Returns HsWrapper :: actual ~ expected -tcSubTypeSigma ctxt ty_actual ty_expected - = do { dflags <- getDynFlags - ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected } - where - eq_orig = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = Nothing - , uo_visible = True } +tcSubTypeSigma orig ctxt ty_actual ty_expected + = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected --------------- -tc_sub_type :: DynFlags - -> (TcType -> TcType -> TcM TcCoercionN) -- How to unify +tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify -> CtOrigin -- Used when instantiating -> UserTypeCtxt -- Used when skolemising -> TcSigmaType -- Actual; a sigma-type @@ -655,7 +649,7 @@ tc_sub_type :: DynFlags -- Checks that actual_ty is more polymorphic than expected_ty -- If wrap = tc_sub_type t1 t2 -- => wrap :: t1 ~> t2 -tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected +tc_sub_type unify inst_orig ctxt ty_actual ty_expected | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily] , not (possibly_poly ty_actual) = do { traceTc "tc_sub_type (drop to equality)" $ @@ -683,7 +677,7 @@ tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected | (tvs, theta, tau) <- tcSplitSigmaTy ty , (tv:_) <- tvs , null theta - , checkTyVarEq dflags tv tau `cterHasProblem` cteInsolubleOccurs + , checkTyVarEq tv tau `cterHasProblem` cteInsolubleOccurs = True | otherwise = False @@ -1067,7 +1061,7 @@ take care: can yield /very/ confusing error messages, because we can get [W] C Int b1 -- from f_blah [W] C Int b2 -- from g_blan - and fundpes can yield [D] b1 ~ b2, even though the two functions have + and fundpes can yield [W] b1 ~ b2, even though the two functions have literally nothing to do with each other. #14185 is an example. Building an implication keeps them separate. -} @@ -1447,15 +1441,14 @@ uUnfilledVar2 :: CtOrigin -> TcTauType -- Type 2, zonked -> TcM Coercion uUnfilledVar2 origin t_or_k swapped tv1 ty2 - = do { dflags <- getDynFlags - ; cur_lvl <- getTcLevel - ; go dflags cur_lvl } + = do { cur_lvl <- getTcLevel + ; go cur_lvl } where - go dflags cur_lvl + go cur_lvl | isTouchableMetaTyVar cur_lvl tv1 -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles , canSolveByUnification (metaTyVarInfo tv1) ty2 - , cterHasNoProblem (checkTyVarEq dflags tv1 ty2) + , cterHasNoProblem (checkTyVarEq tv1 ty2) -- See Note [Prevent unification with type families] = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ @@ -1471,7 +1464,8 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 ; return (mkTcNomReflCo ty2) } else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical - -- Note [Equalities with incompatible kinds] + -- Note [Equalities with incompatible kinds] for how + -- this will be dealt with in the solver | otherwise = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) @@ -1485,14 +1479,20 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 -canSolveByUnification :: MetaInfo -> TcType -> Bool --- See Note [Unification preconditions, (TYVAR-TV)] +-- | Checks (TYVAR-TV) and (COERCION-HOLE) of Note [Unification preconditions]; +-- returns True if these conditions are satisfied. But see the Note for other +-- preconditions, too. +canSolveByUnification :: MetaInfo -> TcType -- zonked + -> Bool +canSolveByUnification _ xi + | hasCoercionHoleTy xi -- (COERCION-HOLE) check + = False canSolveByUnification info xi = case info of CycleBreakerTv -> False TyVarTv -> case tcGetTyVar_maybe xi of Nothing -> False - Just tv -> case tcTyVarDetails tv of + Just tv -> case tcTyVarDetails tv of -- (TYVAR-TV) wrinkle MetaTv { mtv_info = info } -> case info of TyVarTv -> True @@ -1552,7 +1552,7 @@ unify alpha := ty? This note only applied to /homogeneous/ equalities, in which both sides have the same kind. -There are three reasons not to unify: +There are four reasons not to unify: 1. (SKOL-ESC) Skolem-escape Consider the constraint @@ -1590,8 +1590,22 @@ There are three reasons not to unify: * CycleBreakerTv: never unified, except by restoreTyVarCycles. +4. (COERCION-HOLE) Confusing coercion holes + Suppose our equality is + (alpha :: k) ~ (Int |> {co}) + where co :: Type ~ k is an unsolved wanted. Note that this + equality is homogeneous; both sides have kind k. Unifying here + is sensible, but it can lead to very confusing error messages. + It's very much like a Wanted rewriting a Wanted. Even worse, + unifying a variable essentially turns an equality into a Given, + and so we could not use the tracking mechansim in + Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. + We thus simply do not unify in this case. + + This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds] + in GHC.Tc.Solver.Canonical. -Needless to say, all three have wrinkles: +Needless to say, all there are wrinkles: * (SKOL-ESC) Promotion. Given alpha[n] ~ ty, what if beta[k] is free in 'ty', where beta is a unification variable, and k>n? 'beta' @@ -1653,7 +1667,7 @@ So we look for a positive reason to swap, using a three-step test: Generally speaking we always try to put a MetaTv on the left in preference to SkolemTv or RuntimeUnkTv: a) Because the MetaTv may be touchable and can be unified - b) Even if it's not touchable, GHC.Tc.Solver.floatEqualities + b) Even if it's not touchable, GHC.Tc.Solver.floatConstraints looks for meta tyvars on the left Tie-breaking rules for MetaTvs: @@ -1909,23 +1923,22 @@ with (forall k. k->*) ---------------- {-# NOINLINE checkTyVarEq #-} -- checkTyVarEq becomes big after the `inline` fires -checkTyVarEq :: DynFlags -> TcTyVar -> TcType -> CheckTyEqResult -checkTyVarEq dflags tv ty - = inline checkTypeEq dflags (TyVarLHS tv) ty +checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult +checkTyVarEq tv ty + = inline checkTypeEq (TyVarLHS tv) ty -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away {-# NOINLINE checkTyFamEq #-} -- checkTyFamEq becomes big after the `inline` fires -checkTyFamEq :: DynFlags - -> TyCon -- type function +checkTyFamEq :: TyCon -- type function -> [TcType] -- args, exactly saturated -> TcType -- RHS -> CheckTyEqResult -- always drops cteTypeFamily -checkTyFamEq dflags fun_tc fun_args ty - = inline checkTypeEq dflags (TyFamLHS fun_tc fun_args) ty +checkTyFamEq fun_tc fun_args ty + = inline checkTypeEq (TyFamLHS fun_tc fun_args) ty `cterRemoveProblem` cteTypeFamily -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away -checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult +checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult -- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs -- is a canonical CEqCan. -- @@ -1933,8 +1946,7 @@ checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult -- (a) a forall type (forall a. blah) -- (b) a predicate type (c => ty) -- (c) a type family; see Note [Prevent unification with type families] --- (d) a blocking coercion hole --- (e) an occurrence of the LHS (occurs check) +-- (d) an occurrence of the LHS (occurs check) -- -- Note that an occurs-check does not mean "definite error". For example -- type family F a @@ -1945,20 +1957,18 @@ checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult -- certainly can't unify b0 := F b0 -- -- For (a), (b), and (c) we check only the top level of the type, NOT --- inside the kinds of variables it mentions. For (d) we look deeply --- in coercions when the LHS is a tyvar (but skip coercions for type family --- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. +-- inside the kinds of variables it mentions, and for (d) see +-- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint. -- -- checkTypeEq is called from -- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the -- case-analysis on 'lhs') -- * checkEqCanLHSFinish, which does not know the form of 'lhs' -checkTypeEq dflags lhs ty +checkTypeEq lhs ty = go ty where impredicative = cteProblem cteImpredicative type_family = cteProblem cteTypeFamily - hole_blocker = cteProblem cteHoleBlocker insoluble_occurs = cteProblem cteInsolubleOccurs soluble_occurs = cteProblem cteSolubleOccurs @@ -2029,21 +2039,11 @@ checkTypeEq dflags lhs ty -- inferred go_co co | TyVarLHS tv <- lhs , tv `elemVarSet` tyCoVarsOfCo co - = soluble_occurs S.<> maybe_hole_blocker + = soluble_occurs -- Don't check coercions for type families; see commentary at top of function | otherwise - = maybe_hole_blocker - where - -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds] - -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for - -- deferred type errors - maybe_hole_blocker | not (gopt Opt_DeferTypeErrors dflags) - , hasCoercionHoleCo co - = hole_blocker - - | otherwise - = cteOK + = cteOK check_tc :: TyCon -> CheckTyEqResult check_tc diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index 436543b095..ba6c98905f 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -68,7 +68,6 @@ import GHC.Utils.Outputable import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Utils.Panic.Plain -import GHC.Utils.Constants (debugIsOn) import GHC.Core.Multiplicity import GHC.Core @@ -511,14 +510,14 @@ zonkLocalBinds env (HsIPBinds x (IPBinds dict_binds binds )) = do new_binds <- mapM (wrapLocMA zonk_ip_bind) binds let env1 = extendIdZonkEnvRec env - [ n | (L _ (IPBind _ (Right n) _)) <- new_binds] + [ n | (L _ (IPBind n _ _)) <- new_binds] (env2, new_dict_binds) <- zonkTcEvBinds env1 dict_binds return (env2, HsIPBinds x (IPBinds new_dict_binds new_binds)) where - zonk_ip_bind (IPBind x n e) - = do n' <- mapIPNameTc (zonkIdBndr env) n + zonk_ip_bind (IPBind dict_id n e) + = do dict_id' <- zonkIdBndr env dict_id e' <- zonkLExpr env e - return (IPBind x n' e') + return (IPBind dict_id' n e') --------------------------------------------- zonkRecMonoBinds :: ZonkEnv -> LHsBinds GhcTc -> TcM (ZonkEnv, LHsBinds GhcTc) @@ -1318,13 +1317,6 @@ zonkRecUpdFields env = mapM zonk_rbind ; return (L l (fld { hfbLHS = fmap ambiguousFieldOcc new_id , hfbRHS = new_expr })) } -------------------------------------------------------------------------- -mapIPNameTc :: (a -> TcM b) -> Either (LocatedAn NoEpAnns HsIPName) a - -> TcM (Either (LocatedAn NoEpAnns HsIPName) b) -mapIPNameTc _ (Left x) = return (Left x) -mapIPNameTc f (Right x) = do r <- f x - return (Right r) - {- ************************************************************************ * * @@ -1833,6 +1825,13 @@ commitFlexi flexi tv zonked_kind SkolemiseFlexi -> return (mkTyVarTy (mkTyVar name zonked_kind)) DefaultFlexi + -- Normally, RuntimeRep variables are defaulted in TcMType.defaultTyVar + -- But that sees only type variables that appear in, say, an inferred type + -- Defaulting here in the zonker is needed to catch e.g. + -- y :: Bool + -- y = (\x -> True) undefined + -- We need *some* known RuntimeRep for the x and undefined, but no one + -- will choose it until we get here, in the zonker. | isRuntimeRepTy zonked_kind -> do { traceTc "Defaulting flexi tyvar to LiftedRep:" (pprTyVar tv) ; return liftedRepTy } @@ -1877,11 +1876,6 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) -- (undeferred) type errors. Originally, I put in a panic -- here, but that caused too many uses of `failIfErrsM`. Nothing -> do { traceTc "Zonking unfilled coercion hole" (ppr hole) - ; when debugIsOn $ - whenNoErrs $ - massertPpr False - (text "Type-correct unfilled coercion hole" - <+> ppr hole) ; cv' <- zonkCoVar cv ; return $ mkCoVarCo cv' } } -- This will be an out-of-scope variable, but keeping |