diff options
21 files changed, 638 insertions, 610 deletions
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 98c47aa767..61a374b38e 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -19,7 +19,7 @@ Note [The Type-related module hierarchy] -- We expose the relevant stuff from this module via the Type module {-# OPTIONS_HADDOCK not-home #-} -{-# LANGUAGE CPP, DeriveDataTypeable, MultiWayIf, PatternSynonyms, BangPatterns #-} +{-# LANGUAGE CPP, MultiWayIf, PatternSynonyms, BangPatterns, DeriveDataTypeable #-} module GHC.Core.TyCo.Rep ( TyThing(..), tyThingCategory, pprTyThingCategory, pprShortTyThing, @@ -2025,6 +2025,12 @@ GHC.Core.Multiplicity above this module. -- | A shorthand for data with an attached 'Mult' element (the multiplicity). data Scaled a = Scaled Mult a deriving (Data.Data) + -- You might think that this would be a natural candiate for + -- Functor, Traversable but Krzysztof says (!3674) "it was too easy + -- to accidentally lift functions (substitutions, zonking etc.) from + -- Type -> Type to Scaled Type -> Scaled Type, ignoring + -- multiplicities and causing bugs". So we don't. + instance (Outputable a) => Outputable (Scaled a) where ppr (Scaled _cnt t) = ppr t diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 5bb11a9ee7..a0865b1820 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -48,7 +48,7 @@ module GHC.Core.Type ( mkSpecForAllTy, mkSpecForAllTys, mkVisForAllTys, mkTyCoInvForAllTy, mkInfForAllTy, mkInfForAllTys, - splitForAllTys, splitSomeForAllTys, + splitForAllTys, splitForAllTysReq, splitForAllTysInvis, splitForAllVarBndrs, splitForAllTy_maybe, splitForAllTy, @@ -284,7 +284,7 @@ import GHC.Data.List.SetOps import GHC.Types.Unique ( nonDetCmpUnique ) import GHC.Data.Maybe ( orElse, expectJust ) -import Data.Maybe ( isJust, mapMaybe ) +import Data.Maybe ( isJust ) import Control.Monad ( guard ) -- $type_classification @@ -1526,46 +1526,34 @@ splitForAllTys ty = split ty ty [] split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs split orig_ty _ tvs = (reverse tvs, orig_ty) --- | Like 'splitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@ --- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and --- @argf_pred@ is a predicate over visibilities provided as an argument to this --- function. Furthermore, each returned tyvar is annotated with its @argf@. -splitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type) +-- | Splits the longest initial sequence of ForAllTys' that satisfy +-- @argf_pred@, returning the binders transformed by @argf_pred@ +splitSomeForAllTys :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type) splitSomeForAllTys argf_pred ty = split ty ty [] where - split _ (ForAllTy tvb@(Bndr _ argf) ty) tvs - | argf_pred argf = split ty ty (tvb:tvs) + split _ (ForAllTy (Bndr tcv argf) ty) tvs + | Just argf' <- argf_pred argf = split ty ty (Bndr tcv argf' : tvs) split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs split orig_ty _ tvs = (reverse tvs, orig_ty) -- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Required' type -- variable binders. Furthermore, each returned tyvar is annotated with '()'. splitForAllTysReq :: Type -> ([ReqTVBinder], Type) -splitForAllTysReq ty = - let (all_bndrs, body) = splitSomeForAllTys isVisibleArgFlag ty - req_bndrs = mapMaybe mk_req_bndr_maybe all_bndrs in - ASSERT( req_bndrs `equalLength` all_bndrs ) - (req_bndrs, body) +splitForAllTysReq ty = splitSomeForAllTys argf_pred ty where - mk_req_bndr_maybe :: TyCoVarBinder -> Maybe ReqTVBinder - mk_req_bndr_maybe (Bndr tv argf) = case argf of - Required -> Just $ Bndr tv () - Invisible _ -> Nothing + argf_pred :: ArgFlag -> Maybe () + argf_pred Required = Just () + argf_pred (Invisible {}) = Nothing -- | Like 'splitForAllTys', but only splits 'ForAllTy's with 'Invisible' type -- variable binders. Furthermore, each returned tyvar is annotated with its -- 'Specificity'. splitForAllTysInvis :: Type -> ([InvisTVBinder], Type) -splitForAllTysInvis ty = - let (all_bndrs, body) = splitSomeForAllTys isInvisibleArgFlag ty - inv_bndrs = mapMaybe mk_inv_bndr_maybe all_bndrs in - ASSERT( inv_bndrs `equalLength` all_bndrs ) - (inv_bndrs, body) +splitForAllTysInvis ty = splitSomeForAllTys argf_pred ty where - mk_inv_bndr_maybe :: TyCoVarBinder -> Maybe InvisTVBinder - mk_inv_bndr_maybe (Bndr tv argf) = case argf of - Invisible s -> Just $ Bndr tv s - Required -> Nothing + argf_pred :: ArgFlag -> Maybe Specificity + argf_pred Required = Nothing + argf_pred (Invisible spec) = Just spec -- | Like splitForAllTys, but split only for tyvars. -- This always succeeds, even if it returns only an empty list. Note that the diff --git a/compiler/GHC/Core/UsageEnv.hs b/compiler/GHC/Core/UsageEnv.hs index a03343ee9f..867b9533f0 100644 --- a/compiler/GHC/Core/UsageEnv.hs +++ b/compiler/GHC/Core/UsageEnv.hs @@ -1,7 +1,7 @@ {-# LANGUAGE ViewPatterns #-} module GHC.Core.UsageEnv (UsageEnv, addUsage, scaleUsage, zeroUE, lookupUE, scaleUE, deleteUE, addUE, Usage(..), unitUE, - supUE, supUEs) where + bottomUE, supUE, supUEs) where import Data.Foldable import GHC.Prelude diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index d5ecbcbe45..e8954914e3 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -599,22 +599,13 @@ tcExpr (HsCase x scrut matches) res_ty tcExpr (HsIf x pred b1 b2) res_ty = do { pred' <- tcLExpr pred (mkCheckExpType boolTy) - ; res_ty <- tauifyExpType res_ty - -- Just like Note [Case branches must never infer a non-tau type] - -- in GHC.Tc.Gen.Match (See #10619) ; (u1,b1') <- tcCollectingUsage $ tcLExpr b1 res_ty ; (u2,b2') <- tcCollectingUsage $ tcLExpr b2 res_ty ; tcEmitBindingUsage (supUE u1 u2) ; return (HsIf x pred' b1' b2') } tcExpr (HsMultiIf _ alts) res_ty - = do { res_ty <- if isSingleton alts - then return res_ty - else tauifyExpType res_ty - -- Just like GHC.Tc.Gen.Match - -- Note [Case branches must never infer a non-tau type] - - ; alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts + = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts ; res_ty <- readExpType res_ty ; return (HsMultiIf res_ty alts') } where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody } diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index 39dae3bf95..ee428cbc42 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -164,80 +164,47 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (mkCheckExpType res_ty) match_ctxt = MC { mc_what = PatBindRhs, mc_body = tcBody } -{- -************************************************************************ +{- ********************************************************************* * * -\subsection{tcMatch} + tcMatch * * -************************************************************************ - -Note [Case branches must never infer a non-tau type] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - - case ... of - ... -> \(x :: forall a. a -> a) -> x - ... -> \y -> y - -Should that type-check? The problem is that, if we check the second branch -first, then we'll get a type (b -> b) for the branches, which won't unify -with the polytype in the first branch. If we check the first branch first, -then everything is OK. This order-dependency is terrible. So we want only -proper tau-types in branches (unless a sigma-type is pushed down). -This is what expTypeToType ensures: it replaces an Infer with a fresh -tau-type. - -An even trickier case looks like - - f x True = x undefined - f x False = x () - -Here, we see that the arguments must also be non-Infer. Thus, we must -use expTypeToType on the output of matchExpectedFunTys, not the input. - -But we make a special case for a one-branch case. This is so that - - f = \(x :: forall a. a -> a) -> x - -still gets assigned a polytype. --} +********************************************************************* -} --- | When the MatchGroup has multiple RHSs, convert an Infer ExpType in the --- expected type into TauTvs. --- See Note [Case branches must never infer a non-tau type] -tauifyMultipleMatches :: [LMatch id body] - -> [Scaled ExpType] -> TcM [Scaled ExpType] -tauifyMultipleMatches group exp_tys - | isSingletonMatchGroup group = return exp_tys - | otherwise = mapM (\(Scaled m t) -> - fmap (Scaled m) (tauifyExpType t)) exp_tys - -- NB: In the empty-match case, this ensures we fill in the ExpType +data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module + = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is + mc_body :: Located (body GhcRn) -- Type checker for a body of + -- an alternative + -> ExpRhoType + -> TcM (Located (body GhcTc)) } -- | Type-check a MatchGroup. tcMatches :: (Outputable (body GhcRn)) => TcMatchCtxt body -> [Scaled ExpSigmaType] -- Expected pattern types - -> ExpRhoType -- Expected result-type of the Match. + -> ExpRhoType -- Expected result-type of the Match. -> MatchGroup GhcRn (Located (body GhcRn)) -> TcM (MatchGroup GhcTc (Located (body GhcTc))) -data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module - = MC { mc_what :: HsMatchContext GhcRn, -- What kind of thing this is - mc_body :: Located (body GhcRn) -- Type checker for a body of - -- an alternative - -> ExpRhoType - -> TcM (Located (body GhcTc)) } tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches , mg_origin = origin }) - = do { (Scaled _ rhs_ty):pat_tys <- tauifyMultipleMatches matches ((Scaled One rhs_ty):pat_tys) -- return type has implicitly multiplicity 1, it doesn't matter all that much in this case since it isn't used and is eliminated immediately. - -- See Note [Case branches must never infer a non-tau type] + | null matches -- Deal with case e of {} + -- Since there are no branches, no one else will fill in rhs_ty + -- when in inference mode, so we must do it ourselves, + -- here, using expTypeToType + = do { tcEmitBindingUsage bottomUE + ; pat_tys <- mapM scaledExpTypeToType pat_tys + ; rhs_ty <- expTypeToType rhs_ty + ; return (MG { mg_alts = L l [] + , mg_ext = MatchGroupTc pat_tys rhs_ty + , mg_origin = origin }) } - ; umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches + | otherwise + = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches ; let (usages,matches') = unzip umatches ; tcEmitBindingUsage $ supUEs usages - ; pat_tys <- mapM (\(Scaled m t) -> fmap (Scaled m) (readExpType t)) pat_tys + ; pat_tys <- mapM readScaledExpType pat_tys ; rhs_ty <- readExpType rhs_ty - ; return (MG { mg_alts = L l matches' - , mg_ext = MatchGroupTc pat_tys rhs_ty + ; return (MG { mg_alts = L l matches' + , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } ------------- diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 181f87304e..c8d021a4fe 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -220,8 +220,9 @@ tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl = do { (co, bndr_ty) <- case scaledThing exp_pat_ty of Check pat_ty -> promoteTcType bind_lvl pat_ty Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res ) - -- If we were under a constructor that bumped - -- the level, we'd be in checking mode + -- If we were under a constructor that bumped the + -- level, we'd be in checking mode (see tcConArg) + -- hence this assertion do { bndr_ty <- inferResultToType infer_res ; return (mkTcNomReflCo bndr_ty, bndr_ty) } ; let bndr_mult = scaledMult exp_pat_ty @@ -629,10 +630,9 @@ There are two bits of rebindable syntax: lit1_ty and lit2_ty could conceivably be different. var_ty is the type inferred for x, the variable in the pattern. -If the pushed-down pattern type isn't a tau-type, the two pat_ty's above -could conceivably be different specializations. But this is very much -like the situation in Note [Case branches must be taus] in GHC.Tc.Gen.Match. -So we tauify the pat_ty before proceeding. +If the pushed-down pattern type isn't a tau-type, the two pat_ty's +above could conceivably be different specializations. So we use +expTypeToType on pat_ty before proceeding. Note that we need to type-check the literal twice, because it is used twice, and may be used at different types. The second HsOverLit stored in the diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index 89fcff3079..aee53733f4 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -36,7 +36,7 @@ import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType import GHC.Tc.Validity ( checkValidType ) import GHC.Tc.Utils.Unify( tcSkolemise, unifyType ) -import GHC.Tc.Utils.Instantiate( topInstantiate ) +import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs ) import GHC.Tc.Utils.Env( tcLookupId ) import GHC.Tc.Types.Evidence( HsWrapper, (<.>) ) import GHC.Core.Type ( mkTyVarBinders ) @@ -488,7 +488,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst -- Instantiate a type signature; only used with plan InferGen tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc }) = setSrcSpan loc $ -- Set the binding site of the tyvars - do { (tv_prs, theta, tau) <- tcInstTypeBndrs newMetaTyVarTyVars poly_id + do { (tv_prs, theta, tau) <- tcInstTypeBndrs poly_id -- See Note [Pattern bindings and complete signatures] ; return (TISI { sig_inst_sig = sig diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index 1df66632a2..5446a756a3 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -16,6 +16,7 @@ import GHC.Prelude import GHC.Tc.Utils.Env import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Instantiate( tcInstType ) import GHC.Tc.Instance.Typeable import GHC.Tc.Utils.TcMType import GHC.Tc.Types.Evidence diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs index 9be5c4675b..8a2c5b0e7a 100644 --- a/compiler/GHC/Tc/Instance/Family.hs +++ b/compiler/GHC/Tc/Instance/Family.hs @@ -21,6 +21,7 @@ import GHC.Core.Coercion import GHC.Tc.Types.Evidence import GHC.Iface.Load import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.Instantiate( freshenTyVarBndrs, freshenCoVarBndrsX ) import GHC.Types.SrcLoc as SrcLoc import GHC.Core.TyCon import GHC.Tc.Utils.TcType @@ -35,7 +36,6 @@ import GHC.Data.Maybe import GHC.Core.TyCo.Rep import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Ppr ( pprWithExplicitKindsWhen ) -import GHC.Tc.Utils.TcMType import GHC.Types.Name import GHC.Utils.Panic import GHC.Types.Var.Set diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs index fe9dcf72d9..4430e0e682 100644 --- a/compiler/GHC/Tc/TyCl/Class.hs +++ b/compiler/GHC/Tc/TyCl/Class.hs @@ -31,11 +31,12 @@ where import GHC.Prelude import GHC.Hs -import GHC.Tc.Utils.Env import GHC.Tc.Gen.Sig import GHC.Tc.Types.Evidence ( idHsWrapper ) import GHC.Tc.Gen.Bind +import GHC.Tc.Utils.Env import GHC.Tc.Utils.Unify +import GHC.Tc.Utils.Instantiate( tcSuperSkolTyVars ) import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType import GHC.Core.Type ( piResultTys ) diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index e72e5742a6..385cd634e8 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -16,6 +16,12 @@ module GHC.Tc.Utils.Instantiate ( instCall, instDFunType, instStupidTheta, instTyVarsWith, newWanted, newWanteds, + tcInstType, tcInstTypeBndrs, + tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt, + tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX, + + freshenTyVarBndrs, freshenCoVarBndrsX, + tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder, newOverloadedLit, mkOverLit, @@ -63,7 +69,7 @@ import GHC.Types.Id.Make( mkDictFunId ) import GHC.Core( Expr(..) ) -- For the Coercion constructor import GHC.Types.Id import GHC.Types.Name -import GHC.Types.Var ( EvVar, tyVarName, VarBndr(..) ) +import GHC.Types.Var import GHC.Core.DataCon import GHC.Types.Var.Env import GHC.Builtin.Names @@ -74,7 +80,7 @@ import GHC.Utils.Outputable import GHC.Types.Basic ( TypeOrKind(..) ) import qualified GHC.LanguageExtensions as LangExt -import Data.List ( sortBy ) +import Data.List ( sortBy, mapAccumL ) import Control.Monad( unless ) import Data.Function ( on ) @@ -451,15 +457,192 @@ mkEqBoxTy co ty1 ty2 mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co] where k = tcTypeKind ty1 -{- -************************************************************************ +{- ********************************************************************* * * - Literals + SkolemTvs (immutable) * * -************************************************************************ +********************************************************************* -} +tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) + -- ^ How to instantiate the type variables + -> Id -- ^ Type to instantiate + -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result + -- (type vars, preds (incl equalities), rho) +tcInstType inst_tyvars id + | null tyvars -- There may be overloading despite no type variables; + -- (?x :: Int) => Int -> Int + = return ([], theta, tau) + | otherwise + = do { (subst, tyvars') <- inst_tyvars tyvars + ; let tv_prs = map tyVarName tyvars `zip` tyvars' + subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho) + ; return (tv_prs, substTheta subst' theta, substTy subst' tau) } + where + (tyvars, rho) = tcSplitForAllTys (idType id) + (theta, tau) = tcSplitPhiTy rho + +tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType) + -- (type vars, preds (incl equalities), rho) +-- Instantiate the binders of a type signature with TyVarTvs +tcInstTypeBndrs id + | null tyvars -- There may be overloading despite no type variables; + -- (?x :: Int) => Int -> Int + = return ([], theta, tau) + | otherwise + = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars + ; let tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars' + subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho) + ; return (tv_prs, substTheta subst' theta, substTy subst' tau) } + where + (tyvars, rho) = splitForAllTysInvis (idType id) + (theta, tau) = tcSplitPhiTy rho + + inst_invis_bndr :: TCvSubst -> InvisTVBinder + -> TcM (TCvSubst, InvisTVBinder) + inst_invis_bndr subst (Bndr tv spec) + = do { (subst', tv') <- newMetaTyVarTyVarX subst tv + ; return (subst', Bndr tv' spec) } + +tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type signature with skolem constants. +-- We could give them fresh names, but no need to do so +tcSkolDFunType dfun + = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun + ; return (map snd tv_prs, theta, tau) } + +tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar]) +-- Make skolem constants, but do *not* give them new names, as above +-- Moreover, make them "super skolems"; see comments with superSkolemTv +-- see Note [Kind substitution when instantiating] +-- Precondition: tyvars should be ordered by scoping +tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst + +tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar) +tcSuperSkolTyVar subst tv + = (extendTvSubstWithClone subst tv new_tv, new_tv) + where + kind = substTyUnchecked subst (tyVarKind tv) + new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv + +-- | Given a list of @['TyVar']@, skolemize the type variables, +-- returning a substitution mapping the original tyvars to the +-- skolems, and the list of newly bound skolems. +tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) +-- See Note [Skolemising type variables] +tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst + +tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) +-- See Note [Skolemising type variables] +tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False + +tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) +-- See Note [Skolemising type variables] +tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst + +tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) +-- See Note [Skolemising type variables] +tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst + +tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar] + -> TcM (TCvSubst, [TcTyVar]) +-- Skolemise one level deeper, hence pushTcLevel +-- See Note [Skolemising type variables] +tcInstSkolTyVarsPushLevel overlappable subst tvs + = do { tc_lvl <- getTcLevel + ; let pushed_lvl = pushTcLevel tc_lvl + ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs } + +tcInstSkolTyVarsAt :: TcLevel -> Bool + -> TCvSubst -> [TyVar] + -> TcM (TCvSubst, [TcTyVar]) +tcInstSkolTyVarsAt lvl overlappable subst tvs + = freshenTyCoVarsX new_skol_tv subst tvs + where + details = SkolemTv lvl overlappable + new_skol_tv name kind = mkTcTyVar name kind details + +------------------ +freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar]) +-- ^ Give fresh uniques to a bunch of TyVars, but they stay +-- as TyVars, rather than becoming TcTyVars +-- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst' +freshenTyVarBndrs = freshenTyCoVars mkTyVar + +freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar]) +-- ^ Give fresh uniques to a bunch of CoVars +-- Used in "GHC.Tc.Instance.Family.newFamInst" +freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst + +------------------ +freshenTyCoVars :: (Name -> Kind -> TyCoVar) + -> [TyVar] -> TcM (TCvSubst, [TyCoVar]) +freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst + +freshenTyCoVarsX :: (Name -> Kind -> TyCoVar) + -> TCvSubst -> [TyCoVar] + -> TcM (TCvSubst, [TyCoVar]) +freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv) + +freshenTyCoVarX :: (Name -> Kind -> TyCoVar) + -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar) +-- This a complete freshening operation: +-- the skolems have a fresh unique, and a location from the monad +-- See Note [Skolemising type variables] +freshenTyCoVarX mk_tcv subst tycovar + = do { loc <- getSrcSpanM + ; uniq <- newUnique + ; let old_name = tyVarName tycovar + new_name = mkInternalName uniq (getOccName old_name) loc + new_kind = substTyUnchecked subst (tyVarKind tycovar) + new_tcv = mk_tcv new_name new_kind + subst1 = extendTCvSubstWithClone subst tycovar new_tcv + ; return (subst1, new_tcv) } + +{- Note [Skolemising type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The tcInstSkolTyVars family of functions instantiate a list of TyVars +to fresh skolem TcTyVars. Important notes: + +a) Level allocation. We generally skolemise /before/ calling + pushLevelAndCaptureConstraints. So we want their level to the level + of the soon-to-be-created implication, which has a level ONE HIGHER + than the current level. Hence the pushTcLevel. It feels like a + slight hack. + +b) The [TyVar] should be ordered (kind vars first) + See Note [Kind substitution when instantiating] + +c) It's a complete freshening operation: the skolems have a fresh + unique, and a location from the monad + +d) The resulting skolems are + non-overlappable for tcInstSkolTyVars, + but overlappable for tcInstSuperSkolTyVars + See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example + of where this matters. + +Note [Kind substitution when instantiating] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we instantiate a bunch of kind and type variables, first we +expect them to be topologically sorted. +Then we have to instantiate the kind variables, build a substitution +from old variables to the new variables, then instantiate the type +variables substituting the original kind. + +Exemple: If we want to instantiate + [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)] +we want + [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)] +instead of the bogus + [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)] -} +{- ********************************************************************* +* * + Literals +* * +********************************************************************* -} + {- In newOverloadedLit we convert directly to an Int or Integer if we know that's what we want. This may save some time, by not @@ -474,8 +657,6 @@ newOverloadedLit :: HsOverLit GhcRn newOverloadedLit lit@(OverLit { ol_val = val, ol_ext = rebindable }) res_ty | not rebindable - -- all built-in overloaded lits are tau-types, so we can just - -- tauify the ExpType = do { res_ty <- expTypeToType res_ty ; dflags <- getDynFlags ; let platform = targetPlatform dflags diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 34e4bfe0bb..e8ae500075 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -32,15 +32,6 @@ module GHC.Tc.Utils.TcMType ( isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- - -- Expected types - ExpType(..), ExpSigmaType, ExpRhoType, - mkCheckExpType, - newInferExpType, - readExpType, readExpType_maybe, - expTypeToType, checkingExpType_maybe, checkingExpType, - tauifyExpType, inferResultToType, - - -------------------------------- -- Creating new evidence variables newEvVar, newEvVars, newDict, newWanted, newWanteds, cloneWanted, cloneWC, @@ -58,14 +49,18 @@ module GHC.Tc.Utils.TcMType ( -------------------------------- -- Instantiation newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, - newMetaTyVarTyVars, newMetaTyVarTyVarX, + newMetaTyVarTyVarX, newTyVarTyVar, cloneTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX, - tcInstType, tcInstTypeBndrs, - tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt, - tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX, - freshenTyVarBndrs, freshenCoVarBndrsX, + -------------------------------- + -- Expected types + ExpType(..), ExpSigmaType, ExpRhoType, + mkCheckExpType, newInferExpType, tcInfer, + readExpType, readExpType_maybe, readScaledExpType, + expTypeToType, scaledExpTypeToType, + checkingExpType_maybe, checkingExpType, + inferResultToType, fillInferResult, promoteTcType, -------------------------------- -- Zonking and tidying @@ -99,6 +94,8 @@ module GHC.Tc.Utils.TcMType ( -- friends: import GHC.Prelude +import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType {- , unifyKind -} ) + import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr import GHC.Tc.Utils.TcType @@ -133,7 +130,6 @@ import GHC.Types.Basic ( TypeOrKind(..) ) import Control.Monad import GHC.Data.Maybe -import Data.List ( mapAccumL ) import Control.Arrow ( second ) import qualified Data.Semigroup as Semi @@ -387,16 +383,14 @@ checkCoercionHole cv co | otherwise = False -{- -************************************************************************ +{- ********************************************************************** * - Expected types + ExpType functions * -************************************************************************ - -Note [ExpType] -~~~~~~~~~~~~~~ +********************************************************************** -} +{- Note [ExpType] +~~~~~~~~~~~~~~~~~ An ExpType is used as the "expected type" when type-checking an expression. An ExpType can hold a "hole" that can be filled in by the type-checker. This allows us to have one tcExpr that works in both checking mode and @@ -426,14 +420,12 @@ Consider This is a classic untouchable-variable / ambiguous GADT return type scenario. But, with ExpTypes, we'll be inferring the type of the RHS. -And, because there is only one branch of the case, we won't trigger -Note [Case branches must never infer a non-tau type] of GHC.Tc.Gen.Match. We thus must track a TcLevel in an Inferring ExpType. If we try to -fill the ExpType and find that the TcLevels don't work out, we -fill the ExpType with a tau-tv at the low TcLevel, hopefully to -be worked out later by some means. This is triggered in -test gadt/gadt-escape1. +fill the ExpType and find that the TcLevels don't work out, we fill +the ExpType with a tau-tv at the low TcLevel, hopefully to be worked +out later by some means -- see fillInferResult, and Note [fillInferResult] +This behaviour triggered in test gadt/gadt-escape1. -} -- actual data definition is in GHC.Tc.Utils.TcType @@ -453,6 +445,12 @@ readExpType_maybe :: ExpType -> TcM (Maybe TcType) readExpType_maybe (Check ty) = return (Just ty) readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref +-- | Same as readExpType, but for Scaled ExpTypes +readScaledExpType :: Scaled ExpType -> TcM (Scaled Type) +readScaledExpType (Scaled m exp_ty) + = do { ty <- readExpType exp_ty + ; return (Scaled m ty) } + -- | Extract a type out of an ExpType. Otherwise, panics. readExpType :: ExpType -> TcM TcType readExpType exp_ty @@ -472,12 +470,10 @@ checkingExpType :: String -> ExpType -> TcType checkingExpType _ (Check ty) = ty checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et) -tauifyExpType :: ExpType -> TcM ExpType --- ^ Turn a (Infer hole) type into a (Check alpha), --- where alpha is a fresh unification variable -tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) -tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res - ; return (Check ty) } +scaledExpTypeToType :: Scaled ExpType -> TcM (Scaled TcType) +scaledExpTypeToType (Scaled m exp_ty) + = do { ty <- expTypeToType exp_ty + ; return (Scaled m ty) } -- | Extracts the expected type if there is one, or generates a new -- TauTv if there isn't. @@ -488,209 +484,279 @@ expTypeToType (Infer inf_res) = inferResultToType inf_res inferResultToType :: InferResult -> TcM Type inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl , ir_ref = ref }) - = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy - ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr) - -- See Note [TcLevel of ExpType] - ; writeMutVar ref (Just tau) + = do { mb_inferred_ty <- readTcRef ref + ; tau <- case mb_inferred_ty of + Just ty -> do { ensureMonoType ty + -- See Note [inferResultToType] + ; return ty } + Nothing -> do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy + ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr) + -- See Note [TcLevel of ExpType] + ; writeMutVar ref (Just tau) + ; return tau } ; traceTc "Forcing ExpType to be monomorphic:" (ppr u <+> text ":=" <+> ppr tau) ; return tau } +{- Note [inferResultToType] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +expTypeToType and inferResultType convert an InferResult to a monotype. +It must be a monotype because if the InferResult isn't already filled in, +we fill it in with a unification variable (hence monotype). So to preserve +order-independence we check for mono-type-ness even if it *is* filled in +already. + +See also Note [TcLevel of ExpType] above, and +Note [fillInferResult]. +-} + +-- | Infer a type using a fresh ExpType +-- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" +tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tcInfer tc_check + = do { res_ty <- newInferExpType + ; result <- tc_check res_ty + ; res_ty <- readExpType res_ty + ; return (result, res_ty) } + +fillInferResult :: TcType -> InferResult -> TcM TcCoercionN +-- If co = fillInferResult t1 t2 +-- => co :: t1 ~ t2 +-- See Note [fillInferResult] +fillInferResult act_res_ty (IR { ir_uniq = u, ir_lvl = res_lvl + , ir_ref = ref }) + = do { mb_exp_res_ty <- readTcRef ref + ; case mb_exp_res_ty of + Just exp_res_ty + -> do { traceTc "Joining inferred ExpType" $ + ppr u <> colon <+> ppr act_res_ty <+> char '~' <+> ppr exp_res_ty + ; cur_lvl <- getTcLevel + ; unless (cur_lvl `sameDepthAs` res_lvl) $ + ensureMonoType act_res_ty + ; unifyType Nothing act_res_ty exp_res_ty } + Nothing + -> do { traceTc "Filling inferred ExpType" $ + ppr u <+> text ":=" <+> ppr act_res_ty + ; (prom_co, act_res_ty) <- promoteTcType res_lvl act_res_ty + ; writeTcRef ref (Just act_res_ty) + ; return prom_co } + } + + +{- Note [fillInferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~ +When inferring, we use fillInferResult to "fill in" the hole in InferResult + data InferResult = IR { ir_uniq :: Unique + , ir_lvl :: TcLevel + , ir_ref :: IORef (Maybe TcType) } + +There are two things to worry about: + +1. What if it is under a GADT or existential pattern match? + - GADTs: a unification variable (and Infer's hole is similar) is untouchable + - Existentials: be careful about skolem-escape + +2. What if it is filled in more than once? E.g. multiple branches of a case + case e of + T1 -> e1 + T2 -> e2 + +Our typing rules are: + +* The RHS of a existential or GADT alternative must always be a + monotype, regardless of the number of alternatives. + +* Multiple non-existential/GADT branches can have (the same) + higher rank type (#18412). E.g. this is OK: + case e of + True -> hr + False -> hr + where hr:: (forall a. a->a) -> Int + c.f. Section 7.1 of "Practical type inference for arbitrary-rank types" + We use choice (2) in that Section. + (GHC 8.10 and earlier used choice (1).) + + But note that + case e of + True -> hr + False -> \x -> hr x + will fail, because we still /infer/ both branches, so the \x will get + a (monotype) unification variable, which will fail to unify with + (forall a. a->a) + +For (1) we can detect the GADT/existential situation by seeing that +the current TcLevel is greater than that stored in ir_lvl of the Infer +ExpType. We bump the level whenever we go past a GADT/existential match. + +Then, before filling the hole use promoteTcType to promote the type +to the outer ir_lvl. promoteTcType does this + - create a fresh unification variable alpha at level ir_lvl + - emits an equality alpha[ir_lvl] ~ ty + - fills the hole with alpha +That forces the type to be a monotype (since unification variables can +only unify with monotypes); and catches skolem-escapes because the +alpha is untouchable until the equality floats out. + +For (2), we simply look to see if the hole is filled already. + - if not, we promote (as above) and fill the hole + - if it is filled, we simply unify with the type that is + already there + +There is one wrinkle. Suppose we have + case e of + T1 -> e1 :: (forall a. a->a) -> Int + G2 -> e2 +where T1 is not GADT or existential, but G2 is a GADT. Then supppose the +T1 alternative fills the hole with (forall a. a->a) -> Int, which is fine. +But now the G2 alternative must not *just* unify with that else we'd risk +allowing through (e2 :: (forall a. a->a) -> Int). If we'd checked G2 first +we'd have filled the hole with a unification variable, which enforces a +monotype. + +So if we check G2 second, we still want to emit a constraint that restricts +the RHS to be a monotype. This is done by ensureMonoType, and it works +by simply generating a constraint (alpha ~ ty), where alpha is a fresh +unification variable. We discard the evidence. + +-} {- ********************************************************************* * * - SkolemTvs (immutable) + Promoting types * * ********************************************************************* -} -tc_inst_internal :: ([VarBndr TyVar flag] -> TcM (TCvSubst, [VarBndr TcTyVar flag])) - -- ^ How to instantiate the type variables - -> [VarBndr TyVar flag] -- ^ Type variable to instantiate - -> Type -- ^ rho - -> TcM ([(Name, VarBndr TcTyVar flag)], TcThetaType, TcType) -- ^ Result - -- (type vars, preds (incl equalities), rho) -tc_inst_internal _inst_tyvars [] rho = - let -- There may be overloading despite no type variables; - -- (?x :: Int) => Int -> Int - (theta, tau) = tcSplitPhiTy rho - in - return ([], theta, tau) -tc_inst_internal inst_tyvars tyvars rho = - do { (subst, tyvars') <- inst_tyvars tyvars - ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho) - tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars' - ; return (tv_prs, theta, tau) } - -tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) - -- ^ How to instantiate the type variables - -> Id -- ^ Type to instantiate - -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result - -- (type vars, preds (incl equalities), rho) -tcInstType inst_tyvars id = - do { let (tyvars, rho) = splitForAllTys (idType id) - tyvars' = mkTyVarBinders () tyvars - ; (tv_prs, preds, rho) <- tc_inst_internal inst_tyvar_bndrs tyvars' rho - ; let tv_prs' = map (\(name, bndr) -> (name, binderVar bndr)) tv_prs - ; return (tv_prs', preds, rho) } - where - inst_tyvar_bndrs :: [VarBndr TyVar ()] -> TcM (TCvSubst, [VarBndr TcTyVar ()]) - inst_tyvar_bndrs bndrs = do { (subst, tvs) <- inst_tyvars $ binderVars bndrs - ; let tvbnds = map (\tv -> Bndr tv ()) tvs - ; return (subst, tvbnds) } - -tcInstTypeBndrs :: ([VarBndr TyVar Specificity] -> TcM (TCvSubst, [VarBndr TcTyVar Specificity])) - -- ^ How to instantiate the type variables - -> Id -- ^ Type to instantiate - -> TcM ([(Name, VarBndr TcTyVar Specificity)], TcThetaType, TcType) -- ^ Result - -- (type vars, preds (incl equalities), rho) -tcInstTypeBndrs inst_tyvars id = - let (tyvars, rho) = splitForAllTysInvis (idType id) - in tc_inst_internal inst_tyvars tyvars rho - -tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type signature with skolem constants. --- We could give them fresh names, but no need to do so -tcSkolDFunType dfun - = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun - ; return (map snd tv_prs, theta, tau) } - -tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar]) --- Make skolem constants, but do *not* give them new names, as above --- Moreover, make them "super skolems"; see comments with superSkolemTv --- see Note [Kind substitution when instantiating] --- Precondition: tyvars should be ordered by scoping -tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst - -tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar) -tcSuperSkolTyVar subst tv - = (extendTvSubstWithClone subst tv new_tv, new_tv) - where - kind = substTyUnchecked subst (tyVarKind tv) - new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv - --- | Given a list of @['TyVar']@, skolemize the type variables, --- returning a substitution mapping the original tyvars to the --- skolems, and the list of newly bound skolems. -tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) --- See Note [Skolemising type variables] -tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst - -tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) --- See Note [Skolemising type variables] -tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False - -tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) --- See Note [Skolemising type variables] -tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst - -tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) --- See Note [Skolemising type variables] -tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst - -tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar] - -> TcM (TCvSubst, [TcTyVar]) --- Skolemise one level deeper, hence pushTcLevel --- See Note [Skolemising type variables] -tcInstSkolTyVarsPushLevel overlappable subst tvs - = do { tc_lvl <- getTcLevel - ; let pushed_lvl = pushTcLevel tc_lvl - ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs } - -tcInstSkolTyVarsAt :: TcLevel -> Bool - -> TCvSubst -> [TyVar] - -> TcM (TCvSubst, [TcTyVar]) -tcInstSkolTyVarsAt lvl overlappable subst tvs - = freshenTyCoVarsX new_skol_tv subst tvs +ensureMonoType :: TcType -> TcM () +-- Assuming that the argument type is of kind (TYPE r), +-- ensure that it is a /monotype/ +-- If it is not a monotype we can see right away (since unification +-- varibles and type-function applications stand for monotypes), but +-- we emit a Wanted equality just to delay the error message until later +ensureMonoType res_ty + | isTauTy res_ty -- isTauTy doesn't need zonking or anything + = return () + | otherwise + = do { mono_ty <- newOpenFlexiTyVarTy + ; let eq_orig = TypeEqOrigin { uo_actual = res_ty + , uo_expected = mono_ty + , uo_thing = Nothing + , uo_visible = False } + + ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty + ; return () } + +promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType) +-- See Note [Promoting a type] +-- See also Note [fillInferResult] +-- promoteTcType level ty = (co, ty') +-- * Returns ty' whose max level is just 'level' +-- and whose kind is ~# to the kind of 'ty' +-- and whose kind has form TYPE rr +-- * and co :: ty ~ ty' +-- * and emits constraints to justify the coercion +-- +-- NB: we expect that 'ty' has already kind (TYPE rr) for +-- some rr::RuntimeRep. It is, after all, the type of a term. +promoteTcType dest_lvl ty + = do { cur_lvl <- getTcLevel + ; if (cur_lvl `sameDepthAs` dest_lvl) + then return (mkTcNomReflCo ty, ty) + else promote_it } where - details = SkolemTv lvl overlappable - new_skol_tv name kind = mkTcTyVar name kind details - ------------------- -freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar]) --- ^ Give fresh uniques to a bunch of TyVars, but they stay --- as TyVars, rather than becoming TcTyVars --- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst' -freshenTyVarBndrs = freshenTyCoVars mkTyVar - -freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar]) --- ^ Give fresh uniques to a bunch of CoVars --- Used in "GHC.Tc.Instance.Family.newFamInst" -freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst - ------------------- -freshenTyCoVars :: (Name -> Kind -> TyCoVar) - -> [TyVar] -> TcM (TCvSubst, [TyCoVar]) -freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst - -freshenTyCoVarsX :: (Name -> Kind -> TyCoVar) - -> TCvSubst -> [TyCoVar] - -> TcM (TCvSubst, [TyCoVar]) -freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv) - -freshenTyCoVarX :: (Name -> Kind -> TyCoVar) - -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar) --- This a complete freshening operation: --- the skolems have a fresh unique, and a location from the monad --- See Note [Skolemising type variables] -freshenTyCoVarX mk_tcv subst tycovar - = do { loc <- getSrcSpanM - ; uniq <- newUnique - ; let old_name = tyVarName tycovar - new_name = mkInternalName uniq (getOccName old_name) loc - new_kind = substTyUnchecked subst (tyVarKind tycovar) - new_tcv = mk_tcv new_name new_kind - subst1 = extendTCvSubstWithClone subst tycovar new_tcv - ; return (subst1, new_tcv) } - -{- Note [Skolemising type variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The tcInstSkolTyVars family of functions instantiate a list of TyVars -to fresh skolem TcTyVars. Important notes: - -a) Level allocation. We generally skolemise /before/ calling - pushLevelAndCaptureConstraints. So we want their level to the level - of the soon-to-be-created implication, which has a level ONE HIGHER - than the current level. Hence the pushTcLevel. It feels like a - slight hack. - -b) The [TyVar] should be ordered (kind vars first) - See Note [Kind substitution when instantiating] - -c) It's a complete freshening operation: the skolems have a fresh - unique, and a location from the monad - -d) The resulting skolems are - non-overlappable for tcInstSkolTyVars, - but overlappable for tcInstSuperSkolTyVars - See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example - of where this matters. - -Note [Kind substitution when instantiating] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we instantiate a bunch of kind and type variables, first we -expect them to be topologically sorted. -Then we have to instantiate the kind variables, build a substitution -from old variables to the new variables, then instantiate the type -variables substituting the original kind. - -Exemple: If we want to instantiate - [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)] -we want - [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)] -instead of the buggous - [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)] + promote_it :: TcM (TcCoercion, TcType) + promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty + -- where alpha and rr are fresh and from level dest_lvl + = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy + ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr) + ; let eq_orig = TypeEqOrigin { uo_actual = ty + , uo_expected = prom_ty + , uo_thing = Nothing + , uo_visible = False } + + ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty + ; return (co, prom_ty) } + +{- Note [Promoting a type] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#12427) + + data T where + MkT :: (Int -> Int) -> a -> T + + h y = case y of MkT v w -> v + +We'll infer the RHS type with an expected type ExpType of + (IR { ir_lvl = l, ir_ref = ref, ... ) +where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern +match will increase the level, so we'll end up in tcSubType, trying to +unify the type of v, + v :: Int -> Int +with the expected type. But this attempt takes place at level (l+1), +rightly so, since v's type could have mentioned existential variables, +(like w's does) and we want to catch that. + +So we + - create a new meta-var alpha[l+1] + - fill in the InferRes ref cell 'ref' with alpha + - emit an equality constraint, thus + [W] alpha[l+1] ~ (Int -> Int) + +That constraint will float outwards, as it should, unless v's +type mentions a skolem-captured variable. + +This approach fails if v has a higher rank type; see +Note [Promotion and higher rank types] + + +Note [Promotion and higher rank types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If v had a higher-rank type, say v :: (forall a. a->a) -> Int, +then we'd emit an equality + [W] alpha[l+1] ~ ((forall a. a->a) -> Int) +which will sadly fail because we can't unify a unification variable +with a polytype. But there is nothing really wrong with the program +here. + +We could just about solve this by "promote the type" of v, to expose +its polymorphic "shape" while still leaving constraints that will +prevent existential escape. But we must be careful! Exposing +the "shape" of the type is precisely what we must NOT do under +a GADT pattern match! So in this case we might promote the type +to + (forall a. a->a) -> alpha[l+1] +and emit the constraint + [W] alpha[l+1] ~ Int +Now the promoted type can fill the ref cell, while the emitted +equality can float or not, according to the usual rules. + +But that's not quite right! We are exposing the arrow! We could +deal with that too: + (forall a. mu[l+1] a a) -> alpha[l+1] +with constraints + [W] alpha[l+1] ~ Int + [W] mu[l+1] ~ (->) +Here we abstract over the '->' inside the forall, in case that +is subject to an equality constraint from a GADT match. + +Note that we kept the outer (->) because that's part of +the polymorphic "shape". And because of impredicativity, +GADT matches can't give equalities that affect polymorphic +shape. + +This reasoning just seems too complicated, so I decided not +to do it. These higher-rank notes are just here to record +the thinking. +-} -************************************************************************ +{- ********************************************************************* * * MetaTvs (meta type variables; mutable) * * -************************************************************************ --} +********************************************************************* -} -{- -Note [TyVarTv] -~~~~~~~~~~~~ +{- Note [TyVarTv] +~~~~~~~~~~~~~~~~~ A TyVarTv can unify with type *variables* only, including other TyVarTvs and skolems. Sometimes, they can unify with type variables that the user would @@ -1031,18 +1097,11 @@ newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) -- Make a new unification variable tyvar whose Name and Kind come from -- an existing TyVar. We substitute kind variables in the kind. -newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar - -newMetaTyVarTyVars :: [VarBndr TyVar Specificity] - -> TcM (TCvSubst, [VarBndr TcTyVar Specificity]) -newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst +newMetaTyVarX = new_meta_tv_x TauTv -newMetaTyVarTyVarX :: TCvSubst -> (VarBndr TyVar Specificity) - -> TcM (TCvSubst, VarBndr TcTyVar Specificity) +newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) -- Just like newMetaTyVarX, but make a TyVarTv -newMetaTyVarTyVarX subst (Bndr tv spec) = - do { (subst', tv') <- new_meta_tv_x TyVarTv subst tv - ; return (subst', (Bndr tv' spec)) } +newMetaTyVarTyVarX = new_meta_tv_x TyVarTv newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) newWildCardX subst tv diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 280144ac00..6b0df55f46 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -57,7 +57,7 @@ module GHC.Tc.Utils.TcType ( -- These are important because they do not look through newtypes getTyVar, tcSplitForAllTy_maybe, - tcSplitForAllTys, tcSplitSomeForAllTys, + tcSplitForAllTys, tcSplitForAllTysReq, tcSplitForAllTysInvis, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, tcSplitPhiTy, tcSplitPredFunTy_maybe, @@ -1221,14 +1221,6 @@ tcSplitForAllTys ty = ASSERT( all isTyVar (fst sty) ) sty where sty = splitForAllTys ty --- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@ --- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and --- @argf_pred@ is a predicate over visibilities provided as an argument to this --- function. All split tyvars are annotated with their @argf@. -tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyCoVarBinder], Type) -tcSplitSomeForAllTys argf_pred ty = ASSERT( all (isTyVar . binderVar) (fst sty) ) sty - where sty = splitSomeForAllTys argf_pred ty - -- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type -- variable binders. All split tyvars are annotated with '()'. tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type) diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 5d7afcf057..145520045b 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -61,7 +61,6 @@ import GHC.Types.Name( isSystemName ) import GHC.Tc.Utils.Instantiate import GHC.Core.TyCon import GHC.Builtin.Types -import GHC.Builtin.Types.Prim( tYPE ) import GHC.Types.Var as Var import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -571,10 +570,51 @@ tcSubTypeNC :: CtOrigin -- Used when instantiating -> TcM HsWrapper tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty = case res_ty of - Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res 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] + ; co <- fillInferResult rho inf_res + ; return (mkWpCastN co <.> wrap) } + +{- Note [Instantiation of InferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We now always instantiate before filling in InferResult, so that +the result is a TcRhoType: see #17173 for discussion. + +For example: + +1. Consider + f x = (*) + We want to instantiate the type of (*) before returning, else we + will infer the type + f :: forall {a}. a -> forall b. Num b => b -> b -> b + This is surely confusing for users. + + And worse, the monomorphism restriction won't work properly. The MR is + dealt with in simplifyInfer, and simplifyInfer has no way of + instantiating. This could perhaps be worked around, but it may be + hard to know even when instantiation should happen. + +2. Another reason. Consider + f :: (?x :: Int) => a -> a + g y = let ?x = 3::Int in f + Here want to instantiate f's type so that the ?x::Int constraint + gets discharged by the enclosing implicit-parameter binding. + +3. Suppose one defines plus = (+). If we instantiate lazily, we will + infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism + restriction compels us to infer + plus :: Integer -> Integer -> Integer + (or similar monotype). Indeed, the only way to know whether to apply + the monomorphism restriction at all is to instantiate + +There is one place where we don't want to instantiate eagerly, +namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type +command. See Note [Implementing :type] in GHC.Tc.Module. +-} + --------------- tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- External entry point, but no ExpTypes on either side @@ -768,213 +808,6 @@ tcEqMult origin w_actual w_expected = do ; coercion <- uType TypeLevel origin w_actual w_expected ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion } -{- ********************************************************************** -%* * - ExpType functions: tcInfer, instantiateAndFillInferResult -%* * -%********************************************************************* -} - --- | Infer a type using a fresh ExpType --- See also Note [ExpType] in "GHC.Tc.Utils.TcMType" -tcInfer :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) -tcInfer tc_check - = do { res_ty <- newInferExpType - ; result <- tc_check res_ty - ; res_ty <- readExpType res_ty - ; return (result, res_ty) } - -instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper --- If wrap = instantiateAndFillInferResult t1 t2 --- => wrap :: t1 ~> t2 --- See Note [Instantiation of InferResult] -instantiateAndFillInferResult orig ty inf_res - = do { (wrap, rho) <- topInstantiate orig ty - ; co <- fillInferResult rho inf_res - ; return (mkWpCastN co <.> wrap) } - -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN --- If wrap = fillInferResult t1 t2 --- => wrap :: t1 ~> t2 -fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl - , ir_ref = ref }) - = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty - - ; traceTc "Filling ExpType" $ - ppr u <+> text ":=" <+> ppr ty_to_fill_with - - ; when debugIsOn (check_hole ty_to_fill_with) - - ; writeTcRef ref (Just ty_to_fill_with) - - ; return ty_co } - where - check_hole ty -- Debug check only - = do { let ty_lvl = tcTypeLevel ty - ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), - ppr u $$ ppr res_lvl $$ ppr ty_lvl $$ - ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty ) - ; cts <- readTcRef ref - ; case cts of - Just already_there -> pprPanic "writeExpType" - (vcat [ ppr u - , ppr ty - , ppr already_there ]) - Nothing -> return () } - -{- Note [Instantiation of InferResult] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We now always instantiate before filling in InferResult, so that -the result is a TcRhoType: see #17173 for discussion. - -For example: - -1. Consider - f x = (*) - We want to instantiate the type of (*) before returning, else we - will infer the type - f :: forall {a}. a -> forall b. Num b => b -> b -> b - This is surely confusing for users. - - And worse, the monomorphism restriction won't work properly. The MR is - dealt with in simplifyInfer, and simplifyInfer has no way of - instantiating. This could perhaps be worked around, but it may be - hard to know even when instantiation should happen. - -2. Another reason. Consider - f :: (?x :: Int) => a -> a - g y = let ?x = 3::Int in f - Here want to instantiate f's type so that the ?x::Int constraint - gets discharged by the enclosing implicit-parameter binding. - -3. Suppose one defines plus = (+). If we instantiate lazily, we will - infer plus :: forall a. Num a => a -> a -> a. However, the monomorphism - restriction compels us to infer - plus :: Integer -> Integer -> Integer - (or similar monotype). Indeed, the only way to know whether to apply - the monomorphism restriction at all is to instantiate - -There is one place where we don't want to instantiate eagerly, -namely in GHC.Tc.Module.tcRnExpr, which implements GHCi's :type -command. See Note [Implementing :type] in GHC.Tc.Module. - --} - -{- ********************************************************************* -* * - Promoting types -* * -********************************************************************* -} - -promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType) --- See Note [Promoting a type] --- promoteTcType level ty = (co, ty') --- * Returns ty' whose max level is just 'level' --- and whose kind is ~# to the kind of 'ty' --- and whose kind has form TYPE rr --- * and co :: ty ~ ty' --- * and emits constraints to justify the coercion -promoteTcType dest_lvl ty - = do { cur_lvl <- getTcLevel - ; if (cur_lvl `sameDepthAs` dest_lvl) - then dont_promote_it - else promote_it } - where - promote_it :: TcM (TcCoercion, TcType) - promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty - -- where alpha and rr are fresh and from level dest_lvl - = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy - ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr) - ; let eq_orig = TypeEqOrigin { uo_actual = ty - , uo_expected = prom_ty - , uo_thing = Nothing - , uo_visible = False } - - ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty - ; return (co, prom_ty) } - - dont_promote_it :: TcM (TcCoercion, TcType) - dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr - = do { res_kind <- newOpenTypeKind - ; let ty_kind = tcTypeKind ty - kind_orig = TypeEqOrigin { uo_actual = ty_kind - , uo_expected = res_kind - , uo_thing = Nothing - , uo_visible = False } - ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind - ; let co = mkTcGReflRightCo Nominal ty ki_co - ; return (co, ty `mkCastTy` ki_co) } - -{- Note [Promoting a type] -~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider (#12427) - - data T where - MkT :: (Int -> Int) -> a -> T - - h y = case y of MkT v w -> v - -We'll infer the RHS type with an expected type ExpType of - (IR { ir_lvl = l, ir_ref = ref, ... ) -where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern -match will increase the level, so we'll end up in tcSubType, trying to -unify the type of v, - v :: Int -> Int -with the expected type. But this attempt takes place at level (l+1), -rightly so, since v's type could have mentioned existential variables, -(like w's does) and we want to catch that. - -So we - - create a new meta-var alpha[l+1] - - fill in the InferRes ref cell 'ref' with alpha - - emit an equality constraint, thus - [W] alpha[l+1] ~ (Int -> Int) - -That constraint will float outwards, as it should, unless v's -type mentions a skolem-captured variable. - -This approach fails if v has a higher rank type; see -Note [Promotion and higher rank types] - - -Note [Promotion and higher rank types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If v had a higher-rank type, say v :: (forall a. a->a) -> Int, -then we'd emit an equality - [W] alpha[l+1] ~ ((forall a. a->a) -> Int) -which will sadly fail because we can't unify a unification variable -with a polytype. But there is nothing really wrong with the program -here. - -We could just about solve this by "promote the type" of v, to expose -its polymorphic "shape" while still leaving constraints that will -prevent existential escape. But we must be careful! Exposing -the "shape" of the type is precisely what we must NOT do under -a GADT pattern match! So in this case we might promote the type -to - (forall a. a->a) -> alpha[l+1] -and emit the constraint - [W] alpha[l+1] ~ Int -Now the promoted type can fill the ref cell, while the emitted -equality can float or not, according to the usual rules. - -But that's not quite right! We are exposing the arrow! We could -deal with that too: - (forall a. mu[l+1] a a) -> alpha[l+1] -with constraints - [W] alpha[l+1] ~ Int - [W] mu[l+1] ~ (->) -Here we abstract over the '->' inside the forall, in case that -is subject to an equality constraint from a GADT match. - -Note that we kept the outer (->) because that's part of -the polymorphic "shape". And because of impredicativity, -GADT matches can't give equalities that affect polymorphic -shape. - -This reasoning just seems too complicated, so I decided not -to do it. These higher-rank notes are just here to record -the thinking. --} {- ********************************************************************* * * diff --git a/testsuite/tests/simplCore/should_compile/T17901.stdout b/testsuite/tests/simplCore/should_compile/T17901.stdout index 99969cc0c1..7a09f6e2df 100644 --- a/testsuite/tests/simplCore/should_compile/T17901.stdout +++ b/testsuite/tests/simplCore/should_compile/T17901.stdout @@ -1,14 +1,14 @@ - (wombat1 [Occ=Once*!] :: T -> p) + (wombat1 [Occ=Once*!] :: T -> t) A -> wombat1 T17901.A; B -> wombat1 T17901.B; C -> wombat1 T17901.C - = \ (@p) (wombat1 :: T -> p) (x :: T) -> + = \ (@t) (wombat1 :: T -> t) (x :: T) -> case x of wild { __DEFAULT -> wombat1 wild } - Tmpl= \ (@p) (wombat2 [Occ=Once!] :: S -> p) (x [Occ=Once] :: S) -> + Tmpl= \ (@t) (wombat2 [Occ=Once!] :: S -> t) (x [Occ=Once] :: S) -> case x of wild [Occ=Once] { __DEFAULT -> wombat2 wild }}] - = \ (@p) (wombat2 :: S -> p) (x :: S) -> + = \ (@t) (wombat2 :: S -> t) (x :: S) -> case x of wild { __DEFAULT -> wombat2 wild } - Tmpl= \ (@p) (wombat3 [Occ=Once!] :: W -> p) (x [Occ=Once] :: W) -> + Tmpl= \ (@t) (wombat3 [Occ=Once!] :: W -> t) (x [Occ=Once] :: W) -> case x of wild [Occ=Once] { __DEFAULT -> wombat3 wild }}] - = \ (@p) (wombat3 :: W -> p) (x :: W) -> + = \ (@t) (wombat3 :: W -> t) (x :: W) -> case x of wild { __DEFAULT -> wombat3 wild } diff --git a/testsuite/tests/typecheck/should_compile/T18412.hs b/testsuite/tests/typecheck/should_compile/T18412.hs new file mode 100644 index 0000000000..67fc5cc1db --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T18412.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE RankNTypes #-} + +module T18412 where + +hr :: (forall a. a -> a) -> () +hr _ = () + +foo x = case x of () -> hr + +-- This did not use to be allowed, because the +-- multiple branches have (the same) polytypes +-- Enhancement July 2020 +bar x = case x of True -> hr + False -> hr diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 1ace8dbc15..82a30f50f4 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -716,3 +716,4 @@ test('T17775-viewpats-a', normal, compile, ['']) test('T17775-viewpats-b', normal, compile_fail, ['']) test('T17775-viewpats-c', normal, compile_fail, ['']) test('T17775-viewpats-d', normal, compile_fail, ['']) +test('T18412', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr index 481a08a20c..c26e550f17 100644 --- a/testsuite/tests/typecheck/should_fail/T10619.stderr +++ b/testsuite/tests/typecheck/should_fail/T10619.stderr @@ -1,13 +1,11 @@ -T10619.hs:9:15: error: - • Couldn't match type ‘p’ with ‘forall b. b -> b’ - Expected: p -> p - Actual: (forall a. a -> a) -> forall b. b -> b - ‘p’ is a rigid type variable bound by - the inferred type of foo :: p1 -> p -> p - at T10619.hs:(8,1)-(10,20) - • In the expression: - (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b +T10619.hs:10:14: error: + • Couldn't match type ‘p1’ with ‘forall a. a -> a’ + Expected: (forall a. a -> a) -> forall b. b -> b + Actual: p1 -> p1 + Cannot instantiate unification variable ‘p1’ + with a type involving polytypes: forall a. a -> a + • In the expression: \ y -> y In the expression: if True then ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b) @@ -19,15 +17,13 @@ T10619.hs:9:15: error: ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b) else \ y -> y - • Relevant bindings include - foo :: p1 -> p -> p (bound at T10619.hs:8:1) T10619.hs:14:15: error: • Couldn't match type ‘p’ with ‘forall a. a -> a’ Expected: p -> p Actual: (forall a. a -> a) -> forall b. b -> b ‘p’ is a rigid type variable bound by - the inferred type of bar :: p1 -> p -> p + the inferred type of bar :: p2 -> p -> p at T10619.hs:(12,1)-(14,66) • In the expression: (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b @@ -43,21 +39,16 @@ T10619.hs:14:15: error: else ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b) • Relevant bindings include - bar :: p1 -> p -> p (bound at T10619.hs:12:1) + bar :: p2 -> p -> p (bound at T10619.hs:12:1) -T10619.hs:16:13: error: - • Couldn't match type ‘p’ with ‘forall b. b -> b’ - Expected: p -> p - Actual: (forall a. a -> a) -> forall b. b -> b - ‘p’ is a rigid type variable bound by - the inferred type of baz :: Bool -> p -> p - at T10619.hs:(16,1)-(17,19) - • In the expression: - (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b - In an equation for ‘baz’: - baz True = (\ x -> x) :: (forall a. a -> a) -> forall b. b -> b - • Relevant bindings include - baz :: Bool -> p -> p (bound at T10619.hs:16:1) +T10619.hs:17:13: error: + • Couldn't match type ‘p0’ with ‘forall a. a -> a’ + Expected: (forall a. a -> a) -> forall b. b -> b + Actual: p0 -> p0 + Cannot instantiate unification variable ‘p0’ + with a type involving polytypes: forall a. a -> a + • In the expression: \ y -> y + In an equation for ‘baz’: baz False = \ y -> y T10619.hs:20:14: error: • Couldn't match type ‘p’ with ‘forall a. a -> a’ diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr index 87a2bea3fe..1b496b8380 100644 --- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr +++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr @@ -7,7 +7,7 @@ VtaFail.hs:7:16: error: answer_nosig = pairup_nosig @Int @Bool 5 True VtaFail.hs:14:17: error: - • Cannot apply expression of type ‘p0 -> p0’ + • Cannot apply expression of type ‘p1 -> p1’ to a visible type argument ‘Int’ • In the expression: (\ x -> x) @Int 12 In an equation for ‘answer_lambda’: diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr index 664c910533..7de2d04c08 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr @@ -1,8 +1,8 @@ tcfail002.hs:4:7: error: - • Couldn't match expected type ‘p’ with actual type ‘[p]’ + • Couldn't match expected type ‘a’ with actual type ‘[a]’ • In the expression: z In an equation for ‘c’: c z = z • Relevant bindings include - z :: [p] (bound at tcfail002.hs:4:3) - c :: [p] -> p (bound at tcfail002.hs:3:1) + z :: [a] (bound at tcfail002.hs:4:3) + c :: [a] -> a (bound at tcfail002.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr index 9844b53268..0d9b338216 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr @@ -1,19 +1,22 @@ -tcfail104.hs:14:12: error: +tcfail104.hs:16:12: error: + • Couldn't match type: Char -> Char + with: forall a. a -> a + Expected: (forall a. a -> a) -> Char -> Char + Actual: (Char -> Char) -> Char -> Char + • In the expression: \ x -> x + In the expression: + if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x) + In the expression: + (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c' + +tcfail104.hs:22:12: error: • Couldn't match type: forall a. a -> a with: Char -> Char Expected: (Char -> Char) -> Char -> Char Actual: (forall a. a -> a) -> Char -> Char • In the expression: \ (x :: forall a. a -> a) -> x In the expression: - if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x) + if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x) In the expression: - (if v then (\ (x :: forall a. a -> a) -> x) else (\ x -> x)) id 'c' - -tcfail104.hs:22:15: error: - • Couldn't match expected type: Char -> Char - with actual type: forall a. a -> a - • When checking that the pattern signature: forall a. a -> a - fits the type of its context: Char -> Char - In the pattern: x :: forall a. a -> a - In the expression: \ (x :: forall a. a -> a) -> x + (if v then (\ x -> x) else (\ (x :: forall a. a -> a) -> x)) id 'c' |