diff options
79 files changed, 1322 insertions, 859 deletions
diff --git a/compiler/ghci/RtClosureInspect.hs b/compiler/ghci/RtClosureInspect.hs index 9f671f21dc..eff266090e 100644 --- a/compiler/ghci/RtClosureInspect.hs +++ b/compiler/ghci/RtClosureInspect.hs @@ -1218,7 +1218,7 @@ zonkRttiType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_meta) where zonk_unbound_meta tv = ASSERT( isTcTyVar tv ) - do { tv' <- skolemiseUnboundMetaTyVar tv RuntimeUnk + do { tv' <- skolemiseRuntimeUnk tv -- This is where RuntimeUnks are born: -- otherwise-unconstrained unification variables are -- turned into RuntimeUnks as they leave the diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index f2d3ef014d..e5b802063b 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -225,7 +225,7 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- if deeplyInstantiate ty = (wrap, rho) -- and e :: ty -- then wrap e :: rho --- That is, wrap :: ty "->" rho +-- That is, wrap :: ty ~> rho deeplyInstantiate orig ty | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty @@ -381,7 +381,7 @@ tcInstBinderX _ subst (Anon ty) -- This is the *only* constraint currently handled in types. | Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty = do { let origin = TypeEqOrigin { uo_actual = k1 - , uo_expected = mkCheckExpType k2 + , uo_expected = k2 , uo_thing = Nothing } ; co <- case role of Nominal -> unifyKind noThing k1 k2 diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 8fba643433..09746d3cba 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -33,7 +33,6 @@ import TcEvidence import TcHsType import TcPat import TcMType -import Inst( deeplyInstantiate ) import FamInstEnv( normaliseType ) import FamInst( tcGetFamInstEnvs ) import TyCon @@ -741,7 +740,7 @@ mkExport prag_fn qtvs theta -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int else addErrCtxtM (mk_impedence_match_msg mono_info sel_poly_ty poly_ty) $ - tcSubType_NC sig_ctxt sel_poly_ty (mkCheckExpType poly_ty) + tcSubType_NC sig_ctxt sel_poly_ty poly_ty ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures ; when warn_missing_sigs $ @@ -1117,58 +1116,6 @@ for a non-overloaded function. @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds. The signatures have been dealt with already. - -Note [Pattern bindings] -~~~~~~~~~~~~~~~~~~~~~~~ -The rule for typing pattern bindings is this: - - ..sigs.. - p = e - -where 'p' binds v1..vn, and 'e' may mention v1..vn, -typechecks exactly like - - ..sigs.. - x = e -- Inferred type - v1 = case x of p -> v1 - .. - vn = case x of p -> vn - -Note that - (f :: forall a. a -> a) = id -should not typecheck because - case id of { (f :: forall a. a->a) -> f } -will not typecheck. - -Note [Instantiate when inferring a type] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f = (*) -As there is no incentive to instantiate the RHS, tcMonoBinds will -produce a type of forall a. Num a => a -> a -> a for `f`. This will then go -through simplifyInfer and such, remaining unchanged. - -There are two problems with this: - 1) If the definition were `g _ = (*)`, we get a very unusual type of - `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is - surely confusing for users. - - 2) The monomorphism restriction can't work. 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. - -There is an easy solution to both problems: instantiate (deeply) when -inferring a type. So that's what we do. Note that this decision is -user-facing. - -We do this deep instantiation in tcMonoBinds, in the FunBind case -only, and only when we do not have a type signature. Conveniently, -the fun_co_fn field of FunBind gives a place to record the coercion. - -We do not need to do this - * for PatBinds, because we don't have a function type - * for FunBinds where we have a signature, bucause we aren't doing inference -} data MonoBindInfo = MBI { mbi_poly_name :: Name @@ -1193,27 +1140,21 @@ tcMonoBinds is_rec sig_fn no_gen -- e.g. f = \(x::forall a. a->a) -> <body> -- We want to infer a higher-rank type for f setSrcSpan b_loc $ - do { rhs_ty <- newOpenInferExpType - ; (co_fn, matches') - <- tcExtendIdBndrs [TcIdBndr_ExpType name rhs_ty NotTopLevel] $ + do { ((co_fn, matches'), rhs_ty) + <- tcInferInst $ \ exp_ty -> + -- tcInferInst: see TcUnify, + -- Note [Deep instantiation of InferResult] + tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $ -- We extend the error context even for a non-recursive -- function so that in type error messages we show the -- type of the thing whose rhs we are type checking - tcMatchesFun (L nm_loc name) matches rhs_ty - ; rhs_ty <- readExpType rhs_ty - - -- Deeply instantiate the inferred type - -- See Note [Instantiate when inferring a type] - ; let orig = matchesCtOrigin matches - ; rhs_ty <- zonkTcType rhs_ty -- NB: zonk to uncover any foralls - ; (inst_wrap, rhs_ty) <- addErrCtxtM (instErrCtxt name rhs_ty) $ - deeplyInstantiate orig rhs_ty + tcMatchesFun (L nm_loc name) matches exp_ty ; mono_id <- newLetBndr no_gen name rhs_ty ; return (unitBag $ L b_loc $ FunBind { fun_id = L nm_loc mono_id, fun_matches = matches', bind_fvs = fvs, - fun_co_fn = inst_wrap <.> co_fn, fun_tick = [] }, + fun_co_fn = co_fn, fun_tick = [] }, [MBI { mbi_poly_name = name , mbi_sig = Nothing , mbi_mono_id = mono_id }]) } @@ -1297,7 +1238,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) -- See Note [Existentials in pattern bindings] ; ((pat', nosig_mbis), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ - tcInferInst $ \ exp_ty -> + tcInferNoInst $ \ exp_ty -> tcLetPat inst_sig_fun no_gen pat exp_ty $ mapM lookup_info nosig_names @@ -1761,16 +1702,3 @@ patMonoBindsCtxt :: (OutputableBndrId id, Outputable body) patMonoBindsCtxt pat grhss = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss) -instErrCtxt :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) -instErrCtxt name ty env - = do { let (env', ty') = tidyOpenType env ty - ; return (env', hang (text "When instantiating" <+> quotes (ppr name) <> - text ", initially inferred to have" $$ - text "this overly-general type:") - 2 (ppr ty') $$ - extra) } - where - extra = sdocWithDynFlags $ \dflags -> - ppWhen (xopt LangExt.MonomorphismRestriction dflags) $ - text "NB: This instantiation can be caused by the" <+> - text "monomorphism restriction." diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index f82fc47692..7cf688d2b6 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -142,9 +142,11 @@ reportUnsolved wanted | warn_out_of_scope = HoleWarn | otherwise = HoleDefer - ; report_unsolved (Just binds_var) False type_errors expr_holes + ; report_unsolved binds_var False type_errors expr_holes type_holes out_of_scope_holes wanted - ; getTcEvBinds binds_var } + + ; ev_binds <- getTcEvBindsMap binds_var + ; return (evBindMapBinds ev_binds)} -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on -- However, do not make any evidence bindings, because we don't @@ -155,17 +157,21 @@ reportUnsolved wanted -- and for simplifyDefault. reportAllUnsolved :: WantedConstraints -> TcM () reportAllUnsolved wanted - = report_unsolved Nothing False TypeError HoleError HoleError HoleError wanted + = do { ev_binds <- newTcEvBinds + ; report_unsolved ev_binds False TypeError + HoleError HoleError HoleError wanted } -- | Report all unsolved goals as warnings (but without deferring any errors to -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in -- TcSimplify warnAllUnsolved :: WantedConstraints -> TcM () warnAllUnsolved wanted - = report_unsolved Nothing True TypeWarn HoleWarn HoleWarn HoleWarn wanted + = do { ev_binds <- newTcEvBinds + ; report_unsolved ev_binds True TypeWarn + HoleWarn HoleWarn HoleWarn wanted } -- | Report unsolved goals as errors or warnings. -report_unsolved :: Maybe EvBindsVar -- cec_binds +report_unsolved :: EvBindsVar -- cec_binds -> Bool -- Errors as warnings -> TypeErrorChoice -- Deferred type errors -> HoleChoice -- Expression holes @@ -277,21 +283,15 @@ data ReportErrCtxt -- ic_skols and givens are tidied, rest are not , cec_tidy :: TidyEnv - , cec_binds :: Maybe EvBindsVar - -- Nothing <=> Report all errors, including holes - -- Do not add any evidence bindings, because - -- we have no convenient place to put them - -- See TcErrors.reportAllUnsolved - -- Just ev <=> make some errors (depending on cec_defer) - -- into warnings, and emit evidence bindings - -- into 'ev' for unsolved constraints + , cec_binds :: EvBindsVar -- Make some errors (depending on cec_defer) + -- into warnings, and emit evidence bindings + -- into 'cec_binds' for unsolved constraints , cec_errors_as_warns :: Bool -- Turn all errors into warnings -- (except for Holes, which are -- controlled by cec_type_holes and -- cec_expr_holes) , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime - -- Irrelevant if cec_binds = Nothing -- cec_expr_holes is a union of: -- cec_type_holes - a set of typed holes: '_', '_a', '_foo' @@ -325,7 +325,7 @@ Specifically (see reportWanteds) reportImplic :: ReportErrCtxt -> Implication -> TcM () reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given - , ic_wanted = wanted, ic_binds = m_evb + , ic_wanted = wanted, ic_binds = evb , ic_status = status, ic_info = info , ic_env = tcl_env, ic_tclvl = tc_lvl }) | BracketSkol <- info @@ -356,11 +356,7 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given -- tree rooted here, or we've come across -- a suppress-worthy constraint higher up (Trac #11541) - , cec_binds = cec_binds ctxt *> m_evb } - -- If cec_binds ctxt is Nothing, that means - -- we're reporting *all* errors. Don't change - -- that behavior just because we're going into - -- an implication. + , cec_binds = evb } dead_givens = case status of IC_Solved { ics_dead = dead } -> dead @@ -754,12 +750,12 @@ addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM () addDeferredBinding ctxt err ct | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct -- Only add deferred bindings for Wanted constraints - , Just ev_binds_var <- cec_binds ctxt -- We have somewhere to put the bindings = do { dflags <- getDynFlags ; let err_msg = pprLocErrMsg err err_fs = mkFastString $ showSDoc dflags $ err_msg $$ text "(deferred type error)" err_tm = EvDelayedError pred err_fs + ev_binds_var = cec_binds ctxt ; case dest of EvVarDest evar @@ -1537,8 +1533,8 @@ mkEqInfoMsg ct ty1 ty2 -- mismatched types for suggestion about -fprint-explicit-kinds (act_ty, exp_ty) = case ctOrigin ct of TypeEqOrigin { uo_actual = act - , uo_expected = Check exp } -> (act, exp) - _ -> (ty1, ty2) + , uo_expected = exp } -> (act, exp) + _ -> (ty1, ty2) invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty , not vis @@ -1706,7 +1702,7 @@ mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool -- NotSwapped means (actual, expected), IsSwapped is the reverse -- First return val is whether or not to print a herald above this msg mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act - , uo_expected = Check exp + , uo_expected = exp , uo_thing = maybe_thing }) m_level printExpanded | KindLevel <- level, occurs_check_error = (True, Nothing, empty) diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index aaa1f0c5cd..ae98d38ad1 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -13,7 +13,7 @@ module TcEvidence ( -- Evidence bindings TcEvBinds(..), EvBindsVar(..), EvBindMap(..), emptyEvBindMap, extendEvBinds, - lookupEvBind, evBindMapBinds, foldEvBindMap, + lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap, EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, sccEvBinds, evBindVar, EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors, @@ -283,8 +283,24 @@ data TcEvBinds | EvBinds -- Immutable after zonking (Bag EvBind) -data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique - -- The Unique is for debug printing only +data EvBindsVar + = EvBindsVar { + ebv_uniq :: Unique, + -- The Unique is for debug printing only + + ebv_binds :: IORef EvBindMap, + -- The main payload: the value-level evidence bindings + -- (dictionaries etc) + + ebv_tcvs :: IORef TyCoVarSet + -- The free vars of the (rhss of) the coercion bindings + -- + -- Coercions don't actually have bindings + -- because we plug them in-place (via a mutable + -- variable); but we keep their free variables + -- so that we can report unused given constraints + -- See Note [Tracking redundant constraints] in TcSimplify + } instance Data.Data TcEvBinds where -- Placeholder; we can't travers into TcEvBinds @@ -325,6 +341,9 @@ extendEvBinds bs ev_bind (eb_lhs ev_bind) ev_bind } +isEmptyEvBindMap :: EvBindMap -> Bool +isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m + lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs) @@ -334,6 +353,9 @@ evBindMapBinds = foldEvBindMap consBag emptyBag foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs) +instance Outputable EvBindMap where + ppr (EvBindMap m) = ppr m + ----------------- -- All evidence is bound by EvBinds; no side effects data EvBind @@ -761,10 +783,11 @@ instance Outputable TcEvBinds where ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs))) instance Outputable EvBindsVar where - ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u) + ppr (EvBindsVar { ebv_uniq = u }) + = text "EvBindsVar" <> angleBrackets (ppr u) instance Uniquable EvBindsVar where - getUnique (EvBindsVar _ u) = u + getUnique (EvBindsVar { ebv_uniq = u }) = u instance Outputable EvBind where ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given }) diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index 8ae454c167..c960f6c074 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -141,7 +141,7 @@ tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr) tcInferSigmaNC (L loc expr) = setSrcSpan loc $ - do { (expr', sigma) <- tcInfer (tcExpr expr) + do { (expr', sigma) <- tcInferNoInst (tcExpr expr) ; return (L loc expr', sigma) } tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) @@ -1176,14 +1176,10 @@ tcInferFun (L loc (HsRecFld f)) ; return (L loc fun, ty) } tcInferFun fun - = do { (fun, fun_ty) <- tcInferSigma fun + = tcInferSigma fun + -- NB: tcInferSigma; see TcUnify + -- Note [Deep instantiation of InferResult] - -- Zonk the function type carefully, to expose any polymorphism - -- E.g. (( \(x::forall a. a->a). blah ) e) - -- We can see the rank-2 type of the lambda in time to generalise e - ; fun_ty' <- zonkTcType fun_ty - - ; return (fun, fun_ty') } ---------------- -- | Type-check the arguments to a function, possibly including visible type @@ -1267,7 +1263,7 @@ tcTupArgs args tys tcSyntaxOp :: CtOrigin -> SyntaxExpr Name -> [SyntaxOpType] -- ^ shape of syntax operator arguments - -> ExpType -- ^ overall result type + -> ExpRhoType -- ^ overall result type -> ([TcSigmaType] -> TcM a) -- ^ Type check any arguments -> TcM (a, SyntaxExpr TcId) -- ^ Typecheck a syntax operator @@ -1365,7 +1361,7 @@ tcSynArgE orig sigma_ty syn_ty thing_inside herald = text "This rebindable syntax expects a function with" go rho_ty (SynType the_ty) - = do { wrap <- tcSubTypeET orig the_ty rho_ty + = do { wrap <- tcSubTypeET orig GenSigCtxt the_ty rho_ty ; result <- thing_inside [] ; return (result, wrap) } @@ -1507,8 +1503,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) then return idHsWrapper -- Fast path; also avoids complaint when we infer -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int - else tcSubType_NC ExprSigCtxt inferred_sigma - (mkCheckExpType my_sigma) + else tcSubType_NC ExprSigCtxt inferred_sigma my_sigma ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) ; let poly_wrap = wrap @@ -1581,6 +1576,7 @@ tcInferRecSelId (Ambiguous lbl _) ------------------------ tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType) -- Look up an occurrence of an Id +-- Do not instantiate its type tcInferId id_name | id_name `hasKey` tagToEnumKey = failWithTc (text "tagToEnum# must appear applied to one argument") @@ -1750,7 +1746,7 @@ tcSeq loc fun_name args res_ty -> do { rr_ty <- newFlexiTyVarTy runtimeRepTy ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE rr_ty) -- see Note [Typing rule for seq] - ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg2 res_ty + ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg2 res_ty ; return (term_arg1, term_arg2, mkCheckExpType ty_arg2) } [Left term_arg1, Left term_arg2] -> return (term_arg1, term_arg2, res_ty) @@ -1773,7 +1769,7 @@ tcTagToEnum loc fun_name args res_ty ; arg <- case args of [Right hs_ty_arg, Left term_arg] -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind - ; _ <- tcSubTypeDS GenSigCtxt noThing ty_arg res_ty + ; _ <- tcSubTypeDS (OccurrenceOf fun_name) GenSigCtxt ty_arg res_ty -- other than influencing res_ty, we just -- don't care about a type arg passed in. -- So drop the evidence. diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index efb7dfe30e..618c3c067b 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -1445,8 +1445,9 @@ zonk_tc_ev_binds env (TcEvBinds var) = zonkEvBindsVar env var zonk_tc_ev_binds env (EvBinds bs) = zonkEvBinds env bs zonkEvBindsVar :: ZonkEnv -> EvBindsVar -> TcM (ZonkEnv, Bag EvBind) -zonkEvBindsVar env (EvBindsVar ref _) = do { bs <- readMutVar ref - ; zonkEvBinds env (evBindMapBinds bs) } +zonkEvBindsVar env (EvBindsVar { ebv_binds = ref }) + = do { bs <- readMutVar ref + ; zonkEvBinds env (evBindMapBinds bs) } zonkEvBinds :: ZonkEnv -> Bag EvBind -> TcM (ZonkEnv, Bag EvBind) zonkEvBinds env binds @@ -1598,7 +1599,7 @@ zonkTvSkolemising :: UnboundTyVarZonker -- This variant is used for the LHS of rules -- See Note [Zonking the LHS of a RULE]. zonkTvSkolemising tv - = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv + = do { tv' <- skolemiseUnboundMetaTyVar tv ; return (mkTyVarTy tv') } zonkTypeZapping :: UnboundTyVarZonker diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 055159d988..2d3dee92e5 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -853,7 +853,7 @@ checkExpectedKind :: TcType -- the type whose kind we're checking checkExpectedKind ty act_kind exp_kind = do { (ty', act_kind') <- instantiate ty act_kind exp_kind ; let origin = TypeEqOrigin { uo_actual = act_kind' - , uo_expected = mkCheckExpType exp_kind + , uo_expected = exp_kind , uo_thing = Just $ mkTypeErrorThing ty' } ; co_k <- uType origin KindLevel act_kind' exp_kind @@ -1276,7 +1276,8 @@ kcHsTyVarBndrs name cusk open_fam all_kind_vars , hsq_dependent = dep_names }) thing_inside | cusk = do { kv_kinds <- mk_kv_kinds - ; let scoped_kvs = zipWith mk_skolem_tv kv_ns kv_kinds + ; lvl <- getTcLevel + ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $ do { (tc_binders, res_kind, stuff) <- solveEqualities $ bind_telescope hs_tvs thing_inside @@ -1527,14 +1528,16 @@ tcHsTyVarName m_kind name _ -> do { kind <- case m_kind of Just kind -> return kind Nothing -> newMetaKindVar - ; return (mk_skolem_tv name kind, False) }} + ; tv <- newSkolemTyVar name kind + ; return (tv, False) }} -- makes a new skolem tv newSkolemTyVar :: Name -> Kind -> TcM TcTyVar -newSkolemTyVar name kind = return (mk_skolem_tv name kind) +newSkolemTyVar name kind = do { lvl <- getTcLevel + ; return (mk_skolem_tv lvl name kind) } -mk_skolem_tv :: Name -> Kind -> TcTyVar -mk_skolem_tv n k = mkTcTyVar n k vanillaSkolemTv +mk_skolem_tv :: TcLevel -> Name -> Kind -> TcTyVar +mk_skolem_tv lvl n k = mkTcTyVar n k (SkolemTv lvl False) ------------------ kindGeneralizeType :: Type -> TcM Type @@ -1810,7 +1813,7 @@ tcHsPartialSigType ctxt sig_ty ; tau <- zonkTcType tau ; checkValidType ctxt (mkSpecForAllTys all_tvs $ mkPhiTy theta tau) - ; traceTc "tcHsPatSigType" (ppr all_tvs) + ; traceTc "tcHsPartialSigType" (ppr all_tvs) ; return (wcs, wcx, all_tvs, theta, tau) } where new_implicit_tv name = do { kind <- newMetaKindVar @@ -1889,7 +1892,7 @@ tcPatSig in_pat_bind sig res_ty ; if null sig_tvs then do { -- Just do the subsumption check and return wrap <- addErrCtxtM (mk_msg sig_ty) $ - tcSubTypeET_NC PatSigCtxt res_ty sig_ty + tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty ; return (sig_ty, [], sig_wcs, wrap) } else do -- Type signature binds at least one scoped type variable @@ -1912,7 +1915,7 @@ tcPatSig in_pat_bind sig res_ty -- Now do a subsumption check of the pattern signature against res_ty ; wrap <- addErrCtxtM (mk_msg sig_ty) $ - tcSubTypeET_NC PatSigCtxt res_ty sig_ty + tcSubTypeET PatSigOrigin PatSigCtxt res_ty sig_ty -- Phew! ; return (sig_ty, sig_tvs, sig_wcs, wrap) diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index ab5b75c056..aa97075449 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -810,7 +810,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) , ic_given = dfun_ev_vars , ic_wanted = mkImplicWC sc_meth_implics , ic_status = IC_Unsolved - , ic_binds = Just dfun_ev_binds_var + , ic_binds = dfun_ev_binds_var , ic_env = env , ic_info = InstSkol } @@ -1017,7 +1017,7 @@ checkInstConstraints thing_inside , ic_given = [] , ic_wanted = wanted , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_env = env , ic_info = InstSkol } @@ -1368,8 +1368,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind ; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) hs_sig_ty ; let local_meth_ty = idType local_meth_id ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $ - tcSubType ctxt (Just sel_id) sig_ty - (mkCheckExpType local_meth_ty) + tcSubType_NC ctxt sig_ty local_meth_ty ; return (sig_ty, hs_wrap) } ; inner_meth_name <- newName (nameOccName sel_name) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 678661c56d..0f8bf06412 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -30,9 +30,11 @@ module TcMType ( -------------------------------- -- Expected types ExpType(..), ExpSigmaType, ExpRhoType, - mkCheckExpType, newOpenInferExpType, readExpType, readExpType_maybe, - writeExpType, expTypeToType, checkingExpType_maybe, checkingExpType, - tauifyExpType, + mkCheckExpType, + newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst, + readExpType, readExpType_maybe, + expTypeToType, checkingExpType_maybe, checkingExpType, + tauifyExpType, inferResultToType, promoteTcType, -------------------------------- -- Creating fresh type variables for pm checking @@ -66,7 +68,7 @@ module TcMType ( zonkTidyTcType, zonkTidyOrigin, mkTypeErrorThing, mkTypeErrorThingArgs, tidyEvVar, tidyCt, tidySkolemInfo, - skolemiseUnboundMetaTyVar, + skolemiseUnboundMetaTyVar, skolemiseRuntimeUnk, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkTyCoVarsAndFVList, @@ -335,21 +337,29 @@ test gadt/gadt-escape1. -- actual data definition is in TcType -- | Make an 'ExpType' suitable for inferring a type of kind * or #. -newOpenInferExpType :: TcM ExpType -newOpenInferExpType +newInferExpTypeNoInst :: TcM ExpSigmaType +newInferExpTypeNoInst = newInferExpType False + +newInferExpTypeInst :: TcM ExpRhoType +newInferExpTypeInst = newInferExpType True + +newInferExpType :: Bool -> TcM ExpType +newInferExpType inst = do { rr <- newFlexiTyVarTy runtimeRepTy ; u <- newUnique ; tclvl <- getTcLevel ; let ki = tYPE rr ; traceTc "newOpenInferExpType" (ppr u <+> dcolon <+> ppr ki) ; ref <- newMutVar Nothing - ; return (Infer u tclvl ki ref) } + ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl + , ir_kind = ki, ir_ref = ref + , ir_inst = inst })) } -- | Extract a type out of an ExpType, if one exists. But one should always -- exist. Unless you're quite sure you know what you're doing. readExpType_maybe :: ExpType -> TcM (Maybe TcType) -readExpType_maybe (Check ty) = return (Just ty) -readExpType_maybe (Infer _ _ _ ref) = readMutVar ref +readExpType_maybe (Check ty) = return (Just ty) +readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref -- | Extract a type out of an ExpType. Otherwise, panics. readExpType :: ExpType -> TcM TcType @@ -359,30 +369,6 @@ readExpType exp_ty Just ty -> return ty Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) } --- | Write into an 'ExpType'. It must be an 'Infer'. -writeExpType :: ExpType -> TcType -> TcM () -writeExpType (Infer u tc_lvl ki ref) ty - | debugIsOn - = do { ki1 <- zonkTcType (typeKind ty) - ; ki2 <- zonkTcType ki - ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u ) - ; lvl_now <- getTcLevel - ; MASSERT2( tc_lvl == lvl_now, ppr u $$ ppr tc_lvl $$ ppr lvl_now ) - ; cts <- readTcRef ref - ; case cts of - Just already_there -> pprPanic "writeExpType" - (vcat [ ppr u - , ppr ty - , ppr already_there ]) - Nothing -> write } - | otherwise - = write - where - write = do { traceTc "Filling ExpType" $ - ppr u <+> text ":=" <+> ppr ty - ; writeTcRef ref (Just ty) } -writeExpType (Check ty1) ty2 = pprPanic "writeExpType" (ppr ty1 $$ ppr ty2) - -- | Returns the expected type when in checking mode. checkingExpType_maybe :: ExpType -> Maybe TcType checkingExpType_maybe (Check ty) = Just ty @@ -397,35 +383,132 @@ 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 unificaiton variable -tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) -tauifyExpType (Infer u tc_lvl ki ref) = do { ty <- inferTypeToType u tc_lvl ki ref - ; return (Check ty) } +tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) +tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res + ; return (Check ty) } -- | Extracts the expected type if there is one, or generates a new -- TauTv if there isn't. expTypeToType :: ExpType -> TcM TcType -expTypeToType (Check ty) = return ty -expTypeToType (Infer u tc_lvl ki ref) = inferTypeToType u tc_lvl ki ref - -inferTypeToType :: Unique -> TcLevel -> Kind -> IORef (Maybe TcType) -> TcM Type -inferTypeToType u tc_lvl ki ref - = do { uniq <- newUnique - ; tv_ref <- newMutVar Flexi - ; let details = MetaTv { mtv_info = TauTv - , mtv_ref = tv_ref - , mtv_tclvl = tc_lvl } - name = mkMetaTyVarName uniq (fsLit "t") - tau_tv = mkTcTyVar name ki details - tau = mkTyVarTy tau_tv - -- can't use newFlexiTyVarTy because we need to set the tc_lvl - -- See also Note [TcLevel of ExpType] - +expTypeToType (Check ty) = return ty +expTypeToType (Infer inf_res) = inferResultToType inf_res + +inferResultToType :: InferResult -> TcM Type +inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl + , ir_kind = kind, ir_ref = ref }) + = do { tau_tv <- newMetaTyVarAtLevel tc_lvl kind + -- See Note [TcLevel of ExpType] + ; let tau = mkTyVarTy tau_tv ; writeMutVar ref (Just tau) ; traceTc "Forcing ExpType to be monomorphic:" - (ppr u <+> dcolon <+> ppr ki <+> text ":=" <+> ppr tau) + (ppr u <+> dcolon <+> ppr kind <+> text ":=" <+> ppr tau) ; return tau } -{- +{- ********************************************************************* +* * + 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 the same as 'ty' +-- * 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 + = do { prom_tv <- newMetaTyVarAtLevel dest_lvl (typeKind ty) + ; let prom_ty = mkTyVarTy prom_tv + eq_orig = TypeEqOrigin { uo_actual = ty + , uo_expected = prom_ty + , uo_thing = Nothing } + + ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty + ; return (co, prom_ty) } + + dont_promote_it :: TcM (TcCoercion, TcType) + dont_promote_it = return (mkTcNomReflCo ty, ty) + +{- Note [Promoting a type] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (Trac #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 poromoted 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 (->) becuase that's part of +the polymorphic "shape". And becauuse 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. + + ************************************************************************ * * SkolemTvs (immutable) @@ -493,17 +576,22 @@ tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Get the location from the monad; this is a complete freshening operation tcInstSkolTyVars' overlappable subst tvs = do { loc <- getSrcSpanM - ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs } + ; lvl <- getTcLevel + ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs } -mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar -mkTcSkolTyVar loc overlappable uniq old_name kind - = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc) - kind - (SkolemTv overlappable) +mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker +mkTcSkolTyVar lvl loc overlappable + = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc) + kind details + where + details = SkolemTv (pushTcLevel lvl) overlappable + -- NB: skolems bump the level tcInstSigTyVars :: SrcSpan -> [TyVar] - -> TcRnIf gbl lcl (TCvSubst, [TcTyVar]) -tcInstSigTyVars loc = instSkolTyCoVars (mkTcSkolTyVar loc False) + -> TcM (TCvSubst, [TcTyVar]) +tcInstSigTyVars loc tvs + = do { lvl <- getTcLevel + ; instSkolTyCoVars (mkTcSkolTyVar lvl loc False) tvs } ------------------ freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar]) @@ -522,15 +610,15 @@ freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind ------------------ -instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar) - -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) +type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar +instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst -instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar) +instSkolTyCoVarsX :: TcTyVarMaker -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar]) instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv) -instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar) +instSkolTyCoVarX :: TcTyVarMaker -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar) instSkolTyCoVarX mk_tcv subst tycovar = do { uniq <- newUnique -- using a new unique is critical. See @@ -620,7 +708,7 @@ cloneMetaTyVar tv -- Works for both type and kind variables readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) - readMutVar (metaTvRef tyvar) + readMutVar (metaTyVarRef tyvar) isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable @@ -645,7 +733,7 @@ writeMetaTyVar :: TcTyVar -> TcType -> TcM () writeMetaTyVar tyvar ty | not debugIsOn - = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty + = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty -- Everything from here on only happens if DEBUG is on | not (isTcTyVar tyvar) @@ -669,32 +757,61 @@ writeMetaTyVarRef tyvar ref ty <+> text ":=" <+> ppr ty) ; writeTcRef ref (Indirect ty) } --- Everything from here on only happens if DEBUG is on + -- Everything from here on only happens if DEBUG is on | otherwise = do { meta_details <- readMutVar ref; -- Zonk kinds to allow the error check to work ; zonked_tv_kind <- zonkTcType tv_kind ; zonked_ty_kind <- zonkTcType ty_kind + ; let kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates + -- to coercion variables + || tcEqKind zonked_ty_kind zonked_tv_kind + + kind_msg = hang (text "Ill-kinded update to meta tyvar") + 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind) + <+> text ":=" + <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) + + ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) -- Check for double updates - ; ASSERT2( isFlexi meta_details, - hang (text "Double update of meta tyvar") - 2 (ppr tyvar $$ ppr meta_details) ) - - traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) - ; writeMutVar ref (Indirect ty) - ; when ( not (isPredTy tv_kind) - -- Don't check kinds for updates to coercion variables - && not (zonked_ty_kind `tcEqKind` zonked_tv_kind)) - $ WARN( True, hang (text "Ill-kinded update to meta tyvar") - 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind) - <+> text ":=" - <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) ) - (return ()) } + ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details ) + + -- Check for level OK + -- See Note [Level check when unifying] + ; MASSERT2( level_check_ok, level_check_msg ) + + -- Check Kinds ok + ; MASSERT2( kind_check_ok, kind_msg ) + + -- Do the write + ; writeMutVar ref (Indirect ty) } where tv_kind = tyVarKind tyvar ty_kind = typeKind ty + tv_lvl = tcTyVarLevel tyvar + ty_lvl = tcTypeLevel ty + + level_check_ok = isFmvTyVar tyvar + || not (ty_lvl `strictlyDeeperThan` tv_lvl) + level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty + + double_upd_msg details = hang (text "Double update of meta tyvar") + 2 (ppr tyvar $$ ppr details) + + +{- Note [Level check when unifying] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When unifying + alpha:lvl := ty +we expect that the TcLevel of 'ty' will be <= lvl. +However, during unflatting we do + fuv:l := ty:(l+1) +which is usually wrong; hence the check isFmmvTyVar in level_check_ok. +See Note [TcLevel assignment] in TcType. +-} + {- % Generating fresh variables for pattern match check -} @@ -705,7 +822,8 @@ genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar] -- Precondition: tyvars should be scoping-ordered -- see Note [Kind substitution when instantiating] -- Get the location from the monad; this is a complete freshening operation -genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs +genInstSkolTyVarsX loc subst tvs + = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs {- ************************************************************************ @@ -785,16 +903,26 @@ newWildCardX subst tv ; return (extendTvSubstWithClone subst tv new_tv, new_tv) } new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) -new_meta_tv_x info subst tyvar +new_meta_tv_x info subst tv = do { uniq <- newUnique ; details <- newMetaDetails info - ; let name = mkSystemName uniq (getOccName tyvar) + ; let name = mkSystemName uniq (getOccName tv) -- See Note [Name of an instantiated type variable] - kind = substTy subst (tyVarKind tyvar) + kind = substTy subst (tyVarKind tv) new_tv = mkTcTyVar name kind details - subst1 = extendTvSubstWithClone subst tyvar new_tv + subst1 = extendTvSubstWithClone subst tv new_tv ; return (subst1, new_tv) } +newMetaTyVarAtLevel :: TcLevel -> TcKind -> TcM TcTyVar +newMetaTyVarAtLevel tc_lvl kind + = do { uniq <- newUnique + ; ref <- newMutVar Flexi + ; let name = mkMetaTyVarName uniq (fsLit "p") + details = MetaTv { mtv_info = TauTv + , mtv_ref = ref + , mtv_tclvl = tc_lvl } + ; return (mkTcTyVar name kind details) } + {- Note [Name of an instantiated type variable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At the moment we give a unification variable a System Name, which @@ -960,7 +1088,7 @@ zonkQuantifiedTyVar default_kind tv ; return Nothing } | otherwise - = do { tv' <- skolemiseUnboundMetaTyVar tv vanillaSkolemTv + = do { tv' <- skolemiseUnboundMetaTyVar tv ; return (Just tv') } default_kind_var :: TyVar -> TcM Type @@ -988,13 +1116,21 @@ zonkQuantifiedTyVar default_kind tv Indirect ty -> WARN( True, ppr tv $$ ppr ty ) return () } -skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar +skolemiseRuntimeUnk :: TcTyVar -> TcM TyVar +skolemiseRuntimeUnk tv + = skolemise_tv tv RuntimeUnk + +skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar +skolemiseUnboundMetaTyVar tv + = skolemise_tv tv (SkolemTv (metaTyVarTcLevel tv) False) + +skolemise_tv :: TcTyVar -> TcTyVarDetails -> TcM TyVar -- We have a Meta tyvar with a ref-cell inside it -- Skolemise it, so that -- we are totally out of Meta-tyvar-land -- We create a skolem TyVar, not a regular TyVar -- See Note [Zonking to Skolem] -skolemiseUnboundMetaTyVar tv details +skolemise_tv tv details = ASSERT2( isMetaTyVar tv, ppr tv ) do { span <- getSrcSpanM -- Get the location from "here" -- ie where we are generalising @@ -1448,11 +1584,7 @@ zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act , uo_expected = exp , uo_thing = m_thing }) = do { (env1, act') <- zonkTidyTcType env act - ; mb_exp <- readExpType_maybe exp -- it really should be filled in. - -- unless we're debugging. - ; (env2, exp') <- case mb_exp of - Just ty -> second mkCheckExpType <$> zonkTidyTcType env1 ty - Nothing -> return (env1, exp) + ; (env2, exp') <- zonkTidyTcType env1 exp ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing ; return ( env3, orig { uo_actual = act' , uo_expected = exp' diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs index 85a7e30fdf..01586c0230 100644 --- a/compiler/typecheck/TcMatches.hs +++ b/compiler/typecheck/TcMatches.hs @@ -869,10 +869,9 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names tup_ty = mkBigCoreTupTy tup_elt_tys ; tcExtendIdEnv tup_ids $ do - { stmts_ty <- newOpenInferExpType - ; (stmts', (ret_op', tup_rets)) - <- tcStmtsAndThen ctxt tcDoStmt stmts stmts_ty $ - \ inner_res_ty -> + { ((stmts', (ret_op', tup_rets)), stmts_ty) + <- tcInferInst $ \ exp_ty -> + tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty -> do { tup_rets <- zipWithM tcCheckId tup_names (map mkCheckExpType tup_elt_tys) -- Unify the types of the "final" Ids (which may @@ -881,14 +880,12 @@ tcDoStmt ctxt (RecStmt { recS_stmts = stmts, recS_later_ids = later_names <- tcSyntaxOp DoOrigin ret_op [synKnownType tup_ty] inner_res_ty $ \_ -> return () ; return (ret_op', tup_rets) } - ; stmts_ty <- readExpType stmts_ty - ; mfix_res_ty <- newOpenInferExpType - ; (_, mfix_op') - <- tcSyntaxOp DoOrigin mfix_op - [synKnownType (mkFunTy tup_ty stmts_ty)] mfix_res_ty $ + ; ((_, mfix_op'), mfix_res_ty) + <- tcInferInst $ \ exp_ty -> + tcSyntaxOp DoOrigin mfix_op + [synKnownType (mkFunTy tup_ty stmts_ty)] exp_ty $ \ _ -> return () - ; mfix_res_ty <- readExpType mfix_res_ty ; ((thing, new_res_ty), bind_op') <- tcSyntaxOp DoOrigin bind_op @@ -1014,7 +1011,7 @@ tcApplicativeStmts tcApplicativeStmts ctxt pairs rhs_ty thing_inside = do { body_ty <- newFlexiTyVarTy liftedTypeKind ; let arity = length pairs - ; ts <- replicateM (arity-1) $ newOpenInferExpType + ; ts <- replicateM (arity-1) $ newInferExpTypeInst ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind ; let fun_ty = mkFunTys pat_tys body_ty diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index ea4cf3ec71..9a5fd7d8cb 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -397,7 +397,7 @@ tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty) -- check that overall pattern is more polymorphic than arg type - ; expr_wrap2 <- tcSubTypeET (pe_orig penv) overall_pat_ty inf_arg_ty + ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty -- pattern must have inf_res_ty @@ -502,13 +502,12 @@ tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside ------------------------ -- Literal patterns -tc_pat _ (LitPat simple_lit) pat_ty thing_inside +tc_pat penv (LitPat simple_lit) pat_ty thing_inside = do { let lit_ty = hsLitType simple_lit - ; co <- unifyPatType simple_lit lit_ty pat_ty - -- coi is of kind: pat_ty ~ lit_ty - ; res <- thing_inside + ; wrap <- tcSubTypePat penv pat_ty lit_ty + ; res <- thing_inside ; pat_ty <- readExpType pat_ty - ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty + ; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty , res) } ------------------------ @@ -622,15 +621,6 @@ tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat))) tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut ----------------- -unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion --- In patterns we want a coercion from the --- context type (expected) to the actual pattern type --- But we don't want to reverse the args to unifyType because --- that controls the actual/expected stuff in error messages -unifyPatType thing actual_ty expected_ty - = do { coi <- unifyExpType (Just thing) actual_ty expected_ty - ; return (mkTcSymCo coi) } {- Note [Hopping the LIE in lazy patterns] @@ -841,7 +831,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside prov_theta' = substTheta tenv prov_theta req_theta' = substTheta tenv req_theta - ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty' + ; wrap <- tcSubTypePat penv pat_ty ty' ; traceTc "tcPatSynPat" (ppr pat_syn $$ ppr pat_ty $$ ppr ty' $$ diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index dc973da98b..05d98fff1a 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -72,11 +72,9 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details ; (tclvl, wanted, ((lpat', args), pat_ty)) <- pushLevelAndCaptureConstraints $ - do { pat_ty <- newOpenInferExpType - ; stuff <- tcPat PatSyn lpat pat_ty $ - mapM tcLookupId arg_names - ; pat_ty <- readExpType pat_ty - ; return (stuff, pat_ty) } + tcInferInst $ \ exp_ty -> + tcPat PatSyn lpat exp_ty $ + mapM tcLookupId arg_names ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args @@ -390,11 +388,11 @@ tcPatSynMatcher (L loc name) lpat (args, arg_tys) pat_ty = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc ; tv_name <- newNameAt (mkTyVarOcc "r") loc - ; let rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False) - rr = mkTyVarTy rr_tv - res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False) - is_unlifted = null args && null prov_dicts + ; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv + rr = mkTyVarTy rr_tv + res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv res_ty = mkTyVarTy res_tv + is_unlifted = null args && null prov_dicts (cont_args, cont_arg_tys) | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy]) | otherwise = (args, arg_tys) diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs index c40544035c..0363aa114a 100644 --- a/compiler/typecheck/TcPluginM.hs +++ b/compiler/typecheck/TcPluginM.hs @@ -48,8 +48,7 @@ module TcPluginM ( -- * Manipulating evidence bindings newEvVar, setEvBind, - getEvBindsTcPluginM, - getEvBindsTcPluginM_maybe + getEvBindsTcPluginM #endif ) where @@ -64,12 +63,12 @@ import qualified Finder import FamInstEnv ( FamInstEnv ) import TcRnMonad ( TcGblEnv, TcLclEnv, Ct, CtLoc, TcPluginM - , unsafeTcPluginTcM, getEvBindsTcPluginM_maybe + , unsafeTcPluginTcM, getEvBindsTcPluginM , liftIO, traceTc ) import TcMType ( TcTyVar, TcType ) import TcEnv ( TcTyThing ) import TcEvidence ( TcCoercion, CoercionHole - , EvTerm, EvBind, EvBindsVar, mkGivenEvBind ) + , EvTerm, EvBind, mkGivenEvBind ) import TcRnTypes ( CtEvidence(..) ) import Var ( EvVar ) @@ -84,7 +83,6 @@ import Type import Id import InstEnv import FastString -import Maybes import Unique @@ -190,12 +188,4 @@ setEvBind :: EvBind -> TcPluginM () setEvBind ev_bind = do tc_evbinds <- getEvBindsTcPluginM unsafeTcPluginTcM $ TcM.addTcEvBind tc_evbinds ev_bind - --- | Access the 'EvBindsVar' carried by the 'TcPluginM' during --- constraint solving. This must not be invoked from 'tcPluginInit' --- or 'tcPluginStop', or it will panic. -getEvBindsTcPluginM :: TcPluginM EvBindsVar -getEvBindsTcPluginM = fmap (expectJust oops) getEvBindsTcPluginM_maybe - where - oops = "plugin attempted to read EvBindsVar outside the constraint solver" #endif diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 9f94c12b6a..6c800f4695 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -2486,18 +2486,19 @@ withTcPlugins hsc_env m = do plugins <- liftIO (loadTcPlugins hsc_env) case plugins of [] -> m -- Common fast case - _ -> do (solvers,stops) <- unzip `fmap` mapM startPlugin plugins + _ -> do ev_binds_var <- newTcEvBinds + (solvers,stops) <- unzip `fmap` mapM (startPlugin ev_binds_var) plugins -- This ensures that tcPluginStop is called even if a type -- error occurs during compilation (Fix of #10078) eitherRes <- tryM $ do updGblEnv (\e -> e { tcg_tc_plugins = solvers }) m - mapM_ (flip runTcPluginM Nothing) stops + mapM_ (flip runTcPluginM ev_binds_var) stops case eitherRes of Left _ -> failM Right res -> return res where - startPlugin (TcPlugin start solve stop) = - do s <- runTcPluginM start Nothing + startPlugin ev_binds_var (TcPlugin start solve stop) = + do s <- runTcPluginM start ev_binds_var return (solve s, stop s) loadTcPlugins :: HscEnv -> IO [TcPlugin] diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs index b871daf398..ada89f1e06 100644 --- a/compiler/typecheck/TcRnMonad.hs +++ b/compiler/typecheck/TcRnMonad.hs @@ -91,7 +91,7 @@ module TcRnMonad( -- * Type constraints newTcEvBinds, addTcEvBind, - getTcEvBinds, getTcEvBindsMap, + getTcEvTyCoVars, getTcEvBindsMap, chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitSimple, emitSimples, @@ -1375,28 +1375,30 @@ debugTc thing -} newTcEvBinds :: TcM EvBindsVar -newTcEvBinds = do { ref <- newTcRef emptyEvBindMap +newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap + ; tcvs_ref <- newTcRef emptyVarSet ; uniq <- newUnique ; traceTc "newTcEvBinds" (text "unique =" <+> ppr uniq) - ; return (EvBindsVar ref uniq) } + ; return (EvBindsVar { ebv_binds = binds_ref + , ebv_tcvs = tcvs_ref + , ebv_uniq = uniq }) } + +getTcEvTyCoVars :: EvBindsVar -> TcM TyCoVarSet +getTcEvTyCoVars (EvBindsVar { ebv_tcvs = ev_ref }) + = readTcRef ev_ref + +getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap +getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) + = readTcRef ev_ref addTcEvBind :: EvBindsVar -> EvBind -> TcM () -- Add a binding to the TcEvBinds by side effect -addTcEvBind (EvBindsVar ev_ref u) ev_bind +addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind = do { traceTc "addTcEvBind" $ ppr u $$ ppr ev_bind ; bnds <- readTcRef ev_ref ; writeTcRef ev_ref (extendEvBinds bnds ev_bind) } -getTcEvBinds :: EvBindsVar -> TcM (Bag EvBind) -getTcEvBinds (EvBindsVar ev_ref _) - = do { bnds <- readTcRef ev_ref - ; return (evBindMapBinds bnds) } - -getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap -getTcEvBindsMap (EvBindsVar ev_ref _) - = readTcRef ev_ref - chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName chooseUniqueOccTc fn = do { env <- getGblEnv diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index f5abe16634..c3d18978b4 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -103,6 +103,7 @@ module TcRnTypes( pushErrCtxt, pushErrCtxtSameOrigin, SkolemInfo(..), pprSigSkolInfo, pprSkolInfo, + termEvidenceAllowed, CtEvidence(..), TcEvDest(..), mkGivenLoc, mkKindLoc, toKindLoc, @@ -112,7 +113,7 @@ module TcRnTypes( -- Constraint solver plugins TcPlugin(..), TcPluginResult(..), TcPluginSolver, TcPluginM, runTcPluginM, unsafeTcPluginTcM, - getEvBindsTcPluginM_maybe, + getEvBindsTcPluginM, CtFlavour(..), ctEvFlavour, CtFlavourRole, ctEvFlavourRole, ctFlavourRole, @@ -2150,12 +2151,8 @@ data Implication ic_wanted :: WantedConstraints, -- The wanted - ic_binds :: Maybe EvBindsVar, - -- Points to the place to fill in the + ic_binds :: EvBindsVar, -- Points to the place to fill in the -- abstraction and bindings. - -- is Nothing if we can't deal with - -- non-equality constraints here - -- (this happens in TcS.deferTcSForAllEq) ic_status :: ImplicStatus } @@ -2756,6 +2753,14 @@ data SkolemInfo instance Outputable SkolemInfo where ppr = pprSkolInfo +termEvidenceAllowed :: SkolemInfo -> Bool +-- Whether an implication constraint with this SkolemInfo +-- is permitted to have term-level evidence. There is +-- only one that is not, associated with unifiying +-- forall-types +termEvidenceAllowed (UnifyForAllSkol {}) = False +termEvidenceAllowed _ = True + pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol ctxt ty) = pprSigSkolInfo ctxt ty @@ -2835,7 +2840,7 @@ data CtOrigin -- function or instance | TypeEqOrigin { uo_actual :: TcType - , uo_expected :: ExpType + , uo_expected :: TcType , uo_thing :: Maybe ErrorThing -- ^ The thing that has type "actual" } @@ -3158,9 +3163,9 @@ type TcPluginSolver = [Ct] -- given -> [Ct] -- wanted -> TcPluginM TcPluginResult -newtype TcPluginM a = TcPluginM (Maybe EvBindsVar -> TcM a) +newtype TcPluginM a = TcPluginM (EvBindsVar -> TcM a) -instance Functor TcPluginM where +instance Functor TcPluginM where fmap = liftM instance Applicative TcPluginM where @@ -3178,7 +3183,7 @@ instance MonadFail.MonadFail TcPluginM where fail x = TcPluginM (const $ fail x) #endif -runTcPluginM :: TcPluginM a -> Maybe EvBindsVar -> TcM a +runTcPluginM :: TcPluginM a -> EvBindsVar -> TcM a runTcPluginM (TcPluginM m) = m -- | This function provides an escape for direct access to @@ -3190,8 +3195,8 @@ unsafeTcPluginTcM = TcPluginM . const -- | Access the 'EvBindsVar' carried by the 'TcPluginM' during -- constraint solving. Returns 'Nothing' if invoked during -- 'tcPluginInit' or 'tcPluginStop'. -getEvBindsTcPluginM_maybe :: TcPluginM (Maybe EvBindsVar) -getEvBindsTcPluginM_maybe = TcPluginM return +getEvBindsTcPluginM :: TcPluginM EvBindsVar +getEvBindsTcPluginM = TcPluginM return data TcPlugin = forall s. TcPlugin diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 37740bd1bc..0174b4aca2 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -41,8 +41,8 @@ module TcSMonad ( getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getLclEnv, - getTcEvBinds, getTcEvBindsFromVar, getTcLevel, - getTcEvBindsMap, + getTcEvBindsVar, getTcLevel, + getTcEvBindsAndTCVs, getTcEvBindsMap, tcLookupClass, -- Inerts @@ -2309,9 +2309,7 @@ should do two things differently: data TcSEnv = TcSEnv { - tcs_ev_binds :: Maybe EvBindsVar, - -- this could be Nothing if we can't deal with non-equality - -- constraints, because, say, we're in a top-level type signature + tcs_ev_binds :: EvBindsVar, tcs_unified :: IORef Int, -- The number of unification variables we have filled @@ -2325,10 +2323,6 @@ data TcSEnv -- See Note [Work list priorities] and tcs_worklist :: IORef WorkList, -- Current worklist - tcs_used_tcvs :: IORef TyCoVarSet, - -- these variables were used when filling holes. Don't discard! - -- See also Note [Tracking redundant constraints] in TcSimplify - tcs_need_deriveds :: Bool -- Keep solving, even if all the unsolved constraints are Derived -- See Note [Solving for Derived constraints] @@ -2386,7 +2380,7 @@ traceTcS :: String -> SDoc -> TcS () traceTcS herald doc = wrapTcS (TcM.traceTc herald doc) runTcPluginTcS :: TcPluginM a -> TcS a -runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBinds +runTcPluginTcS m = wrapTcS . runTcPluginM m =<< getTcEvBindsVar instance HasDynFlags TcS where getDynFlags = wrapTcS getDynFlags @@ -2399,14 +2393,6 @@ bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env ; n <- TcM.readTcRef ref ; TcM.writeTcRef ref (n+1) } --- | Mark variables as used filling a coercion hole -useVars :: TyCoVarSet -> TcS () -useVars vars = TcS $ \env -> useVarsTcM (tcs_used_tcvs env) vars - --- | Like 'useVars' but in the TcM monad -useVarsTcM :: IORef TyCoVarSet -> TyCoVarSet -> TcM () -useVarsTcM ref vars = TcM.updTcRef ref (`unionVarSet` vars) - csTraceTcS :: SDoc -> TcS () csTraceTcS doc = wrapTcS $ csTraceTcM 1 (return doc) @@ -2435,7 +2421,7 @@ runTcS :: TcS a -- What to run -> TcM (a, EvBindMap) runTcS tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; res <- runTcSWithEvBinds False (Just ev_binds_var) tcs + ; res <- runTcSWithEvBinds False ev_binds_var tcs ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var ; return (res, ev_binds) } @@ -2445,14 +2431,16 @@ runTcS tcs runTcSDeriveds :: TcS a -> TcM a runTcSDeriveds tcs = do { ev_binds_var <- TcM.newTcEvBinds - ; runTcSWithEvBinds True (Just ev_binds_var) tcs } + ; runTcSWithEvBinds True ev_binds_var tcs } -- | This can deal only with equality constraints. runTcSEqualities :: TcS a -> TcM a -runTcSEqualities = runTcSWithEvBinds False Nothing +runTcSEqualities thing_inside + = do { ev_binds_var <- TcM.newTcEvBinds + ; runTcSWithEvBinds False ev_binds_var thing_inside } runTcSWithEvBinds :: Bool -- ^ keep running even if only Deriveds are left? - -> Maybe EvBindsVar + -> EvBindsVar -> TcS a -> TcM a runTcSWithEvBinds solve_deriveds ev_binds_var tcs @@ -2460,15 +2448,11 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef emptyInert ; wl_var <- TcM.newTcRef emptyWorkList - ; used_var <- TcM.newTcRef emptyVarSet -- never read from, but see - -- nestImplicTcS - ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_unified = unified_var , tcs_count = step_count , tcs_inerts = inert_var , tcs_worklist = wl_var - , tcs_used_tcvs = used_var , tcs_need_deriveds = solve_deriveds } -- Run the computation @@ -2479,16 +2463,15 @@ runTcSWithEvBinds solve_deriveds ev_binds_var tcs csTraceTcM 0 $ return (text "Constraint solver steps =" <+> int count) #ifdef DEBUG - ; whenIsJust ev_binds_var $ \ebv -> - do { ev_binds <- TcM.getTcEvBinds ebv - ; checkForCyclicBinds ev_binds } + ; ev_binds <- TcM.getTcEvBindsMap ev_binds_var + ; checkForCyclicBinds ev_binds #endif ; return res } #ifdef DEBUG -checkForCyclicBinds :: Bag EvBind -> TcM () -checkForCyclicBinds ev_binds +checkForCyclicBinds :: EvBindMap -> TcM () +checkForCyclicBinds ev_binds_map | null cycles = return () | null coercion_cycles @@ -2496,6 +2479,8 @@ checkForCyclicBinds ev_binds | otherwise = pprPanic "Cycle in coercion bindings" $ ppr coercion_cycles where + ev_binds = evBindMapBinds ev_binds_map + cycles :: [[EvBind]] cycles = [c | CyclicSCC c <- stronglyConnCompFromEdgedVerticesUniq edges] @@ -2511,20 +2496,17 @@ checkForCyclicBinds ev_binds -- Note [Deterministic SCC] in Digraph. #endif -setEvBindsTcS :: Maybe EvBindsVar -> TcS a -> TcS a -setEvBindsTcS m_ref (TcS thing_inside) - = TcS $ \ env -> thing_inside (env { tcs_ev_binds = m_ref }) +setEvBindsTcS :: EvBindsVar -> TcS a -> TcS a +setEvBindsTcS ref (TcS thing_inside) + = TcS $ \ env -> thing_inside (env { tcs_ev_binds = ref }) -nestImplicTcS :: Maybe EvBindsVar -> TyCoVarSet -- bound in this implication +nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a - -> TcS (a, TyCoVarSet) -- also returns any vars used when filling - -- coercion holes (for redundant-constraint - -- tracking) -nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside) + -> TcS a +nestImplicTcS ref inner_tclvl (TcS thing_inside) = TcS $ \ TcSEnv { tcs_unified = unified_var , tcs_inerts = old_inert_var , tcs_count = count - , tcs_used_tcvs = used_var , tcs_need_deriveds = solve_deriveds } -> do { inerts <- TcM.readTcRef old_inert_var @@ -2532,35 +2514,21 @@ nestImplicTcS m_ref bound_tcvs inner_tclvl (TcS thing_inside) -- See Note [Do not inherit the flat cache] ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; new_used_var <- TcM.newTcRef emptyVarSet - ; let nest_env = TcSEnv { tcs_ev_binds = m_ref + ; let nest_env = TcSEnv { tcs_ev_binds = ref , tcs_unified = unified_var , tcs_count = count , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var - , tcs_used_tcvs = new_used_var , tcs_need_deriveds = solve_deriveds } ; res <- TcM.setTcLevel inner_tclvl $ thing_inside nest_env #ifdef DEBUG -- Perform a check that the thing_inside did not cause cycles - ; whenIsJust m_ref $ \ ref -> - do { ev_binds <- TcM.getTcEvBinds ref - ; checkForCyclicBinds ev_binds } + ; ev_binds <- TcM.getTcEvBindsMap ref + ; checkForCyclicBinds ev_binds #endif - ; used_tcvs <- TcM.readTcRef new_used_var - - ; local_ev_vars <- case m_ref of - Nothing -> return emptyVarSet - Just ref -> do { binds <- TcM.getTcEvBinds ref - ; return $ mkVarSet $ map evBindVar $ bagToList binds } - ; let all_locals = bound_tcvs `unionVarSet` local_ev_vars - (inner_used_tcvs, outer_used_tcvs) - = partitionVarSet (`elemVarSet` all_locals) used_tcvs - ; useVarsTcM used_var outer_used_tcvs - - ; return (res, inner_used_tcvs) } + ; return res } {- Note [Do not inherit the flat cache] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2684,21 +2652,22 @@ readTcRef ref = wrapTcS (TcM.readTcRef ref) updTcRef :: TcRef a -> (a->a) -> TcS () updTcRef ref upd_fn = wrapTcS (TcM.updTcRef ref upd_fn) -getTcEvBinds :: TcS (Maybe EvBindsVar) -getTcEvBinds = TcS (return . tcs_ev_binds) - -getTcEvBindsFromVar :: EvBindsVar -> TcS (Bag EvBind) -getTcEvBindsFromVar = wrapTcS . TcM.getTcEvBinds +getTcEvBindsVar :: TcS EvBindsVar +getTcEvBindsVar = TcS (return . tcs_ev_binds) getTcLevel :: TcS TcLevel getTcLevel = wrapTcS TcM.getTcLevel +getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet) +getTcEvBindsAndTCVs ev_binds_var + = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var + ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var + ; return (bnds, tcvs) } + getTcEvBindsMap :: TcS EvBindMap getTcEvBindsMap - = do { ev_binds <- getTcEvBinds - ; case ev_binds of - Just (EvBindsVar ev_ref _) -> wrapTcS $ TcM.readTcRef ev_ref - Nothing -> return emptyEvBindMap } + = do { ev_binds_var <- getTcEvBindsVar + ; wrapTcS $ TcM.getTcEvBindsMap ev_binds_var } unifyTyVar :: TcTyVar -> TcType -> TcS () -- Unify a meta-tyvar with a type @@ -2958,10 +2927,17 @@ getEvTerm (Cached evt) = evt setEvBind :: EvBind -> TcS () setEvBind ev_bind - = do { tc_evbinds <- getTcEvBinds - ; case tc_evbinds of - Just evb -> wrapTcS $ TcM.addTcEvBind evb ev_bind - Nothing -> pprPanic "setEvBind" (ppr ev_bind) } + = do { evb <- getTcEvBindsVar + ; wrapTcS $ TcM.addTcEvBind evb ev_bind } + +-- | Mark variables as used filling a coercion hole +useVars :: TyCoVarSet -> TcS () +useVars vars + = do { EvBindsVar { ebv_tcvs = ref } <- getTcEvBindsVar + ; wrapTcS $ + do { tcvs <- TcM.readTcRef ref + ; let tcvs' = tcvs `unionVarSet` vars + ; TcM.writeTcRef ref tcvs' } } -- | Equalities only setWantedEq :: TcEvDest -> Coercion -> TcS () @@ -3152,6 +3128,10 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2) ; (ctev, hole_co) <- newWantedEq loc role phi1 phi2 ; env <- getLclEnv + ; ev_binds <- newTcEvBinds + -- We have nowhere to put these bindings + -- but TcSimplify.setImplicationStatus + -- checks that we don't actually use them ; let new_tclvl = pushTcLevel (tcl_tclvl env) wc = WC { wc_simple = singleCt (mkNonCanonical ctev) , wc_impl = emptyBag @@ -3162,7 +3142,7 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2) , ic_given = [] , ic_wanted = wc , ic_status = IC_Unsolved - , ic_binds = Nothing -- no place to put binds + , ic_binds = ev_binds , ic_env = env , ic_info = skol_info } ; updWorkListTcS (extendWorkListImplic imp) diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index d146c73094..ddf0bce945 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -573,7 +573,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; psig_theta_vars <- mapM TcM.newEvVar psig_theta ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ - runTcSWithEvBinds False (Just ev_binds_var) $ + runTcSWithEvBinds False ev_binds_var $ do { let loc = mkGivenLoc rhs_tclvl UnkSkol tc_lcl_env psig_givens = mkGivens loc psig_theta_vars ; _ <- solveSimpleGivens psig_givens @@ -692,7 +692,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds , ic_given = full_theta_vars , ic_wanted = wanted_transformed , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_info = skol_info , ic_env = tc_lcl_env } ; emitImplication implic @@ -1225,7 +1225,7 @@ solveImplication :: Implication -- Wanted -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value solveImplication imp@(Implic { ic_tclvl = tclvl - , ic_binds = m_ev_binds + , ic_binds = ev_binds_var , ic_skols = skols , ic_given = given_ids , ic_wanted = wanteds @@ -1243,8 +1243,8 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts) -- Solve the nested constraints - ; ((no_given_eqs, given_insols, residual_wanted), used_tcvs) - <- nestImplicTcS m_ev_binds (mkVarSet (skols ++ given_ids)) tclvl $ + ; (no_given_eqs, given_insols, residual_wanted) + <- nestImplicTcS ev_binds_var tclvl $ do { let loc = mkGivenLoc tclvl info env givens = mkGivens loc given_ids ; given_insols <- solveSimpleGivens givens @@ -1265,35 +1265,33 @@ solveImplication imp@(Implic { ic_tclvl = tclvl <- floatEqualities skols no_given_eqs residual_wanted ; traceTcS "solveImplication 2" - (ppr given_insols $$ ppr residual_wanted $$ ppr used_tcvs) + (ppr given_insols $$ ppr residual_wanted) ; let final_wanted = residual_wanted `addInsols` given_insols ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs , ic_wanted = final_wanted }) - used_tcvs - ; evbinds <- TcS.getTcEvBindsMap + ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var ; traceTcS "solveImplication end }" $ vcat [ text "no_given_eqs =" <+> ppr no_given_eqs , text "floated_eqs =" <+> ppr floated_eqs , text "res_implic =" <+> ppr res_implic - , text "implication evbinds = " <+> ppr (evBindMapBinds evbinds) ] + , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) + , text "implication tvcs =" <+> ppr tcvs ] ; return (floated_eqs, res_implic) } ---------------------- -setImplicationStatus :: Implication -> TyCoVarSet -- needed variables - -> TcS (Maybe Implication) +setImplicationStatus :: Implication -> TcS (Maybe Implication) -- Finalise the implication returned from solveImplication: -- * Set the ic_status field -- * Trim the ic_wanted field to remove Derived constraints -- Return Nothing if we can discard the implication altogether -setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var - , ic_info = info +setImplicationStatus implic@(Implic { ic_binds = ev_binds_var + , ic_info = info , ic_tclvl = tc_lvl , ic_wanted = wc - , ic_given = givens }) - used_tcvs + , ic_given = givens }) | some_insoluble = return $ Just $ implic { ic_status = IC_Insoluble @@ -1308,11 +1306,8 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var | otherwise -- Everything is solved; look at the implications -- See Note [Tracking redundant constraints] - = do { ev_binds <- case m_ev_binds_var of - Just (EvBindsVar ref _) -> TcS.readTcRef ref - Nothing -> return emptyEvBindMap - ; let all_needs = neededEvVars ev_binds - (used_tcvs `unionVarSet` implic_needs) + = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var + ; let all_needs = neededEvVars ev_binds implic_needs dead_givens | warnRedundantGivens info = filterOut (`elemVarSet` all_needs) givens @@ -1333,9 +1328,14 @@ setImplicationStatus implic@(Implic { ic_binds = m_ev_binds_var , wc_impl = pruned_implics } } -- We can only prune the child implications (pruned_implics) -- in the IC_Solved status case, because only then we can - -- accumulate their needed evidence variales into the + -- accumulate their needed evidence variables into the -- IC_Solved final_status field of the parent implication. + -- Check that there are no term-level evidence bindings + -- in the cases where we have no place to put them + ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds) + , ppr info $$ ppr ev_binds ) + ; return $ if discard_entire_implication then Nothing else Just final_implic } @@ -1383,12 +1383,12 @@ warnRedundantGivens (SigSkol ctxt _) warnRedundantGivens (InstSkol {}) = True warnRedundantGivens _ = False -neededEvVars :: EvBindMap -> VarSet -> VarSet +neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet -- Find all the evidence variables that are "needed", -- and then delete all those bound by the evidence bindings --- See note [Tracking redundant constraints] -neededEvVars ev_binds initial_seeds - = needed `minusVarSet` bndrs +-- See Note [Tracking redundant constraints] +neededEvVars (ev_binds, tcvs) initial_seeds + = (needed `unionVarSet` tcvs) `minusVarSet` bndrs where seeds = foldEvBindMap add_wanted initial_seeds ev_binds needed = transCloVarSet also_needs seeds @@ -1457,8 +1457,8 @@ works: * When the constraint solver finishes solving all the wanteds in an implication, it sets its status to IC_Solved - - The ics_dead field, of IC_Solved, records the subset of this implication's - ic_given that are redundant (not needed). + - The ics_dead field, of IC_Solved, records the subset of this + implication's ic_given that are redundant (not needed). - The ics_need field of IC_Solved then records all the in-scope (given) evidence variables bound by the context, that @@ -1471,7 +1471,6 @@ works: a) it is free in the RHS of a Wanted EvBind, b) it is free in the RHS of an EvBind whose LHS is needed, c) it is in the ics_need of a nested implication. - d) it is listed in the tcs_used_tcvs field of the nested TcSEnv * We need to be careful not to discard an implication prematurely, even one that is fully solved, because we might @@ -2053,8 +2052,7 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds) = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ]) ; fake_ev_binds_var <- TcS.newTcEvBinds ; tclvl <- TcS.getTcLevel - ; (success, _) <- nestImplicTcS (Just fake_ev_binds_var) emptyVarSet - (pushTcLevel tclvl) try_group + ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group ; if success then -- Success: record the type variable binding, and return diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 5013f470da..159c6dca5c 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -24,13 +24,14 @@ module TcType ( TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet, TcKind, TcCoVar, TcTyCoVar, TcTyBinder, TcTyVarBinder, TcTyCon, - ExpType(..), ExpSigmaType, ExpRhoType, mkCheckExpType, + ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType, SyntaxOpType(..), synKnownType, mkSynFunTys, -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, sameDepthAs, fmvTcLevel, + tcTypeLevel, tcTyVarLevel, maxTcLevel, -------------------------------- -- MetaDetails @@ -40,7 +41,7 @@ module TcType ( isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isFskTyVar, isFmvTyVar, isFlattenTyVar, - isAmbiguousTyVar, metaTvRef, metaTyVarInfo, + isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, isTouchableMetaTyVar, isTouchableOrFmv, @@ -298,19 +299,30 @@ type TcDTyCoVarSet = DTyCoVarSet -- | An expected type to check against during type-checking. -- See Note [ExpType] in TcMType, where you'll also find manipulators. data ExpType = Check TcType - | Infer Unique -- for debugging only - TcLevel -- See Note [TcLevel of ExpType] in TcMType - Kind - (IORef (Maybe TcType)) + | Infer !InferResult + +data InferResult + = IR { ir_uniq :: Unique -- For debugging only + , ir_lvl :: TcLevel -- See Note [TcLevel of ExpType] in TcMType + , ir_inst :: Bool -- True <=> deeply instantiate before returning + -- i.e. return a RhoType + -- False <=> do not instantaite before returning + -- i.e. return a SigmaType + , ir_kind :: Kind + , ir_ref :: IORef (Maybe TcType) } type ExpSigmaType = ExpType type ExpRhoType = ExpType instance Outputable ExpType where - ppr (Check ty) = ppr ty - ppr (Infer u lvl ki _) - = parens (text "Infer" <> braces (ppr u <> comma <> ppr lvl) - <+> dcolon <+> ppr ki) + ppr (Check ty) = text "Check" <> braces (ppr ty) + ppr (Infer ir) = ppr ir + +instance Outputable InferResult where + ppr (IR { ir_uniq = u, ir_lvl = lvl + , ir_kind = ki, ir_inst = inst }) + = text "Infer" <> braces (ppr u <> comma <> ppr lvl <+> ppr inst) + <+> dcolon <+> ppr ki -- | Make an 'ExpType' suitable for checking. mkCheckExpType :: TcType -> ExpType @@ -420,6 +432,7 @@ we would need to enforce the separation. -- See Note [TyVars and TcTyVars] data TcTyVarDetails = SkolemTv -- A skolem + TcLevel -- Level of the implication that binds it Bool -- True <=> this skolem type variable can be overlapped -- when looking up instances -- See Note [Binding when looking up instances] in InstEnv @@ -437,8 +450,8 @@ data TcTyVarDetails vanillaSkolemTv, superSkolemTv :: TcTyVarDetails -- See Note [Binding when looking up instances] in InstEnv -vanillaSkolemTv = SkolemTv False -- Might be instantiated -superSkolemTv = SkolemTv True -- Treat this as a completely distinct type +vanillaSkolemTv = SkolemTv (pushTcLevel topTcLevel) False -- Might be instantiated +superSkolemTv = SkolemTv (pushTcLevel topTcLevel) True -- Treat this as a completely distinct type ----------------------------- data MetaDetails @@ -467,10 +480,10 @@ instance Outputable MetaDetails where pprTcTyVarDetails :: TcTyVarDetails -> SDoc -- For debugging -pprTcTyVarDetails (SkolemTv True) = text "ssk" -pprTcTyVarDetails (SkolemTv False) = text "sk" pprTcTyVarDetails (RuntimeUnk {}) = text "rt" pprTcTyVarDetails (FlatSkol {}) = text "fsk" +pprTcTyVarDetails (SkolemTv lvl True) = text "ssk" <> colon <> ppr lvl +pprTcTyVarDetails (SkolemTv lvl False) = text "sk" <> colon <> ppr lvl pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl }) = pp_info <> colon <> ppr tclvl where @@ -655,6 +668,9 @@ We arrange the TcLevels like this The flatten meta-vars are all at level 0, just to make them untouchable. -} +maxTcLevel :: TcLevel -> TcLevel -> TcLevel +maxTcLevel (TcLevel a) (TcLevel b) = TcLevel (a `max` b) + fmvTcLevel :: TcLevel -> TcLevel -- See Note [TcLevel assignment] fmvTcLevel _ = TcLevel 0 @@ -685,6 +701,24 @@ checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) = ctxt_tclvl >= tv_tclvl +tcTyVarLevel :: TcTyVar -> TcLevel +tcTyVarLevel tv + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + MetaTv { mtv_tclvl = tv_lvl } -> tv_lvl + SkolemTv tv_lvl _ -> tv_lvl + FlatSkol ty -> tcTypeLevel ty + RuntimeUnk -> topTcLevel + +tcTypeLevel :: TcType -> TcLevel +-- Max level of any free var of the type +tcTypeLevel ty + = foldDVarSet add topTcLevel (tyCoVarsOfTypeDSet ty) + where + add v lvl + | isTcTyVar v = lvl `maxTcLevel` tcTyVarLevel v + | otherwise = lvl + instance Outputable TcLevel where ppr (TcLevel us) = ppr us @@ -1034,8 +1068,8 @@ isSkolemTyVar tv isOverlappableTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) case tcTyVarDetails tv of - SkolemTv overlappable -> overlappable - _ -> False + SkolemTv _ overlappable -> overlappable + _ -> False isMetaTyVar tv = ASSERT2( isTcTyVar tv, ppr tv ) @@ -1076,6 +1110,12 @@ metaTyVarTcLevel_maybe tv MetaTv { mtv_tclvl = tclvl } -> Just tclvl _ -> Nothing +metaTyVarRef :: TyVar -> IORef MetaDetails +metaTyVarRef tv + = case tcTyVarDetails tv of + MetaTv { mtv_ref = ref } -> ref + _ -> pprPanic "metaTyVarRef" (ppr tv) + setMetaTyVarTcLevel :: TcTyVar -> TcLevel -> TcTyVar setMetaTyVarTcLevel tv tclvl = case tcTyVarDetails tv of @@ -1088,12 +1128,6 @@ isSigTyVar tv MetaTv { mtv_info = SigTv } -> True _ -> False -metaTvRef :: TyVar -> IORef MetaDetails -metaTvRef tv - = case tcTyVarDetails tv of - MetaTv { mtv_ref = ref } -> ref - _ -> pprPanic "metaTvRef" (ppr tv) - isFlexi, isIndirect :: MetaDetails -> Bool isFlexi Flexi = True isFlexi _ = False diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 2712c4a5c5..4b0b749ab0 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -6,23 +6,23 @@ Type subsumption and unification -} -{-# LANGUAGE CPP, MultiWayIf, TupleSections #-} +{-# LANGUAGE CPP, MultiWayIf, TupleSections, ScopedTypeVariables #-} module TcUnify ( -- Full-blown subsumption tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, - tcSubTypeHR, tcSubType, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O, - tcSubTypeDS_NC, tcSubTypeDS_NC_O, tcSubTypeET, tcSubTypeET_NC, + tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, + tcSubTypeDS_NC_O, tcSubTypeET, checkConstraints, buildImplicationFor, -- Various unifications unifyType, unifyTheta, unifyKind, noThing, - uType, unifyExpType, + uType, swapOverTyVars, canSolveByUnification, -------------------------------- -- Holes - tcInfer, + tcInferInst, tcInferNoInst, matchExpectedListTy, matchExpectedPArrTy, matchExpectedTyConApp, @@ -112,14 +112,15 @@ passed in. -} -- Use this one when you have an "expected" type. -matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] +matchExpectedFunTys :: forall a. + SDoc -- See Note [Herald for matchExpectedFunTys] -> Arity -> ExpRhoType -- deeply skolemised -> ([ExpSigmaType] -> ExpRhoType -> TcM a) -- must fill in these ExpTypes here -> TcM (a, HsWrapper) -- If matchExpectedFunTys n ty = (_, wrap) --- then wrap : (t1 -> ... -> tn -> ty_r) "->" ty, +-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside matchExpectedFunTys herald arity orig_ty thing_inside = case orig_ty of @@ -166,14 +167,16 @@ matchExpectedFunTys herald arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ + defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper) defer acc_arg_tys n fun_ty - = do { more_arg_tys <- replicateM n newOpenInferExpType - ; res_ty <- newOpenInferExpType + = do { more_arg_tys <- replicateM n newInferExpTypeNoInst + ; res_ty <- newInferExpTypeInst ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkFunTys more_arg_tys res_ty - ; wrap <- tcSubTypeDS GenSigCtxt noThing unif_fun_ty fun_ty + ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty + -- Not a good origin at all :-( ; return (result, wrap) } ------------ @@ -198,7 +201,7 @@ matchActualFunTys :: Outputable a -> TcSigmaType -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) -- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) --- then wrap : ty "->" (t1 -> ... -> tn -> ty_r) +-- then wrap : ty ~> (t1 -> ... -> tn -> ty_r) matchActualFunTys herald ct_orig mb_thing arity ty = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity @@ -523,82 +526,36 @@ tcSubTypeHR :: Outputable a -> TcSigmaType -> ExpRhoType -> TcM HsWrapper tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt -tcSubType :: Outputable a - => UserTypeCtxt -> Maybe a -- ^ If present, it has type ty_actual - -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper --- Checks that actual <= expected --- Returns HsWrapper :: actual ~ expected -tcSubType ctxt maybe_thing ty_actual ty_expected - = tcSubTypeO origin ctxt ty_actual ty_expected - where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = mkErrorThing <$> maybe_thing } - - --- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type. --- You probably want this only when looking at patterns, never expressions. -tcSubTypeET :: CtOrigin -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -tcSubTypeET orig ty_actual ty_expected - = uExpTypeX orig ty_expected ty_actual - (return . mkWpCastN . mkTcSymCo) - (\ty_a -> tcSubTypeO orig GenSigCtxt ty_a - (mkCheckExpType ty_expected)) - --- | This is like 'tcSubType' but accepts an 'ExpType' as the /actual/ type. --- You probably want this only when looking at patterns, never expressions. --- Does not add context. -tcSubTypeET_NC :: UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper -tcSubTypeET_NC _ ty_actual@(Infer {}) ty_expected - = mkWpCastN . mkTcSymCo <$> unifyExpType noThing ty_expected ty_actual -tcSubTypeET_NC ctxt (Check ty_actual) ty_expected - = tc_sub_type orig orig ctxt ty_actual ty_expected' +------------------------ +tcSubTypeET :: CtOrigin -> UserTypeCtxt + -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper +-- If wrap = tc_sub_type_et t1 t2 +-- => wrap :: t1 ~> t2 +tcSubTypeET orig ctxt (Check ty_actual) ty_expected + = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected where - ty_expected' = mkCheckExpType ty_expected - orig = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected' - , uo_thing = Nothing } + eq_orig = TypeEqOrigin { uo_actual = ty_expected + , uo_expected = ty_actual + , uo_thing = Nothing } +tcSubTypeET _ _ (Infer inf_res) ty_expected + = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected ) + do { co <- fillInferResult ty_expected inf_res + ; return (mkWpCastN (mkTcSymCo co)) } + +------------------------ tcSubTypeO :: CtOrigin -- ^ of the actual type -> UserTypeCtxt -- ^ of the expected type -> TcSigmaType - -> ExpSigmaType + -> ExpRhoType -> TcM HsWrapper -tcSubTypeO origin ctxt ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubType" (vcat [ pprCtOrigin origin - , pprUserTypeCtxt ctxt - , ppr ty_actual - , ppr ty_expected ]) - ; tc_sub_type eq_orig origin ctxt ty_actual ty_expected } - where - eq_orig | TypeEqOrigin {} <- origin = origin - | otherwise - = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = Nothing } - -tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a -- ^ has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised (hence "DS") -tcSubTypeDS ctxt m_expr ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected - --- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating --- the "actual" type -tcSubTypeDS_O :: Outputable a - => CtOrigin -> UserTypeCtxt - -> Maybe a -> TcSigmaType -> ExpRhoType - -> TcM HsWrapper -tcSubTypeDS_O orig ctxt maybe_thing ty_actual ty_expected +tcSubTypeO orig ctxt ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig , pprUserTypeCtxt ctxt , ppr ty_actual , ppr ty_expected ]) - ; tcSubTypeDS_NC_O orig ctxt maybe_thing ty_actual ty_expected } + ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a addSubTypeCtxt ty_actual ty_expected thing_inside @@ -628,26 +585,24 @@ addSubTypeCtxt ty_actual ty_expected thing_inside -- The "_NC" variants do not add a typechecker-error context; -- the caller is assumed to do that -tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper +tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- Checks that actual <= expected +-- Returns HsWrapper :: actual ~ expected tcSubType_NC ctxt ty_actual ty_expected = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_type origin origin ctxt ty_actual ty_expected } + ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected } where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected , uo_thing = Nothing } -tcSubTypeDS_NC :: Outputable a - => UserTypeCtxt - -> Maybe a -- ^ If present, this has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected - = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected } - where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = mkErrorThing <$> maybe_thing } +tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper +-- Just like tcSubType, but with the additional precondition that +-- ty_expected is deeply skolemised (hence "DS") +tcSubTypeDS orig ctxt ty_actual ty_expected + = addSubTypeCtxt ty_actual ty_expected $ + do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) + ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } tcSubTypeDS_NC_O :: Outputable a => CtOrigin -- origin used for instantiation only @@ -656,56 +611,72 @@ tcSubTypeDS_NC_O :: Outputable a -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that -- ty_expected is deeply skolemised -tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual et - = uExpTypeX eq_orig ty_actual et - (return . mkWpCastN) - (tc_sub_type_ds eq_orig inst_orig ctxt ty_actual) - where - eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = et - , uo_thing = mkErrorThing <$> m_thing } +tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected + = case ty_expected of + Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res + Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty + where + eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty + , uo_thing = mkErrorThing <$> m_thing } --------------- -tc_sub_type :: CtOrigin -- origin used when calling uType - -> CtOrigin -- origin used when instantiating - -> UserTypeCtxt -> TcSigmaType -> ExpSigmaType -> TcM HsWrapper -tc_sub_type eq_orig inst_orig ctxt ty_actual et - = uExpTypeX eq_orig ty_actual et - (return . mkWpCastN) - (tc_sub_tc_type eq_orig inst_orig ctxt ty_actual) - tc_sub_tc_type :: CtOrigin -- used when calling uType -> CtOrigin -- used when instantiating -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- If wrap = tc_sub_type t1 t2 +-- => wrap :: t1 ~> t2 tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected - | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types] - = do { lookup_res <- lookupTcTyVar tv_actual - ; case lookup_res of - Filled ty_actual' -> tc_sub_tc_type eq_orig inst_orig - ctxt ty_actual' ty_expected - - -- It's tempting to see if tv_actual can unify with a polytype - -- and, if so, call uType; otherwise, skolemise first. But this - -- is wrong, because skolemising will bump the TcLevel and the - -- unification will fail anyway. - -- It's also tempting to call uUnfilledVar directly, but calling - -- uType seems safer in the presence of possible refactoring - -- later. - Unfilled _ -> mkWpCastN <$> - uType eq_orig TypeLevel ty_actual ty_expected } - - | otherwise -- See Note [Deep skolemisation] - = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ - \ _ sk_rho -> + | is_poly ty_expected -- See Note [Don't skolemise unnecessarily] + , not (is_poly ty_actual) + = do { traceTc "tc_sub_tc_type (drop to equality)" $ + vcat [ text "ty_actual =" <+> ppr ty_actual + , text "ty_expected =" <+> ppr ty_expected ] + ; mkWpCastN <$> + uType eq_orig TypeLevel ty_actual ty_expected } + + | otherwise -- This is the general case + = do { traceTc "tc_sub_tc_type (general case)" $ + vcat [ text "ty_actual =" <+> ppr ty_actual + , text "ty_expected =" <+> ppr ty_expected ] + ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ + \ _ sk_rho -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual sk_rho ; return (sk_wrap <.> inner_wrap) } + where + is_poly ty + | isForAllTy ty = True + | Just (_, res) <- splitFunTy_maybe ty = is_poly res + | otherwise = False + -- NB *not* tcSplitFunTy, because here we want + -- to decompose type-class arguments too + + +{- Note [Don't skolemise unnecessarily] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are trying to solve + (Char->Char) <= (forall a. a->a) +We could skolemise the 'forall a', and then complain +that (Char ~ a) is insoluble; but that's a pretty obscure +error. It's better to say that + (Char->Char) ~ (forall a. a->a) +fails. + +In general, + * if the RHS type an outermost forall (i.e. skolemisation + is the next thing we'd do) + * and the LHS has no top-level polymorphism (but looking deeply) +then we can revert to simple equality. +-} --------------- tc_sub_type_ds :: CtOrigin -- used when calling uType -> CtOrigin -- used when instantiating -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised +-- If wrap = tc_sub_type_ds t1 t2 +-- => wrap :: t1 ~> t2 +-- Here is where the work actually happens! +-- Precondition: ty_expected is deeply skolemised tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected = go ty_actual ty_expected where @@ -739,8 +710,8 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected (SigSkol GenSigCtxt exp_arg)) ctxt exp_arg act_arg ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) } - -- arg_wrap :: exp_arg ~ act_arg - -- res_wrap :: act-res ~ exp_res + -- arg_wrap :: exp_arg ~> act_arg + -- res_wrap :: act-res ~> exp_res go ty_a ty_e | let (tvs, theta, _) = tcSplitSigmaTy ty_a @@ -748,8 +719,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a ; body_wrap <- tc_sub_type_ds (eq_orig { uo_actual = in_rho - , uo_expected = - mkCheckExpType ty_expected }) + , uo_expected = ty_expected }) inst_orig ctxt in_rho ty_e ; return (body_wrap <.> in_wrap) } @@ -815,23 +785,124 @@ wrapFunResCoercion arg_tys co_fn_res = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) } ------------------------------------ + +{- ********************************************************************** +%* * + ExpType functions: tcInfer, fillInferResult +%* * +%********************************************************************* -} + -- | Infer a type using a fresh ExpType -- See also Note [ExpType] in TcMType -tcInfer :: (ExpRhoType -> TcM a) -> TcM (a, TcType) -tcInfer tc_check - = do { res_ty <- newOpenInferExpType +-- Does not attempt to instantiate the inferred type +tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tcInferNoInst = tcInfer False + +tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType) +tcInferInst = tcInfer True + +tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) +tcInfer instantiate tc_check + = do { res_ty <- newInferExpType instantiate ; result <- tc_check res_ty ; res_ty <- readExpType res_ty ; return (result, res_ty) } -{- -************************************************************************ +fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper +-- If wrap = fillInferResult_Inst t1 t2 +-- => wrap :: t1 ~> t2 +-- See Note [Deep instantiation of InferResult] +fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me }) + | instantiate_me + = do { (wrap, rho) <- deeplyInstantiate orig ty + ; co <- fillInferResult rho inf_res + ; return (mkWpCastN co <.> wrap) } + + | otherwise + = do { co <- fillInferResult ty inf_res + ; return (mkWpCastN co) } + +fillInferResult :: TcType -> InferResult -> TcM TcCoercionN +-- If wrap = fillInferResult t1 t2 +-- => wrap :: t1 ~> t2 +fillInferResult ty (IR { ir_uniq = u, ir_lvl = res_lvl + , ir_kind = res_kind, ir_ref = ref }) + = do { (ty_co, ty) <- promoteTcType res_lvl ty + ; ki_co <- uType kind_orig KindLevel ty_kind res_kind + ; let ty_to_fill_with = ty `mkCastTy` ki_co + co = ty_co `mkTcCoherenceRightCo` ki_co + + ; when debugIsOn (check_hole ty_to_fill_with) + + ; traceTc "Filling ExpType" $ + ppr u <+> text ":=" <+> ppr ty_to_fill_with + + ; writeTcRef ref (Just ty) + + ; return co } + where + ty_kind = typeKind ty + kind_orig = TypeEqOrigin { uo_actual = ty_kind + , uo_expected = res_kind + , uo_thing = Nothing } + + check_hole ty -- Debug check only + = do { ki1 <- zonkTcType (typeKind ty) + ; ki2 <- zonkTcType res_kind + ; MASSERT2( ki1 `eqType` ki2, ppr ki1 $$ ppr ki2 $$ ppr u ) + ; let ty_lvl = tcTypeLevel ty + ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), + ppr u $$ ppr res_lvl $$ ppr ty_lvl ) + ; cts <- readTcRef ref + ; case cts of + Just already_there -> pprPanic "writeExpType" + (vcat [ ppr u + , ppr ty + , ppr already_there ]) + Nothing -> return () } + +{- Note [Deep instantiation of InferResult] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In some cases we want to deeply instantiate before filling in +an InferResult, and in some cases not. That's why InferReult +has the ir_inst flag. + +* ir_inst = True: deeply instantantiate + + 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 the monomorphism restriction won't 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. + + 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. + +* ir_inst = False: do not instantantiate + + Consider this (which uses visible type application): + + (let { f :: forall a. a -> a; f x = x } in f) @Int + + We'll call TcExpr.tcInferFun to infer the type of the (let .. in f) + And we don't want to instantite the type of 'f' when we reach it, + else the outer visible type application won't work +-} + +{- ********************************************************************* * * -\subsection{Generalisation} + Generalisation * * -************************************************************************ --} +********************************************************************* -} -- | Take an "expected type" and strip off quantifiers to expose the -- type underneath, binding the new skolems for the @thing_inside@. @@ -949,7 +1020,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted , ic_given = given , ic_wanted = wanted , ic_status = IC_Unsolved - , ic_binds = Just ev_binds_var + , ic_binds = ev_binds_var , ic_env = env , ic_info = skol_info } @@ -972,19 +1043,9 @@ unifyType :: Outputable a => Maybe a -- ^ If present, has type 'ty1' -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 = uType origin TypeLevel ty1 ty2 where - origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2 + origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 , uo_thing = mkErrorThing <$> thing } --- | Variant of 'unifyType' that takes an 'ExpType' as its second type -unifyExpType :: Outputable a => Maybe a - -> TcTauType -> ExpType -> TcM TcCoercionN -unifyExpType mb_thing ty1 ty2 - = uExpType ty_orig ty1 ty2 - where - ty_orig = TypeEqOrigin { uo_actual = ty1 - , uo_expected = ty2 - , uo_thing = mkErrorThing <$> mb_thing } - -- | Use this instead of 'Nothing' when calling 'unifyType' without -- a good "thing" (where the "thing" has the "actual" type passed in) -- This has an 'Outputable' instance, avoiding amgiguity problems. @@ -993,7 +1054,7 @@ noThing = Nothing unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN unifyKind thing ty1 ty2 = uType origin KindLevel ty1 ty2 - where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = mkCheckExpType ty2 + where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 , uo_thing = mkErrorThing <$> thing } --------------- @@ -1020,34 +1081,6 @@ unifyTheta theta1 theta2 uType is the heart of the unifier. -} -uExpType :: CtOrigin -> TcType -> ExpType -> TcM CoercionN -uExpType orig ty1 et - = uExpTypeX orig ty1 et return $ - uType orig TypeLevel ty1 - --- | Tries to unify with an ExpType. If the ExpType is filled in, calls the first --- continuation with the produced coercion. Otherwise, calls the second --- continuation. This can happen either with a Check or with an untouchable --- ExpType that reverts to a tau-type. See Note [TcLevel of ExpType] -uExpTypeX :: CtOrigin -> TcType -> ExpType - -> (TcCoercionN -> TcM a) -- Infer case, co :: TcType ~N ExpType - -> (TcType -> TcM a) -- Check / untouchable case - -> TcM a -uExpTypeX orig ty1 et@(Infer _ tc_lvl ki _) coercion_cont type_cont - = do { cur_lvl <- getTcLevel - ; if cur_lvl `sameDepthAs` tc_lvl - then do { ki_co <- uType kind_orig KindLevel (typeKind ty1) ki - ; writeExpType et (ty1 `mkCastTy` ki_co) - ; coercion_cont $ mkTcNomReflCo ty1 `mkTcCoherenceRightCo` ki_co } - else do { traceTc "Preventing writing to untouchable ExpType" empty - ; tau <- expTypeToType et -- See Note [TcLevel of ExpType] - ; type_cont tau }} - where - kind_orig = KindEqOrigin ty1 Nothing orig (Just TypeLevel) -uExpTypeX _ _ (Check ty2) _ type_cont - = type_cont ty2 - ------------- uType, uType_defer :: CtOrigin -> TypeOrKind @@ -1059,23 +1092,18 @@ uType, uType_defer -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] uType_defer origin t_or_k ty1 ty2 - = do { hole <- newCoercionHole - ; loc <- getCtLocM origin (Just t_or_k) - ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_dest = HoleDest hole - , ctev_pred = mkPrimEqPred ty1 ty2 - , ctev_loc = loc } + = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 -- Error trace only - -- NB. do *not* call mkErrInfo unless tracing is on, because - -- it is hugely expensive (#5631) + -- NB. do *not* call mkErrInfo unless tracing is on, + -- because it is hugely expensive (#5631) ; whenDOptM Opt_D_dump_tc_trace $ do { ctxt <- getErrCtxt ; doc <- mkErrInfo emptyTidyEnv ctxt - ; traceTc "utype_defer" (vcat [ppr hole, ppr ty1, + ; traceTc "utype_defer" (vcat [ppr co, ppr ty1, ppr ty2, pprCtOrigin origin, doc]) } - ; return (mkHoleCo hole Nominal ty1 ty2) } + ; return co } -------------- uType origin t_or_k orig_ty1 orig_ty2 @@ -1667,9 +1695,330 @@ matchExpectedFunKind num_args_remaining ty = go ; let new_fun = mkFunTy arg_kind res_kind thing = mkTypeErrorThingArgs ty num_args_remaining origin = TypeEqOrigin { uo_actual = k - , uo_expected = mkCheckExpType new_fun + , uo_expected = new_fun , uo_thing = Just thing } ; co <- uType origin KindLevel k new_fun ; return (co, arg_kind, res_kind) } - where + + +{- ********************************************************************* +* * + Occurrence checking +* * +********************************************************************* -} + + +{- Note [Occurs check expansion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid +of occurrences of tv outside type function arguments, if that is +possible; otherwise, it returns Nothing. + +For example, suppose we have + type F a b = [a] +Then + occCheckExpand b (F Int b) = Just [Int] +but + occCheckExpand a (F a Int) = Nothing + +We don't promise to do the absolute minimum amount of expanding +necessary, but we try not to do expansions we don't need to. We +prefer doing inner expansions first. For example, + type F a b = (a, Int, a, [a]) + type G b = Char +We have + occCheckExpand b (F (G b)) = Just (F Char) +even though we could also expand F to get rid of b. + +The two variants of the function are to support TcUnify.checkTauTvUpdate, +which wants to prevent unification with type families. For more on this +point, see Note [Prevent unification with type families] in TcUnify. + +Note [Occurrence checking: look inside kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we are considering unifying + (alpha :: *) ~ Int -> (beta :: alpha -> alpha) +This may be an error (what is that alpha doing inside beta's kind?), +but we must not make the mistake of actuallyy unifying or we'll +build an infinite data structure. So when looking for occurrences +of alpha in the rhs, we must look in the kinds of type variables +that occur there. + +NB: we may be able to remove the problem via expansion; see + Note [Occurs check expansion]. So we have to try that. + +Note [Checking for foralls] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Unless we have -XImpredicativeTypes (which is a totally unsupported +feature), we do not want to unify + alpha ~ (forall a. a->a) -> Int +So we look for foralls hidden inside the type, and it's convenient +to do that at the same time as the occurs check (which looks for +occurrences of alpha). + +However, it's not just a question of looking for foralls /anywhere/! +Consider + (alpha :: forall k. k->*) ~ (beta :: forall k. k->*) +This is legal; e.g. dependent/should_compile/T11635. + +We don't want to reject it because of the forall in beta's kind, +but (see Note [Occurrence checking: look inside kinds]) we do +need to look in beta's kind. So we carry a flag saying if a 'forall' +is OK, and sitch the flag on when stepping inside a kind. + +Why is it OK? Why does it not count as impredicative polymorphism? +The reason foralls are bad is because we reply on "seeing" foralls +when doing implicit instantiation. But the forall inside the kind is +fine. We'll generate a kind equality constraint + (forall k. k->*) ~ (forall k. k->*) +to check that the kinds of lhs and rhs are compatible. If alpha's +kind had instead been + (alpha :: kappa) +then this kind equality would rightly complain about unifying kappa +with (forall k. k->*) + +-} + +data OccCheckResult a + = OC_OK a + | OC_Bad -- Forall or type family + | OC_Occurs + +instance Functor OccCheckResult where + fmap = liftM + +instance Applicative OccCheckResult where + pure = OC_OK + (<*>) = ap + +instance Monad OccCheckResult where + OC_OK x >>= k = k x + OC_Bad >>= _ = OC_Bad + OC_Occurs >>= _ = OC_Occurs + +occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult () +-- Just for error-message generation; so we return OccCheckResult +-- so the caller can report the right kind of error +-- Check whether +-- a) the given variable occurs in the given type. +-- b) there is a forall in the type (unless we have -XImpredicativeTypes) +occCheckForErrors dflags tv ty + = case preCheck dflags True tv ty of + OC_OK _ -> OC_OK () + OC_Bad -> OC_Bad + OC_Occurs -> case occCheckExpand tv ty of + Nothing -> OC_Occurs + Just _ -> OC_OK () + +---------------- +metaTyVarUpdateOK :: DynFlags + -> TcTyVar -- tv :: k1 + -> TcType -- ty :: k2 + -> Maybe TcType -- possibly-expanded ty +-- (metaTyFVarUpdateOK tv ty) +-- We are about to update the meta-tyvar tv with ty, in +-- our on-the-flyh unifier +-- Check (a) that tv doesn't occur in ty (occurs check) +-- (b) that ty does not have any foralls +-- (in the impredicative case), or type functions +-- +-- We have two possible outcomes: +-- (1) Return the type to update the type variable with, +-- [we know the update is ok] +-- (2) Return Nothing, +-- [the update might be dodgy] +-- +-- Note that "Nothing" does not mean "definite error". For example +-- type family F a +-- type instance F Int = Int +-- consider +-- a ~ F a +-- This is perfectly reasonable, if we later get a ~ Int. For now, though, +-- we return Nothing, leaving it to the later constraint simplifier to +-- sort matters out. +-- +-- See Note [Refactoring hazard: checkTauTvUpdate] + +metaTyVarUpdateOK dflags tv ty + = case preCheck dflags False tv ty of + -- False <=> type families not ok + -- See Note [Prevent unification with type families] + OC_OK _ -> Just ty + OC_Bad -> Nothing -- forall or type function + OC_Occurs -> occCheckExpand tv ty + +preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult () +-- A quick check for +-- (a) a forall type (unless -XImpredivativeTypes) +-- (b) a type family +-- (c) an occurrence of the type variable (occurs check) +-- +-- For (a) and (b) we check only the top level of the type, NOT +-- inside the kinds of variables it mentions. But for (c) we do +-- look in the kinds of course. + +preCheck dflags ty_fam_ok tv ty + = fast_check ty + where + details = tcTyVarDetails tv + impredicative_ok = canUnifyWithPolyType dflags details + + ok :: OccCheckResult () + ok = OC_OK () + + fast_check :: TcType -> OccCheckResult () + fast_check (TyVarTy tv') + | tv == tv' = OC_Occurs + | otherwise = fast_check_occ (tyVarKind tv') + -- See Note [Occurrence checking: look inside kinds] + + fast_check (TyConApp tc tys) + | bad_tc tc = OC_Bad + | otherwise = mapM fast_check tys >> ok + fast_check (LitTy {}) = ok + fast_check (FunTy a r) = fast_check a >> fast_check r + fast_check (AppTy fun arg) = fast_check fun >> fast_check arg + fast_check (CastTy ty co) = fast_check ty >> fast_check_co co + fast_check (CoercionTy co) = fast_check_co co + fast_check (ForAllTy (TvBndr tv' _) ty) + | not impredicative_ok = OC_Bad + | tv == tv' = ok + | otherwise = do { fast_check_occ (tyVarKind tv') + ; fast_check_occ ty } + -- Under a forall we look only for occurrences of + -- the type variable + + -- For kinds, we only do an occurs check; we do not worry + -- about type families or foralls + -- See Note [Checking for foralls] + fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs + | otherwise = ok + + -- For coercions, we are only doing an occurs check here; + -- no bother about impredicativity in coercions, as they're + -- inferred + fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs + | otherwise = ok + + bad_tc :: TyCon -> Bool + bad_tc tc + | not (impredicative_ok || isTauTyCon tc) = True + | not (ty_fam_ok || isFamFreeTyCon tc) = True + | otherwise = False + +occCheckExpand :: TcTyVar -> TcType -> Maybe TcType +-- See Note [Occurs check expansion] +-- We may have needed to do some type synonym unfolding in order to +-- get rid of the variable (or forall), so we also return the unfolded +-- version of the type, which is guaranteed to be syntactically free +-- of the given type variable. If the type is already syntactically +-- free of the variable, then the same type is returned. +occCheckExpand tv ty + = go emptyVarEnv ty + where + go :: VarEnv TyVar -> Type -> Maybe Type + -- The VarEnv carries mappings necessary + -- because of kind expansion + go env (TyVarTy tv') + | tv == tv' = Nothing + | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'') + | otherwise = do { k' <- go env (tyVarKind tv') + ; return (mkTyVarTy $ + setTyVarKind tv' k') } + -- See Note [Occurrence checking: look inside kinds] + + go _ ty@(LitTy {}) = return ty + go env (AppTy ty1 ty2) = do { ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkAppTy ty1' ty2') } + go env (FunTy ty1 ty2) = do { ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkFunTy ty1' ty2') } + go env ty@(ForAllTy (TvBndr tv' vis) body_ty) + | tv == tv' = return ty + | otherwise = do { ki' <- go env (tyVarKind tv') + ; let tv'' = setTyVarKind tv' ki' + env' = extendVarEnv env tv' tv'' + ; body' <- go env' body_ty + ; return (ForAllTy (TvBndr tv'' vis) body') } + + -- For a type constructor application, first try expanding away the + -- offending variable from the arguments. If that doesn't work, next + -- see if the type constructor is a type synonym, and if so, expand + -- it and try again. + go env ty@(TyConApp tc tys) + = case mapM (go env) tys of + Just tys' -> return (mkTyConApp tc tys') + Nothing | Just ty' <- coreView ty -> go env ty' + | otherwise -> Nothing + -- Failing that, try to expand a synonym + + go env (CastTy ty co) = do { ty' <- go env ty + ; co' <- go_co env co + ; return (mkCastTy ty' co') } + go env (CoercionTy co) = do { co' <- go_co env co + ; return (mkCoercionTy co') } + + ------------------ + go_co env (Refl r ty) = do { ty' <- go env ty + ; return (mkReflCo r ty') } + -- Note: Coercions do not contain type synonyms + go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args + ; return (mkTyConAppCo r tc args') } + go_co env (AppCo co arg) = do { co' <- go_co env co + ; arg' <- go_co env arg + ; return (mkAppCo co' arg') } + go_co env co@(ForAllCo tv' kind_co body_co) + | tv == tv' = return co + | otherwise = do { kind_co' <- go_co env kind_co + ; let tv'' = setTyVarKind tv' $ + pFst (coercionKind kind_co') + env' = extendVarEnv env tv' tv'' + ; body' <- go_co env' body_co + ; return (ForAllCo tv'' kind_co' body') } + go_co env (CoVarCo c) = do { k' <- go env (varType c) + ; return (mkCoVarCo (setVarType c k')) } + go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args + ; return (mkAxiomInstCo ax ind args') } + go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p + ; ty1' <- go env ty1 + ; ty2' <- go env ty2 + ; return (mkUnivCo p' r ty1' ty2') } + go_co env (SymCo co) = do { co' <- go_co env co + ; return (mkSymCo co') } + go_co env (TransCo co1 co2) = do { co1' <- go_co env co1 + ; co2' <- go_co env co2 + ; return (mkTransCo co1' co2') } + go_co env (NthCo n co) = do { co' <- go_co env co + ; return (mkNthCo n co') } + go_co env (LRCo lr co) = do { co' <- go_co env co + ; return (mkLRCo lr co') } + go_co env (InstCo co arg) = do { co' <- go_co env co + ; arg' <- go_co env arg + ; return (mkInstCo co' arg') } + go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1 + ; co2' <- go_co env co2 + ; return (mkCoherenceCo co1' co2') } + go_co env (KindCo co) = do { co' <- go_co env co + ; return (mkKindCo co') } + go_co env (SubCo co) = do { co' <- go_co env co + ; return (mkSubCo co') } + go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs + ; return (mkAxiomRuleCo ax cs') } + + ------------------ + go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv + go_prov env (PhantomProv co) = PhantomProv <$> go_co env co + go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co + go_prov _ p@(PluginProv _) = return p + go_prov _ p@(HoleProv _) = return p + +canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool +canUnifyWithPolyType dflags details + = case details of + MetaTv { mtv_info = SigTv } -> False + MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags + _other -> True + -- We can have non-meta tyvars in given constraints + diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 49767fe1a8..31859e1a1c 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -206,7 +206,7 @@ checkAmbiguity ctxt ty ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $ captureConstraints $ - tcSubType_NC ctxt ty (mkCheckExpType ty) + tcSubType_NC ctxt ty ty ; simplifyAmbiguityCheck ty wanted ; traceTc "Done ambiguity check for" (ppr ty) } diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 1765ff5fe7..bf92c37034 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -1270,11 +1270,13 @@ splitForAllTyVarBndrs ty = split ty ty [] -- | Checks whether this is a proper forall (with a named binder) isForAllTy :: Type -> Bool +isForAllTy ty | Just ty' <- coreView ty = isForAllTy ty' isForAllTy (ForAllTy {}) = True isForAllTy _ = False -- | Is this a function or forall? isPiTy :: Type -> Bool +isPiTy ty | Just ty' <- coreView ty = isForAllTy ty' isPiTy (ForAllTy {}) = True isPiTy (FunTy {}) = True isPiTy _ = False diff --git a/compiler/vectorise/Vectorise/Generic/PData.hs b/compiler/vectorise/Vectorise/Generic/PData.hs index d4abeae51b..e5b94b1f38 100644 --- a/compiler/vectorise/Vectorise/Generic/PData.hs +++ b/compiler/vectorise/Vectorise/Generic/PData.hs @@ -44,7 +44,7 @@ buildDataFamInst :: Name -> TyCon -> TyCon -> AlgTyConRhs -> VM FamInst buildDataFamInst name' fam_tc vect_tc rhs = do { axiom_name <- mkDerivedName mkInstTyCoOcc name' - ; (_, tyvars') <- liftDs $ tcInstSigTyVars (getSrcSpan name') tyvars + ; (_, tyvars') <- liftDs $ freshenTyVarBndrs tyvars ; let ax = mkSingleCoAxiom Representational axiom_name tyvars' [] fam_tc pat_tys rep_ty tys' = mkTyVarTys tyvars' rep_ty = mkTyConApp rep_tc tys' diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr index 20f04d01e7..6f9e16f2b4 100644 --- a/testsuite/tests/ado/ado004.stderr +++ b/testsuite/tests/ado/ado004.stderr @@ -30,9 +30,9 @@ TYPE SIGNATURES (Num t, Monad m) => (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1 test6 :: - forall a (m :: * -> *) t. + forall a (m :: * -> *) p. (Num (m a), Monad m) => - (m a -> m (m a)) -> t -> m a + (m a -> m (m a)) -> p -> m a TYPE CONSTRUCTORS COERCION AXIOMS Dependent modules: [] diff --git a/testsuite/tests/annotations/should_fail/annfail10.stderr b/testsuite/tests/annotations/should_fail/annfail10.stderr index 6782f27228..6e7732f938 100644 --- a/testsuite/tests/annotations/should_fail/annfail10.stderr +++ b/testsuite/tests/annotations/should_fail/annfail10.stderr @@ -1,8 +1,8 @@ annfail10.hs:9:1: error: - • Ambiguous type variable ‘t0’ arising from an annotation - prevents the constraint ‘(Data.Data.Data t0)’ from being solved. - Probable fix: use a type annotation to specify what ‘t0’ should be. + • Ambiguous type variable ‘p0’ arising from an annotation + prevents the constraint ‘(Data.Data.Data p0)’ from being solved. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instances exist: instance (Data.Data.Data a, Data.Data.Data b) => Data.Data.Data (Either a b) @@ -15,9 +15,9 @@ annfail10.hs:9:1: error: • In the annotation: {-# ANN f 1 #-} annfail10.hs:9:11: error: - • Ambiguous type variable ‘t0’ arising from the literal ‘1’ - prevents the constraint ‘(Num t0)’ from being solved. - Probable fix: use a type annotation to specify what ‘t0’ should be. + • Ambiguous type variable ‘p0’ arising from the literal ‘1’ + prevents the constraint ‘(Num p0)’ from being solved. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instances exist: instance Num Integer -- Defined in ‘GHC.Num’ instance Num Double -- Defined in ‘GHC.Float’ diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr index b5a5f1d349..770135a338 100644 --- a/testsuite/tests/driver/T2182.stderr +++ b/testsuite/tests/driver/T2182.stderr @@ -1,24 +1,24 @@ T2182.hs:5:5: error: - No instance for (Show (t1 -> t1)) arising from a use of ‘show’ - (maybe you haven't applied a function to enough arguments?) - In the expression: show (\ x -> x) - In an equation for ‘y’: y = show (\ x -> x) + • No instance for (Show (p1 -> p1)) arising from a use of ‘show’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: show (\ x -> x) + In an equation for ‘y’: y = show (\ x -> x) T2182.hs:6:5: error: - No instance for (Eq (t0 -> t0)) arising from a use of ‘==’ - (maybe you haven't applied a function to enough arguments?) - In the expression: (\ x -> x) == (\ y -> y) - In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) + • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: (\ x -> x) == (\ y -> y) + In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) T2182.hs:5:5: error: - No instance for (Show (t1 -> t1)) arising from a use of ‘show’ - (maybe you haven't applied a function to enough arguments?) - In the expression: show (\ x -> x) - In an equation for ‘y’: y = show (\ x -> x) + • No instance for (Show (p1 -> p1)) arising from a use of ‘show’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: show (\ x -> x) + In an equation for ‘y’: y = show (\ x -> x) T2182.hs:6:5: error: - No instance for (Eq (t0 -> t0)) arising from a use of ‘==’ - (maybe you haven't applied a function to enough arguments?) - In the expression: (\ x -> x) == (\ y -> y) - In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) + • No instance for (Eq (p0 -> p0)) arising from a use of ‘==’ + (maybe you haven't applied a function to enough arguments?) + • In the expression: (\ x -> x) == (\ y -> y) + In an equation for ‘z’: z = (\ x -> x) == (\ y -> y) diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr index 056d451a09..41322f9cbc 100644 --- a/testsuite/tests/gadt/gadt-escape1.stderr +++ b/testsuite/tests/gadt/gadt-escape1.stderr @@ -1,19 +1,19 @@ gadt-escape1.hs:19:58: error: - • Couldn't match type ‘t’ with ‘ExpGADT Int’ - ‘t’ is untouchable - inside the constraints: t1 ~ Int + • Couldn't match type ‘p’ with ‘ExpGADT Int’ + ‘p’ is untouchable + inside the constraints: t ~ Int bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int, in a case alternative at gadt-escape1.hs:19:43-50 - ‘t’ is a rigid type variable bound by - the inferred type of weird1 :: t at gadt-escape1.hs:19:1-58 + ‘p’ is a rigid type variable bound by + the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58 Possible fix: add a type signature for ‘weird1’ - Expected type: t - Actual type: ExpGADT t1 + Expected type: p + Actual type: ExpGADT t • In the expression: a In a case alternative: Hidden (ExpInt _) a -> a In the expression: case (hval :: Hidden) of { Hidden (ExpInt _) a -> a } • Relevant bindings include - weird1 :: t (bound at gadt-escape1.hs:19:1) + weird1 :: p (bound at gadt-escape1.hs:19:1) diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr index e304430b51..6673ff68b0 100644 --- a/testsuite/tests/gadt/gadt13.stderr +++ b/testsuite/tests/gadt/gadt13.stderr @@ -1,17 +1,17 @@ gadt13.hs:15:13: error: - • Couldn't match expected type ‘t’ + • Couldn't match expected type ‘p’ with actual type ‘String -> [Char]’ - ‘t’ is untouchable + ‘p’ is untouchable inside the constraints: a ~ Int bound by a pattern with constructor: I :: Int -> Term Int, in an equation for ‘shw’ at gadt13.hs:15:6-8 - ‘t’ is a rigid type variable bound by - the inferred type of shw :: Term a -> t at gadt13.hs:15:1-30 + ‘p’ is a rigid type variable bound by + the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30 Possible fix: add a type signature for ‘shw’ • Possible cause: ‘(.)’ is applied to too many arguments In the expression: ("I " ++) . shows t In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t • Relevant bindings include - shw :: Term a -> t (bound at gadt13.hs:15:1) + shw :: Term a -> p (bound at gadt13.hs:15:1) diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr index e66226eaea..f75e8c5bff 100644 --- a/testsuite/tests/gadt/gadt7.stderr +++ b/testsuite/tests/gadt/gadt7.stderr @@ -1,20 +1,20 @@ gadt7.hs:16:38: error: - • Couldn't match expected type ‘t’ with actual type ‘t1’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘p1’ + ‘p1’ is untouchable inside the constraints: a ~ Int bound by a pattern with constructor: K :: T Int, in a case alternative at gadt7.hs:16:33 - ‘t’ is a rigid type variable bound by - the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44 - ‘t1’ is a rigid type variable bound by - the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44 + ‘p1’ is a rigid type variable bound by + the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44 + ‘p’ is a rigid type variable bound by + the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44 Possible fix: add a type signature for ‘i1b’ • In the expression: y1 In a case alternative: K -> y1 In the expression: case t1 of { K -> y1 } • Relevant bindings include - y1 :: t1 (bound at gadt7.hs:16:16) - y :: t1 (bound at gadt7.hs:16:7) - i1b :: T a -> t1 -> t (bound at gadt7.hs:16:1) + y1 :: p1 (bound at gadt7.hs:16:16) + y :: p1 (bound at gadt7.hs:16:7) + i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1) diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout index 904f0cd3e8..2e86b42713 100644 --- a/testsuite/tests/ghci.debugger/scripts/break012.stdout +++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout @@ -1,14 +1,14 @@ Stopped in Main.g, break012.hs:5:10-18 -_result :: (t, a1 -> a1, (), a -> a -> a) = _ -a :: t = _ +_result :: (p, a1 -> a1, (), a -> a -> a) = _ +a :: p = _ b :: a2 -> a2 = _ c :: () = _ d :: a -> a -> a = _ -a :: t +a :: p b :: a2 -> a2 c :: () d :: a -> a -> a -a = (_t1::t) +a = (_t1::p) b = (_t2::a2 -> a2) c = (_t3::()) d = (_t4::a -> a -> a) diff --git a/testsuite/tests/ghci.debugger/scripts/print022.stdout b/testsuite/tests/ghci.debugger/scripts/print022.stdout index 40d2b59544..5d81c044c4 100644 --- a/testsuite/tests/ghci.debugger/scripts/print022.stdout +++ b/testsuite/tests/ghci.debugger/scripts/print022.stdout @@ -2,7 +2,7 @@ test = C 1 32 1.2 1.23 'x' 1 1.2 1.23 Breakpoint 0 activated at print022.hs:11:7 Stopped in Main.f, print022.hs:11:7 -_result :: t = _ -x :: t = _ +_result :: p = _ +x :: p = _ x = C2 1 (W# 32) (TwoFields 'a' 3) x :: T2 diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout index 164e0cf256..27122574e9 100644 --- a/testsuite/tests/ghci/scripts/T11524a.stdout +++ b/testsuite/tests/ghci/scripts/T11524a.stdout @@ -2,7 +2,7 @@ without -fprint-explicit-foralls ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ pattern P :: Bool -- Defined at <interactive>:16:1 pattern Pe :: a -> Ex -- Defined at <interactive>:17:1 -pattern Pu :: t -> t -- Defined at <interactive>:18:1 +pattern Pu :: p -> p -- Defined at <interactive>:18:1 pattern Pue :: a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1 pattern Pur :: (Num a, Eq a) => a -> [a] -- Defined at <interactive>:20:1 @@ -26,7 +26,7 @@ with -fprint-explicit-foralls pattern P :: Bool -- Defined at <interactive>:16:1 pattern Pe :: () => forall {a}. a -> Ex -- Defined at <interactive>:17:1 -pattern Pu :: forall {t}. t -> t -- Defined at <interactive>:18:1 +pattern Pu :: forall {p}. p -> p -- Defined at <interactive>:18:1 pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a] diff --git a/testsuite/tests/ghci/scripts/T2182ghci.stderr b/testsuite/tests/ghci/scripts/T2182ghci.stderr index 8a8d3dd65b..5f601942ca 100644 --- a/testsuite/tests/ghci/scripts/T2182ghci.stderr +++ b/testsuite/tests/ghci/scripts/T2182ghci.stderr @@ -1,25 +1,25 @@ <interactive>:2:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:10:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:19:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:28:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it <interactive>:49:1: error: - • No instance for (Show (t0 -> t0)) arising from a use of ‘print’ + • No instance for (Show (p0 -> p0)) arising from a use of ‘print’ (maybe you haven't applied a function to enough arguments?) • In a stmt of an interactive GHCi command: print it diff --git a/testsuite/tests/indexed-types/should_fail/T12386.hs b/testsuite/tests/indexed-types/should_fail/T12386.hs new file mode 100644 index 0000000000..c07881a6bd --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T12386.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE TypeFamilies #-} + +module T12386 where + +class C a where + type family F a t :: * + + type family T a :: * + type T a = F a diff --git a/testsuite/tests/indexed-types/should_fail/T12386.stderr b/testsuite/tests/indexed-types/should_fail/T12386.stderr new file mode 100644 index 0000000000..66d812e1fd --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T12386.stderr @@ -0,0 +1,7 @@ + +T12386.hs:9:15: error: + • Expecting one more argument to ‘F a’ + Expected a type, but ‘F a’ has kind ‘* -> *’ + • In the type ‘F a’ + In the default type instance declaration for ‘T’ + In the class declaration for ‘C’ diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr index f1ae705f5e..9cc8912814 100644 --- a/testsuite/tests/indexed-types/should_fail/T5439.stderr +++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr @@ -1,13 +1,15 @@ -T5439.hs:82:28: error: - • Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’ - with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’ - Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0)) - Actual type: f (Attempt (WaitOpResult (WaitOps rs))) - • In the first argument of ‘complete’, namely ‘ev’ - In the expression: complete ev +T5439.hs:82:33: error: + • Couldn't match expected type ‘Attempt (HElemOf rs)’ + with actual type ‘Attempt (HHead (HDrop n0 l0)) + -> Attempt (HElemOf l0)’ + • In the second argument of ‘($)’, namely + ‘inj $ Failure (e :: SomeException)’ In a stmt of a 'do' block: c <- complete ev $ inj $ Failure (e :: SomeException) + In the expression: + do { c <- complete ev $ inj $ Failure (e :: SomeException); + return $ c || not first } • Relevant bindings include register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool (bound at T5439.hs:64:9) diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr index 0332181394..b7b70b8f4e 100644 --- a/testsuite/tests/indexed-types/should_fail/T7354.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr @@ -1,11 +1,11 @@ T7354.hs:28:11: error: • Occurs check: cannot construct the infinite type: - t ~ Base t1 (Prim [t] t) - Expected type: Prim [t] t -> Base t1 (Prim [t] t) - Actual type: Prim [t] t -> t + p ~ Base t (Prim [p] p) + Expected type: Prim [p] p -> Base t (Prim [p] p) + Actual type: Prim [p] p -> p • In the first argument of ‘ana’, namely ‘alg’ In the expression: ana alg In an equation for ‘foo’: foo = ana alg • Relevant bindings include - foo :: Prim [t] t -> t1 (bound at T7354.hs:28:1) + foo :: Prim [p] p -> t (bound at T7354.hs:28:1) diff --git a/testsuite/tests/parser/should_compile/read014.stderr b/testsuite/tests/parser/should_compile/read014.stderr index 09e79ee52c..228672b7a5 100644 --- a/testsuite/tests/parser/should_compile/read014.stderr +++ b/testsuite/tests/parser/should_compile/read014.stderr @@ -1,7 +1,7 @@ read014.hs:4:1: warning: [-Wmissing-signatures (in -Wall)] Top-level binding with no type signature: - ng1 :: Num a => t -> a -> a + ng1 :: Num a => p -> a -> a read014.hs:4:5: warning: [-Wunused-matches (in -Wextra)] Defined but not used: ‘x’ diff --git a/testsuite/tests/parser/should_fail/T7848.stderr b/testsuite/tests/parser/should_fail/T7848.stderr index f7617ee606..fe949d944a 100644 --- a/testsuite/tests/parser/should_fail/T7848.stderr +++ b/testsuite/tests/parser/should_fail/T7848.stderr @@ -1,10 +1,7 @@ T7848.hs:6:1: error: • Occurs check: cannot construct the infinite type: - t ~ t0 -> t1 -> A -> A -> A -> A -> t2 -> t - • When checking that: - t0 -> t1 -> A -> A -> A -> A -> forall t2. t2 -> t - is more polymorphic than: t + t ~ p0 -> p1 -> A -> A -> A -> A -> p2 -> t • Relevant bindings include x :: t (bound at T7848.hs:6:1) T7848.hs:10:9: error: diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr index 963bc50d72..2dca583aba 100644 --- a/testsuite/tests/parser/should_fail/readFail003.stderr +++ b/testsuite/tests/parser/should_fail/readFail003.stderr @@ -1,7 +1,7 @@ readFail003.hs:4:27: error: • Occurs check: cannot construct the infinite type: - t ~ (t, [a1], [a]) + a2 ~ (a2, [a1], [a]) • In the expression: a In a pattern binding: ~(a, b, c) @@ -11,6 +11,6 @@ readFail003.hs:4:27: error: where nullity = null • Relevant bindings include - a :: t (bound at readFail003.hs:4:3) + a :: a2 (bound at readFail003.hs:4:3) b :: [a1] (bound at readFail003.hs:4:5) c :: [a] (bound at readFail003.hs:4:7) diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr index ebf2a759b7..c5238bb474 100644 --- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr @@ -1,8 +1,8 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘t2’ - Where: ‘t2’ is a rigid type variable bound by - the inferred type of g :: t2 -> t2 at T10438.hs:(6,9)-(8,21) + • Found type wildcard ‘_’ standing for ‘p2’ + Where: ‘p2’ is a rigid type variable bound by + the inferred type of g :: p2 -> p2 at T10438.hs:(6,9)-(8,21) • In the type signature: x :: _ In an equation for ‘g’: g r @@ -20,7 +20,7 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)] x :: _ x = r • Relevant bindings include - r :: t2 (bound at T10438.hs:6:11) - g :: t2 -> t2 (bound at T10438.hs:6:9) - f :: t1 (bound at T10438.hs:5:5) - foo :: t1 -> forall t. t -> t (bound at T10438.hs:5:1) + r :: p2 (bound at T10438.hs:6:11) + g :: p2 -> p2 (bound at T10438.hs:6:9) + f :: p1 (bound at T10438.hs:5:5) + foo :: p1 -> p -> p (bound at T10438.hs:5:1) diff --git a/testsuite/tests/partial-sigs/should_compile/T11192.stderr b/testsuite/tests/partial-sigs/should_compile/T11192.stderr index 7abf6e5845..8e47c4bb70 100644 --- a/testsuite/tests/partial-sigs/should_compile/T11192.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T11192.stderr @@ -1,8 +1,8 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘Int -> t -> t’ - Where: ‘t’ is a rigid type variable bound by - the inferred type of go :: Int -> t -> t at T11192.hs:8:8-17 + • Found type wildcard ‘_’ standing for ‘Int -> p -> p’ + Where: ‘p’ is a rigid type variable bound by + the inferred type of go :: Int -> p -> p at T11192.hs:8:8-17 • In the type signature: go :: _ In the expression: let @@ -18,11 +18,11 @@ T11192.hs:7:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Relevant bindings include fails :: a (bound at T11192.hs:6:1) T11192.hs:13:14: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘t1 -> t -> t’ - Where: ‘t1’ is a rigid type variable bound by - the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17 - ‘t’ is a rigid type variable bound by - the inferred type of go :: t1 -> t -> t at T11192.hs:14:8-17 + • Found type wildcard ‘_’ standing for ‘p1 -> p -> p’ + Where: ‘p1’ is a rigid type variable bound by + the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17 + ‘p’ is a rigid type variable bound by + the inferred type of go :: p1 -> p -> p at T11192.hs:14:8-17 • In the type signature: go :: _ In the expression: let diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr index 9c438dd176..838d75c3c7 100644 --- a/testsuite/tests/patsyn/should_compile/T11213.stderr +++ b/testsuite/tests/patsyn/should_compile/T11213.stderr @@ -8,7 +8,7 @@ T11213.hs:20:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] T11213.hs:21:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] Pattern synonym with no type signature: - pattern Pu :: forall t. t -> t + pattern Pu :: forall p. p -> p T11213.hs:22:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)] Pattern synonym with no type signature: diff --git a/testsuite/tests/patsyn/should_fail/mono.stderr b/testsuite/tests/patsyn/should_fail/mono.stderr index 20714e7565..8f370ce2f0 100644 --- a/testsuite/tests/patsyn/should_fail/mono.stderr +++ b/testsuite/tests/patsyn/should_fail/mono.stderr @@ -1,8 +1,8 @@ mono.hs:7:4: error: • Couldn't match type ‘Bool’ with ‘Int’ - Expected type: [Int] - Actual type: [Bool] + Expected type: [Bool] + Actual type: [Int] • In the pattern: Single x In an equation for ‘f’: f (Single x) = x diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr index 9f8f62e25e..7a079ff102 100644 --- a/testsuite/tests/polykinds/T7438.stderr +++ b/testsuite/tests/polykinds/T7438.stderr @@ -1,19 +1,19 @@ T7438.hs:6:14: error: - • Couldn't match expected type ‘t’ with actual type ‘t1’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘p1’ + ‘p1’ is untouchable inside the constraints: b ~ a bound by a pattern with constructor: Nil :: forall k (a :: k). Thrist a a, in an equation for ‘go’ at T7438.hs:6:4-6 - ‘t’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16 - ‘t1’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> t1 -> t at T7438.hs:6:1-16 + ‘p1’ is a rigid type variable bound by + the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16 + ‘p’ is a rigid type variable bound by + the inferred type of go :: Thrist a b -> p1 -> p at T7438.hs:6:1-16 Possible fix: add a type signature for ‘go’ • In the expression: acc In an equation for ‘go’: go Nil acc = acc • Relevant bindings include - acc :: t1 (bound at T7438.hs:6:8) - go :: Thrist a b -> t1 -> t (bound at T7438.hs:6:1) + acc :: p1 (bound at T7438.hs:6:8) + go :: Thrist a b -> p1 -> p (bound at T7438.hs:6:1) diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr index 241cf76962..712724d28f 100644 --- a/testsuite/tests/rebindable/rebindable6.stderr +++ b/testsuite/tests/rebindable/rebindable6.stderr @@ -25,15 +25,15 @@ rebindable6.hs:110:17: error: return b } rebindable6.hs:111:17: error: - • Ambiguous type variables ‘t1’, ‘t0’ arising from a do statement + • Ambiguous type variables ‘p0’, ‘t0’ arising from a do statement prevents the constraint ‘(HasBind - (IO (Maybe b) -> (Maybe b -> t1) -> t0))’ from being solved. + (IO (Maybe b) -> (Maybe b -> p0) -> t0))’ from being solved. (maybe you haven't applied a function to enough arguments?) Relevant bindings include g :: IO (Maybe b) (bound at rebindable6.hs:108:19) test_do :: IO a -> IO (Maybe b) -> IO b (bound at rebindable6.hs:108:9) - Probable fix: use a type annotation to specify what ‘t1’, ‘t0’ should be. + Probable fix: use a type annotation to specify what ‘p0’, ‘t0’ should be. These potential instance exist: instance HasBind (IO a -> (a -> IO b) -> IO b) -- Defined at rebindable6.hs:51:18 @@ -49,15 +49,15 @@ rebindable6.hs:111:17: error: return b } rebindable6.hs:112:17: error: - • Ambiguous type variable ‘t1’ arising from a use of ‘return’ - prevents the constraint ‘(HasReturn (b -> t1))’ from being solved. + • Ambiguous type variable ‘p0’ arising from a use of ‘return’ + prevents the constraint ‘(HasReturn (b -> p0))’ from being solved. (maybe you haven't applied a function to enough arguments?) Relevant bindings include b :: b (bound at rebindable6.hs:111:23) g :: IO (Maybe b) (bound at rebindable6.hs:108:19) test_do :: IO a -> IO (Maybe b) -> IO b (bound at rebindable6.hs:108:9) - Probable fix: use a type annotation to specify what ‘t1’ should be. + Probable fix: use a type annotation to specify what ‘p0’ should be. These potential instance exist: instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:46:18 • In a stmt of a 'do' block: return b diff --git a/testsuite/tests/rename/should_compile/T12597.stderr b/testsuite/tests/rename/should_compile/T12597.stderr index 8364fd07b3..e3df440372 100644 --- a/testsuite/tests/rename/should_compile/T12597.stderr +++ b/testsuite/tests/rename/should_compile/T12597.stderr @@ -1,3 +1,3 @@ T12597.hs:5:1: warning: [-Wmissing-signatures (in -Wall)] - Top-level binding with no type signature: f :: t -> t + Top-level binding with no type signature: f :: p -> p diff --git a/testsuite/tests/roles/should_compile/T8958.stderr b/testsuite/tests/roles/should_compile/T8958.stderr index 982686868f..df20e67f3a 100644 --- a/testsuite/tests/roles/should_compile/T8958.stderr +++ b/testsuite/tests/roles/should_compile/T8958.stderr @@ -65,7 +65,8 @@ AbsBinds [a] [] Exported types: T8958.$fRepresentationala [InlPrag=[ALWAYS] CONLIKE] :: forall a. Representational a [LclIdX[DFunId], - Unf=DFun: \ (@ a[ssk]) -> T8958.C:Representational TYPE: a[ssk]] + Unf=DFun: \ (@ a[ssk:2]) -> + T8958.C:Representational TYPE: a[ssk:2]] Binds: $dRepresentational = T8958.C:Representational @ a Evidence: [EvBinds{}]} AbsBinds [a] [] @@ -74,7 +75,7 @@ AbsBinds [a] [] Exported types: T8958.$fNominala [InlPrag=[ALWAYS] CONLIKE] :: forall a. Nominal a [LclIdX[DFunId], - Unf=DFun: \ (@ a[ssk]) -> T8958.C:Nominal TYPE: a[ssk]] + Unf=DFun: \ (@ a[ssk:2]) -> T8958.C:Nominal TYPE: a[ssk:2]] Binds: $dNominal = T8958.C:Nominal @ a Evidence: [EvBinds{}]} diff --git a/testsuite/tests/simplCore/should_compile/noinline01.stderr b/testsuite/tests/simplCore/should_compile/noinline01.stderr index cecaad16f0..b100172381 100644 --- a/testsuite/tests/simplCore/should_compile/noinline01.stderr +++ b/testsuite/tests/simplCore/should_compile/noinline01.stderr @@ -1,7 +1,7 @@ ==================== Pre unarise: ==================== Noinline01.f [InlPrag=INLINE (sat-args=1)] - :: forall t. t -> GHC.Types.Bool + :: forall p. p -> GHC.Types.Bool [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] = \r [eta] GHC.Types.True []; @@ -26,7 +26,7 @@ Noinline01.$trModule :: GHC.Types.Module ==================== STG syntax: ==================== Noinline01.f [InlPrag=INLINE (sat-args=1)] - :: forall t. t -> GHC.Types.Bool + :: forall p. p -> GHC.Types.Bool [GblId, Arity=1, Caf=NoCafRefs, Str=<L,A>, Unf=OtherCon []] = \r [eta] GHC.Types.True []; diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr index f59fcbd7d2..32064a9c78 100644 --- a/testsuite/tests/th/T11452.stderr +++ b/testsuite/tests/th/T11452.stderr @@ -7,7 +7,7 @@ T11452.hs:6:14: error: In an equation for ‘impred’: impred = $$([|| \ _ -> () ||]) T11452.hs:6:14: error: - • Cannot instantiate unification variable ‘t0’ + • Cannot instantiate unification variable ‘p0’ with a type involving foralls: forall a. a -> a GHC doesn't yet support impredicative polymorphism • In the Template Haskell quotation [|| \ _ -> () ||] diff --git a/testsuite/tests/th/T2222.stderr b/testsuite/tests/th/T2222.stderr index 4ddf100bf6..3265a5e938 100644 --- a/testsuite/tests/th/T2222.stderr +++ b/testsuite/tests/th/T2222.stderr @@ -1,4 +1,4 @@ -inside b: t_0 +inside b: p_0 inside d: GHC.Types.Bool type of c: GHC.Types.Bool inside f: GHC.Types.Bool diff --git a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr index 696bff740d..6cc24fcaf6 100644 --- a/testsuite/tests/typecheck/should_compile/ExPatFail.stderr +++ b/testsuite/tests/typecheck/should_compile/ExPatFail.stderr @@ -1,6 +1,6 @@ ExPatFail.hs:12:15: error: - • Couldn't match expected type ‘t’ with actual type ‘a’ + • Couldn't match expected type ‘p’ with actual type ‘a’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: @@ -11,4 +11,4 @@ ExPatFail.hs:12:15: error: In a pattern binding: MkT y _ = x In the expression: let MkT y _ = x in y • Relevant bindings include - f :: T -> t (bound at ExPatFail.hs:12:1) + f :: T -> p (bound at ExPatFail.hs:12:1) diff --git a/testsuite/tests/typecheck/should_compile/T12427.stderr b/testsuite/tests/typecheck/should_compile/T12427.stderr new file mode 100644 index 0000000000..0519ecba6e --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427.stderr @@ -0,0 +1 @@ +
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr new file mode 100644 index 0000000000..fc2aece398 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr @@ -0,0 +1,33 @@ + +T12427a.hs:17:29: error: + • Couldn't match expected type ‘p’ + with actual type ‘(forall b. [b] -> [b]) -> Int’ + ‘p’ is untouchable + inside the constraints: () + bound by a pattern with constructor: + T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T, + in a case alternative + at T12427a.hs:17:19-24 + ‘p’ is a rigid type variable bound by + the inferred type of h11 :: T -> p at T12427a.hs:17:1-29 + Possible fix: add a type signature for ‘h11’ + • In the expression: v + In a case alternative: T1 _ v -> v + In the expression: case y of { T1 _ v -> v } + • Relevant bindings include + h11 :: T -> p (bound at T12427a.hs:17:1) + +T12427a.hs:28:6: error: + • Couldn't match expected type ‘p’ + with actual type ‘(forall b. [b] -> [b]) -> Int’ + ‘p’ is untouchable + inside the constraints: () + bound by a pattern with constructor: + T1 :: forall a. a -> ((forall b. [b] -> [b]) -> Int) -> T, + in a pattern binding + at T12427a.hs:28:1-7 + ‘p’ is a rigid type variable bound by + the inferred type of x1 :: p at T12427a.hs:28:1-19 + Possible fix: add a type signature for ‘x1’ + • In the pattern: T1 _ x1 + In a pattern binding: T1 _ x1 = undefined diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr index d205fa9ced..7d0f0815dc 100644 --- a/testsuite/tests/typecheck/should_compile/tc141.stderr +++ b/testsuite/tests/typecheck/should_compile/tc141.stderr @@ -35,7 +35,7 @@ tc141.hs:13:13: error: in v tc141.hs:15:18: error: - • Couldn't match expected type ‘a2’ with actual type ‘t’ + • Couldn't match expected type ‘a2’ with actual type ‘p’ because type variable ‘a2’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: @@ -50,5 +50,5 @@ tc141.hs:15:18: error: in v • Relevant bindings include v :: a2 (bound at tc141.hs:15:14) - b :: t (bound at tc141.hs:13:5) - g :: a1 -> t -> forall a. a (bound at tc141.hs:13:1) + b :: p (bound at tc141.hs:13:5) + g :: a1 -> p -> a (bound at tc141.hs:13:1) diff --git a/testsuite/tests/typecheck/should_fail/T10495.stderr b/testsuite/tests/typecheck/should_fail/T10495.stderr index e09e60af23..5067d25183 100644 --- a/testsuite/tests/typecheck/should_fail/T10495.stderr +++ b/testsuite/tests/typecheck/should_fail/T10495.stderr @@ -1,8 +1,8 @@ -T10495.hs:5:1: error: +T10495.hs:5:7: error: • Couldn't match representation of type ‘a0’ with that of ‘b0’ arising from a use of ‘coerce’ - • When instantiating ‘foo’, initially inferred to have - this overly-general type: - forall a b. Coercible a b => a -> b - NB: This instantiation can be caused by the monomorphism restriction. + • In the expression: coerce + In an equation for ‘foo’: foo = coerce + • Relevant bindings include + foo :: a0 -> b0 (bound at T10495.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T10619.stderr b/testsuite/tests/typecheck/should_fail/T10619.stderr index 7a27229369..fde2daf8c6 100644 --- a/testsuite/tests/typecheck/should_fail/T10619.stderr +++ b/testsuite/tests/typecheck/should_fail/T10619.stderr @@ -17,7 +17,7 @@ T10619.hs:9:15: error: else \ y -> y • Relevant bindings include - foo :: t -> (b -> b) -> b -> b (bound at T10619.hs:8:1) + foo :: p -> (b -> b) -> b -> b (bound at T10619.hs:8:1) T10619.hs:14:15: error: • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’ @@ -37,7 +37,7 @@ T10619.hs:14:15: error: else ((\ x -> x) :: (forall a. a -> a) -> forall b. b -> b) • Relevant bindings include - bar :: t -> (b -> b) -> b -> b (bound at T10619.hs:12:1) + bar :: p -> (b -> b) -> b -> b (bound at T10619.hs:12:1) T10619.hs:16:13: error: • Couldn't match type ‘forall a. a -> a’ with ‘b -> b’ diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr index 48bf94d2ce..03c885a577 100644 --- a/testsuite/tests/typecheck/should_fail/T12177.stderr +++ b/testsuite/tests/typecheck/should_fail/T12177.stderr @@ -2,27 +2,24 @@ T12177.hs:3:19: error: • Found hole: _ :: t Where: ‘t’ is a rigid type variable bound by - the inferred type of bar :: t2 -> t1 -> t - at T12177.hs:3:1-19 + the inferred type of bar :: p1 -> p -> t at T12177.hs:3:1-19 • In the expression: _ In the expression: \ x -> _ In the expression: \ x -> \ x -> _ • Relevant bindings include - x :: t1 (bound at T12177.hs:3:14) - bar :: t2 -> t1 -> t (bound at T12177.hs:3:1) + x :: p (bound at T12177.hs:3:14) + bar :: p1 -> p -> t (bound at T12177.hs:3:1) T12177.hs:5:37: error: • Found hole: _ :: t Where: ‘t’ is a rigid type variable bound by - the inferred type of baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t + the inferred type of baz :: p4 -> p3 -> p2 -> p1 -> p -> t at T12177.hs:5:1-37 • In the expression: _ In the expression: \ z -> _ In the expression: \ x -> \ z -> _ • Relevant bindings include - z :: t1 (bound at T12177.hs:5:32) - x :: t2 (bound at T12177.hs:5:26) - y :: t4 (bound at T12177.hs:5:14) - baz :: t5 -> t4 -> t3 -> t2 -> t1 -> t - (bound at T12177.hs:5:1) -
\ No newline at end of file + z :: p (bound at T12177.hs:5:32) + x :: p1 (bound at T12177.hs:5:26) + y :: p3 (bound at T12177.hs:5:14) + baz :: p4 -> p3 -> p2 -> p1 -> p -> t (bound at T12177.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T3102.hs b/testsuite/tests/typecheck/should_fail/T3102.hs index dd5abb25e1..910ac06ee9 100644 --- a/testsuite/tests/typecheck/should_fail/T3102.hs +++ b/testsuite/tests/typecheck/should_fail/T3102.hs @@ -1,5 +1,5 @@ {-# OPTIONS -XImplicitParams -XRankNTypes #-} - module Bug where +module Bug where t :: forall a. ((?p :: Int) => a) -> String t _ = "Hello" @@ -10,3 +10,7 @@ f _ = 3 result :: Int result = f t + +-- This should work. +-- Elaborated result = f (/\a. \x:a. t @a (\p::Int. x)) +-- But it did not work in 8.0.1; fixed in HEAD diff --git a/testsuite/tests/typecheck/should_fail/T3102.stderr b/testsuite/tests/typecheck/should_fail/T3102.stderr index 66979ddf8b..e69de29bb2 100644 --- a/testsuite/tests/typecheck/should_fail/T3102.stderr +++ b/testsuite/tests/typecheck/should_fail/T3102.stderr @@ -1,12 +0,0 @@ - -T3102.hs:11:12: error: - • Couldn't match type ‘a’ with ‘(?p::Int) => a0’ - ‘a’ is a rigid type variable bound by - a type expected by the context: - forall a. a -> String - at T3102.hs:11:10-12 - Expected type: a -> String - Actual type: ((?p::Int) => a0) -> String - • In the first argument of ‘f’, namely ‘t’ - In the expression: f t - In an equation for ‘result’: result = f t diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr index 6b8e920004..9157e116f5 100644 --- a/testsuite/tests/typecheck/should_fail/T7453.stderr +++ b/testsuite/tests/typecheck/should_fail/T7453.stderr @@ -1,13 +1,13 @@ T7453.hs:9:15: error: - • Couldn't match type ‘t’ with ‘t1’ - because type variable ‘t1’ would escape its scope + • Couldn't match type ‘p’ with ‘t’ + because type variable ‘t’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: Id t1 + z :: Id t at T7453.hs:8:11-19 - Expected type: Id t1 - Actual type: Id t + Expected type: Id t + Actual type: Id p • In the expression: aux In an equation for ‘z’: z = aux @@ -22,20 +22,20 @@ T7453.hs:9:15: error: where aux = Id v • Relevant bindings include - aux :: Id t (bound at T7453.hs:10:21) - z :: Id t1 (bound at T7453.hs:9:11) - v :: t (bound at T7453.hs:7:7) - cast1 :: t -> a (bound at T7453.hs:7:1) + aux :: Id p (bound at T7453.hs:10:21) + z :: Id t (bound at T7453.hs:9:11) + v :: p (bound at T7453.hs:7:7) + cast1 :: p -> a (bound at T7453.hs:7:1) T7453.hs:15:15: error: - • Couldn't match type ‘t1’ with ‘t2’ - because type variable ‘t2’ would escape its scope + • Couldn't match type ‘p’ with ‘t1’ + because type variable ‘t1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: () -> t2 + z :: () -> t1 at T7453.hs:14:11-22 - Expected type: () -> t2 - Actual type: () -> t1 + Expected type: () -> t1 + Actual type: () -> p • In the expression: aux In an equation for ‘z’: z = aux @@ -50,17 +50,17 @@ T7453.hs:15:15: error: where aux = const v • Relevant bindings include - aux :: forall b. b -> t1 (bound at T7453.hs:16:21) - z :: () -> t2 (bound at T7453.hs:15:11) - v :: t1 (bound at T7453.hs:13:7) - cast2 :: t1 -> t (bound at T7453.hs:13:1) + aux :: forall b. b -> p (bound at T7453.hs:16:21) + z :: () -> t1 (bound at T7453.hs:15:11) + v :: p (bound at T7453.hs:13:7) + cast2 :: p -> t (bound at T7453.hs:13:1) T7453.hs:21:15: error: - • Couldn't match expected type ‘t2’ with actual type ‘t1’ - because type variable ‘t2’ would escape its scope + • Couldn't match expected type ‘t1’ with actual type ‘p’ + because type variable ‘t1’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: - z :: t2 + z :: t1 at T7453.hs:20:11-16 • In the expression: v In an equation for ‘z’: @@ -76,7 +76,7 @@ T7453.hs:21:15: error: where aux = const v • Relevant bindings include - aux :: forall b. b -> t1 (bound at T7453.hs:22:21) - z :: t2 (bound at T7453.hs:21:11) - v :: t1 (bound at T7453.hs:19:7) - cast3 :: t1 -> forall t. t (bound at T7453.hs:19:1) + aux :: forall b. b -> p (bound at T7453.hs:22:21) + z :: t1 (bound at T7453.hs:21:11) + v :: p (bound at T7453.hs:19:7) + cast3 :: p -> t (bound at T7453.hs:19:1) diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr index 8553fdb888..a39b0488c3 100644 --- a/testsuite/tests/typecheck/should_fail/T7734.stderr +++ b/testsuite/tests/typecheck/should_fail/T7734.stderr @@ -1,18 +1,18 @@ T7734.hs:4:13: error: - • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1 + • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘f’: x `f` y = x x • Relevant bindings include - x :: t2 -> t1 (bound at T7734.hs:4:1) - f :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:4:3) + x :: t1 -> t (bound at T7734.hs:4:1) + f :: (t1 -> t) -> p -> t (bound at T7734.hs:4:3) T7734.hs:5:13: error: - • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1 + • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘&’: (&) x y = x x • Relevant bindings include - x :: t2 -> t1 (bound at T7734.hs:5:5) - (&) :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:5:1) + x :: t1 -> t (bound at T7734.hs:5:5) + (&) :: (t1 -> t) -> p -> t (bound at T7734.hs:5:1) diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr index ce1b09d51c..f30c49bde6 100644 --- a/testsuite/tests/typecheck/should_fail/T9109.stderr +++ b/testsuite/tests/typecheck/should_fail/T9109.stderr @@ -1,14 +1,14 @@ T9109.hs:8:13: error: - • Couldn't match expected type ‘t’ with actual type ‘Bool’ - ‘t’ is untouchable + • Couldn't match expected type ‘p’ with actual type ‘Bool’ + ‘p’ is untouchable inside the constraints: a ~ Bool bound by a pattern with constructor: GBool :: G Bool, in an equation for ‘foo’ at T9109.hs:8:5-9 - ‘t’ is a rigid type variable bound by - the inferred type of foo :: G a -> t at T9109.hs:8:1-16 + ‘p’ is a rigid type variable bound by + the inferred type of foo :: G a -> p at T9109.hs:8:1-16 Possible fix: add a type signature for ‘foo’ • In the expression: True In an equation for ‘foo’: foo GBool = True - • Relevant bindings include foo :: G a -> t (bound at T9109.hs:8:1) + • Relevant bindings include foo :: G a -> p (bound at T9109.hs:8:1) diff --git a/testsuite/tests/typecheck/should_fail/T9318.stderr b/testsuite/tests/typecheck/should_fail/T9318.stderr index 218ae97b77..c637788a7e 100644 --- a/testsuite/tests/typecheck/should_fail/T9318.stderr +++ b/testsuite/tests/typecheck/should_fail/T9318.stderr @@ -1,7 +1,7 @@ -T9318.hs:12:5: - Couldn't match type ‘Char’ with ‘Bool’ - Expected type: F Int - Actual type: Char - In the pattern: 'x' - In an equation for ‘bar’: bar 'x' = () +T9318.hs:12:5: error: + • Couldn't match type ‘Bool’ with ‘Char’ + Expected type: F Int + Actual type: Char + • In the pattern: 'x' + In an equation for ‘bar’: bar 'x' = () diff --git a/testsuite/tests/typecheck/should_fail/VtaFail.stderr b/testsuite/tests/typecheck/should_fail/VtaFail.stderr index ff90a738c9..17486dfefa 100644 --- a/testsuite/tests/typecheck/should_fail/VtaFail.stderr +++ b/testsuite/tests/typecheck/should_fail/VtaFail.stderr @@ -13,7 +13,7 @@ VtaFail.hs:12:26: error: answer_constraint_fail = addOne @Bool 5 VtaFail.hs:14:17: error: - • Cannot apply expression of type ‘t1 -> t1’ + • Cannot apply expression of type ‘p0 -> p0’ 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/all.T b/testsuite/tests/typecheck/should_fail/all.T index 98c57e833e..4f2dbc43d5 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -208,7 +208,7 @@ test('T2806', normal, compile_fail, ['']) test('T3323', normal, compile_fail, ['']) test('T3406', normal, compile_fail, ['']) test('T3540', normal, compile_fail, ['']) -test('T3102', normal, compile_fail, ['']) +test('T3102', normal, compile, ['']) test('T3613', normal, compile_fail, ['']) test('fd-loop', normal, compile_fail, ['']) test('T3950', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr index 6755636682..d72a34065e 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: - • Occurs check: cannot construct the infinite type: t ~ [t] + • Occurs check: cannot construct the infinite type: p ~ [p] • In the expression: z In an equation for ‘c’: c z = z • Relevant bindings include - z :: [t] (bound at tcfail002.hs:4:3) - c :: [t] -> t (bound at tcfail002.hs:3:1) + z :: [p] (bound at tcfail002.hs:4:3) + c :: [p] -> p (bound at tcfail002.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr index 41a55c1ea9..7bf64d841a 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr @@ -1,9 +1,9 @@ tcfail004.hs:3:9: error: - • Couldn't match expected type ‘(t1, t)’ + • Couldn't match expected type ‘(a, b)’ with actual type ‘(Integer, Integer, Integer)’ • In the expression: (1, 2, 3) In a pattern binding: (f, g) = (1, 2, 3) • Relevant bindings include - f :: t1 (bound at tcfail004.hs:3:2) - g :: t (bound at tcfail004.hs:3:4) + f :: a (bound at tcfail004.hs:3:2) + g :: b (bound at tcfail004.hs:3:4) diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr index 77437cf583..56db4cf58b 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr @@ -1,9 +1,9 @@ tcfail005.hs:3:9: error: - • Couldn't match expected type ‘[t]’ + • Couldn't match expected type ‘[a]’ with actual type ‘(Integer, Char)’ • In the expression: (1, 'a') In a pattern binding: (h : i) = (1, 'a') • Relevant bindings include - h :: t (bound at tcfail005.hs:3:2) - i :: [t] (bound at tcfail005.hs:3:4) + h :: a (bound at tcfail005.hs:3:2) + i :: [a] (bound at tcfail005.hs:3:4) diff --git a/testsuite/tests/typecheck/should_fail/tcfail013.stderr b/testsuite/tests/typecheck/should_fail/tcfail013.stderr index f3e815bb6e..3803d9ce95 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail013.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail013.stderr @@ -4,4 +4,4 @@ tcfail013.hs:4:3: error: • In the pattern: True In an equation for ‘f’: f True = 2 • Relevant bindings include - f :: [a] -> t (bound at tcfail013.hs:3:1) + f :: [a] -> p (bound at tcfail013.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr index a186fb1310..f506bff6f8 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr @@ -1,9 +1,9 @@ tcfail014.hs:5:33: error: - • Occurs check: cannot construct the infinite type: t7 ~ t7 -> t8 + • Occurs check: cannot construct the infinite type: t4 ~ t4 -> t5 • In the first argument of ‘z’, namely ‘z’ In the expression: z z In an equation for ‘h’: h z = z z • Relevant bindings include - z :: t7 -> t8 (bound at tcfail014.hs:5:27) - h :: (t7 -> t8) -> t8 (bound at tcfail014.hs:5:25) + z :: t4 -> t5 (bound at tcfail014.hs:5:27) + h :: (t4 -> t5) -> t5 (bound at tcfail014.hs:5:25) diff --git a/testsuite/tests/typecheck/should_fail/tcfail018.stderr b/testsuite/tests/typecheck/should_fail/tcfail018.stderr index 57060a87db..d5594c7c41 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail018.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail018.stderr @@ -1,5 +1,5 @@ tcfail018.hs:5:10: error: - • No instance for (Num [t0]) arising from the literal ‘1’ + • No instance for (Num [a0]) arising from the literal ‘1’ • In the expression: 1 In a pattern binding: (a : []) = 1 diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr index 583e6e3ce5..d2912b2b94 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr @@ -1,6 +1,6 @@ tcfail032.hs:14:8: error: - • Couldn't match expected type ‘a1 -> Int’ with actual type ‘t’ + • Couldn't match expected type ‘a1 -> Int’ with actual type ‘p’ because type variable ‘a1’ would escape its scope This (rigid, skolem) type variable is bound by an expression type signature: @@ -9,5 +9,5 @@ tcfail032.hs:14:8: error: • In the expression: (x :: (Eq a) => a -> Int) In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int) • Relevant bindings include - x :: t (bound at tcfail032.hs:14:3) - f :: t -> forall a. Eq a => a -> Int (bound at tcfail032.hs:14:1) + x :: p (bound at tcfail032.hs:14:3) + f :: p -> a -> Int (bound at tcfail032.hs:14:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail099.stderr b/testsuite/tests/typecheck/should_fail/tcfail099.stderr index f3908f36e4..bc30866ec2 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail099.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail099.stderr @@ -1,6 +1,6 @@ tcfail099.hs:9:20: error: - • Couldn't match expected type ‘a’ with actual type ‘t’ + • Couldn't match expected type ‘a’ with actual type ‘p’ because type variable ‘a’ would escape its scope This (rigid, skolem) type variable is bound by a pattern with constructor: C :: forall a. (a -> Int) -> DS, @@ -10,6 +10,6 @@ tcfail099.hs:9:20: error: In the expression: f arg In an equation for ‘call’: call (C f) arg = f arg • Relevant bindings include - arg :: t (bound at tcfail099.hs:9:12) + arg :: p (bound at tcfail099.hs:9:12) f :: a -> Int (bound at tcfail099.hs:9:9) - call :: DS -> t -> Int (bound at tcfail099.hs:9:1) + call :: DS -> p -> Int (bound at tcfail099.hs:9:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail104.stderr b/testsuite/tests/typecheck/should_fail/tcfail104.stderr index a0a6595231..44d8e4888c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail104.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail104.stderr @@ -3,15 +3,15 @@ tcfail104.hs:14:12: error: • Couldn't match type ‘forall a. a -> a’ with ‘Char -> Char’ Expected type: (Char -> Char) -> Char -> Char Actual type: (forall a. a -> a) -> Char -> Char - • When checking that: (forall a. a -> a) -> forall a. a -> a - is more polymorphic than: (Char -> Char) -> Char -> Char - In the expression: (\ (x :: forall a. a -> a) -> x) + • In the expression: (\ (x :: forall a. a -> a) -> 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:15: error: - • Couldn't match expected type ‘forall a. a -> a’ - with actual type ‘Char -> Char’ + • 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 diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr index f75f77c38a..85217315ca 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr @@ -16,7 +16,7 @@ tcfail140.hs:12:10: error: In the expression: 3 `f` 4 In an equation for ‘rot’: rot xs = 3 `f` 4 • Relevant bindings include - rot :: t1 -> t (bound at tcfail140.hs:12:1) + rot :: p -> t (bound at tcfail140.hs:12:1) tcfail140.hs:14:15: error: • Couldn't match expected type ‘t -> b’ with actual type ‘Int’ @@ -36,6 +36,6 @@ tcfail140.hs:16:8: error: In the expression: (\ Just x -> x) :: Maybe a -> a tcfail140.hs:19:1: error: - • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’ + • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’ • The equation(s) for ‘g’ have two arguments, but its type ‘Int -> Int’ has only one diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr index a231133fd4..30e27b8bb7 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr @@ -3,7 +3,7 @@ tcfail181.hs:17:9: error: • Could not deduce (Monad m0) arising from a use of ‘foo’ from the context: Monad m bound by the inferred type of - wog :: Monad m => t -> Something (m Bool) e + wog :: Monad m => p -> Something (m Bool) e at tcfail181.hs:17:1-30 The type variable ‘m0’ is ambiguous These potential instances exist: diff --git a/testsuite/tests/warnings/should_compile/T12574.stderr b/testsuite/tests/warnings/should_compile/T12574.stderr index ded88331fa..db435541c1 100644 --- a/testsuite/tests/warnings/should_compile/T12574.stderr +++ b/testsuite/tests/warnings/should_compile/T12574.stderr @@ -1,4 +1,4 @@ T12574.hs:3:1: warning: [-Wmissing-local-signatures] Polymorphic local binding with no type signature: - T12574.id :: forall t. t -> t + T12574.id :: forall p. p -> p |