diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-07-16 14:35:42 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simonpj@microsoft.com> | 2020-09-24 08:22:36 +0100 |
| commit | 89831ac862914568a77fbdcb82b616af49e1b994 (patch) | |
| tree | 0fa8937b960b53872b16f937a50604bc64845365 | |
| parent | b83009b1eea18345786971274eff3735a5d28378 (diff) | |
| download | haskell-wip/T18126.tar.gz | |
Improve kind generalisation, error messageswip/T18126
This patch does two things:
* It refactors GHC.Tc.Errors a bit. In debugging Quick Look I was
forced to look in detail at error messages, and ended up doing a bit
of refactoring, esp in mkTyVarEqErr'. It's still quite a mess, but
a bit better, I think.
* It makes a significant improvement to the kind checking of type and
class declarations. Specifically, we now ensure that if kind
checking fails with an unsolved constraint, all the skolems are in
scope. That wasn't the case before, which led to some obscure error
messages; and occasional failures with "no skolem info" (eg #16245).
Both of these, and the main Quick Look patch itself, affect a /lot/ of
error messages, as you can see from the number of files changed. I've
checked them all; I think they are as good or better than before.
Smaller things
* I documented the various instances of VarBndr better.
See Note [The VarBndr tyep and its uses] in GHC.Types.Var
* Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds
* A bit of refactoring in bindExplicitTKTele, to avoid the
footwork with Either. Simpler now.
* Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType
Fixes #16245 (comment 211369), memorialised as
typecheck/polykinds/T16245a
Also fixes the three bugs in #18640
141 files changed, 1329 insertions, 964 deletions
diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index f4211fac5e..fc6aaf7d7b 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -427,11 +427,10 @@ See also: ************************************************************************ -} -type TyConBinder = VarBndr TyVar TyConBndrVis - --- In the whole definition of @data TyCon@, only @PromotedDataCon@ will really --- contain CoVar. +type TyConBinder = VarBndr TyVar TyConBndrVis type TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis + -- Only PromotedDataCon has TyConTyCoBinders + -- See Note [Promoted GADT data construtors] data TyConBndrVis = NamedTCB ArgFlag @@ -899,6 +898,7 @@ data TyCon -- See Note [The binders/kind/arity fields of a TyCon] tyConBinders :: [TyConTyCoBinder], -- ^ Full binders + -- TyConTyCoBinder: see Note [Promoted GADT data construtors] tyConResKind :: Kind, -- ^ Result kind tyConKind :: Kind, -- ^ Kind of this TyCon tyConArity :: Arity, -- ^ Arity @@ -937,7 +937,6 @@ data TyCon -- ^ What sort of 'TyCon' this represents. } {- Note [Scoped tyvars in a TcTyCon] - ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The tcTyConScopedTyVars field records the lexicial-binding connection between the original, user-specified Name (i.e. thing in scope) and @@ -952,6 +951,17 @@ where * tyConArity = length required_tvs See also Note [How TcTyCons work] in GHC.Tc.TyCl + +Note [Promoted GADT data constructors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Any promoted GADT data constructor will have a type with equality +constraints in its type; e.g. + K :: forall a b. (a ~# [b]) => a -> b -> T a + +So, when promoted to become a type constructor, the tyConBinders +will include CoVars. That is why we use [TyConTyCoBinder] for the +tyconBinders field. TyConTyCoBinder is a synonym for TyConBinder, +but with the clue that the binder can be a CoVar not just a TyVar. -} -- | Represents right-hand-sides of 'TyCon's for algebraic types diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index d597c95b72..93c047ca32 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -69,7 +69,7 @@ import GHC.Utils.FV ( fvVarList, unionFV ) import Control.Monad ( when ) import Data.Foldable ( toList ) -import Data.List ( partition, mapAccumL, nub, sortBy, unfoldr ) +import Data.List ( partition, mapAccumL, sortBy, unfoldr ) import {-# SOURCE #-} GHC.Tc.Errors.Hole ( findValidHoleFits ) @@ -215,7 +215,13 @@ report_unsolved type_errors expr_holes -- If we are deferring we are going to need /all/ evidence around, -- including the evidence produced by unflattening (zonkWC) ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs - free_tvs = tyCoVarsOfWCList wanted + free_tvs = filterOut isCoVar $ + tyCoVarsOfWCList wanted + -- tyCoVarsOfWC returns free coercion *holes*, even though + -- they are "bound" by other wanted constraints. They in + -- turn may mention variables bound further in, which makes + -- no sense. Really we should not return those holes at all; + -- for now we just filter them out. ; traceTc "reportUnsolved (after zonking):" $ vcat [ text "Free tyvars:" <+> pprTyVars free_tvs @@ -832,7 +838,11 @@ eq_lhs_type ct1 ct2 _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2) cmp_loc :: Ct -> Ct -> Ordering -cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2) +cmp_loc ct1 ct2 = get ct1 `compare` get ct2 + where + get ct = realSrcSpanStart (ctLocSpan (ctLoc ct)) + -- Reduce duplication by reporting only one error from each + -- /starting/ location even if the end location differs reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter reportGroup mk_err ctxt cts = @@ -1451,14 +1461,15 @@ mkTyVarEqErr dflags ctxt report ct tv1 ty2 ; mkTyVarEqErr' dflags ctxt report ct tv1 ty2 } mkTyVarEqErr' dflags ctxt report ct tv1 ty2 - | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar; we would have - -- swapped in Solver.Canonical.canEqTyVarHomo + | isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have + -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) || ctEqRel ct == ReprEq -- The cases below don't really apply to ReprEq (except occurs check) = mkErrorMsgFromCt ctxt ct $ mconcat [ headline_msg , extraTyVarEqInfo ctxt tv1 ty2 + , suggestAddSig ctxt ty1 ty2 , report ] @@ -1594,17 +1605,6 @@ mkEqInfoMsg ct ty1 ty2 <+> text "is a non-injective type family" | otherwise = empty -isUserSkolem :: ReportErrCtxt -> TcTyVar -> Bool --- See Note [Reporting occurs-check errors] -isUserSkolem ctxt tv - = isSkolemTyVar tv && any is_user_skol_tv (cec_encl ctxt) - where - is_user_skol_tv (Implic { ic_skols = sks, ic_info = skol_info }) - = tv `elem` sks && is_user_skol_info skol_info - - is_user_skol_info (InferSkol {}) = False - is_user_skol_info _ = True - misMatchOrCND :: Bool -> ReportErrCtxt -> Ct -> TcType -> TcType -> Report -- If oriented then ty1 is actual, ty2 is expected @@ -1724,21 +1724,29 @@ extraTyVarInfo ctxt tv suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report -- See Note [Suggest adding a type signature] -suggestAddSig ctxt ty1 ty2 - | null inferred_bndrs +suggestAddSig ctxt ty1 _ty2 + | null inferred_bndrs -- No let-bound inferred binders in context = mempty | [bndr] <- inferred_bndrs = important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr) | otherwise = important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs) where - inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2) - get_inf ty | Just tv <- tcGetTyVar_maybe ty - , isSkolemTyVar tv - , ((InferSkol prs, _) : _) <- getSkolemInfo (cec_encl ctxt) [tv] - = map fst prs - | otherwise - = [] + inferred_bndrs = case tcGetTyVar_maybe ty1 of + Just tv | isSkolemTyVar tv -> find (cec_encl ctxt) False tv + _ -> [] + + -- 'find' returns the binders of an InferSkol for 'tv', + -- provided there is an intervening implication with + -- ic_no_eqs = False (i.e. a GADT match) + find [] _ _ = [] + find (implic:implics) seen_eqs tv + | tv `elem` ic_skols implic + , InferSkol prs <- ic_info implic + , seen_eqs + = map fst prs + | otherwise + = find implics (seen_eqs || not (ic_no_eqs implic)) tv -------------------- misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report @@ -2183,9 +2191,8 @@ sameOccExtra ty1 ty2 mod = nameModule nm loc = nameSrcSpan nm -{- -Note [Suggest adding a type signature] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Suggest adding a type signature] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The OutsideIn algorithm rejects GADT programs that don't have a principal type, and indeed some that do. Example: data T a where @@ -2199,6 +2206,15 @@ untouchable type variable. So suggestAddSig sees if the offending type variable is bound by an *inferred* signature, and suggests adding a declared signature instead. +More specifically, we suggest adding a type sig if we have p ~ ty, and +p is a skolem bound by an InferSkol. Those skolems were created from +unification variables in simplifyInfer. Why didn't we unify? It must +have been because of an intervening GADT or existential, making it +untouchable. Either way, a type signature would help. For GADTs, it +might make it typeable; for existentials the attempt to write a +signature will fail -- or at least will produce a better error message +next time + This initially came up in #8968, concerning pattern synonyms. Note [Disambiguating (X ~ X) errors] diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs index 06a75e2a1f..3ff2312903 100644 --- a/compiler/GHC/Tc/Errors/Hole.hs +++ b/compiler/GHC/Tc/Errors/Hole.hs @@ -44,7 +44,7 @@ import Data.List ( partition, sort, sortOn, nubBy ) import Data.Graph ( graphFromEdges, topSort ) -import GHC.Tc.Solver ( simpl_top, runTcSDeriveds ) +import GHC.Tc.Solver ( simplifyTopWanteds, runTcSDeriveds ) import GHC.Tc.Utils.Unify ( tcSubTypeSigma ) import GHC.HsToCore.Docs ( extractDocs ) @@ -957,7 +957,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $ w_rel_cts = addSimples wanted cloned_relevants final_wc = foldr (setWCAndBinds fresh_binds) w_rel_cts outermost_first ; traceTc "final_wc is: " $ ppr final_wc - ; rem <- runTcSDeriveds $ simpl_top final_wc + ; rem <- runTcSDeriveds $ simplifyTopWanteds final_wc -- We don't want any insoluble or simple constraints left, but -- solved implications are ok (and necessary for e.g. undefined) ; traceTc "rems was:" $ ppr rem diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs index 1bd06ddc63..d37f26df40 100644 --- a/compiler/GHC/Tc/Gen/Default.hs +++ b/compiler/GHC/Tc/Gen/Default.hs @@ -71,7 +71,7 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _) tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type tc_default_ty deflt_clss hs_ty - = do { ty <- solveEqualities $ + = do { ty <- solveEqualities "tc_default_ty" $ tcInferLHsType hs_ty ; ty <- zonkTcTypeToType ty -- establish Type invariants ; checkValidType DefaultDeclCtxt ty diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 550d859c81..9c778a1b4b 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -49,8 +49,6 @@ module GHC.Tc.Gen.HsType ( tcInferLHsTypeKind, tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType, tcHsMbContext, tcHsContext, tcLHsPredType, - failIfEmitsConstraints, - solveEqualities, -- useful re-export kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone, @@ -87,7 +85,6 @@ import GHC.Tc.Solver import GHC.Tc.Utils.Zonk import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr -import GHC.Tc.Errors ( reportAllUnsolved ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.Instantiate ( tcInstInvisibleTyBindersN, tcInstInvisibleTyBinder ) import GHC.Core.Type @@ -187,43 +184,122 @@ these variables. Note [Recipe for checking a signature] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Checking a user-written signature requires several steps: +Kind-checking a user-written signature requires several steps: - 1. Generate constraints. - 2. Solve constraints. - 3. Promote tyvars and/or kind-generalize. - 4. Zonk. - 5. Check validity. + 0. Bump the TcLevel + 1. Bind any lexically-scoped type variables. + 2. Generate constraints. + 3. Solve constraints. + 4. Sort any implicitly-bound variables into dependency order + 5. Promote tyvars and/or kind-generalize. + 6. Zonk. + 7. Check validity. -There may be some surprises in here: +Very similar steps also apply when kind-checking a type or class +declaration. -Step 2 is necessary for two reasons: most signatures also bring -implicitly quantified variables into scope, and solving is necessary -to get these in the right order (see Note [Keeping implicitly -quantified variables in order]). Additionally, solving is necessary in -order to kind-generalize correctly: otherwise, we do not know which -metavariables are left unsolved. +The general pattern looks something like this. (But NB every +specific instance varies in one way or another!) -Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to -kindGeneralize{All,Some,None}. Here, we have to deal with the fact that -metatyvars generated in the type may have a bumped TcLevel, because explicit -foralls raise the TcLevel. To avoid these variables from ever being visible in -the surrounding context, we must obey the following dictum: + do { (tclvl, wanted, (spec_tkvs, ty)) + <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $ + bindImplicitTKBndrs_Skol sig_vars $ + <kind-check the type> + + ; spec_tkvs <- zonkAndScopedSort spec_tkvs + + ; reportUnsolvedEqualities skol_info spec_tkvs tclvl wanted + + ; let ty1 = mkSpecForAllTys spec_tkvs ty + ; kvs <- kindGeneralizeAll ty1 + + ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1) + + ; checkValidType final_ty + +This pattern is repeated many times in GHC.Tc.Gen.HsType, +GHC.Tc.Gen.Sig, and GHC.Tc.TyCl, with variations. In more detail: + +* pushLevelAndSolveEqualitiesX (Step 0, step 3) bumps the TcLevel, + calls the thing inside to generate constraints, solves those + constraints as much as possible, returning the residual unsolved + constraints in 'wanted'. + +* bindImplicitTKBndrs_Skol (Step 1) binds the user-specified type + variables E.g. when kind-checking f :: forall a. F a -> a we must + bring 'a' into scope before kind-checking (F a -> a) + +* zonkAndScopedSort (Step 4) puts those user-specified variables in + the dependency order. (For "implicit" variables the order is no + user-specified. E.g. forall (a::k1) (b::k2). blah k1 and k2 are + implicitly brought into scope. + +* reportUnsolvedEqualities (Step 3 continued) reports any unsolved + equalities, carefully wrapping them in an implication that binds the + skolems. We can't do that in pushLevelAndSolveEqualitiesX because + that function doesn't have access to the skolems. + +* kindGeneralize (Step 5). See Note [Kind generalisation] + +* The final zonkTcTypeToType must happen after promoting/generalizing, + because promoting and generalizing fill in metavariables. + + +Doing Step 3 (constraint solving) eagerly (rather than building an +implication constraint and solving later) is necessary for several +reasons: + +* Exactly as for Solver.simplifyInfer: when generalising, we solve all + the constraints we can so that we don't have to quantify over them + or, since we don't quantify over constraints in kinds, float them + and inhibit generalisation. + +* Most signatures also bring implicitly quantified variables into + scope, and solving is necessary to get these in the right order + (Step 4) see Note [Keeping implicitly quantified variables in + order]). + +Note [Kind generalisation] +~~~~~~~~~~~~~~~~~~~~~~~~~~ +Step 5 of Note [Recipe for checking a signature], namely +kind-generalisation, is done by + kindGeneraliseAll + kindGeneraliseSome + kindGeneraliseNone + +Here, we have to deal with the fact that metatyvars generated in the +type will have a bumped TcLevel, because explicit foralls raise the +TcLevel. To avoid these variables from ever being visible in the +surrounding context, we must obey the following dictum: Every metavariable in a type must either be (A) generalized, or (B) promoted, or See Note [Promotion in signatures] - (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType + (C) a cause to error See Note [Naughty quantification candidates] + in GHC.Tc.Utils.TcMType + +There are three steps (look at kindGeneraliseSome): + +1. candidateQTyVarsOfType finds the free variables of the type or kind, + to generalise + +2. filterConstrainedCandidates filters out candidates that appear + in the unsolved 'wanteds', and promotes the ones that get filtered out + thereby. + +3. quantifyTyVars quantifies the remaining type variables The kindGeneralize functions do not require pre-zonking; they zonk as they go. -If you are actually doing kind-generalization, you need to bump the level -before generating constraints, as we will only generalize variables with -a TcLevel higher than the ambient one. +kindGeneraliseAll specialises for the case where step (2) is vacuous. +kindGeneraliseNone specialises for the case where we do no quantification, +but we must still promote. -After promoting/generalizing, we need to zonk again because both -promoting and generalizing fill in metavariables. +If you are actually doing kind-generalization, you need to bump the +level before generating constraints, as we will only generalize +variables with a TcLevel higher than the ambient one. +Hence the "pushLevel" in pushLevelAndSolveEqualities. Note [Promotion in signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -301,10 +377,9 @@ kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM () kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars , hsib_body = hs_ty }) = addSigCtxt (funsSigCtxt names) hs_ty $ - do { (tc_lvl, (wanted, (spec_tkvs, _))) - <- pushTcLevelM $ - solveLocalEqualitiesX "kcClassSigType" $ - bindImplicitTKBndrs_Skol sig_vars $ + do { (tc_lvl, wanted, (spec_tkvs, _)) + <- pushLevelAndSolveEqualitiesX "kcClassSigType" $ + bindImplicitTKBndrs_Skol sig_vars $ tcLHsType hs_ty liftedTypeKind ; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted } @@ -364,27 +439,19 @@ tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -- Returns also an implication for the unsolved constraints tc_hs_sig_type skol_info hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type - = do { (tc_lvl, (wanted, (spec_tkvs, ty))) - <- pushTcLevelM $ - solveLocalEqualitiesX "tc_hs_sig_type" $ + = do { (tc_lvl, wanted, (spec_tkvs, ty)) + <- pushLevelAndSolveEqualitiesX "tc_hs_sig_type" $ -- See Note [Failure in local type signatures] bindImplicitTKBndrs_Skol sig_vars $ do { kind <- newExpectedKind ctxt_kind ; tcLHsType hs_ty kind } - -- Any remaining variables (unsolved in the solveLocalEqualities) + -- Any remaining variables (unsolved in the solveEqualities) -- should be in the global tyvars, and therefore won't be quantified ; spec_tkvs <- zonkAndScopedSort spec_tkvs ; let ty1 = mkSpecForAllTys spec_tkvs ty - -- This bit is very much like decideMonoTyVars in GHC.Tc.Solver, - -- but constraints are so much simpler in kinds, it is much - -- easier here. (In particular, we never quantify over a - -- constraint in a type.) - ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted) - ; let should_gen = not . (`elemVarSet` constrained) - - ; kvs <- kindGeneralizeSome should_gen ty1 + ; kvs <- kindGeneralizeSome wanted ty1 -- Build an implication for any as-yet-unsolved kind equalities -- See Note [Skolem escape in type signatures] @@ -448,16 +515,18 @@ tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type tc_top_lhs_type mode hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { traceTc "tcTopLHsType {" (ppr hs_ty) - ; (spec_tkvs, ty) - <- pushTcLevelM_ $ - solveEqualities $ - bindImplicitTKBndrs_Skol sig_vars $ + ; (tclvl, wanted, (spec_tkvs, ty)) + <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $ + bindImplicitTKBndrs_Skol sig_vars $ do { kind <- newExpectedKind ctxt_kind ; tc_lhs_type mode hs_ty kind } ; spec_tkvs <- zonkAndScopedSort spec_tkvs + ; reportUnsolvedEqualities InstSkol spec_tkvs tclvl wanted + ; let ty1 = mkSpecForAllTys spec_tkvs ty - ; kvs <- kindGeneralizeAll ty1 -- "All" because it's a top-level type + ; kvs <- kindGeneralizeAll ty1 + ; final_ty <- zonkTcTypeToType (mkInfForAllTys kvs ty1) ; traceTc "End tcTopLHsType }" (vcat [ppr hs_ty, ppr final_ty]) ; return final_ty} @@ -533,7 +602,7 @@ tcHsTypeApp wc_ty kind = do { mode <- mkHoleMode TypeLevel HM_VTA -- HM_VTA: See Note [Wildcards in visible type application] ; ty <- addTypeCtxt hs_ty $ - solveLocalEqualities "tcHsTypeApp" $ + solveEqualities "tcHsTypeApp" $ -- We are looking at a user-written type, very like a -- signature so we want to solve its equalities right now tcNamedWildCardBinders sig_wcs $ \ _ -> @@ -985,8 +1054,9 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind --------- Foralls tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind = do { (tclvl, wanted, (tv_bndrs, ty')) - <- pushLevelAndCaptureConstraints $ - bindExplicitTKTele_Skol_M mode tele $ + <- pushLevelAndCaptureConstraints $ + -- No need to solve equalities here; we will do that later + bindExplicitTKTele_Skol_M mode tele $ -- The _M variant passes on the mode from the type, to -- any wildards in kind signatures on the forall'd variables -- e.g. f :: _ -> Int -> forall (a :: _). blah @@ -1000,22 +1070,15 @@ tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind map ppr hs_tvs HsForAllInvis { hsf_invis_bndrs = hs_tvs } -> map ppr hs_tvs - tv_bndrs' = construct_bndrs tv_bndrs - skol_tvs = binderVars tv_bndrs' + skol_tvs = binderVars tv_bndrs + ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted ; emitImplication implic -- /Always/ emit this implication even if wanted is empty -- We need the implication so that we check for a bad telescope -- See Note [Skolem escape and forall-types] - ; return (mkForAllTys tv_bndrs' ty') } - where - construct_bndrs :: Either [TcReqTVBinder] [TcInvisTVBinder] - -> [TcTyVarBinder] - construct_bndrs (Left req_tv_bndrs) = - map (mkTyVarBinder Required . binderVar) req_tv_bndrs - construct_bndrs (Right inv_tv_bndrs) = - map tyVarSpecToBinder inv_tv_bndrs + ; return (mkForAllTys tv_bndrs ty') } tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind | null (unLoc ctxt) @@ -2194,11 +2257,10 @@ kcCheckDeclHeader_cusk name flav -- CUSK case -- See note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl = addTyConFlavCtxt name flav $ - do { (scoped_kvs, (tc_tvs, res_kind)) - <- pushTcLevelM_ $ - solveEqualities $ - bindImplicitTKBndrs_Q_Skol kv_ns $ - bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $ + do { (tclvl, wanted, (scoped_kvs, (tc_tvs, res_kind))) + <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_cusk" $ + bindImplicitTKBndrs_Q_Skol kv_ns $ + bindExplicitTKBndrs_Q_Skol ctxt_kind hs_tvs $ newExpectedKind =<< kc_res_ki -- Now, because we're in a CUSK, @@ -2234,6 +2296,10 @@ kcCheckDeclHeader_cusk name flav tycon = mkTcTyCon name final_tc_binders res_kind all_tv_prs True -- it is generalised flav + + ; reportUnsolvedEqualities skol_info (binderVars final_tc_binders) + tclvl wanted + -- If the ordering from -- Note [Required, Specified, and Inferred for types] in GHC.Tc.TyCl -- doesn't work, we catch it here, before an error cascade @@ -2256,6 +2322,7 @@ kcCheckDeclHeader_cusk name flav ; return tycon } where + skol_info = TyConSkol flav name ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind @@ -2358,11 +2425,10 @@ kcCheckDeclHeader_sig kisig name flav -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars ; (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders - ; (implicit_tvs, (invis_binders, r_ki)) - <- pushTcLevelM_ $ - solveEqualities $ -- #16687 - bindImplicitTKBndrs_Tv implicit_nms $ - tcExtendNameTyVarEnv explicit_tv_prs $ + ; (tclvl, wanted, (implicit_tvs, (invis_binders, r_ki))) + <- pushLevelAndSolveEqualitiesX "kcCheckDeclHeader_sig" $ -- #16687 + bindImplicitTKBndrs_Tv implicit_nms $ + tcExtendNameTyVarEnv explicit_tv_prs $ do { -- Check that inline kind annotations on binders are valid. -- For example: -- @@ -2416,7 +2482,11 @@ kcCheckDeclHeader_sig kisig name flav ; let tcbs = vis_tcbs ++ invis_tcbs implicit_tv_prs = implicit_nms `zip` implicit_tvs all_tv_prs = implicit_tv_prs ++ explicit_tv_prs - tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav + tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav + skol_info = TyConSkol flav name + + -- Check that there are no unsolved equalities + ; reportUnsolvedEqualities skol_info (binderVars tcbs) tclvl wanted ; traceTc "kcCheckDeclHeader_sig done:" $ vcat [ text "tyConName = " <+> ppr (tyConName tc) @@ -2506,7 +2576,7 @@ kcCheckDeclHeader_sig kisig name flav KindedTyVar _ _ v v_hs_ki -> do v_ki <- tcLHsKindSig (TyVarBndrKindCtxt (unLoc v)) v_hs_ki discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] - unifyKind (Just (HsTyVar noExtField NotPromoted v)) + unifyKind (Just (ppr v)) (tyBinderType tb) v_ki @@ -2960,19 +3030,22 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar -------------------------------------- -- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope. --- Returns 'Left' for visible @forall@s and 'Right' for invisible @forall@s. bindExplicitTKTele_Skol_M :: TcTyMode -> HsForAllTelescope GhcRn -> TcM a - -> TcM (Either [TcReqTVBinder] [TcInvisTVBinder], a) + -> TcM ([TcTyVarBinder], a) bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of - HsForAllVis { hsf_vis_bndrs = bndrs } -> do - (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside - pure (Left req_tv_bndrs, thing) - HsForAllInvis { hsf_invis_bndrs = bndrs } -> do - (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside - pure (Right inv_tv_bndrs, thing) + HsForAllVis { hsf_vis_bndrs = bndrs } + -> do { (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside + -- req_tv_bndrs :: [VarBndr TyVar ()], + -- but we want [VarBndr TyVar ArgFlag] + ; return (tyVarReqToBinders req_tv_bndrs, thing) } + HsForAllInvis { hsf_invis_bndrs = bndrs } + -> do { (inv_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside + -- inv_tv_bndrs :: [VarBndr TyVar Specificity], + -- but we want [VarBndr TyVar ArgFlag] + ; return (tyVarSpecToBinders inv_tv_bndrs, thing) } bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv :: (OutputableBndrFlag flag) @@ -3012,10 +3085,10 @@ bindExplicitTKBndrsX_Q -- with the passed-in [LHsTyVarBndr] bindExplicitTKBndrsX_Q tc_tv hs_tvs thing_inside = do { (tv_bndrs,res) <- bindExplicitTKBndrsX tc_tv hs_tvs thing_inside - ; return ((binderVars tv_bndrs),res) } + ; return (binderVars tv_bndrs,res) } bindExplicitTKBndrsX :: (OutputableBndrFlag flag) - => (HsTyVarBndr flag GhcRn -> TcM TcTyVar) + => (HsTyVarBndr flag GhcRn -> TcM TyVar) -> [LHsTyVarBndr flag GhcRn] -> TcM a -> TcM ([VarBndr TyVar flag], a) -- Returned [TcTyVar] are in 1-1 correspondence @@ -3035,7 +3108,7 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside -- See GHC.Tc.Utils.TcMType Note [Cloning for tyvar binders] ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $ go hs_tvs - ; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) } + ; return (Bndr tv (hsTyVarBndrFlag hs_tv):tvs, res) } ----------------- tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar) @@ -3066,7 +3139,7 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) ; mb_tv <- tcLookupLcl_maybe tv_nm ; case mb_tv of Just (ATyVar _ tv) - -> do { discardResult $ unifyKind (Just hs_tv) + -> do { discardResult $ unifyKind (Just (ppr tv_nm)) kind (tyVarKind tv) -- This unify rejects: -- class C (m :: * -> *) where @@ -3074,9 +3147,6 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) ; return tv } _ -> new_tv tv_nm kind } - where - hs_tv = HsTyVar noExtField NotPromoted (noLoc tv_nm) - -- Used for error messages only -------------------------------------- -- Binding type/class variables in the @@ -3116,56 +3186,63 @@ zonkAndScopedSort spec_tkvs -- | Generalize some of the free variables in the given type. -- All such variables should be *kind* variables; any type variables -- should be explicitly quantified (with a `forall`) before now. --- The supplied predicate says which free variables to quantify. --- But in all cases, --- generalize only those variables whose TcLevel is strictly greater --- than the ambient level. This "strictly greater than" means that --- you likely need to push the level before creating whatever type --- gets passed here. Any variable whose level is greater than the --- ambient level but is not selected to be generalized will be --- promoted. (See [Promoting unification variables] in "GHC.Tc.Solver" --- and Note [Recipe for checking a signature].) --- The resulting KindVar are the variables to --- quantify over, in the correct, well-scoped order. They should --- generally be Inferred, not Specified, but that's really up to --- the caller of this function. -kindGeneralizeSome :: (TcTyVar -> Bool) +-- +-- The WantedConstraints are un-solved kind constraints. Generally +-- they'll be reported as errors later, but meanwhile we refrain +-- from quantifying over any variable free in these unsolved +-- constraints. See Note [Failure in local type signatures]. +-- +-- But in all cases, generalize only those variables whose TcLevel is +-- strictly greater than the ambient level. This "strictly greater +-- than" means that you likely need to push the level before creating +-- whatever type gets passed here. +-- +-- Any variable whose level is greater than the ambient level but is +-- not selected to be generalized will be promoted. (See [Promoting +-- unification variables] in "GHC.Tc.Solver" and Note [Recipe for +-- checking a signature].) +-- +-- The resulting KindVar are the variables to quantify over, in the +-- correct, well-scoped order. They should generally be Inferred, not +-- Specified, but that's really up to the caller of this function. +kindGeneralizeSome :: WantedConstraints -> TcType -- ^ needn't be zonked -> TcM [KindVar] -kindGeneralizeSome should_gen kind_or_type - = do { traceTc "kindGeneralizeSome {" (ppr kind_or_type) - - -- use the "Kind" variant here, as any types we see +kindGeneralizeSome wanted kind_or_type + = do { -- Use the "Kind" variant here, as any types we see -- here will already have all type variables quantified; -- thus, every free variable is really a kv, never a tv. ; dvs <- candidateQTyVarsOfKind kind_or_type - - -- So 'dvs' are the variables free in kind_or_type, with a level greater - -- than the ambient level, hence candidates for quantification - -- Next: filter out the ones we don't want to generalize (specified by should_gen) - -- and promote them instead - - ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen) - + ; dvs <- filterConstrainedCandidates wanted dvs + ; quantifyTyVars dvs } + +filterConstrainedCandidates + :: WantedConstraints -- Don't quantify over variables free in these + -- Not necessarily fully zonked + -> CandidatesQTvs -- Candidates for quantification + -> TcM CandidatesQTvs +-- filterConstrainedCandidates removes any candidates that are free in +-- 'wanted'; instead, it promotes them. This bit is very much like +-- decideMonoTyVars in GHC.Tc.Solver, but constraints are so much +-- simpler in kinds, it is much easier here. (In particular, we never +-- quantify over a constraint in a type.) +filterConstrainedCandidates wanted dvs + | isEmptyWC wanted -- Fast path for a common case + = return dvs + | otherwise + = do { wc_tvs <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted) + ; let (to_promote, dvs') = partitionCandidates dvs (`elemVarSet` wc_tvs) ; _ <- promoteTyVarSet to_promote - ; qkvs <- quantifyTyVars dvs' - - ; traceTc "kindGeneralizeSome }" $ - vcat [ text "Kind or type:" <+> ppr kind_or_type - , text "dvs:" <+> ppr dvs - , text "dvs':" <+> ppr dvs' - , text "to_promote:" <+> ppr to_promote - , text "qkvs:" <+> pprTyVars qkvs ] - - ; return qkvs } - --- | Specialized version of 'kindGeneralizeSome', but where all variables --- can be generalized. Use this variant when you can be sure that no more --- constraints on the type's metavariables will arise or be solved. -kindGeneralizeAll :: TcType -- needn't be zonked - -> TcM [KindVar] -kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty - ; kindGeneralizeSome (const True) ty } + ; return dvs' } + +-- |- Specialised verison of 'kindGeneralizeSome', but with empty +-- WantedConstraints, so no filtering is needed +-- i.e. kindGeneraliseAll = kindGeneralizeSome emptyWC +kindGeneralizeAll :: TcType -> TcM [KindVar] +kindGeneralizeAll kind_or_type + = do { traceTc "kindGeneralizeAll" (ppr kind_or_type) + ; dvs <- candidateQTyVarsOfKind kind_or_type + ; quantifyTyVars dvs } -- | Specialized version of 'kindGeneralizeSome', but where no variables -- can be generalized, but perhaps some may neeed to be promoted. @@ -3177,11 +3254,11 @@ kindGeneralizeAll ty = do { traceTc "kindGeneralizeAll" empty -- Note [Promotion in signatures]. kindGeneralizeNone :: TcType -- needn't be zonked -> TcM () -kindGeneralizeNone ty - = do { traceTc "kindGeneralizeNone" empty - ; kvs <- kindGeneralizeSome (const False) ty - ; MASSERT( null kvs ) - } +kindGeneralizeNone kind_or_type + = do { traceTc "kindGeneralizeNone" (ppr kind_or_type) + ; dvs <- candidateQTyVarsOfKind kind_or_type + ; _ <- promoteTyVarSet (candidateKindVars dvs) + ; return () } {- Note [Levels and generalisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -3508,10 +3585,10 @@ tcHsPartialSigType ctxt sig_ty = addSigCtxt ctxt hs_ty $ do { mode <- mkHoleMode TypeLevel HM_Sig ; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau))) - <- solveLocalEqualities "tcHsPartialSigType" $ + <- solveEqualities "tcHsPartialSigType" $ -- See Note [Failure in local type signatures] - tcNamedWildCardBinders sig_wcs $ \ wcs -> - bindImplicitTKBndrs_Tv implicit_hs_tvs $ + tcNamedWildCardBinders sig_wcs $ \ wcs -> + bindImplicitTKBndrs_Tv implicit_hs_tvs $ bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $ do { -- Instantiate the type-class context; but if there -- is an extra-constraints wildcard, just discard it here @@ -3718,11 +3795,11 @@ tcHsPatSigType ctxt do { sig_tkv_prs <- mapM new_implicit_tv sig_ns ; mode <- mkHoleMode TypeLevel HM_Sig ; (wcs, sig_ty) - <- addTypeCtxt hs_ty $ - solveLocalEqualities "tcHsPatSigType" $ + <- addTypeCtxt hs_ty $ + solveEqualities "tcHsPatSigType" $ -- See Note [Failure in local type signatures] -- and c.f #16033 - tcNamedWildCardBinders sig_wcs $ \ wcs -> + tcNamedWildCardBinders sig_wcs $ \ wcs -> tcExtendNameTyVarEnv sig_tkv_prs $ do { ek <- newOpenTypeKind ; sig_ty <- tc_lhs_type mode hs_ty ek @@ -3768,7 +3845,7 @@ Here It must be a skolem so that it retains its identity, and GHC.Tc.Errors.getSkolemInfo can thereby find the binding site for the skolem. - * The type signature pattern (f :: b -> c) makes freshs meta-tyvars + * The type signature pattern (f :: b -> c) makes fresh meta-tyvars beta and gamma (TauTvs), and binds "b" :-> beta, "c" :-> gamma in the environment @@ -3796,7 +3873,7 @@ For RULE binders, though, things are a bit different (yuk). RULE "foo" forall (x::a) (y::[a]). f x y = ... Here this really is the binding site of the type variable so we'd like to use a skolem, so that we get a complaint if we unify two of them -together. Hence the new_tv function in tcHsPatSigType. +together. Hence the new_implicit_tv function in tcHsPatSigType. ************************************************************************ @@ -3835,7 +3912,7 @@ tc_lhs_kind_sig mode ctxt hs_kind -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType -- Result is zonked = do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $ - solveLocalEqualities "tcLHsKindSig" $ + solveEqualities "tcLHsKindSig" $ tc_lhs_type mode hs_kind liftedTypeKind ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind) -- No generalization: @@ -3876,19 +3953,6 @@ promotionErr name err -} --- | If the inner action emits constraints, report them as errors and fail; --- otherwise, propagates the return value. Useful as a wrapper around --- 'tcImplicitTKBndrs', which uses solveLocalEqualities, when there won't be --- another chance to solve constraints -failIfEmitsConstraints :: TcM a -> TcM a -failIfEmitsConstraints thing_inside - = checkNoErrs $ -- We say that we fail if there are constraints! - -- c.f same checkNoErrs in solveEqualities - do { (res, lie) <- captureConstraints thing_inside - ; reportAllUnsolved lie - ; return res - } - -- | Make an appropriate message for an error in a function argument. -- Used for both expressions and types. funAppCtxt :: (Outputable fun, Outputable arg) => fun -> arg -> Int -> SDoc diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index 6226bbc65e..170930c2ff 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -14,7 +14,7 @@ module GHC.Tc.Gen.Sig( TcSigFun, isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName, - completeSigPolyId_maybe, + completeSigPolyId_maybe, isCompleteHsSig, tcTySigs, tcUserTypeSig, completeSigFromId, tcInstSig, @@ -30,6 +30,7 @@ import GHC.Prelude import GHC.Hs import GHC.Tc.Gen.HsType import GHC.Tc.Types +import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities ) import GHC.Tc.Utils.Monad import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType @@ -360,23 +361,18 @@ Once we get to type checking, we decompose it into its parts, in tcPatSynSig. * After we kind-check the pieces and convert to Types, we do kind generalisation. -Note [solveEqualities in tcPatSynSig] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Report unsolved equalities in tcPatSynSig] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's important that we solve /all/ the equalities in a pattern synonym signature, because we are going to zonk the signature to a Type (not a TcType), in GHC.Tc.TyCl.PatSyn.tc_patsyn_finish, and that fails if there are un-filled-in coercion variables mentioned in the type (#15694). -The best thing is simply to use solveEqualities to solve all the -equalites, rather than leaving them in the ambient constraints -to be solved later. Pattern synonyms are top-level, so there's -no problem with completely solving them. - -(NB: this solveEqualities wraps newImplicitTKBndrs, which itself -does a solveLocalEqualities; so solveEqualities isn't going to -make any further progress; it'll just report any unsolved ones, -and fail, as it should.) +So we solve all the equalities we can, and report any unsolved ones, +rather than leaving them in the ambient constraints to be solved +later. Pattern synonyms are top-level, so there's no problem with +completely solving them. -} tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo @@ -388,12 +384,11 @@ tcPatSynSig name sig_ty , (univ_hs_tvbndrs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty , (ex_hs_tvbndrs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1 = do { traceTc "tcPatSynSig 1" (ppr sig_ty) - ; (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty)))) - <- pushTcLevelM_ $ - solveEqualities $ -- See Note [solveEqualities in tcPatSynSig] - bindImplicitTKBndrs_Skol implicit_hs_tvs $ - bindExplicitTKBndrs_Skol univ_hs_tvbndrs $ - bindExplicitTKBndrs_Skol ex_hs_tvbndrs $ + ; (tclvl, wanted, (implicit_tvs, (univ_tvbndrs, (ex_tvbndrs, (req, prov, body_ty))))) + <- pushLevelAndSolveEqualitiesX "tcPatSynSig" $ + bindImplicitTKBndrs_Skol implicit_hs_tvs $ + bindExplicitTKBndrs_Skol univ_hs_tvbndrs $ + bindExplicitTKBndrs_Skol ex_hs_tvbndrs $ do { req <- tcHsContext hs_req ; prov <- tcHsContext hs_prov ; body_ty <- tcHsOpenType hs_body_ty @@ -401,6 +396,7 @@ tcPatSynSig name sig_ty -- e.g. pattern Zero <- 0# (#12094) ; return (req, prov, body_ty) } + ; implicit_tvs <- zonkAndScopedSort implicit_tvs ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvbndrs req ex_tvbndrs prov body_ty @@ -408,61 +404,46 @@ tcPatSynSig name sig_ty ; kvs <- kindGeneralizeAll ungen_patsyn_ty ; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty) + ; let skol_tvs = kvs ++ implicit_tvs ++ binderVars (univ_tvbndrs ++ ex_tvbndrs) + skol_info = DataConSkol name + ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted + -- See Note [Report unsolved equalities in tcPatSynSig] + -- These are /signatures/ so we zonk to squeeze out any kind - -- unification variables. Do this after kindGeneralize which may + -- unification variables. Do this after kindGeneralizeAll which may -- default kind variables to *. - ; implicit_tvs <- zonkAndScopedSort implicit_tvs + ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs ; univ_tvbndrs <- mapM zonkTyCoVarKindBinder univ_tvbndrs ; ex_tvbndrs <- mapM zonkTyCoVarKindBinder ex_tvbndrs ; req <- zonkTcTypes req ; prov <- zonkTcTypes prov ; body_ty <- zonkTcType body_ty - -- Skolems have TcLevels too, though they're used only for debugging. - -- If you don't do this, the debugging checks fail in GHC.Tc.TyCl.PatSyn. - -- Test case: patsyn/should_compile/T13441 -{- - ; tclvl <- getTcLevel - ; let env0 = mkEmptyTCvSubst $ mkInScopeSet $ mkVarSet kvs - (env1, implicit_tvs') = promoteSkolemsX tclvl env0 implicit_tvs - (env2, univ_tvs') = promoteSkolemsX tclvl env1 univ_tvs - (env3, ex_tvs') = promoteSkolemsX tclvl env2 ex_tvs - req' = substTys env3 req - prov' = substTys env3 prov - body_ty' = substTy env3 body_ty --} - ; let implicit_tvs' = implicit_tvs - univ_tvbndrs' = univ_tvbndrs - ex_tvbndrs' = ex_tvbndrs - req' = req - prov' = prov - body_ty' = body_ty - -- Now do validity checking ; checkValidType ctxt $ - build_patsyn_type kvs implicit_tvs' univ_tvbndrs' req' ex_tvbndrs' prov' body_ty' + build_patsyn_type kvs implicit_tvs univ_tvbndrs req ex_tvbndrs prov body_ty -- arguments become the types of binders. We thus cannot allow -- levity polymorphism here - ; let (arg_tys, _) = tcSplitFunTys body_ty' + ; let (arg_tys, _) = tcSplitFunTys body_ty ; mapM_ (checkForLevPoly empty . scaledThing) arg_tys ; traceTc "tcTySig }" $ - vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs' + vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs , text "kvs" <+> ppr_tvs kvs - , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs') - , text "req" <+> ppr req' - , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs') - , text "prov" <+> ppr prov' - , text "body_ty" <+> ppr body_ty' ] + , text "univ_tvs" <+> ppr_tvs (binderVars univ_tvbndrs) + , text "req" <+> ppr req + , text "ex_tvs" <+> ppr_tvs (binderVars ex_tvbndrs) + , text "prov" <+> ppr prov + , text "body_ty" <+> ppr body_ty ] ; return (TPSI { patsig_name = name , patsig_implicit_bndrs = mkTyVarBinders InferredSpec kvs ++ - mkTyVarBinders SpecifiedSpec implicit_tvs' - , patsig_univ_bndrs = univ_tvbndrs' - , patsig_req = req' - , patsig_ex_bndrs = ex_tvbndrs' - , patsig_prov = prov' - , patsig_body_ty = body_ty' }) } + mkTyVarBinders SpecifiedSpec implicit_tvs + , patsig_univ_bndrs = univ_tvbndrs + , patsig_req = req + , patsig_ex_bndrs = ex_tvbndrs + , patsig_prov = prov + , patsig_body_ty = body_ty }) } where ctxt = PatSynCtxt name diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index c18ce5f3cf..5871eb99ea 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -1435,11 +1435,17 @@ reifyInstances th_nm th_tys rnImplicitBndrs Nothing tv_rdrs $ \ tv_names -> do { (rn_ty, fvs) <- rnLHsType doc rdr_ty ; return ((tv_names, rn_ty), fvs) } - ; (_tvs, ty) - <- pushTcLevelM_ $ - solveEqualities $ -- Avoid error cascade if there are unsolved - bindImplicitTKBndrs_Skol tv_names $ + + ; (tclvl, wanted, (tvs, ty)) + <- pushLevelAndSolveEqualitiesX "reifyInstances" $ + bindImplicitTKBndrs_Skol tv_names $ tcInferLHsType rn_ty + + ; tvs <- zonkAndScopedSort tvs + + -- Avoid error cascade if there are unsolved + ; reportUnsolvedEqualities ReifySkol tvs tclvl wanted + ; ty <- zonkTcTypeToType ty -- Substitute out the meta type variables -- In particular, the type might have kind diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index f29378122c..784625f3a2 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -2589,18 +2589,18 @@ tcRnType hsc_env flexi normalise rdr_type -- It can have any rank or kind -- First bring into scope any wildcards ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type]) - ; (ty, kind) <- pushTcLevelM_ $ - -- must push level to satisfy level precondition of - -- kindGeneralize, below - solveEqualities $ - tcNamedWildCardBinders wcs $ \ wcs' -> - do { mapM_ emitNamedTypeHole wcs' - ; tcInferLHsTypeUnsaturated rn_type } + ; (_tclvl, wanted, (ty, kind)) + <- pushLevelAndSolveEqualitiesX "tcRnType" $ + tcNamedWildCardBinders wcs $ \ wcs' -> + do { mapM_ emitNamedTypeHole wcs' + ; tcInferLHsTypeUnsaturated rn_type } + + ; checkNoErrs (reportAllUnsolved wanted) -- Do kind generalisation; see Note [Kind-generalise in tcRnType] ; kvs <- kindGeneralizeAll kind - ; e <- mkEmptyZonkEnv flexi + ; e <- mkEmptyZonkEnv flexi ; ty <- zonkTcTypeToTypeX e ty -- Do validity checking on type @@ -2615,6 +2615,7 @@ tcRnType hsc_env flexi normalise rdr_type ; return (ty', mkInfForAllTys kvs (tcTypeKind ty')) } + {- Note [TcRnExprMode] ~~~~~~~~~~~~~~~~~~~~~~ How should we infer a type when a user asks for the type of an expression e diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index ad0ea2ed3c..2aa1189bcf 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -7,14 +7,16 @@ module GHC.Tc.Solver( simplifyDefault, simplifyTop, simplifyTopImplic, simplifyInteractive, - solveEqualities, solveLocalEqualities, solveLocalEqualitiesX, + solveEqualities, + pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX, + reportUnsolvedEqualities, simplifyWantedsTcM, tcCheckSatisfiability, tcNormalise, captureTopConstraints, - simpl_top, + simplifyTopWanteds, promoteTyVarSet, emitFlatConstraints, @@ -42,8 +44,9 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Solver.Interact import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack ) import GHC.Tc.Solver.Flatten ( flattenType ) -import GHC.Tc.Utils.TcMType as TcM -import GHC.Tc.Utils.Monad as TcM +import GHC.Tc.Utils.Unify ( buildTvImplication ) +import GHC.Tc.Utils.TcMType as TcM +import GHC.Tc.Utils.Monad as TcM import GHC.Tc.Solver.Monad as TcS import GHC.Tc.Types.Constraint import GHC.Core.Predicate @@ -56,7 +59,6 @@ import GHC.Utils.Misc import GHC.Utils.Panic import GHC.Types.Var import GHC.Types.Var.Set -import GHC.Types.Unique.Set import GHC.Types.Basic ( IntWithInf, intGtLimit ) import GHC.Utils.Error ( emptyMessages ) import qualified GHC.LanguageExtensions as LangExt @@ -85,7 +87,7 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) -- -- Importantly, if captureTopConstraints propagates an exception, it -- reports any insoluble constraints first, lest they be lost --- altogether. This is important, because solveLocalEqualities (maybe +-- altogether. This is important, because solveEqualities (maybe -- other things too) throws an exception without adding any error -- messages; it just puts the unsolved constraints back into the -- monad. See GHC.Tc.Utils.Monad Note [Constraints and errors] @@ -129,7 +131,7 @@ simplifyTop :: WantedConstraints -> TcM (Bag EvBind) simplifyTop wanteds = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds ; ((final_wc, unsafe_ol), binds1) <- runTcS $ - do { final_wc <- simpl_top wanteds + do { final_wc <- simplifyTopWanteds wanteds ; unsafe_ol <- getSafeOverlapFailures ; return (final_wc, unsafe_ol) } ; traceTc "End simplifyTop }" empty @@ -155,16 +157,54 @@ simplifyTop wanteds ; return (evBindMapBinds binds1 `unionBags` binds2) } +pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a +-- Push level, and solve all resulting equalities +-- If there are any unsolved equalities, report them +-- and fail (in the monad) +-- +-- Panics if we solve any non-equality constraints. (In runTCSEqualities +-- we use an error thunk for the evidence bindings.) +pushLevelAndSolveEqualities skol_info skol_tvs thing_inside + = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX + "pushLevelAndSolveEqualities" thing_inside + ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted + ; return res } + +pushLevelAndSolveEqualitiesX :: String -> TcM a + -> TcM (TcLevel, WantedConstraints, a) +-- Push the level, gather equality constraints, and then solve them. +-- Returns any remaining unsolved equalities. +-- Does not report errors. +-- +-- Panics if we solve any non-equality constraints. (In runTCSEqualities +-- we use an error thunk for the evidence bindings.) +pushLevelAndSolveEqualitiesX callsite thing_inside + = do { traceTc "pushLevelAndSolveEqualitiesX {" (text "Called from" <+> text callsite) + ; (tclvl, (wanted, res)) + <- pushTcLevelM $ + do { (res, wanted) <- captureConstraints thing_inside + ; wanted <- runTcSEqualities (simplifyTopWanteds wanted) + ; return (wanted,res) } + ; traceTc "pushLevelAndSolveEqualities }" (vcat [ text "Residual:" <+> ppr wanted + , text "Level:" <+> ppr tclvl ]) + ; return (tclvl, wanted, res) } -- | Type-check a thing that emits only equality constraints, solving any --- constraints we can and re-emitting constraints that we can't. The thing_inside --- should generally bump the TcLevel to make sure that this run of the solver --- doesn't affect anything lying around. -solveLocalEqualities :: String -> TcM a -> TcM a --- Note [Failure in local type signatures] -solveLocalEqualities callsite thing_inside - = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside - ; emitFlatConstraints wanted +-- constraints we can and re-emitting constraints that we can't. +-- Use this variant only when we'll get another crack at it later +-- See Note [Failure in local type signatures] +-- +-- Panics if we solve any non-equality constraints. (In runTCSEqualities +-- we use an error thunk for the evidence bindings.) +solveEqualities :: String -> TcM a -> TcM a +solveEqualities callsite thing_inside + = do { traceTc "solveEqualities {" (text "Called from" <+> text callsite) + ; (res, wanted) <- captureConstraints thing_inside + ; residual_wanted <- runTcSEqualities (solveWantedsAndDrop wanted) + ; emitFlatConstraints residual_wanted + -- emitFlatConstraints fails outright unless the only unsolved + -- constraints are soluble-looking equalities that can float out + ; traceTc "solveEqualities }" (text "Residual: " <+> ppr residual_wanted) ; return res } emitFlatConstraints :: WantedConstraints -> TcM () @@ -176,7 +216,7 @@ emitFlatConstraints wanted ; emitConstraints wanted -- So they get reported! ; failM } Just (simples, holes) - -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples) + -> do { _ <- TcM.promoteTyVarSet (tyCoVarsOfCts simples) ; traceTc "emitFlatConstraints:" $ vcat [ text "simples:" <+> ppr simples , text "holes: " <+> ppr holes ] @@ -226,10 +266,21 @@ floatKindEqualities wc = float_wc emptyVarSet wc {- Note [Failure in local type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When kind checking a type signature, we like to fail fast if we can't -solve all the kind equality constraints: see Note [Fail fast on kind -errors]. But what about /local/ type signatures, mentioning in-scope -type variables for which there might be given equalities. Here's -an example (T15076b): +solve all the kind equality constraints, for two reasons: + + * A kind-bogus type signature may cause a cascade of knock-on + errors if we let it pass + + * More seriously, we don't have a convenient term-level place to add + deferred bindings for unsolved kind-equality constraints. In + earlier GHCs this led to un-filled-in coercion holes, which caused + GHC to crash with "fvProv falls into a hole" See #11563, #11520, + #11516, #11399 + +But what about /local/ type signatures, mentioning in-scope type +variables for which there might be 'given' equalities? For these we +might not be able to solve all the equalities locally. Here's an +example (T15076b): class (a ~ b) => C a b data SameKind :: k -> k -> Type where { SK :: SameKind a b } @@ -238,7 +289,7 @@ an example (T15076b): C a b => Proxy a -> Proxy b -> () bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y) -Consider the type singature on 'undefined'. It's ill-kinded unless +Consider the type signature on 'undefined'. It's ill-kinded unless a~b. But the superclass of (C a b) means that indeed (a~b). So all should be well. BUT it's hard to see that when kind-checking the signature for undefined. We want to emit a residual (a~b) constraint, to solve @@ -264,13 +315,15 @@ hoping to solve it later, we might end up filling in the holes co1 and co2 with coercions involving 'a' and 'b' -- but by now we've instantiated the type. Chaos! -Moreover, the unsolved constraints might be skolem-escpae things, and +Moreover, the unsolved constraints might be skolem-escape things, and if we proceed with f bound to a nonsensical type, we get a cascade of follow-up errors. For example polykinds/T12593, T15577, and many others. -So here's the plan: +So here's the plan (see tcHsSigType): -* solveLocalEqualitiesX: try to solve the constraints (solveLocalEqualitiesX) +* pushLevelAndSolveEqualitiesX: try to solve the constraints + +* kindGeneraliseSome: do kind generalisation * buildTvImplication: build an implication for the residual, unsolved constraint @@ -292,54 +345,49 @@ So here's the plan: All this is done: -* in solveLocalEqualities, where there is no kind-generalisation - to complicate matters. - -* in GHC.Tc.Gen.HsType.tcHsSigType, where quantification intervenes. - -See also #18062, #11506 --} - -solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a) -solveLocalEqualitiesX callsite thing_inside - = do { traceTc "solveLocalEqualitiesX {" (vcat [ text "Called from" <+> text callsite ]) +* In GHC.Tc.Gen.HsType.tcHsSigType, as above - ; (result, wanted) <- captureConstraints thing_inside +* solveEqualities. Use this when there no kind-generalisation + step to complicate matters; then we don't need to push levels, + and can solve the equalities immediately without needing to + wrap it in an implication constraint. (You'll generally see + a kindGeneraliseNone nearby.) - ; traceTc "solveLocalEqualities: running solver" (ppr wanted) - ; residual_wanted <- runTcSEqualities (solveWanteds wanted) +* In GHC.Tc.TyCl and GHC.Tc.TyCl.Instance; see calls to + pushLevelAndSolveEqualitiesX, followed by quantification, and + then reportUnsolvedEqualities. - ; traceTc "solveLocalEqualitiesX end }" $ - text "residual_wanted =" <+> ppr residual_wanted + NB: we call reportUnsolvedEqualities before zonkTcTypeToType + because the latter does not expect to see any un-filled-in + coercions, which will happen if we have unsolved equalities. + By calling reportUnsolvedEqualities first, which fails after + reporting errors, we avoid that happening. - ; return (residual_wanted, result) } - --- | Type-check a thing that emits only equality constraints, then --- solve those constraints. Fails outright if there is trouble. --- Use this if you're not going to get another crack at solving --- (because, e.g., you're checking a datatype declaration) -solveEqualities :: TcM a -> TcM a -solveEqualities thing_inside - = checkNoErrs $ -- See Note [Fail fast on kind errors] - do { lvl <- TcM.getTcLevel - ; traceTc "solveEqualities {" (text "level =" <+> ppr lvl) +See also #18062, #11506 +-} - ; (result, wanted) <- captureConstraints thing_inside - ; traceTc "solveEqualities: running solver" $ text "wanted = " <+> ppr wanted - ; final_wc <- runTcSEqualities $ simpl_top wanted - -- NB: Use simpl_top here so that we potentially default RuntimeRep - -- vars to LiftedRep. This is needed to avoid #14991. +reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel + -> WantedConstraints -> TcM () +-- Reports all unsolved wanteds provided; fails in the monad if there are any. +-- +-- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to +-- provide skolem info for any errors. +-- +reportUnsolvedEqualities skol_info skol_tvs tclvl wanted + | isEmptyWC wanted + = return () + | otherwise + = checkNoErrs $ -- Fail + do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted + ; reportAllUnsolved (mkImplicWC (unitBag implic)) } - ; traceTc "End solveEqualities }" empty - ; reportAllUnsolved final_wc - ; return result } -- | Simplify top-level constraints, but without reporting any unsolved -- constraints nor unsafe overlapping. -simpl_top :: WantedConstraints -> TcS WantedConstraints +simplifyTopWanteds :: WantedConstraints -> TcS WantedConstraints -- See Note [Top-level Defaulting Plan] -simpl_top wanteds +simplifyTopWanteds wanteds = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds) -- This is where the main work happens ; dflags <- getDynFlags @@ -424,29 +472,8 @@ defaultCallStacks wanteds = return (Just ct) -{- Note [Fail fast on kind errors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -solveEqualities is used to solve kind equalities when kind-checking -user-written types. If solving fails we should fail outright, rather -than just accumulate an error message, for two reasons: - - * A kind-bogus type signature may cause a cascade of knock-on - errors if we let it pass - - * More seriously, we don't have a convenient term-level place to add - deferred bindings for unsolved kind-equality constraints, so we - don't build evidence bindings (by usine reportAllUnsolved). That - means that we'll be left with a type that has coercion holes - in it, something like - <type> |> co-hole - where co-hole is not filled in. Eeek! That un-filled-in - hole actually causes GHC to crash with "fvProv falls into a hole" - See #11563, #11520, #11516, #11399 - -So it's important to use 'checkNoErrs' here! - -Note [When to do type-class defaulting] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [When to do type-class defaulting] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC was false, on the grounds that defaulting can't help solve insoluble constraints. But if we *don't* do defaulting we may report a whole @@ -592,7 +619,7 @@ How is this implemented? It's complicated! So we'll step through it all: `InertCans`. 4) `GHC.Tc.Solver.simplifyTop`: - * Call simpl_top, the top-level function for driving the simplifier for + * Call simplifyTopWanteds, the top-level function for driving the simplifier for constraint resolution. * Once finished, call `getSafeOverlapFailures` to retrieve the @@ -629,7 +656,7 @@ How is this implemented? It's complicated! So we'll step through it all: Note [No defaulting in the ambiguity check] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When simplifying constraints for the ambiguity check, we use -solveWantedsAndDrop, not simpl_top, so that we do no defaulting. +solveWantedsAndDrop, not simplifyTopWanteds, so that we do no defaulting. #11947 was an example: f :: Num a => Int -> Int This is ambiguous of course, but we don't want to default the @@ -970,7 +997,7 @@ mkResidualConstraints rhs_tclvl ev_binds_var ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars - ; _ <- promoteTyVarSet (tyCoVarsOfCts outer_simple) + ; _ <- TcM.promoteTyVarSet (tyCoVarsOfCts outer_simple) ; let inner_wanted = wanteds { wc_simple = inner_simple } ; implics <- if isEmptyWC inner_wanted @@ -2174,29 +2201,6 @@ we'll get more Givens (a unification is like adding a Given) to allow the implication to make progress. -} -promoteTyVar :: TcTyVar -> TcM Bool --- When we float a constraint out of an implication we must restore --- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType --- Return True <=> we did some promotion --- Also returns either the original tyvar (no promotion) or the new one --- See Note [Promoting unification variables] -promoteTyVar tv - = do { tclvl <- TcM.getTcLevel - ; if (isFloatedTouchableMetaTyVar tclvl tv) - then do { cloned_tv <- TcM.cloneMetaTyVar tv - ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl - ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) - ; return True } - else return False } - --- Returns whether or not *any* tyvar is defaulted -promoteTyVarSet :: TcTyVarSet -> TcM Bool -promoteTyVarSet tvs - = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs) - -- Non-determinism is OK because order of promotion doesn't matter - - ; return (or bools) } - promoteTyVarTcS :: TcTyVar -> TcS () -- When we float a constraint out of an implication we must restore -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 2cefd67c7f..9cd0b2a66c 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -30,6 +30,8 @@ import GHC.Prelude import GHC.Hs import GHC.Driver.Types import GHC.Tc.TyCl.Build +import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX + , reportUnsolvedEqualities ) import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Env import GHC.Tc.Validity @@ -38,7 +40,6 @@ import GHC.Tc.TyCl.Utils import GHC.Tc.TyCl.Class import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 ) import GHC.Tc.Deriv (DerivInfo(..)) -import GHC.Tc.Utils.Unify ( checkTvConstraints ) import GHC.Tc.Gen.HsType import GHC.Tc.Instance.Class( AssocInstInfo(..) ) import GHC.Tc.Utils.TcMType @@ -644,13 +645,18 @@ kcTyClGroup kisig_env decls | otherwise = Left d - ; checked_tcs <- checkInitialKinds kinded_decls + ; checked_tcs <- checkNoErrs $ + checkInitialKinds kinded_decls + -- checkNoErrs because we are about to extend + -- the envt with these tycons, and we get + -- knock-on errors if we have tycons with + -- malformed kinds + ; inferred_tcs - <- tcExtendKindEnvWithTyCons checked_tcs $ - pushTcLevelM_ $ -- We are going to kind-generalise, so - -- unification variables in here must - -- be one level in - solveEqualities $ + <- tcExtendKindEnvWithTyCons checked_tcs $ + pushLevelAndSolveEqualities UnkSkol [] $ + -- We are going to kind-generalise, so unification + -- variables in here must be one level in do { -- Step 1: Bind kind variables for all decls mono_tcs <- inferInitialKinds kindless_decls @@ -2300,10 +2306,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs roles = roles_info tycon_name -- for TyCon and Class ; (ctxt, fds, sig_stuff, at_stuff) - <- pushTcLevelM_ $ - solveEqualities $ - checkTvConstraints skol_info (binderVars binders) $ - -- The checkTvConstraints is needed bring into scope the + <- pushLevelAndSolveEqualities skol_info (binderVars binders) $ + -- The (binderVars binders) is needed bring into scope the -- skolems bound by the class decl header (#17841) do { ctxt <- tcHsContext hs_ctxt ; fds <- mapM (addLocM tc_fundep) fundeps @@ -2311,7 +2315,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs ; at_stuff <- tcClassATs class_name clas ats at_defs ; return (ctxt, fds, sig_stuff, at_stuff) } - -- The solveEqualities will report errors for any + + -- The pushLevelAndSolveEqualities will report errors for any -- unsolved equalities, so these zonks should not encounter -- any unfilled coercion variables unless there is such an error -- The zonk also squeeze out the TcTyCons, and converts @@ -2703,13 +2708,13 @@ tcTySynRhs roles_info tc_name hs_ty = bindTyClTyVars tc_name $ \ _ binders res_kind -> do { env <- getLclEnv ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env)) - ; rhs_ty <- pushTcLevelM_ $ - solveEqualities $ + ; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $ tcCheckLHsType hs_ty (TheKind res_kind) ; rhs_ty <- zonkTcTypeToType rhs_ty ; let roles = roles_info tc_name - tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty - ; return tycon } + ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) } + where + skol_info = TyConSkol TypeSynonymFlavour tc_name tcDataDefn :: SDoc -> RolesInfo -> Name -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo]) @@ -2739,7 +2744,9 @@ tcDataDefn err_ctxt roles_info tc_name ; unless (mk_permissive_kind hsc_src cons) $ checkDataKindSig (DataDeclSort new_or_data) final_res_kind - ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt + ; let skol_tvs = binderVars tycon_binders + ; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $ + tcHsContext ctxt ; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta ; kind_signatures <- xoptM LangExt.KindSignatures @@ -2775,6 +2782,9 @@ tcDataDefn err_ctxt roles_info tc_name ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs) ; return (tycon, [deriv_info]) } where + skol_info = TyConSkol flav tc_name + flav = newOrDataToFlavour new_or_data + -- Abstract data types in hsig files can have arbitrary kinds, -- because they may be implemented by type synonyms -- (which themselves can have arbitrary kinds, not just *). See #13955. @@ -2912,40 +2922,38 @@ or (Type -> Type) for the equations above) and the instantiated kind. Note [Generalising in tcTyFamInstEqnGuts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have something like - type instance forall (a::k) b. F t1 t2 = rhs + type instance forall (a::k) b. F (Proxy t1) _ = rhs Then imp_vars = [k], exp_bndrs = [a::k, b] -We want to quantify over - * k, a, and b (all user-specified) - * and any inferred free kind vars from - - the kinds of k, a, b - - the types t1, t2 +We want to quantify over all the free vars of the LHS including + * any invisible kind variables arising from instantiating tycons, + such as Proxy + * wildcards such as '_' above -However, unlike a type signature like - f :: forall (a::k). blah +So, the simple thing is + - Gather candidates from the LHS + - Include any user-specified forall'd variables, so that we get an + error from Validity.checkFamPatBinders if a forall'd variable is + not bound on the LHS + - Quantify over them +Note that, unlike a type signature like + f :: forall (a::k). blah we do /not/ care about the Inferred/Specified designation or order for the final quantified tyvars. Type-family instances are not invoked directly in Haskell source code, so visible type application etc plays no role. -So, the simple thing is - - gather candidates from [k, a, b] and pats - - quantify over them - -Hence the slightly mysterious call: - candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs) +See also Note [Re-quantify type variables in rules] in +GHC.Tc.Gen.Rule, which explains a /very/ similar design when +generalising over the type of a rewrite rule. -Simple, neat, but a little non-obvious! - -See also Note [Re-quantify type variables in rules] in GHC.Tc.Gen.Rule, which explains -a very similar design when generalising over the type of a rewrite rule. -} -------------------------- tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo - -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicicit binder + -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicit binder -> HsTyPats GhcRn -- Patterns -> LHsType GhcRn -- RHS -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs) @@ -2958,11 +2966,10 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty -- This code is closely related to the code -- in GHC.Tc.Gen.HsType.kcCheckDeclHeader_cusk - ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))) - <- pushTcLevelM_ $ - solveEqualities $ - bindImplicitTKBndrs_Q_Skol imp_vars $ - bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ + ; (tclvl, wanted, (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty)))) + <- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $ + bindImplicitTKBndrs_Q_Skol imp_vars $ + bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats -- Ensure that the instance is consistent with its -- parent class (#16008) @@ -2970,21 +2977,20 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; rhs_ty <- tcCheckLHsType hs_rhs_ty (TheKind rhs_kind) ; return (lhs_ty, rhs_ty) } - -- See Note [Generalising in tcTyFamInstEqnGuts] -- This code (and the stuff immediately above) is very similar -- to that in tcDataFamInstHeader. Maybe we should abstract the -- common code; but for the moment I concluded that it's -- clearer to duplicate it. Still, if you fix a bug here, -- check there too! - ; let scoped_tvs = imp_tvs ++ exp_tvs - ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) + + -- See Note [Generalising in tcTyFamInstEqnGuts] + ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs)) ; qtvs <- quantifyTyVars dvs + ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted ; traceTc "tcTyFamInstEqnGuts 2" $ vcat [ ppr fam_tc - , text "scoped_tvs" <+> pprTyVars scoped_tvs , text "lhs_ty" <+> ppr lhs_ty - , text "dvs" <+> ppr dvs , text "qtvs" <+> pprTyVars qtvs ] ; (ze, qtvs) <- zonkTyBndrs qtvs @@ -3167,11 +3173,11 @@ tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied! -> TcM [DataCon] tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data - (ConDeclH98 { con_name = name + (ConDeclH98 { con_name = lname@(L _ name) , con_ex_tvs = explicit_tkv_nms , con_mb_cxt = hs_ctxt , con_args = hs_args }) - = addErrCtxt (dataConCtxtName [name]) $ + = addErrCtxt (dataConCtxtName [lname]) $ do { -- NB: the tyvars from the declaration header are in scope -- Get hold of the existential type variables @@ -3182,62 +3188,63 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ]) - ; (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)) - <- pushTcLevelM_ $ - solveEqualities $ - bindExplicitTKBndrs_Skol explicit_tkv_nms $ + ; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts))) + <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $ + bindExplicitTKBndrs_Skol explicit_tkv_nms $ do { ctxt <- tcHsMbContext hs_ctxt ; let exp_kind = getArgExpKind new_or_data res_kind ; btys <- tcConArgs exp_kind hs_args - ; field_lbls <- lookupConstructorFields (unLoc name) + ; field_lbls <- lookupConstructorFields name ; let (arg_tys, stricts) = unzip btys ; return (ctxt, arg_tys, field_lbls, stricts) } + ; let tmpl_tvs = binderVars tmpl_bndrs + ; let fake_ty = mkSpecForAllTys tmpl_tvs $ + mkInvisForAllTys exp_tvbndrs $ + mkPhiTy ctxt $ + mkVisFunTys arg_tys $ + unitTy + -- That type is a lie, of course. (It shouldn't end in ()!) + -- And we could construct a proper result type from the info + -- at hand. But the result would mention only the tmpl_tvs, + -- and so it just creates more work to do it right. Really, + -- we're only doing this to find the right kind variables to + -- quantify over, and this type is fine for that purpose. -- exp_tvs have explicit, user-written binding sites -- the kvs below are those kind variables entirely unmentioned by the user -- and discovered only by generalization - ; kvs <- kindGeneralizeAll (mkSpecForAllTys tmpl_tvs $ - mkInvisForAllTys exp_tvbndrs $ - mkPhiTy ctxt $ - mkVisFunTys arg_tys $ - unitTy) - -- That type is a lie, of course. (It shouldn't end in ()!) - -- And we could construct a proper result type from the info - -- at hand. But the result would mention only the tmpl_tvs, - -- and so it just creates more work to do it right. Really, - -- we're only doing this to find the right kind variables to - -- quantify over, and this type is fine for that purpose. + ; kvs <- kindGeneralizeAll fake_ty + + ; let skol_tvs = kvs ++ tmpl_tvs ++ binderVars exp_tvbndrs + ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted -- Zonk to Types ; (ze, qkvs) <- zonkTyBndrs kvs ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs - ; let user_qtvs = binderVars user_qtvbndrs ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys ; ctxt <- zonkTcTypesToTypesX ze ctxt - ; fam_envs <- tcGetFamInstEnvs - -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls) ; let univ_tvbs = tyConInvisTVBinders tmpl_bndrs univ_tvs = binderVars univ_tvbs - ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ - user_qtvbndrs - ex_tvs = qkvs ++ user_qtvs + ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs + ex_tvs = binderVars ex_tvbs -- For H98 datatypes, the user-written tyvar binders are precisely -- the universals followed by the existentials. -- See Note [DataCon user type variable binders] in GHC.Core.DataCon. user_tvbs = univ_tvbs ++ ex_tvbs - buildOneDataCon (L _ name) = do - { is_infix <- tcConIsInfixH98 name hs_args - ; rep_nm <- newTyConRepName name - ; buildDataCon fam_envs name is_infix rep_nm + ; traceTc "tcConDecl 2" (ppr name) + ; is_infix <- tcConIsInfixH98 name hs_args + ; rep_nm <- newTyConRepName name + ; fam_envs <- tcGetFamInstEnvs + ; dc <- buildDataCon fam_envs name is_infix rep_nm stricts Nothing field_lbls univ_tvs ex_tvs user_tvbs [{- no eq_preds -}] ctxt arg_tys @@ -3245,10 +3252,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data -- NB: we put data_tc, the type constructor gotten from the -- constructor type signature into the data constructor; -- that way checkValidDataCon can complain if it's wrong. - } - ; traceTc "tcConDecl 2" (ppr name) - ; mapM buildOneDataCon [name] - } + + ; return [dc] } + where + skol_info = DataConSkol name tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- NB: don't use res_kind here, as it's ill-scoped. Instead, @@ -3262,12 +3269,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data do { traceTc "tcConDecl 1 gadt" (ppr names) ; let (L _ name : _) = names - ; (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts))) - <- pushTcLevelM_ $ -- We are going to generalise - solveEqualities $ -- We won't get another crack, and we don't - -- want an error cascade - bindImplicitTKBndrs_Skol implicit_tkv_nms $ - bindExplicitTKBndrs_Skol explicit_tkv_nms $ + ; (tclvl, wanted, (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))) + <- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $ + bindImplicitTKBndrs_Skol implicit_tkv_nms $ + bindExplicitTKBndrs_Skol explicit_tkv_nms $ do { ctxt <- tcHsMbContext cxt ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty -- See Note [GADT return kinds] @@ -3281,17 +3286,19 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data ; return (ctxt, arg_tys, res_ty, field_lbls, stricts) } ; imp_tvs <- zonkAndScopedSort imp_tvs - - ; tkvs <- kindGeneralizeAll (mkSpecForAllTys imp_tvs $ - mkInvisForAllTys exp_tvbndrs $ - mkPhiTy ctxt $ - mkVisFunTys arg_tys $ - res_ty) - - ; let tvbndrs = (mkTyVarBinders InferredSpec tkvs) - ++ (mkTyVarBinders SpecifiedSpec imp_tvs) + ; let con_ty = mkSpecForAllTys imp_tvs $ + mkInvisForAllTys exp_tvbndrs $ + mkPhiTy ctxt $ + mkVisFunTys arg_tys $ + res_ty + ; kvs <- kindGeneralizeAll con_ty + + ; let tvbndrs = mkTyVarBinders InferredSpec kvs + ++ mkTyVarBinders SpecifiedSpec imp_tvs ++ exp_tvbndrs + ; reportUnsolvedEqualities skol_info (binderVars tvbndrs) tclvl wanted + -- Zonk to Types ; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys @@ -3306,11 +3313,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data arg_tys' = substScaledTys arg_subst arg_tys res_ty' = substTy arg_subst res_ty - - ; fam_envs <- tcGetFamInstEnvs - -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls) + ; fam_envs <- tcGetFamInstEnvs ; let buildOneDataCon (L _ name) = do { is_infix <- tcConIsInfixGADT name hs_args @@ -3325,9 +3330,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- constructor type signature into the data constructor; -- that way checkValidDataCon can complain if it's wrong. } - ; traceTc "tcConDecl 2" (ppr names) - ; mapM buildOneDataCon names - } + ; mapM buildOneDataCon names } + where + skol_info = DataConSkol (unLoc (head names)) {- Note [GADT return kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 36d25d0eaf..b0dfa80f90 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -30,6 +30,7 @@ import GHC.Tc.TyCl.Utils ( addTyConsToGblEnv ) import GHC.Tc.TyCl.Class ( tcClassDecl2, tcATDefault, HsSigFun, mkHsSigFun, badMethodErr, findMethodBind, instantiateMethod ) +import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities ) import GHC.Tc.Gen.Sig import GHC.Tc.Utils.Monad import GHC.Tc.Validity @@ -856,11 +857,10 @@ tcDataFamInstHeader tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons new_or_data = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats) - ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind))) - <- pushTcLevelM_ $ - solveEqualities $ - bindImplicitTKBndrs_Q_Skol imp_vars $ - bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ + ; (tclvl, wanted, (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))) + <- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $ + bindImplicitTKBndrs_Q_Skol imp_vars $ + bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ do { stupid_theta <- tcHsContext hs_ctxt ; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats ; (lhs_applied_ty, lhs_applied_kind) @@ -882,7 +882,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity -- is compatible with the explicit signature (or Type, if there -- is none) ; let hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats - ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind + ; _ <- unifyKind (Just (ppr hs_lhs)) lhs_applied_kind res_kind ; traceTc "tcDataFamInstHeader" $ vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ] @@ -891,19 +891,20 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity , lhs_applied_kind , res_kind ) } - -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts] -- This code (and the stuff immediately above) is very similar -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the -- common code; but for the moment I concluded that it's -- clearer to duplicate it. Still, if you fix a bug here, -- check there too! - ; let scoped_tvs = imp_tvs ++ exp_tvs - ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) + + -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts] + ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs)) ; qtvs <- quantifyTyVars dvs + ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted -- Zonk the patterns etc into the Type world ; (ze, qtvs) <- zonkTyBndrs qtvs - ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty + ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta ; master_res_kind <- zonkTcTypeToTypeX ze master_res_kind ; instance_res_kind <- zonkTcTypeToTypeX ze instance_res_kind @@ -925,9 +926,9 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; return (qtvs, pats, master_res_kind, stupid_theta) } where - fam_name = tyConName fam_tc - data_ctxt = DataKindCtxt fam_name - exp_bndrs = mb_bndrs `orElse` [] + fam_name = tyConName fam_tc + data_ctxt = DataKindCtxt fam_name + exp_bndrs = mb_bndrs `orElse` [] -- See Note [Implementation of UnliftedNewtypes] in GHC.Tc.TyCl, wrinkle (2). tc_kind_sig Nothing diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index fd2d1f00ce..71f628aa3a 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -969,17 +969,23 @@ addHoles wc holes dropMisleading :: WantedConstraints -> WantedConstraints -- Drop misleading constraints; really just class constraints -- See Note [Constraints and errors] in GHC.Tc.Utils.Monad +-- for why this function is so strange, treating the 'simples' +-- and the implications differently. Sigh. dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) - = WC { wc_simple = filterBag keep_ct simples + = WC { wc_simple = filterBag insolubleCt simples , wc_impl = mapBag drop_implic implics , wc_holes = filterBag isOutOfScopeHole holes } where drop_implic implic - = implic { ic_wanted = dropMisleading (ic_wanted implic) } - keep_ct ct - = case classifyPredType (ctPred ct) of - ClassPred {} -> False - _ -> True + = implic { ic_wanted = drop_wanted (ic_wanted implic) } + drop_wanted (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) + = WC { wc_simple = filterBag keep_ct simples + , wc_impl = mapBag drop_implic implics + , wc_holes = filterBag isOutOfScopeHole holes } + + keep_ct ct = case classifyPredType (ctPred ct) of + ClassPred {} -> False + _ -> True isSolvedStatus :: ImplicStatus -> Bool isSolvedStatus (IC_Solved {}) = True diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 985cbae01b..9d46f8ba16 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -461,7 +461,7 @@ use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level evidence bindings are allowed. Notebly (): - Places in types where we are solving kind constraints (all of which - are equalities); see solveEqualities, solveLocalEqualities + are equalities); see solveEqualities - When unifying forall-types -} @@ -763,7 +763,7 @@ important) are solved in three steps: EvCsEmpty - (see GHC.Tc.Solver.simpl_top and GHC.Tc.Solver.defaultCallStacks) + (see GHC.Tc.Solver.simplifyTopWanteds and GHC.Tc.Solver.defaultCallStacks) This provides a lightweight mechanism for building up call-stacks explicitly, but is notably limited by the fact that the stack will diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 96bff3d261..f50cab2bb7 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -1816,10 +1816,33 @@ Here 'p' is out of scope, so we get an insoluble Hole constraint. But the visible type application fails in the monad (throws an exception). We must not discard the out-of-scope error. -So we /retain the insoluble constraints/ if there is an exception. -Hence: - - insolublesOnly in tryCaptureConstraints - - emitConstraints in the Left case of captureConstraints +It's distressingly delicate though: + +* If we discard too /many/ constraints we may fail to report the error + that led us to interrupte the constraint gathering process. + + One particular example "variable out of scope" Hole constraints. For + example (#12529): + f = p @ Int + Here 'p' is out of scope, so we get an insoluble Hole constraint. But + the visible type application fails in the monad (throws an exception). + We must not discard the out-of-scope error. + + Also GHC.Tc.Solver.emitFlatConstraints may fail having emitted some + constraints with skolem-escape problems. + +* If we discard too /few/ constraints, we may get the misleading + class constraints mentioned above. But we may /also/ end up taking + constraints built at some inner level, and emitting them at some + outer level, and then breaking the TcLevel invariants + See Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType + +So dropMisleading has a horridly ad-hoc structure. It keeps only +/insoluble/ flat constraints (which are unlikely to very visibly trip +up on the TcLevel invariant, but all /implication/ constraints (except +the class constraints inside them). The implication constraints are +OK because they set the ambient level before attempting to solve any +inner constraints. Ugh! I hate this. But it seems to work. However note that freshly-generated constraints like (Int ~ Bool), or ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 62e39879d7..88c354fd80 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -4,7 +4,7 @@ -} -{-# LANGUAGE CPP, TupleSections, MultiWayIf, PatternSynonyms #-} +{-# LANGUAGE CPP, TupleSections, MultiWayIf, PatternSynonyms, BangPatterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} @@ -21,9 +21,9 @@ module GHC.Tc.Utils.TcMType ( newNamedFlexiTyVar, newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] - newOpenFlexiTyVarTy, newOpenTypeKind, + newOpenFlexiTyVar, newOpenFlexiTyVarTy, newOpenTypeKind, newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, - cloneMetaTyVar, + newAnonMetaTyVar, cloneMetaTyVar, newFmvTyVar, newFskTyVar, newMultiplicityVar, @@ -70,19 +70,23 @@ module GHC.Tc.Utils.TcMType ( zonkTcTyVarToTyVar, zonkInvisTVBinder, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV, zonkTyCoVarsAndFVList, - candidateQTyVarsOfType, candidateQTyVarsOfKind, - candidateQTyVarsOfTypes, candidateQTyVarsOfKinds, - CandidatesQTvs(..), delCandidates, candidateKindVars, partitionCandidates, - zonkAndSkolemise, skolemiseQuantifiedTyVar, - defaultTyVar, quantifyTyVars, isQuantifiableTv, + zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, zonkTyCoVarKindBinder, - zonkEvVar, zonkWC, zonkImplication, zonkSimples, zonkId, zonkCoVar, zonkCt, zonkSkolemInfo, - skolemiseUnboundMetaTyVar, + --------------------------------- + -- Promotion, defaulting, skolemisation + defaultTyVar, promoteTyVar, promoteTyVarSet, + quantifyTyVars, isQuantifiableTv, + skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar, + + candidateQTyVarsOfType, candidateQTyVarsOfKind, + candidateQTyVarsOfTypes, candidateQTyVarsOfKinds, + CandidatesQTvs(..), delCandidates, + candidateKindVars, partitionCandidates, ------------------------------ -- Levity polymorphism @@ -464,7 +468,7 @@ readExpType exp_ty -- | Returns the expected type when in checking mode. checkingExpType_maybe :: ExpType -> Maybe TcType checkingExpType_maybe (Check ty) = Just ty -checkingExpType_maybe _ = Nothing +checkingExpType_maybe (Infer {}) = Nothing -- | Returns the expected type when in checking mode. Panics if in inference -- mode. @@ -759,7 +763,6 @@ the thinking. {- Note [TyVarTv] ~~~~~~~~~~~~~~~~~ - A TyVarTv can unify with type *variables* only, including other TyVarTvs and skolems. Sometimes, they can unify with type variables that the user would rather keep distinct; see #11203 for an example. So, any client of this @@ -774,7 +777,7 @@ types (GHC Proposal 29). The remaining uses of newTyVarTyVars are * In kind signatures, see GHC.Tc.TyCl Note [Inferring kinds for type declarations] - and Note [Kind checking for GADTs] + and Note [Kind checking for GADTs] * In partial type signatures, see Note [Quantified variables in partial type signatures] -} @@ -1080,8 +1083,13 @@ newOpenTypeKind -- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh newOpenFlexiTyVarTy :: TcM TcType newOpenFlexiTyVarTy + = do { tv <- newOpenFlexiTyVar + ; return (mkTyVarTy tv) } + +newOpenFlexiTyVar :: TcM TcTyVar +newOpenFlexiTyVar = do { kind <- newOpenTypeKind - ; newFlexiTyVarTy kind } + ; newFlexiTyVar kind } newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Instantiate with META type variables @@ -1619,11 +1627,11 @@ alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for generalisation, and so we generalise it. alpha[1] does not, and so we leave it alone. -Note that not *every* variable with a higher level will get generalised, -either due to the monomorphism restriction or other quirks. See, for -example, the code in GHC.Tc.Solver.decideMonoTyVars and in -GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude certain otherwise-eligible -variables from being generalised. +Note that not *every* variable with a higher level will get +generalised, either due to the monomorphism restriction or other +quirks. See, for example, the code in GHC.Tc.Solver.decideMonoTyVars +and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude +certain otherwise-eligible variables from being generalised. Using level numbers for quantification is implemented in the candidateQTyVars... functions, by adding only those variables with a level strictly higher than @@ -1643,10 +1651,9 @@ For more information about deterministic sets see Note [Deterministic UniqFM] in GHC.Types.Unique.DFM. -} -quantifyTyVars - :: CandidatesQTvs -- See Note [Dependent type variables] - -- Already zonked - -> TcM [TcTyVar] +quantifyTyVars :: CandidatesQTvs -- See Note [Dependent type variables] + -- Already zonked + -> TcM [TcTyVar] -- See Note [quantifyTyVars] -- Can be given a mixture of TcTyVars and TyVars, in the case of -- associated type declarations. Also accepts covars, but *never* returns any. @@ -1654,28 +1661,28 @@ quantifyTyVars -- invariants on CandidateQTvs, we do not have to filter out variables -- free in the environment here. Just quantify unconditionally, subject -- to the restrictions in Note [quantifyTyVars]. -quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) +quantifyTyVars dvs@(DV{ dv_kvs = dep_kv_set, dv_tvs = nondep_tkv_set }) -- short-circuit common case - | isEmptyDVarSet dep_tkvs - , isEmptyDVarSet nondep_tkvs + | isEmptyDVarSet dep_kv_set + , isEmptyDVarSet nondep_tkv_set = do { traceTc "quantifyTyVars has nothing to quantify" empty ; return [] } | otherwise - = do { traceTc "quantifyTyVars 1" (ppr dvs) + = do { traceTc "quantifyTyVars {" (ppr dvs) - ; let dep_kvs = scopedSort $ dVarSetElems dep_tkvs - -- scopedSort: put the kind variables into - -- well-scoped order. - -- E.g. [k, (a::k)] not the other way round + ; let dep_kvs = scopedSort $ dVarSetElems dep_kv_set + -- scopedSort: put the kind variables into + -- well-scoped order. + -- E.g. [k, (a::k)] not the other way round - nondep_tvs = dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs) + nondep_tvs = dVarSetElems (nondep_tkv_set `minusDVarSet` dep_kv_set) -- See Note [Dependent type variables] -- The `minus` dep_tkvs removes any kind-level vars -- e.g. T k (a::k) Since k appear in a kind it'll -- be in dv_kvs, and is dependent. So remove it from -- dv_tvs which will also contain k - -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV + -- NB kinds of tvs are already zonked -- In the non-PolyKinds case, default the kind variables -- to *, and zonk the tyvars as usual. Notice that this @@ -1689,7 +1696,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) -- mentioned in the kinds of the nondep_tvs' -- now refer to the dep_kvs' - ; traceTc "quantifyTyVars 2" + ; traceTc "quantifyTyVars }" (vcat [ text "nondep:" <+> pprTyVars nondep_tvs , text "dep:" <+> pprTyVars dep_kvs , text "dep_kvs'" <+> pprTyVars dep_kvs' @@ -2018,14 +2025,45 @@ Consider this: All very silly. I think its harmless to ignore the problem. We'll end up with a \/\a in the final result but all the occurrences of a will be zonked to () +-} -************************************************************************ +{- ********************************************************************* * * - Zonking types + Promotion * * -************************************************************************ +********************************************************************* -} --} +promoteTyVar :: TcTyVar -> TcM Bool +-- When we float a constraint out of an implication we must restore +-- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType +-- Return True <=> we did some promotion +-- Also returns either the original tyvar (no promotion) or the new one +-- See Note [Promoting unification variables] +promoteTyVar tv + = do { tclvl <- getTcLevel + ; if (isFloatedTouchableMetaTyVar tclvl tv) + then do { cloned_tv <- cloneMetaTyVar tv + ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl + ; writeMetaTyVar tv (mkTyVarTy rhs_tv) + ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv) + ; return True } + else do { traceTc "promoteTyVar: no" (ppr tv) + ; return False } } + +-- Returns whether or not *any* tyvar is defaulted +promoteTyVarSet :: TcTyVarSet -> TcM Bool +promoteTyVarSet tvs + = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs) + -- Non-determinism is OK because order of promotion doesn't matter + + ; return (or bools) } + + +{- ********************************************************************* +* * + Zonking types +* * +********************************************************************* -} zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet -- Zonk a type and take its free variables diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs index edee58e53d..a11fc335d3 100644 --- a/compiler/GHC/Types/Var.hs +++ b/compiler/GHC/Types/Var.hs @@ -76,7 +76,8 @@ module GHC.Types.Var ( binderVar, binderVars, binderArgFlag, binderType, mkTyCoVarBinder, mkTyCoVarBinders, mkTyVarBinder, mkTyVarBinders, - isTyVarBinder, tyVarSpecToBinder, tyVarSpecToBinders, + isTyVarBinder, + tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders, mapVarBndr, mapVarBndrs, lookupVarBndr, -- ** Constructing TyVar's @@ -596,20 +597,40 @@ Note [Types for coercions, predicates, and evidence] * * ********************************************************************* -} --- Variable Binder --- --- VarBndr is polymorphic in both var and visibility fields. --- Currently there are nine different uses of 'VarBndr': --- * Var.TyVarBinder = VarBndr TyVar ArgFlag --- * Var.TyCoVarBinder = VarBndr TyCoVar ArgFlag --- * Var.InvisTVBinder = VarBndr TyVar Specificity --- * Var.ReqTVBinder = VarBndr TyVar () --- * TyCon.TyConBinder = VarBndr TyVar TyConBndrVis --- * TyCon.TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis --- * IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ArgFlag --- * IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis --- * IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity +{- Note [The VarBndr type and its uses] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +VarBndr is polymorphic in both var and visibility fields. +Currently there are nine different uses of 'VarBndr': + +* Var.TyCoVarBinder = VarBndr TyCoVar ArgFlag + Binder of a forall-type; see ForAllTy in GHC.Core.TyCo.Rep + +* Var.TyVarBinder = VarBndr TyVar ArgFlag + Subset of TyCoVarBinder when we are sure the binder is a TyVar + +* Var.InvisTVBinder = VarBndr TyVar Specificity + Specialised form of TyVarBinder, when ArgFlag = Invisible s + See GHC.Core.Type.splitForAllTysInvis + +* Var.ReqTVBinder = VarBndr TyVar () + Specialised form of TyVarBinder, when ArgFlag = Required + See GHC.Core.Type.splitForAllTysReq + This one is barely used + +* TyCon.TyConBinder = VarBndr TyVar TyConBndrVis + Binders of a TyCon; see TyCon in GHC.Core.TyCon + +* TyCon.TyConTyCoBinder = VarBndr TyCoVar TyConBndrVis + Binders of a PromotedDataCon + See Note [Promoted GADT data construtors] in GHC.Core.TyCon + +* IfaceType.IfaceForAllBndr = VarBndr IfaceBndr ArgFlag +* IfaceType.IfaceForAllSpecBndr = VarBndr IfaceBndr Specificity +* IfaceType.IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis +-} + data VarBndr var argf = Bndr var argf + -- See Note [The VarBndr type and its uses] deriving( Data ) -- | Variable Binder @@ -627,9 +648,15 @@ type ReqTVBinder = VarBndr TyVar () tyVarSpecToBinders :: [VarBndr a Specificity] -> [VarBndr a ArgFlag] tyVarSpecToBinders = map tyVarSpecToBinder -tyVarSpecToBinder :: (VarBndr a Specificity) -> (VarBndr a ArgFlag) +tyVarSpecToBinder :: VarBndr a Specificity -> VarBndr a ArgFlag tyVarSpecToBinder (Bndr tv vis) = Bndr tv (Invisible vis) +tyVarReqToBinders :: [VarBndr a ()] -> [VarBndr a ArgFlag] +tyVarReqToBinders = map tyVarReqToBinder + +tyVarReqToBinder :: VarBndr a () -> VarBndr a ArgFlag +tyVarReqToBinder (Bndr tv _) = Bndr tv Required + binderVar :: VarBndr tv argf -> tv binderVar (Bndr v _) = v @@ -643,12 +670,12 @@ binderType :: VarBndr TyCoVar argf -> Type binderType (Bndr tv _) = varType tv -- | Make a named binder -mkTyCoVarBinder :: vis -> TyCoVar -> (VarBndr TyCoVar vis) +mkTyCoVarBinder :: vis -> TyCoVar -> VarBndr TyCoVar vis mkTyCoVarBinder vis var = Bndr var vis -- | Make a named binder -- 'var' should be a type variable -mkTyVarBinder :: vis -> TyVar -> (VarBndr TyVar vis) +mkTyVarBinder :: vis -> TyVar -> VarBndr TyVar vis mkTyVarBinder vis var = ASSERT( isTyVar var ) Bndr var vis diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst index 92dc51e00f..93b72979b8 100644 --- a/docs/users_guide/ghci.rst +++ b/docs/users_guide/ghci.rst @@ -2960,6 +2960,11 @@ commonly used commands. *X> :type length length :: Foldable t => t a -> Int +.. ghci-cmd:: :type +v; ⟨expression⟩ + + Infers and prints the type of ⟨expression⟩, binding inferred type variables + with :ref:`*specified* visibility <inferred-vs-specified>`. + .. ghci-cmd:: :type +d; ⟨expression⟩ Infers and prints the type of ⟨expression⟩, instantiating *all* the forall diff --git a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr index 41f5d7cd4c..90c3cd671a 100644 --- a/testsuite/tests/dependent/should_fail/RAE_T32a.stderr +++ b/testsuite/tests/dependent/should_fail/RAE_T32a.stderr @@ -1,7 +1,6 @@ RAE_T32a.hs:29:1: error: - • Expected kind ‘k0 -> *’, - but ‘Sing Sigma (Sigma p r)’ has kind ‘*’ + • Expected kind ‘k -> *’, but ‘Sing Sigma (Sigma p r)’ has kind ‘*’ • In the data instance declaration for ‘Sing’ RAE_T32a.hs:29:20: error: diff --git a/testsuite/tests/dependent/should_fail/T11407.stderr b/testsuite/tests/dependent/should_fail/T11407.stderr index df87248f2e..b24559ea9a 100644 --- a/testsuite/tests/dependent/should_fail/T11407.stderr +++ b/testsuite/tests/dependent/should_fail/T11407.stderr @@ -1,8 +1,8 @@ T11407.hs:10:40: error: - • Expected kind ‘x a’, but ‘a’ has kind ‘k0’ + • Expected kind ‘x a’, but ‘a’ has kind ‘k’ + ‘k’ is a rigid type variable bound by + a family instance declaration + at T11407.hs:10:1-72 • In the second argument of ‘UhOh’, namely ‘(a :: x a)’ In the data instance declaration for ‘UhOh’ - • Type variable kinds: - x :: k0 -> * - a :: k0 diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr index 5253ed0dbd..6cdcf96369 100644 --- a/testsuite/tests/dependent/should_fail/T13780a.stderr +++ b/testsuite/tests/dependent/should_fail/T13780a.stderr @@ -2,6 +2,9 @@ T13780a.hs:9:40: error: • Couldn't match kind ‘a’ with ‘Bool’ Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’ + ‘a’ is a rigid type variable bound by + a family instance declaration + at T13780a.hs:9:20-31 • In the second argument of ‘(~)’, namely ‘MkFoo’ In the definition of data constructor ‘SMkFoo’ In the data instance declaration for ‘Sing’ diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index b103b16187..caa062e392 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,9 +1,9 @@ T14066e.hs:13:65: error: - • Expected a type, but ‘c'’ has kind ‘k1’ - ‘k1’ is a rigid type variable bound by + • Expected a type, but ‘c'’ has kind ‘k’ + ‘k’ is a rigid type variable bound by the type signature for: - j :: forall {k1} {k2} (c :: k1) (b :: k2). + j :: forall {k} {k1} (c :: k) (b :: k1). Proxy a -> Proxy b -> Proxy c -> Proxy b at T14066e.hs:12:5-61 • In the kind ‘c'’ diff --git a/testsuite/tests/dependent/should_fail/T15859.hs b/testsuite/tests/dependent/should_fail/T15859.hs index e7adc5fc98..1f9fafaee4 100644 --- a/testsuite/tests/dependent/should_fail/T15859.hs +++ b/testsuite/tests/dependent/should_fail/T15859.hs @@ -1,14 +1,10 @@ {-# Language PolyKinds #-} {-# Language TypeApplications #-} -{-# Language ImpredicativeTypes #-} {-# Language LiberalTypeSynonyms #-} module T15859 where import Data.Kind -data A k :: k -> Type +a = (undefined :: forall k -> k -> Type) @Int -type KindOf (a :: k) = k - -a = (undefined :: KindOf A) @Int diff --git a/testsuite/tests/dependent/should_fail/T15859.stderr b/testsuite/tests/dependent/should_fail/T15859.stderr index ec0e091055..be25e98708 100644 --- a/testsuite/tests/dependent/should_fail/T15859.stderr +++ b/testsuite/tests/dependent/should_fail/T15859.stderr @@ -1,8 +1,8 @@ -T15859.hs:14:19: error: +T15859.hs:9:19: error: • Illegal visible, dependent quantification in the type of a term: - forall k -> k -> * + forall k -> k -> * (GHC does not yet support this) - • In the expansion of type synonym ‘KindOf’ - In an expression type signature: KindOf A - In the expression: undefined :: KindOf A + • In an expression type signature: forall k -> k -> Type + In the expression: undefined :: forall k -> k -> Type + In the expression: (undefined :: forall k -> k -> Type) @Int diff --git a/testsuite/tests/dependent/should_fail/T15859a.hs b/testsuite/tests/dependent/should_fail/T15859a.hs new file mode 100644 index 0000000000..e76b298e85 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15859a.hs @@ -0,0 +1,19 @@ +{-# Language PolyKinds #-} +{-# Language TypeApplications #-} +{-# Language LiberalTypeSynonyms #-} + +module T15859 where + +import Data.Kind + +-- A :: forall (k :: Type) -> k -> Type +data A k :: k -> Type + +-- KindOf :: forall (k::Type). k -> Type +type KindOf (a :: k) = k + +-- This variant requires impredicative instantiation of KindOf +-- KindOf @(forall k -> k -> Type) A +-- which GHC does not (yet) support at the kind level, even +-- with Quick Look +a = (undefined :: KindOf A) @Int diff --git a/testsuite/tests/dependent/should_fail/T15859a.stderr b/testsuite/tests/dependent/should_fail/T15859a.stderr new file mode 100644 index 0000000000..1fdac765f2 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15859a.stderr @@ -0,0 +1,6 @@ + +T15859a.hs:19:5: error: + • Cannot apply expression of type ‘KindOf A’ + to a visible type argument ‘Int’ + • In the expression: (undefined :: KindOf A) @Int + In an equation for ‘a’: a = (undefined :: KindOf A) @Int diff --git a/testsuite/tests/dependent/should_fail/T16344a.stderr b/testsuite/tests/dependent/should_fail/T16344a.stderr index d838d14e57..8325bf4169 100644 --- a/testsuite/tests/dependent/should_fail/T16344a.stderr +++ b/testsuite/tests/dependent/should_fail/T16344a.stderr @@ -1,6 +1,9 @@ T16344a.hs:11:36: error: • Expected a type, but ‘a’ has kind ‘ka’ + ‘ka’ is a rigid type variable bound by + the data constructor ‘MkT2’ + at T16344a.hs:11:9-10 • In the second argument of ‘T2’, namely ‘a’ In the type ‘(T2 Type a)’ In the definition of data constructor ‘MkT2’ diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index af95d1b333..e8705af1e5 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -39,6 +39,7 @@ test('T15743c', normal, compile_fail, ['']) test('T15743d', normal, compile_fail, ['']) test('T15825', normal, compile_fail, ['']) test('T15859', normal, compile_fail, ['']) +test('T15859a', normal, compile_fail, ['']) test('T15264', normal, compile_fail, ['']) test('T16326_Fail1', normal, compile_fail, ['']) test('T16326_Fail2', normal, compile_fail, ['']) diff --git a/testsuite/tests/gadt/T12468.stderr b/testsuite/tests/gadt/T12468.stderr index 402a93d82d..5abe870814 100644 --- a/testsuite/tests/gadt/T12468.stderr +++ b/testsuite/tests/gadt/T12468.stderr @@ -1,8 +1,7 @@ T12468.hs:9:7: error: • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f I = _ + • In an equation for ‘f’: f I = _ • Relevant bindings include f :: T a -> a (bound at T12468.hs:9:1) Constraints include a ~ Int (from T12468.hs:9:3) Valid hole fits include diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr index 19aa501a4c..d771c63828 100644 --- a/testsuite/tests/gadt/gadt-escape1.stderr +++ b/testsuite/tests/gadt/gadt-escape1.stderr @@ -1,13 +1,12 @@ gadt-escape1.hs:19:58: error: - • Couldn't match type ‘p’ with ‘ExpGADT Int’ + • Could not deduce: p ~ ExpGADT Int + from the context: t ~ Int + bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int, + in a case alternative + at gadt-escape1.hs:19:43-50 Expected: p Actual: ExpGADT t - ‘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 ‘p’ is a rigid type variable bound by the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58 diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr index cea221944b..49eb2bc96f 100644 --- a/testsuite/tests/gadt/gadt13.stderr +++ b/testsuite/tests/gadt/gadt13.stderr @@ -1,12 +1,10 @@ gadt13.hs:15:13: error: - • Couldn't match expected type ‘p’ - with actual type ‘String -> [Char]’ - ‘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 + • Could not deduce: p ~ (String -> [Char]) + from the context: a ~ Int + bound by a pattern with constructor: I :: Int -> Term Int, + in an equation for ‘shw’ + at gadt13.hs:15:6-8 ‘p’ is a rigid type variable bound by the inferred type of shw :: Term a -> p at gadt13.hs:15:1-30 diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr index bb179975fb..679ec3b00e 100644 --- a/testsuite/tests/gadt/gadt7.stderr +++ b/testsuite/tests/gadt/gadt7.stderr @@ -1,15 +1,16 @@ gadt7.hs:16:38: error: - • Couldn't match expected type ‘p1’ with actual type ‘p’ - ‘p’ 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 + • Could not deduce: p ~ p1 + from the context: a ~ Int + bound by a pattern with constructor: K :: T Int, + in a case alternative + at gadt7.hs:16:33 ‘p’ is a rigid type variable bound by - the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44 + the inferred type of i1b :: T a -> p -> p1 + at gadt7.hs:16:1-44 ‘p1’ is a rigid type variable bound by - the inferred type of i1b :: T a -> p -> p1 at gadt7.hs:16:1-44 + the inferred type of i1b :: T a -> p -> p1 + at gadt7.hs:16:1-44 Possible fix: add a type signature for ‘i1b’ • In the expression: y1 In a case alternative: K -> y1 diff --git a/testsuite/tests/ghci.debugger/scripts/T14628.stderr b/testsuite/tests/ghci.debugger/scripts/T14628.stderr index 8990cdb97b..fbce771874 100644 --- a/testsuite/tests/ghci.debugger/scripts/T14628.stderr +++ b/testsuite/tests/ghci.debugger/scripts/T14628.stderr @@ -3,10 +3,6 @@ • Couldn't match type ‘m’ with ‘(,) a0’ Expected: (a0, ((), Int)) Actual: m ((), Int) - ‘m’ is untouchable - inside the constraints: () - bound by the inferred type of it :: ((), Int) - at <interactive>:4:1-25 ‘m’ is an interactive-debugger skolem • In the second argument of ‘($)’, namely ‘runStateT _result 0’ In the expression: snd $ runStateT _result 0 diff --git a/testsuite/tests/ghci/scripts/T10249.stderr b/testsuite/tests/ghci/scripts/T10249.stderr index c8215663a5..b15f205ebb 100644 --- a/testsuite/tests/ghci/scripts/T10249.stderr +++ b/testsuite/tests/ghci/scripts/T10249.stderr @@ -4,6 +4,5 @@ Where: ‘t’ is a rigid type variable bound by the inferred type of it :: t at <interactive>:1:1 - • In the expression: _ - In an equation for ‘it’: it = _ + • In an equation for ‘it’: it = _ • Relevant bindings include it :: t (bound at <interactive>:1:1) diff --git a/testsuite/tests/ghci/scripts/T8353.stderr b/testsuite/tests/ghci/scripts/T8353.stderr index a84b0b7e83..bf737eb3fb 100644 --- a/testsuite/tests/ghci/scripts/T8353.stderr +++ b/testsuite/tests/ghci/scripts/T8353.stderr @@ -6,8 +6,7 @@ Defer03.hs:4:5: warning: [-Wdeferred-type-errors (in -Wdefault)] Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: Int (bound at Defer03.hs:7:1) Valid hole fits include f :: Int (bound at Defer03.hs:7:1) @@ -28,8 +27,7 @@ Defer03.hs:4:5: error: Defer03.hs:7:5: error: • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: Int (bound at Defer03.hs:7:1) Valid hole fits include f :: Int (bound at Defer03.hs:7:1) @@ -50,8 +48,7 @@ Defer03.hs:4:5: warning: [-Wdeferred-type-errors (in -Wdefault)] Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: Int (bound at Defer03.hs:7:1) Valid hole fits include f :: Int (bound at Defer03.hs:7:1) @@ -72,8 +69,7 @@ Defer03.hs:4:5: error: Defer03.hs:7:5: error: • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: Int (bound at Defer03.hs:7:1) Valid hole fits include f :: Int (bound at Defer03.hs:7:1) @@ -94,8 +90,7 @@ Defer03.hs:4:5: warning: [-Wdeferred-type-errors (in -Wdefault)] Defer03.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: Int (bound at Defer03.hs:7:1) Valid hole fits include f :: Int (bound at Defer03.hs:7:1) diff --git a/testsuite/tests/ghci/should_run/T15007.stderr b/testsuite/tests/ghci/should_run/T15007.stderr index da1dc5d1ed..e6a98b0bcb 100644 --- a/testsuite/tests/ghci/should_run/T15007.stderr +++ b/testsuite/tests/ghci/should_run/T15007.stderr @@ -4,6 +4,5 @@ Where: ‘t’ is a rigid type variable bound by the inferred type of it :: t at <interactive>:3:1 - • In the expression: _ - In an equation for ‘it’: it = _ + • In an equation for ‘it’: it = _ • Relevant bindings include it :: t (bound at <interactive>:3:1) diff --git a/testsuite/tests/impredicative/boxy.hs b/testsuite/tests/impredicative/boxy.hs index 475b5c1c5e..ec42d38fa5 100644 --- a/testsuite/tests/impredicative/boxy.hs +++ b/testsuite/tests/impredicative/boxy.hs @@ -29,6 +29,9 @@ t2 = sing id t3 :: forall a. a -> a t3 = head ids +t4 :: forall b. (forall a. a->a, b->b) +t4 = (id, id) + {--------------- Examples from QMLF paper -------------------} qF :: (forall a. a -> a -> a) -> (Bool, Char) @@ -46,8 +49,11 @@ choose x y = x impred1 :: (Bool, Char) impred1 = ($) qF choose --- impredicative instantiation for $ -impred2 :: (forall a. a -> a -> a) -> (Bool, Char) -impred2 = id qF +impred2 :: (Bool, Char) +impred2 = qF $ choose --- impredicative instantiation for $ + +impred3 :: (forall a. a -> a -> a) -> (Bool, Char) +impred3 = id qF {------ Examples for Garrique/Remy paper -------} diff --git a/testsuite/tests/indexed-types/should_fail/T14887.stderr b/testsuite/tests/indexed-types/should_fail/T14887.stderr index ff7e14b464..6b5c57977e 100644 --- a/testsuite/tests/indexed-types/should_fail/T14887.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14887.stderr @@ -5,12 +5,3 @@ T14887.hs:13:1: error: NB: Specified variables (namely: (a :: k)) always come first Perhaps try this order instead: k (a :: k) (e :: a :~: a) • In the type family declaration for ‘Foo2’ - -T14887.hs:14:11: error: - • Couldn't match kind ‘k1’ with ‘k’ - When matching kinds - a0 :: k - a :: k1 - Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’ - • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ - In the type family declaration for ‘Foo2’ diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr index 2cba04fd97..ce087941ea 100644 --- a/testsuite/tests/indexed-types/should_fail/T15870.stderr +++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr @@ -2,6 +2,9 @@ T15870.hs:32:34: error: • Couldn't match kind ‘k’ with ‘*’ Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’ + ‘k’ is a rigid type variable bound by + a family instance declaration + at T15870.hs:(27,1)-(32,35) • In the second argument of ‘Get’, namely ‘g2’ In the type ‘Get a g2’ In the type instance declaration for ‘Get’ diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr index 5dcce91edb..c7f230654e 100644 --- a/testsuite/tests/indexed-types/should_fail/T5439.stderr +++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr @@ -3,7 +3,8 @@ 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 + • Probable cause: ‘($)’ is applied to too few arguments + In the second argument of ‘($)’, namely ‘inj $ Failure (e :: SomeException)’ In a stmt of a 'do' block: c <- complete ev $ inj $ Failure (e :: SomeException) diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr index 1a20e096f1..f8ebc7d923 100644 --- a/testsuite/tests/indexed-types/should_fail/T7354.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr @@ -3,6 +3,9 @@ T7354.hs:28:11: error: • Couldn't match type ‘p’ with ‘Base t (Prim [p] p)’ Expected: Prim [p] p -> Base t (Prim [p] p) Actual: Prim [p] p -> p + ‘p’ is a rigid type variable bound by + the inferred type of foo :: Prim [p] p -> t + at T7354.hs:28:1-13 • In the first argument of ‘ana’, namely ‘alg’ In the expression: ana alg In an equation for ‘foo’: foo = ana alg diff --git a/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr index 4abdd1c18c..61d7aa2f45 100644 --- a/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr +++ b/testsuite/tests/linear/should_fail/LinearConfusedDollar.stderr @@ -1,6 +1,8 @@ LinearConfusedDollar.hs:12:7: error: - • Couldn't match type ‘'Many’ with ‘'One’ - arising from an application - • In the expression: f $ x + • Couldn't match type ‘'One’ with ‘'Many’ + Expected: a -> a + Actual: a #-> a + • In the first argument of ‘($)’, namely ‘f’ + In the expression: f $ x In an equation for ‘g’: g x = f $ x diff --git a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr index 836b27f9e5..73a1b9b4d8 100644 --- a/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr +++ b/testsuite/tests/overloadedrecflds/should_fail/overloadedrecfldsfail07.stderr @@ -1,6 +1,7 @@ overloadedrecfldsfail07.hs:7:7: error: • Couldn't match expected type ‘T’ with actual type ‘T -> Int’ - • In the first argument of ‘x’, namely ‘x’ + • Probable cause: ‘x’ is applied to too few arguments + In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘y’: y = x x diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr index dbcc63f419..f43a759083 100644 --- a/testsuite/tests/parser/should_fail/readFail003.stderr +++ b/testsuite/tests/parser/should_fail/readFail003.stderr @@ -2,6 +2,12 @@ readFail003.hs:4:27: error: • Couldn't match expected type ‘(a, [a1], [a2])’ with actual type ‘a’ + ‘a’ is a rigid type variable bound by + the inferred types of + a :: a + b :: [a1] + c :: [a2] + at readFail003.hs:(4,1)-(8,26) • In the expression: a In a pattern binding: ~(a, b, c) diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr index e59a28a99d..a3cdc763fc 100644 --- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr @@ -36,8 +36,8 @@ T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)] ...plus two instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the second argument of ‘(.)’, namely ‘fmap (const ())’ - In the expression: H . fmap (const ()) In the expression: (H . fmap (const ())) (fmap f b) + In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b) T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)] • Couldn't match type ‘f0’ with ‘B t’ diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr index ced11e50a2..0e7967a276 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr @@ -1,7 +1,7 @@ T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)] • Could not deduce (SingI a) arising from a use of ‘sing’ - from the context: (Action act, Monoid a, Good m1) + from the context: (Action act, Monoid a, Good m) bound by the instance declaration at T14584.hs:54:10-89 • In the second argument of ‘fromSing’, namely ‘(sing @m @a :: Sing _)’ @@ -11,10 +11,10 @@ T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)] act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Could not deduce: m1 ~ * - from the context: (Action act, Monoid a, Good m1) + • Could not deduce: m ~ * + from the context: (Action act, Monoid a, Good m) bound by the instance declaration at T14584.hs:54:10-89 - ‘m1’ is a rigid type variable bound by + ‘m’ is a rigid type variable bound by the instance declaration at T14584.hs:54:10-89 • In the type ‘a’ diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr index 9d7ab35dd5..c3e957b9dd 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr @@ -1,14 +1,15 @@ T14584a.hs:12:5: warning: [-Wdeferred-type-errors (in -Wdefault)] • Couldn't match expected type ‘()’ with actual type ‘m -> m’ - • In the expression: id @m :: _ + • Probable cause: ‘id @m :: _’ is applied to too few arguments + In the expression: id @m :: _ In an equation for ‘f’: f = id @m :: _ T14584a.hs:12:9: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Expected a type, but ‘m’ has kind ‘k2’ - ‘k2’ is a rigid type variable bound by + • Expected a type, but ‘m’ has kind ‘k’ + ‘k’ is a rigid type variable bound by the type signature for: - f :: forall {k2} (m :: k2). () + f :: forall {k} (m :: k). () at T14584a.hs:11:1-17 • In the type ‘m’ In the expression: id @m :: _ @@ -18,7 +19,7 @@ T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Found type wildcard ‘_’ standing for ‘m -> m’ Where: ‘m’, ‘k’ are rigid type variables bound by the type signature for: - f :: forall {k2} (m :: k2). () + f :: forall {k} (m :: k). () at T14584a.hs:11:1-17 • In an expression type signature: _ In the expression: id @m :: _ @@ -26,10 +27,10 @@ T14584a.hs:12:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Relevant bindings include f :: () (bound at T14584a.hs:12:1) T14584a.hs:15:17: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Expected a type, but ‘m’ has kind ‘k2’ - ‘k2’ is a rigid type variable bound by + • Expected a type, but ‘m’ has kind ‘k’ + ‘k’ is a rigid type variable bound by the type signature for: - g :: forall {k2} (m :: k2). () + g :: forall {k} (m :: k). () at T14584a.hs:14:1-17 • In the type ‘m’ In the expression: id @m diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr index 37627b852b..e081453659 100644 --- a/testsuite/tests/patsyn/should_fail/T15685.stderr +++ b/testsuite/tests/patsyn/should_fail/T15685.stderr @@ -1,19 +1,13 @@ T15685.hs:13:24: error: - • Couldn't match kind ‘a1’ with ‘[k0]’ - When matching types - f :: a1 -> * - NP a0 :: [k0] -> * - Expected: f a2 - Actual: NP a0 b0 - ‘a1’ is untouchable - inside the constraints: as ~ (a2 : as1) - bound by a pattern with constructor: - Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]). - f a2 -> NS f (a2 : as), - in a pattern synonym declaration - at T15685.hs:13:19-26 - ‘a1’ is a rigid type variable bound by + • Could not deduce: a ~ [k0] + from the context: as ~ (a1 : as1) + bound by a pattern with constructor: + Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]). + f a2 -> NS f (a2 : as), + in a pattern synonym declaration + at T15685.hs:13:19-26 + ‘a’ is a rigid type variable bound by the inferred type of HereNil :: NS f as at T15685.hs:13:9-15 Possible fix: add a type signature for ‘HereNil’ diff --git a/testsuite/tests/patsyn/should_fail/T15694.stderr b/testsuite/tests/patsyn/should_fail/T15694.stderr index 360fb30ba2..7e1507c332 100644 --- a/testsuite/tests/patsyn/should_fail/T15694.stderr +++ b/testsuite/tests/patsyn/should_fail/T15694.stderr @@ -1,4 +1,7 @@ T15694.hs:22:35: error: - • Expected kind ‘k1 -> k00’, but ‘f a1’ has kind ‘ks’ + • Expected kind ‘k1 -> k0’, but ‘f a1’ has kind ‘ks’ + ‘ks’ is a rigid type variable bound by + the data constructor ‘ASSO’ + at T15694.hs:18:30-31 • In the first argument of ‘(~~)’, namely ‘f a1 a2’ diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr index 2e834c6d08..82398e15a7 100644 --- a/testsuite/tests/patsyn/should_fail/T15695.stderr +++ b/testsuite/tests/patsyn/should_fail/T15695.stderr @@ -1,7 +1,7 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)] • Could not deduce: a2 ~ NA 'VO - from the context: ((* -> * -> *) ~ (k1 -> k2 -> *), Either ~~ f, + from the context: ((* -> * -> *) ~ (k -> k1 -> *), Either ~~ f, ctx ~~ (a2 ':&: (a3 ':&: 'E)), f a2 ~~ f1, f1 a3 ~~ a4) bound by a pattern with pattern synonym: ASSO :: forall kind (a :: kind) (b :: Ctx kind). diff --git a/testsuite/tests/plugins/test-hole-plugin.stderr b/testsuite/tests/plugins/test-hole-plugin.stderr index 7ca539e8d7..109736fa78 100644 --- a/testsuite/tests/plugins/test-hole-plugin.stderr +++ b/testsuite/tests/plugins/test-hole-plugin.stderr @@ -2,8 +2,7 @@ test-hole-plugin.hs:12:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _too_long :: [Int] -> Int Or perhaps ‘_too_long’ is mis-spelled, or not in scope - • In the expression: _too_long - In an equation for ‘f’: f = _too_long + • In an equation for ‘f’: f = _too_long • Relevant bindings include f :: [Int] -> Int (bound at test-hole-plugin.hs:12:1) Valid hole fits include @@ -11,8 +10,7 @@ test-hole-plugin.hs:12:5: warning: [-Wtyped-holes (in -Wdefault)] test-hole-plugin.hs:13:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: [Int] -> Int - • In the expression: _ - In an equation for ‘j’: j = _ + • In an equation for ‘j’: j = _ • Relevant bindings include j :: [Int] -> Int (bound at test-hole-plugin.hs:13:1) Valid hole fits include @@ -27,8 +25,7 @@ test-hole-plugin.hs:13:5: warning: [-Wtyped-holes (in -Wdefault)] test-hole-plugin.hs:14:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _sort_by_mod_desc :: [Int] -> Int Or perhaps ‘_sort_by_mod_desc’ is mis-spelled, or not in scope - • In the expression: _sort_by_mod_desc - In an equation for ‘i’: i = _sort_by_mod_desc + • In an equation for ‘i’: i = _sort_by_mod_desc • Relevant bindings include i :: [Int] -> Int (bound at test-hole-plugin.hs:14:1) Valid hole fits include @@ -43,8 +40,7 @@ test-hole-plugin.hs:14:5: warning: [-Wtyped-holes (in -Wdefault)] test-hole-plugin.hs:15:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _only_Data_List :: [Int] -> Int Or perhaps ‘_only_Data_List’ is mis-spelled, or not in scope - • In the expression: _only_Data_List - In an equation for ‘g’: g = _only_Data_List + • In an equation for ‘g’: g = _only_Data_List • Relevant bindings include g :: [Int] -> Int (bound at test-hole-plugin.hs:15:1) Valid hole fits include @@ -54,8 +50,7 @@ test-hole-plugin.hs:15:5: warning: [-Wtyped-holes (in -Wdefault)] test-hole-plugin.hs:16:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _only_Prelude :: [Int] -> Int Or perhaps ‘_only_Prelude’ is mis-spelled, or not in scope - • In the expression: _only_Prelude - In an equation for ‘h’: h = _only_Prelude + • In an equation for ‘h’: h = _only_Prelude • Relevant bindings include h :: [Int] -> Int (bound at test-hole-plugin.hs:16:1) Valid hole fits include diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr index 11a81baf62..156f8490e8 100644 --- a/testsuite/tests/polykinds/T11520.stderr +++ b/testsuite/tests/polykinds/T11520.stderr @@ -1,6 +1,9 @@ T11520.hs:15:77: error: • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’ + ‘k’ is a rigid type variable bound by + the instance declaration + at T11520.hs:(15,1)-(16,23) • In the second argument of ‘Compose’, namely ‘g’ In the first argument of ‘Typeable’, namely ‘(Compose f g)’ In the instance declaration for ‘Typeable (Compose f g)’ diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr index 5ce7b07187..fcf194ba50 100644 --- a/testsuite/tests/polykinds/T12593.stderr +++ b/testsuite/tests/polykinds/T12593.stderr @@ -1,16 +1,9 @@ -T12593.hs:11:16: error: - • Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’ - • In the type signature: - run :: k2 q => - Free k k1 k2 p a b - -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b - T12593.hs:12:31: error: • Expecting one more argument to ‘k’ Expected a type, but ‘k’ has kind - ‘((k2 -> Constraint) -> k3 -> *) -> Constraint’ + ‘((k0 -> Constraint) -> k1 -> *) -> Constraint’ • In the kind ‘k’ In the type signature: run :: k2 q => diff --git a/testsuite/tests/polykinds/T14172.hs b/testsuite/tests/polykinds/T14172.hs index 10fff5af69..06956be91a 100644 --- a/testsuite/tests/polykinds/T14172.hs +++ b/testsuite/tests/polykinds/T14172.hs @@ -5,3 +5,8 @@ import T14172a traverseCompose :: (a -> f b) -> g a -> f (h _) traverseCompose = _Wrapping Compose . traverse + +-- traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) +-- (.) :: (y->z) -> (x->y) -> (x -> z) +-- x := a -> f b +-- z := g a -> f (h a1) diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr index d27f45bb9c..0f5d0271b4 100644 --- a/testsuite/tests/polykinds/T14172.stderr +++ b/testsuite/tests/polykinds/T14172.stderr @@ -15,6 +15,10 @@ T14172.hs:7:19: error: Expected: (f'0 a -> f (f'0 b)) -> Compose f'0 g'0 a -> f (h a') Actual: (Unwrapped (Compose f'0 g'0 a) -> f (Unwrapped (h a'))) -> Compose f'0 g'0 a -> f (h a') + ‘a’ is a rigid type variable bound by + the inferred type of + traverseCompose :: (a -> f b) -> g a -> f (h a') + at T14172.hs:6:1-47 • In the first argument of ‘(.)’, namely ‘_Wrapping Compose’ In the expression: _Wrapping Compose . traverse In an equation for ‘traverseCompose’: diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 2d49b819a0..8ff308ba1d 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -5,14 +5,14 @@ T14846.hs:38:8: error: Actual: Hom riki a a ‘ríki’ is a rigid type variable bound by the type signature for: - i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5) - (a :: Struct cls3) (ríki :: Struct cls3 -> Struct cls3 -> *). + i :: forall {k4} {k5} {cls2 :: k5 -> Constraint} (xx :: k4) + (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *). StructI xx a => ríki a a at T14846.hs:38:8-48 • When checking that instance signature for ‘i’ is more general than its signature in the class - Instance sig: forall {k1} {k2} {cls :: k2 -> Constraint} (xx :: k1) + Instance sig: forall {k1} {k3} {cls :: k3 -> Constraint} (xx :: k1) (a :: Struct cls). StructI xx a => Hom riki a a @@ -23,10 +23,10 @@ T14846.hs:38:8: error: In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:44: error: - • Couldn't match kind ‘k4’ with ‘Struct cls3’ - Expected kind ‘Struct cls3 -> Constraint’, - but ‘cls’ has kind ‘k4 -> Constraint’ - ‘k4’ is a rigid type variable bound by + • Couldn't match kind ‘k3’ with ‘Struct cls2’ + Expected kind ‘Struct cls2 -> Constraint’, + but ‘cls’ has kind ‘k3 -> Constraint’ + ‘k3’ is a rigid type variable bound by the instance declaration at T14846.hs:37:10-65 • In the second argument of ‘Structured’, namely ‘cls’ diff --git a/testsuite/tests/polykinds/T15787.stderr b/testsuite/tests/polykinds/T15787.stderr index 88eca5c1ac..7241e2f7fb 100644 --- a/testsuite/tests/polykinds/T15787.stderr +++ b/testsuite/tests/polykinds/T15787.stderr @@ -1,6 +1,9 @@ T15787.hs:15:14: error: • Expected a type, but ‘k’ has kind ‘ob’ + ‘ob’ is a rigid type variable bound by + the data constructor ‘Kl’ + at T15787.hs:15:3-43 • In the type ‘k’ In the definition of data constructor ‘Kl’ In the data declaration for ‘Kl_kind’ diff --git a/testsuite/tests/polykinds/T16221a.stderr b/testsuite/tests/polykinds/T16221a.stderr index 27edc2c8ec..7b550b6c8f 100644 --- a/testsuite/tests/polykinds/T16221a.stderr +++ b/testsuite/tests/polykinds/T16221a.stderr @@ -1,6 +1,12 @@ T16221a.hs:6:49: error: - • Expected kind ‘k1’, but ‘b’ has kind ‘k’ + • Expected kind ‘k’, but ‘b’ has kind ‘k1’ + ‘k1’ is a rigid type variable bound by + the data constructor ‘MkT2’ + at T16221a.hs:6:20 + ‘k’ is a rigid type variable bound by + the data constructor ‘MkT2’ + at T16221a.hs:6:20 • In the second argument of ‘SameKind’, namely ‘b’ In the type ‘(SameKind a b)’ In the definition of data constructor ‘MkT2’ diff --git a/testsuite/tests/polykinds/T16245a.hs b/testsuite/tests/polykinds/T16245a.hs new file mode 100644 index 0000000000..d649701261 --- /dev/null +++ b/testsuite/tests/polykinds/T16245a.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeInType #-} +module Bug where + +import Data.Kind + +type Const a b = a +data SameKind :: k -> k -> Type + +newtype T (k :: Const Type a) = MkT (forall (b :: k). SameKind a b) diff --git a/testsuite/tests/polykinds/T16245a.stderr b/testsuite/tests/polykinds/T16245a.stderr new file mode 100644 index 0000000000..6279ba18bb --- /dev/null +++ b/testsuite/tests/polykinds/T16245a.stderr @@ -0,0 +1,12 @@ + +T16245a.hs:10:66: error: + • Expected kind ‘k’, but ‘b’ has kind ‘k1’ + ‘k1’ is a rigid type variable bound by + the data constructor ‘MkT’ + at T16245a.hs:10:12 + ‘k’ is a rigid type variable bound by + the data constructor ‘MkT’ + at T16245a.hs:10:1-67 + • In the second argument of ‘SameKind’, namely ‘b’ + In the type ‘(forall (b :: k). SameKind a b)’ + In the definition of data constructor ‘MkT’ diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr index 2da3e41c36..61d1b0a2ae 100644 --- a/testsuite/tests/polykinds/T16902.stderr +++ b/testsuite/tests/polykinds/T16902.stderr @@ -1,6 +1,9 @@ T16902.hs:11:10: error: • Expected a type, but found something with kind ‘a’ + ‘a’ is a rigid type variable bound by + the data constructor ‘MkF’ + at T16902.hs:11:3-12 • In the type ‘F a’ In the definition of data constructor ‘MkF’ In the data declaration for ‘F’ diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr index de33036dcf..739e4f2680 100644 --- a/testsuite/tests/polykinds/T17841.stderr +++ b/testsuite/tests/polykinds/T17841.stderr @@ -1,7 +1,7 @@ T17841.hs:7:45: error: - • Expected a type, but ‘t’ has kind ‘k2’ - ‘k2’ is a rigid type variable bound by + • Expected a type, but ‘t’ has kind ‘k’ + ‘k’ is a rigid type variable bound by the class declaration for ‘Foo’ at T17841.hs:7:12-17 • In the kind ‘t’ diff --git a/testsuite/tests/polykinds/T17963.stderr b/testsuite/tests/polykinds/T17963.stderr index 5cade1ded2..e38d216faf 100644 --- a/testsuite/tests/polykinds/T17963.stderr +++ b/testsuite/tests/polykinds/T17963.stderr @@ -1,10 +1,10 @@ T17963.hs:15:23: error: - • Couldn't match kind ‘rep1’ with ‘'LiftedRep’ + • Couldn't match kind ‘rep’ with ‘'LiftedRep’ When matching kinds k0 :: * - ob :: TYPE rep1 - ‘rep1’ is a rigid type variable bound by + ob :: TYPE rep + ‘rep’ is a rigid type variable bound by the class declaration for ‘Category'’ at T17963.hs:13:27-29 • In the first argument of ‘cat’, namely ‘a’ diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr index 34440d774e..dd953fa69a 100644 --- a/testsuite/tests/polykinds/T7438.stderr +++ b/testsuite/tests/polykinds/T7438.stderr @@ -1,16 +1,17 @@ T7438.hs:6:14: error: - • Couldn't match expected type ‘p1’ with actual type ‘p’ - ‘p’ 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 + • Could not deduce: p ~ p1 + from the context: 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 ‘p’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16 + the inferred type of go :: Thrist a b -> p -> p1 + at T7438.hs:6:1-16 ‘p1’ is a rigid type variable bound by - the inferred type of go :: Thrist a b -> p -> p1 at T7438.hs:6:1-16 + the inferred type of go :: Thrist a b -> p -> p1 + 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 diff --git a/testsuite/tests/polykinds/T7594.stderr b/testsuite/tests/polykinds/T7594.stderr index ea5484d464..fc0aa1fcc3 100644 --- a/testsuite/tests/polykinds/T7594.stderr +++ b/testsuite/tests/polykinds/T7594.stderr @@ -1,13 +1,12 @@ T7594.hs:37:12: error: - • Couldn't match type ‘b’ with ‘IO ()’ + • Could not deduce: b ~ IO () + from the context: (:&:) c0 Real a + bound by a type expected by the context: + forall a. (:&:) c0 Real a => a -> b + at T7594.hs:37:12-16 Expected: a -> b Actual: a -> IO () - ‘b’ is untouchable - inside the constraints: (:&:) c0 Real a - bound by a type expected by the context: - forall a. (:&:) c0 Real a => a -> b - at T7594.hs:37:12-16 ‘b’ is a rigid type variable bound by the inferred type of bar2 :: b at T7594.hs:37:1-19 diff --git a/testsuite/tests/polykinds/T7805.stderr b/testsuite/tests/polykinds/T7805.stderr index 869ecc9200..e4fdff52e0 100644 --- a/testsuite/tests/polykinds/T7805.stderr +++ b/testsuite/tests/polykinds/T7805.stderr @@ -1,8 +1,6 @@ T7805.hs:7:21: error: - • Expected kind ‘forall a. a -> a’, but ‘x’ has kind ‘k0’ - Cannot instantiate unification variable ‘k0’ - with a kind involving polytypes: forall a. a -> a + • Expected kind ‘forall a. a -> a’, but ‘x’ has kind ‘*’ • In the first argument of ‘HR’, namely ‘x’ In the first argument of ‘F’, namely ‘(HR x)’ In the type instance declaration for ‘F’ diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index 653f3beb1a..71c2f00584 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -1,14 +1,12 @@ -T8616.hs:8:16: error: - • Couldn't match kind ‘k1’ with ‘*’ - When matching types - Any :: k1 - Proxy kproxy :: * - ‘k1’ is a rigid type variable bound by +T8616.hs:8:30: error: + • Expected a type, but ‘Any :: k’ has kind ‘k’ + ‘k’ is a rigid type variable bound by the type signature for: - withSomeSing :: forall k1 (kproxy :: k1). Proxy kproxy + withSomeSing :: forall k (kproxy :: k). Proxy kproxy at T8616.hs:7:1-52 - • In the expression: undefined :: (Any :: k) + • In an expression type signature: (Any :: k) + In the expression: undefined :: (Any :: k) In an equation for ‘withSomeSing’: withSomeSing = undefined :: (Any :: k) • Relevant bindings include diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr index 2fc5bb1792..b18efe0111 100644 --- a/testsuite/tests/polykinds/T9017.stderr +++ b/testsuite/tests/polykinds/T9017.stderr @@ -1,15 +1,14 @@ T9017.hs:8:7: error: - • Couldn't match kind ‘k2’ with ‘*’ + • Couldn't match kind ‘k’ with ‘*’ When matching types a0 :: * -> * -> * - a :: k2 -> k3 -> * + a :: k -> k1 -> * Expected: a b (m b) Actual: a0 b0 (m0 b0) - ‘k2’ is a rigid type variable bound by + ‘k’ is a rigid type variable bound by the type signature for: - foo :: forall {k2} {k3} (a :: k2 -> k3 -> *) (b :: k2) - (m :: k2 -> k3). + foo :: forall {k} {k1} (a :: k -> k1 -> *) (b :: k) (m :: k -> k1). a b (m b) at T9017.hs:7:1-16 • In the expression: arr return diff --git a/testsuite/tests/polykinds/TyVarTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr index 67da965d09..b0b7924444 100644 --- a/testsuite/tests/polykinds/TyVarTvKinds3.stderr +++ b/testsuite/tests/polykinds/TyVarTvKinds3.stderr @@ -1,6 +1,12 @@ TyVarTvKinds3.hs:9:62: error: • Expected kind ‘k1’, but ‘b’ has kind ‘k2’ + ‘k2’ is a rigid type variable bound by + the data constructor ‘MkBad’ + at TyVarTvKinds3.hs:9:22-23 + ‘k1’ is a rigid type variable bound by + the data constructor ‘MkBad’ + at TyVarTvKinds3.hs:9:19-20 • In the second argument of ‘SameKind’, namely ‘b’ In the first argument of ‘Bad’, namely ‘(SameKind a b)’ In the type ‘Bad (SameKind a b)’ diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 1ff66e63ab..b167b930dc 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -213,6 +213,7 @@ test('T16221', normal, compile, ['']) test('T16221a', normal, compile_fail, ['']) test('T16244', normal, compile_fail, ['']) test('T16245', normal, compile_fail, ['']) +test('T16245a', normal, compile_fail, ['']) test('T16342', normal, compile, ['']) test('T16263', normal, compile_fail, ['']) test('T16902', normal, compile_fail, ['']) diff --git a/testsuite/tests/saks/should_fail/saks_fail019.stderr b/testsuite/tests/saks/should_fail/saks_fail019.stderr index 30882c15ec..b34a7e1905 100644 --- a/testsuite/tests/saks/should_fail/saks_fail019.stderr +++ b/testsuite/tests/saks/should_fail/saks_fail019.stderr @@ -3,4 +3,7 @@ saks_fail019.hs:9:1: error: • Couldn't match kind ‘a’ with ‘*’ Expected: a -> * Actual: * -> * + ‘a’ is a rigid type variable bound by + the data type declaration for ‘T’ + at saks_fail019.hs:9:8 • In the data type declaration for ‘T’ diff --git a/testsuite/tests/simplCore/should_compile/simpl017.stderr b/testsuite/tests/simplCore/should_compile/simpl017.stderr index 96c8e1ea2d..0326e339fb 100644 --- a/testsuite/tests/simplCore/should_compile/simpl017.stderr +++ b/testsuite/tests/simplCore/should_compile/simpl017.stderr @@ -1,22 +1,46 @@ -simpl017.hs:50:15: error: +simpl017.hs:55:5: error: • Couldn't match type: [E m i] -> E' v0 m a with: forall v. [E m i] -> E' v m a - Expected: E m (forall v. [E m i] -> E' v m a) - Actual: E' RValue m ([E m i] -> E' v0 m a) - • In the expression: + Expected: m (forall v. [E m i] -> E' v m a) + Actual: m ([E m i] -> E' v0 m a) + • In a stmt of a 'do' block: return f + In the first argument of ‘E’, namely + ‘(do let ix :: [E m i] -> m i + ix [i] = runE i + {-# INLINE f #-} + .... + return f)’ + In the expression: E (do let ix :: [E m i] -> m i ix [i] = runE i {-# INLINE f #-} .... return f) - In an equation for ‘liftArray’: - liftArray a - = E (do let ix :: [E m i] -> m i - ix [i] = runE i - .... - return f) • Relevant bindings include + f :: [E m i] -> E' v0 m a (bound at simpl017.hs:54:9) + ix :: [E m i] -> m i (bound at simpl017.hs:52:9) a :: arr i a (bound at simpl017.hs:50:11) liftArray :: arr i a -> E m (forall v. [E m i] -> E' v m a) (bound at simpl017.hs:50:1) + +simpl017.hs:71:10: error: + • Couldn't match type: forall v. [E (ST s) Int] -> E' v (ST s) Int + with: [E (ST t0) Int] -> E (ST s) Int + Expected: E' RValue (ST s) ([E (ST t0) Int] -> E (ST s) Int) + Actual: E (ST s) (forall v. [E (ST s) Int] -> E' v (ST s) Int) + • In a stmt of a 'do' block: a <- liftArray ma + In the second argument of ‘($)’, namely + ‘do a <- liftArray ma + let one :: E (ST t) Int + one = return 1 + a [one] `plus` a [one]’ + In the expression: + runE + $ do a <- liftArray ma + let one :: E (ST t) Int + one = return 1 + a [one] `plus` a [one] + • Relevant bindings include + ma :: STArray s Int Int (bound at simpl017.hs:70:5) + foo :: STArray s Int Int -> ST s Int (bound at simpl017.hs:70:1) diff --git a/testsuite/tests/th/T10267.stderr b/testsuite/tests/th/T10267.stderr index 6262bf72ff..2f5598fa1d 100644 --- a/testsuite/tests/th/T10267.stderr +++ b/testsuite/tests/th/T10267.stderr @@ -5,8 +5,7 @@ T10267.hs:8:1: error: the type signature for: j :: forall a. a -> a at T10267.hs:(8,1)-(12,14) - • In the expression: _ - In an equation for ‘j’: j x = _ + • In an equation for ‘j’: j x = _ • Relevant bindings include x :: a (bound at T10267.hs:8:1) j :: a -> a (bound at T10267.hs:8:1) @@ -19,8 +18,7 @@ T10267.hs:8:1: error: i :: forall a. a -> a at T10267.hs:(8,1)-(12,14) Or perhaps ‘_foo’ is mis-spelled, or not in scope - • In the expression: _foo - In an equation for ‘i’: i = _foo + • In an equation for ‘i’: i = _foo • Relevant bindings include i :: a -> a (bound at T10267.hs:8:1) Valid hole fits include i :: a -> a (bound at T10267.hs:8:1) diff --git a/testsuite/tests/th/T15321.stderr b/testsuite/tests/th/T15321.stderr index 3054f02afc..1de67decef 100644 --- a/testsuite/tests/th/T15321.stderr +++ b/testsuite/tests/th/T15321.stderr @@ -1,8 +1,7 @@ T15321.hs:9:9: error: • Found hole: _ :: String -> Language.Haskell.TH.Lib.Internal.ExpQ - • In the expression: _ - In the expression: _ "baz" + • In the expression: _ "baz" In the untyped splice: $(_ "baz") • Valid hole fits include fail :: forall (m :: * -> *) a. MonadFail m => String -> m a diff --git a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs index 69e4fb31c7..dbbec52eaa 100644 --- a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs +++ b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.hs @@ -1,32 +1,34 @@ {-# LANGUAGE TypeFamilies, LiberalTypeSynonyms, ImpredicativeTypes #-} -module PolyTypeDecomp where +module PolyTypeDecomp where -{- The purpose of this test is to check if decomposition of wanted +{- The purpose of this test is to check if decomposition of wanted equalities in the /constraint solver/ (vs. the unifier) works properly. - Unfortunately most equalities between polymorphic types are converted to + Unfortunately most equalities between polymorphic types are converted to implication constraints early on in the unifier, so we have to make things - a bit more convoluted by introducing the myLength function. The wanted + a bit more convoluted by introducing the myLength function. The wanted constraints we get for this program are: [forall a. Maybe a] ~ Id alpha - [forall a. F [a]] ~ Id alpha - Which, /after reactions/ should create a fresh implication: + [forall a. F [a]] ~ Id alpha + Which, /after reactions/ should create a fresh implication: forall a. Maybe a ~ F [a] that is perfectly soluble. -} - + type family F a -type instance F [a] = Maybe a +type instance F [a] = Maybe a -type family Id a +type family Id a type instance Id a = a f :: [forall a. F [a]] f = undefined +-- This can't possibly work, even with Quick Look g :: [forall a. Maybe a] -> Int g x = myLength [x,f] +-- [x,f] :: [[forall a. Maybe a]] -myLength :: [Id a] -> Int +myLength :: [Id a] -> Int myLength = undefined diff --git a/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr new file mode 100644 index 0000000000..bde2a0d703 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/PolytypeDecomp.stderr @@ -0,0 +1,20 @@ + +PolytypeDecomp.hs:30:17: error: + • Couldn't match type ‘a0’ with ‘[forall a. Maybe a]’ + Expected: Id a0 + Actual: [forall a. Maybe a] + Cannot instantiate unification variable ‘a0’ + with a type involving polytypes: [forall a. Maybe a] + • In the expression: x + In the first argument of ‘myLength’, namely ‘[x, f]’ + In the expression: myLength [x, f] + +PolytypeDecomp.hs:30:19: error: + • Couldn't match type ‘a0’ with ‘[forall a. F [a]]’ + Expected: Id a0 + Actual: [forall a. F [a]] + Cannot instantiate unification variable ‘a0’ + with a type involving polytypes: [forall a. F [a]] + • In the expression: f + In the first argument of ‘myLength’, namely ‘[x, f]’ + In the expression: myLength [x, f] diff --git a/testsuite/tests/typecheck/should_compile/T10971a.stderr b/testsuite/tests/typecheck/should_compile/T10971a.stderr index 96330fd61a..800dc84efa 100644 --- a/testsuite/tests/typecheck/should_compile/T10971a.stderr +++ b/testsuite/tests/typecheck/should_compile/T10971a.stderr @@ -35,8 +35,8 @@ T10971a.hs:9:6: warning: [-Wname-shadowing (in -Wall)] T10971a.hs:9:14: warning: [-Wtype-defaults (in -Wall)] • Defaulting the following constraints to type ‘[]’ (Traversable t0) - arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-28 - (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-38 + arising from a use of ‘fmapDefault’ at T10971a.hs:9:14-24 + (Foldable t0) arising from a use of ‘length’ at T10971a.hs:9:31-36 • In the expression: fmapDefault f x In the expression: (fmapDefault f x, length x) In the expression: \ f x -> (fmapDefault f x, length x) diff --git a/testsuite/tests/typecheck/should_compile/T13050.stderr b/testsuite/tests/typecheck/should_compile/T13050.stderr index 89f2b80d3b..92db8e2b63 100644 --- a/testsuite/tests/typecheck/should_compile/T13050.stderr +++ b/testsuite/tests/typecheck/should_compile/T13050.stderr @@ -1,8 +1,7 @@ T13050.hs:4:9: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int -> Int -> Int - • In the expression: _ - In the expression: _ x y + • In the expression: _ x y In an equation for ‘f’: f x y = _ x y • Relevant bindings include y :: Int (bound at T13050.hs:4:5) diff --git a/testsuite/tests/typecheck/should_compile/T9404b.hs b/testsuite/tests/typecheck/should_compile/T9404b.hs index f9db0a3897..2fe837f70e 100644 --- a/testsuite/tests/typecheck/should_compile/T9404b.hs +++ b/testsuite/tests/typecheck/should_compile/T9404b.hs @@ -11,5 +11,5 @@ bar _ = () myconst :: ((forall r. ListTF r -> Int) -> ()) -> x -> (forall r. ListTF r -> Int) -> () myconst x _ = x -foo = (bar `myconst` ()) $ length +foo = (bar `myconst` ()) $ length foo2 = (myconst bar ()) $ length diff --git a/testsuite/tests/typecheck/should_compile/T9497a.stderr b/testsuite/tests/typecheck/should_compile/T9497a.stderr index d24849df79..114a7046ca 100644 --- a/testsuite/tests/typecheck/should_compile/T9497a.stderr +++ b/testsuite/tests/typecheck/should_compile/T9497a.stderr @@ -2,8 +2,7 @@ T9497a.hs:2:8: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _main :: IO () Or perhaps ‘_main’ is mis-spelled, or not in scope - • In the expression: _main - In an equation for ‘main’: main = _main + • In an equation for ‘main’: main = _main • Relevant bindings include main :: IO () (bound at T9497a.hs:2:1) Valid hole fits include main :: IO () (bound at T9497a.hs:2:1) diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr index 8182d7c992..57214ba181 100644 --- a/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr @@ -1,8 +1,7 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: [Integer] -> Integer - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: [Integer] -> Integer (bound at abstract_refinement_hole_fits.hs:4:1) @@ -125,8 +124,7 @@ abstract_refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)] abstract_refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Integer -> [Integer] -> Integer - • In the expression: _ - In the expression: _ 0 + • In the expression: _ 0 In an equation for ‘g’: g = _ 0 • Relevant bindings include g :: [Integer] -> Integer diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 9e4e80dba8..a74a84f461 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -216,7 +216,7 @@ test('tc207', normal, compile, ['']) test('tc208', normal, compile, ['']) test('tc209', normal, compile, ['']) test('tc210', normal, compile, ['']) -test('tc211', normal, compile_fail, ['']) +test('tc211', normal, compile, ['']) test('tc212', normal, compile, ['']) test('tc213', normal, compile, ['']) test('tc214', normal, compile, ['']) @@ -364,7 +364,7 @@ test('T3108', normal, compile, ['']) test('T5792',normal, makefile_test, []) -test('PolytypeDecomp', normal, compile, ['']) +test('PolytypeDecomp', normal, compile_fail, ['']) test('T6011', normal, compile, ['']) test('T6055', normal, compile, ['']) test('DfltProb1', normal, compile, ['-O']) diff --git a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr index adb507ea92..ffc02228f2 100644 --- a/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr @@ -5,8 +5,7 @@ constraint_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: g :: forall a. Ord a => [a] -> a at constraint_hole_fits.hs:3:1-22 - • In the expression: _ - In an equation for ‘g’: g = _ + • In an equation for ‘g’: g = _ • Relevant bindings include g :: [a] -> a (bound at constraint_hole_fits.hs:4:1) Constraints include Ord a (from constraint_hole_fits.hs:3:1-22) diff --git a/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr index 851e92e5fd..eee461b708 100644 --- a/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr @@ -10,9 +10,9 @@ free_monad_hole_fits.hs:14:28: warning: [-Wtyped-holes (in -Wdefault)] the instance declaration at free_monad_hole_fits.hs:10:10-38 Or perhaps ‘_a’ is mis-spelled, or not in scope - • In the expression: _a - In the first argument of ‘Free’, namely ‘(_a go fa)’ + • In the first argument of ‘Free’, namely ‘(_a go fa)’ In the expression: Free (_a go fa) + In an equation for ‘go’: go (Free fa) = Free (_a go fa) • Relevant bindings include fa :: f (Free f a) (bound at free_monad_hole_fits.hs:14:16) go :: Free f a -> Free f b (bound at free_monad_hole_fits.hs:12:7) diff --git a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr index c1796aad12..2e32b1b92a 100644 --- a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr +++ b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr @@ -5,8 +5,7 @@ hole_constraints.hs:8:6: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: f1 :: forall a. Eq a => a at hole_constraints.hs:7:1-15 - • In the expression: _ - In an equation for ‘f1’: f1 = _ + • In an equation for ‘f1’: f1 = _ • Relevant bindings include f1 :: a (bound at hole_constraints.hs:8:1) Constraints include Eq a (from hole_constraints.hs:7:1-15) @@ -18,8 +17,7 @@ hole_constraints.hs:12:6: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: f2 :: forall a. (Show a, Eq a) => a at hole_constraints.hs:11:1-25 - • In the expression: _ - In an equation for ‘f2’: f2 = _ + • In an equation for ‘f2’: f2 = _ • Relevant bindings include f2 :: a (bound at hole_constraints.hs:12:1) Constraints include @@ -34,8 +32,7 @@ hole_constraints.hs:16:35: warning: [-Wtyped-holes (in -Wdefault)] Where: ‘a’ is a rigid type variable bound by the instance declaration at hole_constraints.hs:16:10-22 - • In the expression: _ - In an equation for ‘f3’: f3 = _ + • In an equation for ‘f3’: f3 = _ In the instance declaration for ‘C [a]’ • Relevant bindings include f3 :: [a] (bound at hole_constraints.hs:16:30) @@ -52,8 +49,7 @@ hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: castWith :: forall a b. (a :~: b) -> a -> b at hole_constraints.hs:19:1-29 - • In the expression: _ - In an equation for ‘castWith’: castWith Refl x = _ + • In an equation for ‘castWith’: castWith Refl x = _ • Relevant bindings include x :: a (bound at hole_constraints.hs:20:15) castWith :: (a :~: b) -> a -> b (bound at hole_constraints.hs:20:1) @@ -62,9 +58,9 @@ hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)] hole_constraints.hs:27:32: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: String - • In the expression: _ - In a case alternative: AnyShow x -> _ + • In a case alternative: AnyShow x -> _ In the expression: case a of { AnyShow x -> _ } + In an equation for ‘foo’: foo a = case a of { AnyShow x -> _ } • Relevant bindings include x :: a (bound at hole_constraints.hs:27:27) a :: AnyShow (bound at hole_constraints.hs:27:5) diff --git a/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr b/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr index 46c0c22a34..6ca50b65b4 100644 --- a/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr +++ b/testsuite/tests/typecheck/should_compile/hole_constraints_nested.stderr @@ -1,9 +1,9 @@ hole_constraints_nested.hs:12:16: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int - • In the expression: _ - In a case alternative: EqOrd -> _ + • In a case alternative: EqOrd -> _ In the expression: case d2 of { EqOrd -> _ } + In a case alternative: Refl -> case d2 of { EqOrd -> _ } • Relevant bindings include d2 :: EqOrd a (bound at hole_constraints_nested.hs:9:6) d1 :: a :~: b (bound at hole_constraints_nested.hs:9:3) diff --git a/testsuite/tests/typecheck/should_compile/holes.stderr b/testsuite/tests/typecheck/should_compile/holes.stderr index 77a6fc9a40..a4f106ab82 100644 --- a/testsuite/tests/typecheck/should_compile/holes.stderr +++ b/testsuite/tests/typecheck/should_compile/holes.stderr @@ -4,15 +4,13 @@ holes.hs:3:5: warning: [-Wtyped-holes (in -Wdefault)] Where: ‘t’ is a rigid type variable bound by the inferred type of f :: t at holes.hs:3:1-5 - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: t (bound at holes.hs:3:1) Valid hole fits include f :: forall {t}. t holes.hs:6:7: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Char - • In the expression: _ - In an equation for ‘g’: g x = _ + • In an equation for ‘g’: g x = _ • Relevant bindings include x :: Int (bound at holes.hs:6:3) g :: Int -> Char (bound at holes.hs:6:1) diff --git a/testsuite/tests/typecheck/should_compile/holes3.stderr b/testsuite/tests/typecheck/should_compile/holes3.stderr index 874fd4459f..2210fc5dea 100644 --- a/testsuite/tests/typecheck/should_compile/holes3.stderr +++ b/testsuite/tests/typecheck/should_compile/holes3.stderr @@ -4,16 +4,14 @@ holes3.hs:3:5: error: Where: ‘t’ is a rigid type variable bound by the inferred type of f :: t at holes3.hs:3:1-5 - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: t (bound at holes3.hs:3:1) Valid hole fits include f :: forall {t}. t holes3.hs:6:7: error: • Found hole: _gr :: Char Or perhaps ‘_gr’ is mis-spelled, or not in scope - • In the expression: _gr - In an equation for ‘g’: g x = _gr + • In an equation for ‘g’: g x = _gr • Relevant bindings include x :: Int (bound at holes3.hs:6:3) g :: Int -> Char (bound at holes3.hs:6:1) diff --git a/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr index 5485d05bef..2cf85f3c1e 100644 --- a/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/local_hole_fits.stderr @@ -5,8 +5,7 @@ local_hole_fits.hs:4:15: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: head :: forall a. [a] -> a at local_hole_fits.hs:3:1-16 - • In the expression: _ - In an equation for ‘head’: head (x : xs) = _ + • In an equation for ‘head’: head (x : xs) = _ • Relevant bindings include xs :: [a] (bound at local_hole_fits.hs:4:9) x :: a (bound at local_hole_fits.hs:4:7) @@ -19,8 +18,7 @@ local_hole_fits.hs:8:11: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: mshow :: forall a. Show a => a -> a at local_hole_fits.hs:7:1-25 - • In the expression: _ - In an equation for ‘mshow’: mshow a = _ + • In an equation for ‘mshow’: mshow a = _ • Relevant bindings include a :: a (bound at local_hole_fits.hs:8:7) mshow :: a -> a (bound at local_hole_fits.hs:8:1) diff --git a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr index 9e97fb51ff..9ed1615215 100644 --- a/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr @@ -1,8 +1,7 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: [Integer] -> Integer - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: [Integer] -> Integer (bound at refinement_hole_fits.hs:4:1) Valid hole fits include @@ -114,8 +113,7 @@ refinement_hole_fits.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)] refinement_hole_fits.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Integer -> [Integer] -> Integer - • In the expression: _ - In the expression: _ 0 + • In the expression: _ 0 In an equation for ‘g’: g = _ 0 • Relevant bindings include g :: [Integer] -> Integer (bound at refinement_hole_fits.hs:7:1) diff --git a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr index 6007ab4d0b..7799aad239 100644 --- a/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr @@ -1,8 +1,7 @@ subsumption_sort_hole_fits.hs:2:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: String -> [String] - • In the expression: _ - In the expression: _ "hello, world" + • In the expression: _ "hello, world" In an equation for ‘f’: f = _ "hello, world" • Relevant bindings include f :: [String] (bound at subsumption_sort_hole_fits.hs:2:1) diff --git a/testsuite/tests/typecheck/should_compile/tc211.hs b/testsuite/tests/typecheck/should_compile/tc211.hs index e132cd8c80..0e23ed1640 100644 --- a/testsuite/tests/typecheck/should_compile/tc211.hs +++ b/testsuite/tests/typecheck/should_compile/tc211.hs @@ -1,4 +1,4 @@ -{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables -XGADTs #-} +{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, GADTs #-} -- Nov 2014: impredicative types are very dodgy so I am -- FAR from confident that these tests give the right errors diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr deleted file mode 100644 index bbffa16943..0000000000 --- a/testsuite/tests/typecheck/should_compile/tc211.stderr +++ /dev/null @@ -1,17 +0,0 @@ - -tc211.hs:21:17: error: - • Couldn't match expected type: a -> a - with actual type: forall a. a -> a - • In the first argument of ‘(:) :: - (forall a. a -> a) - -> [forall a. a -> a] -> [forall a. a -> a]’, namely - ‘(head foo)’ - In the expression: - ((:) :: - (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]) - (head foo) foo - In an equation for ‘bar’: - bar - = ((:) :: - (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]) - (head foo) foo diff --git a/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr index 4757d4915c..9f96ea3505 100644 --- a/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr @@ -3,8 +3,7 @@ type_in_type_hole_fits.hs:79:11: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _a :: [Integer] -> Sorted (O ('NLogN 2 0)) (O N) 'True Integer Or perhaps ‘_a’ is mis-spelled, or not in scope - • In the expression: _a - In the expression: _a [3, 1, 2] + • In the expression: _a [3, 1, 2] In an equation for ‘mySortA’: mySortA = _a [3, 1, 2] • Relevant bindings include mySortA :: Sorted (O (N ^. 2)) (O N) 'True Integer @@ -32,8 +31,7 @@ type_in_type_hole_fits.hs:82:11: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _b :: [Integer] -> Sorted (O ('NLogN 1 1)) (O N) 'False Integer Or perhaps ‘_b’ is mis-spelled, or not in scope - • In the expression: _b - In the expression: _b [3, 1, 2] + • In the expression: _b [3, 1, 2] In an equation for ‘mySortB’: mySortB = _b [3, 1, 2] • Relevant bindings include mySortB :: Sorted (O (N *. LogN)) (O N) 'False Integer @@ -65,8 +63,7 @@ type_in_type_hole_fits.hs:85:11: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _c :: [Integer] -> Sorted (O ('NLogN 1 1)) (O One) 'False Integer Or perhaps ‘_c’ is mis-spelled, or not in scope - • In the expression: _c - In the expression: _c [3, 1, 2] + • In the expression: _c [3, 1, 2] In an equation for ‘mySortC’: mySortC = _c [3, 1, 2] • Relevant bindings include mySortC :: Sorted (O (N *. LogN)) (O One) 'False Integer diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr index 116a18f42f..5830ecb7d7 100644 --- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr @@ -11,12 +11,16 @@ valid_hole_fits.hs:9:6: warning: [-Wdeferred-out-of-scope-variables (in -Wdefaul valid_hole_fits.hs:17:17: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Int -> IO Int - • In the expression: _ - In a stmt of a 'do' block: y <- _ x + • In a stmt of a 'do' block: y <- _ x In the expression: do x <- a 0 y <- _ x return y + In an equation for ‘c’: + c _ + = do x <- a 0 + y <- _ x + return y • Relevant bindings include x :: Int (bound at valid_hole_fits.hs:16:12) c :: Int -> IO Int (bound at valid_hole_fits.hs:16:1) @@ -39,8 +43,7 @@ valid_hole_fits.hs:21:8: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: test :: forall a. [Maybe a] -> [a] at valid_hole_fits.hs:20:1-24 - • In the expression: _ - In an equation for ‘test’: test = _ + • In an equation for ‘test’: test = _ • Relevant bindings include test :: [Maybe a] -> [a] (bound at valid_hole_fits.hs:21:1) Valid hole fits include @@ -55,8 +58,7 @@ valid_hole_fits.hs:21:8: warning: [-Wtyped-holes (in -Wdefault)] valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Integer -> ValidHoleFits.Moo - • In the expression: _ - In an equation for ‘test2’: test2 = _ + • In an equation for ‘test2’: test2 = _ • Relevant bindings include test2 :: Integer -> ValidHoleFits.Moo (bound at valid_hole_fits.hs:24:1) @@ -70,8 +72,7 @@ valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)] valid_hole_fits.hs:27:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: t0 -> Maybe Integer Where: ‘t0’ is an ambiguous type variable - • In the expression: _ - In the expression: _ 2 + • In the expression: _ 2 In an equation for ‘k’: k = _ 2 • Relevant bindings include k :: Maybe Integer (bound at valid_hole_fits.hs:27:1) @@ -128,9 +129,9 @@ valid_hole_fits.hs:30:10: warning: [-Wtyped-holes (in -Wdefault)] valid_hole_fits.hs:34:11: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: Bool -> a0 Where: ‘a0’ is an ambiguous type variable - • In the expression: _ - In the first argument of ‘show’, namely ‘(_ (_ :: Bool))’ + • In the first argument of ‘show’, namely ‘(_ (_ :: Bool))’ In the expression: show (_ (_ :: Bool)) + In an equation for ‘h’: h = show (_ (_ :: Bool)) • Relevant bindings include h :: String (bound at valid_hole_fits.hs:34:1) Valid hole fits include @@ -202,8 +203,7 @@ valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)] the type signature for: myCons :: forall a. a -> [a] -> [a] at valid_hole_fits.hs:37:1-25 - • In the expression: _ - In an equation for ‘myCons’: myCons = _ + • In an equation for ‘myCons’: myCons = _ • Relevant bindings include myCons :: a -> [a] -> [a] (bound at valid_hole_fits.hs:38:1) Valid hole fits include @@ -226,8 +226,7 @@ valid_hole_fits.hs:38:10: warning: [-Wtyped-holes (in -Wdefault)] valid_hole_fits.hs:41:8: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: String -> IO () - • In the expression: _ - In the expression: _ "hello, world" + • In the expression: _ "hello, world" In an equation for ‘main’: main = _ "hello, world" • Relevant bindings include main :: IO () (bound at valid_hole_fits.hs:41:1) diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr index ac4fdc94c7..90f7943f09 100644 --- a/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr +++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr @@ -1,8 +1,7 @@ valid_hole_fits_interactions.hs:15:5: warning: [-Wtyped-holes (in -Wdefault)] • Found hole: _ :: SBool 'True - • In the expression: _ - In an equation for ‘f’: f = _ + • In an equation for ‘f’: f = _ • Relevant bindings include f :: SBool 'True (bound at valid_hole_fits_interactions.hs:15:1) Valid hole fits include diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr index 255b3ad702..6345e2ab1c 100644 --- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr +++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr @@ -1,6 +1,9 @@ FrozenErrorTests.hs:26:9: error: • Couldn't match type ‘a’ with ‘[a]’ arising from a use of ‘goo1’ + ‘a’ is a rigid type variable bound by + the inferred type of test1 :: a + at FrozenErrorTests.hs:26:1-28 • In the expression: goo1 False undefined In an equation for ‘test1’: test1 = goo1 False undefined • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr index 0c810f4185..16056e3e27 100644 --- a/testsuite/tests/typecheck/should_fail/T12177.stderr +++ b/testsuite/tests/typecheck/should_fail/T12177.stderr @@ -4,9 +4,9 @@ T12177.hs:3:19: error: Where: ‘t’ is a rigid type variable bound by the inferred type of bar :: p -> p1 -> t at T12177.hs:3:1-19 - • In the expression: _ - In the expression: \ x -> _ + • In the expression: \ x -> _ In the expression: \ x -> \ x -> _ + In an equation for ‘bar’: bar = \ x -> \ x -> _ • Relevant bindings include x :: p1 (bound at T12177.hs:3:14) bar :: p -> p1 -> t (bound at T12177.hs:3:1) @@ -16,9 +16,9 @@ T12177.hs:5:37: error: Where: ‘t’ is a rigid type variable bound by the inferred type of baz :: p -> p1 -> p2 -> p3 -> p4 -> t at T12177.hs:5:1-37 - • In the expression: _ - In the expression: \ z -> _ + • In the expression: \ z -> _ In the expression: \ x -> \ z -> _ + In the expression: \ z -> \ x -> \ z -> ... • Relevant bindings include z :: p4 (bound at T12177.hs:5:32) x :: p3 (bound at T12177.hs:5:26) diff --git a/testsuite/tests/typecheck/should_fail/T14884.stderr b/testsuite/tests/typecheck/should_fail/T14884.stderr index e1738891a7..c901811f6f 100644 --- a/testsuite/tests/typecheck/should_fail/T14884.stderr +++ b/testsuite/tests/typecheck/should_fail/T14884.stderr @@ -2,8 +2,7 @@ T14884.hs:4:5: error: • Found hole: _ :: (a0 -> IO ()) -> String -> IO () Where: ‘a0’ is an ambiguous type variable - • In the expression: _ - In the expression: _ print "abc" + • In the expression: _ print "abc" In an equation for ‘x’: x = _ print "abc" • Relevant bindings include x :: IO () (bound at T14884.hs:4:1) Valid hole fits include diff --git a/testsuite/tests/typecheck/should_fail/T14904a.stderr b/testsuite/tests/typecheck/should_fail/T14904a.stderr index c0e2b84a80..3b8d005bab 100644 --- a/testsuite/tests/typecheck/should_fail/T14904a.stderr +++ b/testsuite/tests/typecheck/should_fail/T14904a.stderr @@ -1,7 +1,8 @@ T14904a.hs:9:6: error: - • Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’ - Cannot instantiate unification variable ‘k0’ - with a kind involving polytypes: forall (a :: k1). g a + • Expected kind ‘forall (a :: k). g a’, but ‘f’ has kind ‘k1’ + ‘k1’ is a rigid type variable bound by + a family instance declaration + at T14904a.hs:9:3-30 • In the first argument of ‘F’, namely ‘(f :: forall a. g a)’ In the type family declaration for ‘F’ diff --git a/testsuite/tests/typecheck/should_fail/T15799.stderr b/testsuite/tests/typecheck/should_fail/T15799.stderr index f93e043471..4e6d7b4dfd 100644 --- a/testsuite/tests/typecheck/should_fail/T15799.stderr +++ b/testsuite/tests/typecheck/should_fail/T15799.stderr @@ -2,6 +2,3 @@ T15799.hs:46:62: error: • Expected kind ‘Op Nat’, but ‘UnOp b’ has kind ‘Nat’ • In the first argument of ‘(<=)’, namely ‘UnOp b’ - -T15799.hs:46:62: error: - Expected a constraint, but ‘UnOp b <= a’ has kind ‘*’ diff --git a/testsuite/tests/typecheck/should_fail/T15807.stderr b/testsuite/tests/typecheck/should_fail/T15807.stderr index 809398ade0..bac4b5596e 100644 --- a/testsuite/tests/typecheck/should_fail/T15807.stderr +++ b/testsuite/tests/typecheck/should_fail/T15807.stderr @@ -1,6 +1,9 @@ -T15807.hs:12:12: error: - • Expected kind ‘f -> *’, but ‘f’ has kind ‘*’ - • In the type ‘f a’ - In the definition of data constructor ‘MkApp’ +T15807.hs:12:3: error: + • Cannot generalise type; skolem ‘f’ would escape its scope + if I tried to quantify (f0 :: f -> *) in this type: + forall f (a :: f). f a #-> App @f @f0 a + (Indeed, I sometimes struggle even printing this correctly, + due to its ill-scoped nature.) + • In the definition of data constructor ‘MkApp’ In the data declaration for ‘App’ diff --git a/testsuite/tests/typecheck/should_fail/T15862.stderr b/testsuite/tests/typecheck/should_fail/T15862.stderr index 97fbfab166..aeb0f73b9b 100644 --- a/testsuite/tests/typecheck/should_fail/T15862.stderr +++ b/testsuite/tests/typecheck/should_fail/T15862.stderr @@ -1,28 +1,7 @@ -T15862.hs:17:7: error: - • No instance for (Typeable 'MkFoo) arising from a use of ‘typeRep’ - GHC can't yet do polykinded - Typeable ('MkFoo :: (forall a. a) -> Foo) - • In the expression: typeRep @MkFoo - In an equation for ‘foo’: foo = typeRep @MkFoo - -T15862.hs:25:7: error: - • No instance for (Typeable 'MkBar) arising from a use of ‘typeRep’ - GHC can't yet do polykinded Typeable ('MkBar :: Bool -> Bar) - • In the expression: typeRep - In an equation for ‘bar’: bar = typeRep - -T15862.hs:30:8: error: - • No instance for (Typeable 'MkQuux) - arising from a use of ‘typeRep’ - GHC can't yet do polykinded - Typeable ('MkQuux :: (# Bool | Int #) -> Quux) - • In the expression: typeRep - In an equation for ‘quux’: quux = typeRep - -T15862.hs:36:8: error: - • No instance for (Typeable 'MkQuuz) - arising from a use of ‘typeRep’ - GHC can't yet do polykinded Typeable ('MkQuuz :: Quuz) - • In the expression: typeRep - In an equation for ‘quuz’: quuz = typeRep +T15862.hs:16:16: error: + • Expected kind ‘k0’, but ‘MkFoo’ has kind ‘(forall a. a) -> Foo’ + Cannot instantiate unification variable ‘k0’ + with a kind involving polytypes: (forall a. a) -> Foo + • In the first argument of ‘TypeRep’, namely ‘MkFoo’ + In the type signature: foo :: TypeRep MkFoo diff --git a/testsuite/tests/typecheck/should_fail/T15962.stderr b/testsuite/tests/typecheck/should_fail/T15962.stderr index ffab68c98e..49dbb8ce96 100644 --- a/testsuite/tests/typecheck/should_fail/T15962.stderr +++ b/testsuite/tests/typecheck/should_fail/T15962.stderr @@ -1,18 +1,18 @@ -T15962.hs:27:11: - Found hole: _ :: Big ks -> Big (Eval (Map Dual ks)) + +T15962.hs:27:11: error: + • Found hole: _ :: Big ks -> Big (Eval (Map Dual ks)) Where: ‘ks’ is a rigid type variable bound by the type signature for: dualBig :: forall (ks :: [OpKind]). Big ks -> Big (Eval (Map Dual ks)) at T15962.hs:26:1-45 - In the expression: _ - In an equation for ‘dualBig’: dualBig = _ - Relevant bindings include + • In an equation for ‘dualBig’: dualBig = _ + • Relevant bindings include dualBig :: Big ks -> Big (Eval (Map Dual ks)) (bound at T15962.hs:27:1) Valid hole fits include dualBig :: Big ks -> Big (Eval (Map Dual ks)) (bound at T15962.hs:27:1) -T15962.hs:33:12: +T15962.hs:33:12: error: Variable not in scope: iDontExist :: Big ('Conjunction : ks) diff --git a/testsuite/tests/typecheck/should_fail/T16456.stderr b/testsuite/tests/typecheck/should_fail/T16456.stderr index fbc0cc6ed5..5e69b9352a 100644 --- a/testsuite/tests/typecheck/should_fail/T16456.stderr +++ b/testsuite/tests/typecheck/should_fail/T16456.stderr @@ -1,8 +1,7 @@ T16456.hs:7:7: error: • Found hole: _ :: T Int - • In the expression: _ - In an equation for ‘foo’: foo = _ + • In an equation for ‘foo’: foo = _ • Relevant bindings include foo :: T Int (bound at T16456.hs:7:1) Valid hole fits include foo :: T Int (bound at T16456.hs:7:1) diff --git a/testsuite/tests/typecheck/should_fail/T17773.stderr b/testsuite/tests/typecheck/should_fail/T17773.stderr index 401fcc494a..22b3d5577e 100644 --- a/testsuite/tests/typecheck/should_fail/T17773.stderr +++ b/testsuite/tests/typecheck/should_fail/T17773.stderr @@ -8,8 +8,7 @@ T17773.hs:16:22: error: Proxy x -> Proxy y -> Mzero x y :~: (x <|> y) at T17773.hs:(13,1)-(15,41) Or perhaps ‘_Refl’ is mis-spelled, or not in scope - • In the expression: _Refl - In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl + • In an equation for ‘monadPlusMplus’: monadPlusMplus _ _ = _Refl • Relevant bindings include monadPlusMplus :: Proxy x -> Proxy y -> Mzero x y :~: (x <|> y) (bound at T17773.hs:16:1) diff --git a/testsuite/tests/typecheck/should_fail/T18640a.hs b/testsuite/tests/typecheck/should_fail/T18640a.hs new file mode 100644 index 0000000000..b208cfadaa --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640a.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module T18640a where + +import Data.Kind + +type F2 :: forall a b. Type -> a +type family F2 :: forall b. Type -> Type where diff --git a/testsuite/tests/typecheck/should_fail/T18640a.stderr b/testsuite/tests/typecheck/should_fail/T18640a.stderr new file mode 100644 index 0000000000..edc9a83c25 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640a.stderr @@ -0,0 +1,9 @@ + +T18640a.hs:11:1: error: + • Couldn't match kind ‘a’ with ‘*’ + Expected: forall (b :: k). * -> * + Actual: forall (b :: k). * -> a + ‘a’ is a rigid type variable bound by + the type family declaration for ‘F2’ + at T18640a.hs:10:19 + • In the type family declaration for ‘F2’ diff --git a/testsuite/tests/typecheck/should_fail/T18640b.hs b/testsuite/tests/typecheck/should_fail/T18640b.hs new file mode 100644 index 0000000000..f722805ca9 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640b.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module T18640b where + +import Data.Kind + +data family F1 (k :: Type) :: k + +type F3 :: forall (a :: Type) -> forall (b :: Type) -> a +type family F3 a where + F3 a = F1 diff --git a/testsuite/tests/typecheck/should_fail/T18640b.stderr b/testsuite/tests/typecheck/should_fail/T18640b.stderr new file mode 100644 index 0000000000..2a84295a73 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640b.stderr @@ -0,0 +1,12 @@ + +T18640b.hs:14:10: error: + • Couldn't match kind ‘k’ with ‘a’ + Expected kind ‘forall b -> a’, but ‘F1’ has kind ‘forall k -> k’ + ‘k’ is a rigid type variable bound by + the type k + at T18640b.hs:14:3-11 + ‘a’ is a rigid type variable bound by + a family instance declaration + at T18640b.hs:14:6 + • In the type ‘F1’ + In the type family declaration for ‘F3’ diff --git a/testsuite/tests/typecheck/should_fail/T18640c.hs b/testsuite/tests/typecheck/should_fail/T18640c.hs new file mode 100644 index 0000000000..eb6479cc3b --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640c.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module T18640c where + +import Data.Kind + +type F1 :: forall k -> Type +type family F1 k :: Type + +type F2 :: forall x. forall k -> x +type F2 = F1 diff --git a/testsuite/tests/typecheck/should_fail/T18640c.stderr b/testsuite/tests/typecheck/should_fail/T18640c.stderr new file mode 100644 index 0000000000..447882717f --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T18640c.stderr @@ -0,0 +1,10 @@ + +T18640c.hs:14:11: error: + • Couldn't match kind ‘x’ with ‘*’ + Expected kind ‘forall (k1 :: k) -> x’, + but ‘F1’ has kind ‘forall (k1 :: k) -> *’ + ‘x’ is a rigid type variable bound by + the type synonym declaration for ‘F2’ + at T18640c.hs:13:19 + • In the type ‘F1’ + In the type declaration for ‘F2’ diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr index eb84cba7b4..bd4aceed9e 100644 --- a/testsuite/tests/typecheck/should_fail/T1899.stderr +++ b/testsuite/tests/typecheck/should_fail/T1899.stderr @@ -1,5 +1,5 @@ -T1899.hs:14:36: error: +T1899.hs:15:36: error: • Couldn't match type ‘a’ with ‘Proposition a0’ Expected: [Proposition a0] Actual: [a] diff --git a/testsuite/tests/typecheck/should_fail/T2846b.hs b/testsuite/tests/typecheck/should_fail/T2846b.hs index 87468df87e..07f24e7627 100644 --- a/testsuite/tests/typecheck/should_fail/T2846b.hs +++ b/testsuite/tests/typecheck/should_fail/T2846b.hs @@ -3,4 +3,6 @@ module T2846 where f :: String f = show ([1,2,3] :: [Num a => a]) - +-- Rejected with Quick Look +-- The arg of 'show' is a naked 'a' +-- And the actual arg has type (forall a. [Num a => a]), which is polymorphic diff --git a/testsuite/tests/typecheck/should_fail/T2846b.stderr b/testsuite/tests/typecheck/should_fail/T2846b.stderr index 8c52fd7d33..95b30407f2 100644 --- a/testsuite/tests/typecheck/should_fail/T2846b.stderr +++ b/testsuite/tests/typecheck/should_fail/T2846b.stderr @@ -1,7 +1,10 @@ -T2846b.hs:5:5: error: - • No instance for (Show (Num a0 => a0)) - arising from a use of ‘show’ - (maybe you haven't applied a function to enough arguments?) - • In the expression: show ([1, 2, 3] :: [Num a => a]) +T2846b.hs:5:11: error: + • Couldn't match expected type ‘a1’ + with actual type ‘[Num a0 => a0]’ + Cannot instantiate unification variable ‘a1’ + with a type involving polytypes: [Num a0 => a0] + • In the first argument of ‘show’, namely + ‘([1, 2, 3] :: [Num a => a])’ + In the expression: show ([1, 2, 3] :: [Num a => a]) In an equation for ‘f’: f = show ([1, 2, 3] :: [Num a => a]) diff --git a/testsuite/tests/typecheck/should_fail/T5570.stderr b/testsuite/tests/typecheck/should_fail/T5570.stderr index 710104012d..0c12be680e 100644 --- a/testsuite/tests/typecheck/should_fail/T5570.stderr +++ b/testsuite/tests/typecheck/should_fail/T5570.stderr @@ -1,6 +1,6 @@ T5570.hs:7:16: error: • Expecting a lifted type, but ‘Double#’ is unlifted - • In the second argument of ‘($)’, namely ‘D# $ 3.0##’ + • In the first argument of ‘($)’, namely ‘D#’ + In the second argument of ‘($)’, namely ‘D# $ 3.0##’ In the expression: print $ D# $ 3.0## - In an equation for ‘main’: main = print $ D# $ 3.0## diff --git a/testsuite/tests/typecheck/should_fail/T6069.stderr b/testsuite/tests/typecheck/should_fail/T6069.stderr index c70939fee5..ffad9a9534 100644 --- a/testsuite/tests/typecheck/should_fail/T6069.stderr +++ b/testsuite/tests/typecheck/should_fail/T6069.stderr @@ -5,8 +5,8 @@ T6069.hs:13:15: error: Expected: ST s0 Int -> b0 Actual: (forall s. ST s b0) -> b0 • In the second argument of ‘(.)’, namely ‘runST’ - In the expression: print . runST In the expression: (print . runST) fourty_two + In an equation for ‘f1’: f1 = (print . runST) fourty_two T6069.hs:14:15: error: • Couldn't match type: forall s. ST s b1 diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr index bf199cb4c2..f47fd3b393 100644 --- a/testsuite/tests/typecheck/should_fail/T7734.stderr +++ b/testsuite/tests/typecheck/should_fail/T7734.stderr @@ -1,6 +1,9 @@ T7734.hs:4:13: error: • Couldn't match expected type ‘t’ with actual type ‘t -> t1’ + ‘t’ is a rigid type variable bound by + the inferred type of f :: (t -> t1) -> p -> t1 + at T7734.hs:4:1-13 • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘f’: x `f` y = x x @@ -10,6 +13,9 @@ T7734.hs:4:13: error: T7734.hs:5:13: error: • Couldn't match expected type ‘t’ with actual type ‘t -> t1’ + ‘t’ is a rigid type variable bound by + the inferred type of & :: (t -> t1) -> p -> t1 + at T7734.hs:5:1-13 • In the first argument of ‘x’, namely ‘x’ In the expression: x x In an equation for ‘&’: (&) x y = x x diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr index a75d0703c6..9ac0d63643 100644 --- a/testsuite/tests/typecheck/should_fail/T8450.stderr +++ b/testsuite/tests/typecheck/should_fail/T8450.stderr @@ -1,5 +1,5 @@ -T8450.hs:8:20: error: +T8450.hs:8:19: error: • Couldn't match type ‘a’ with ‘Bool’ Expected: Either Bool () Actual: Either a () diff --git a/testsuite/tests/typecheck/should_fail/T8570.stderr b/testsuite/tests/typecheck/should_fail/T8570.stderr index d79ea6581f..183001b577 100644 --- a/testsuite/tests/typecheck/should_fail/T8570.stderr +++ b/testsuite/tests/typecheck/should_fail/T8570.stderr @@ -1,10 +1,4 @@ -T8570.hs:6:11: error: - • Couldn't match expected type ‘Image’ with actual type ‘Field’ - • In the pattern: Image {filepath = x} - In a pattern binding: Image {filepath = x} = logo - In the expression: let Image {filepath = x} = logo in x - T8570.hs:6:18: error: • Constructor ‘Image’ does not have field ‘filepath’ • In the pattern: Image {filepath = x} diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index 4776253f52..e202ca2610 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -1,15 +1,29 @@ T8603.hs:33:17: error: - • Couldn't match type: RV a1 - with: StateT s RV a0 + • Couldn't match kind ‘*’ with ‘* -> *’ + When matching types + (->) [a1] :: * -> * + [a2] :: * Expected: [a2] -> StateT s RV a0 - Actual: t0 ((->) [a1]) (RV a1) + Actual: t0 ((->) [a1]) (StateT s RV a0) • The function ‘lift’ is applied to two value arguments, - but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’ + but its type ‘([a1] -> StateT s RV a0) + -> t0 ((->) [a1]) (StateT s RV a0)’ has only one In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3] In the expression: do prize <- lift uniform [1, 2, ....] return False + +T8603.hs:33:22: error: + • Couldn't match type: RV a1 + with: StateT s RV a0 + Expected: [a1] -> StateT s RV a0 + Actual: [a1] -> RV a1 + • In the first argument of ‘lift’, namely ‘uniform’ + In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3] + In the expression: + do prize <- lift uniform [1, 2, ....] + return False • Relevant bindings include testRVState1 :: RVState s Bool (bound at T8603.hs:32:1) diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr index f30c49bde6..6a4d4988de 100644 --- a/testsuite/tests/typecheck/should_fail/T9109.stderr +++ b/testsuite/tests/typecheck/should_fail/T9109.stderr @@ -1,13 +1,13 @@ T9109.hs:8:13: error: - • 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 + • Could not deduce: p ~ Bool + from the context: a ~ Bool + bound by a pattern with constructor: GBool :: G Bool, + in an equation for ‘foo’ + at T9109.hs:8:5-9 ‘p’ is a rigid type variable bound by - the inferred type of foo :: G a -> p at T9109.hs:8:1-16 + 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 diff --git a/testsuite/tests/typecheck/should_fail/T9497d.stderr b/testsuite/tests/typecheck/should_fail/T9497d.stderr index fff9e2e6a8..42da4bf430 100644 --- a/testsuite/tests/typecheck/should_fail/T9497d.stderr +++ b/testsuite/tests/typecheck/should_fail/T9497d.stderr @@ -2,8 +2,7 @@ T9497d.hs:2:8: error: • Found hole: _main :: IO () Or perhaps ‘_main’ is mis-spelled, or not in scope - • In the expression: _main - In an equation for ‘main’: main = _main + • In an equation for ‘main’: main = _main • Relevant bindings include main :: IO () (bound at T9497d.hs:2:1) Valid hole fits include main :: IO () (bound at T9497d.hs:2:1) diff --git a/testsuite/tests/typecheck/should_fail/T9858e.stderr b/testsuite/tests/typecheck/should_fail/T9858e.stderr index f397723a02..0ea9d4736a 100644 --- a/testsuite/tests/typecheck/should_fail/T9858e.stderr +++ b/testsuite/tests/typecheck/should_fail/T9858e.stderr @@ -1,5 +1,5 @@ -T9858e.hs:9:8: error: +T9858e.hs:9:7: error: • Couldn't match type: Eq Int => Int with: a0 b0 Expected: Proxy (a0 b0) diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 6b10777f12..bc325be674 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -580,3 +580,7 @@ test('T18357b', normal, compile_fail, ['']) test('T18455', normal, compile_fail, ['']) test('T18534', normal, compile_fail, ['']) test('T18714', normal, compile_fail, ['']) +test('too-many', normal, compile_fail, ['']) +test('T18640a', normal, compile_fail, ['']) +test('T18640b', normal, compile_fail, ['']) +test('T18640c', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/tcfail002.stderr b/testsuite/tests/typecheck/should_fail/tcfail002.stderr index 7de2d04c08..4e14032d62 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail002.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail002.stderr @@ -1,6 +1,9 @@ tcfail002.hs:4:7: error: • Couldn't match expected type ‘a’ with actual type ‘[a]’ + ‘a’ is a rigid type variable bound by + the inferred type of c :: [a] -> a + at tcfail002.hs:(3,1)-(4,7) • In the expression: z In an equation for ‘c’: c z = z • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/tcfail014.stderr b/testsuite/tests/typecheck/should_fail/tcfail014.stderr index 65b217ef1f..5525e01510 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail014.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail014.stderr @@ -1,6 +1,9 @@ tcfail014.hs:5:33: error: • Couldn't match expected type ‘t4’ with actual type ‘t4 -> t5’ + ‘t4’ is a rigid type variable bound by + the inferred type of h :: (t4 -> t5) -> t5 + at tcfail014.hs:5:25-33 • In the first argument of ‘z’, namely ‘z’ In the expression: z z In an equation for ‘h’: h z = z z diff --git a/testsuite/tests/typecheck/should_fail/tcfail032.stderr b/testsuite/tests/typecheck/should_fail/tcfail032.stderr index a09941d284..bb7eafc6fb 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail032.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail032.stderr @@ -1,11 +1,9 @@ tcfail032.hs:14:8: error: • 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: - forall a1. Eq a1 => a1 -> Int - at tcfail032.hs:14:13-30 + ‘p’ is a rigid type variable bound by + the inferred type of f :: Eq a => p -> a -> Int + at tcfail032.hs:14:1-31 • In the expression: x :: (Eq a) => a -> Int In an equation for ‘f’: f x = (x :: (Eq a) => a -> Int) • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/tcfail033.stderr b/testsuite/tests/typecheck/should_fail/tcfail033.stderr index a1c5e7d7d0..2b2089d8ec 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail033.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail033.stderr @@ -1,6 +1,9 @@ tcfail033.hs:4:12: error: • Couldn't match expected type ‘(a, b)’ with actual type ‘a’ + ‘a’ is a rigid type variable bound by + the inferred type of buglet :: [(a, b)] + at tcfail033.hs:4:1-32 • In the expression: x In the expression: [x | (x, y) <- buglet] In an equation for ‘buglet’: buglet = [x | (x, y) <- buglet] diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr index 8de86280e1..4e1ced2fc9 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr @@ -9,7 +9,7 @@ tcfail140.hs:10:7: error: tcfail140.hs:12:10: error: • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’ - • The operator ‘f’ takes two value arguments, + • The function ‘f’ is applied to two value arguments, but its type ‘Int -> Int’ has only one In the expression: 3 `f` 4 In an equation for ‘rot’: rot xs = 3 `f` 4 @@ -19,7 +19,7 @@ tcfail140.hs:12:10: error: tcfail140.hs:14:15: error: • Couldn't match expected type ‘a -> b’ with actual type ‘Int’ • The operator ‘f’ takes two value arguments, - but its type ‘Int -> Int’ has only one + but its type ‘Int -> Int’ has only one In the first argument of ‘map’, namely ‘(3 `f`)’ In the expression: map (3 `f`) xs • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/tcfail165.stderr b/testsuite/tests/typecheck/should_fail/tcfail165.stderr index b1f173f447..ecbec54fb5 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail165.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail165.stderr @@ -1,12 +1,17 @@ -tcfail165.hs:19:23: error: - • Couldn't match expected type: forall a. Show a => a -> String - with actual type: b0 -> String - • In the second argument of ‘putMVar’, namely - ‘(show :: forall b. Show b => b -> String)’ - In a stmt of a 'do' block: - putMVar var (show :: forall b. Show b => b -> String) +tcfail165.hs:18:17: error: + • Couldn't match type: forall a. Show a => a -> String + with: b0 -> String + Expected: IO (MVar (b0 -> String)) + Actual: IO (MVar (forall a. Show a => a -> String)) + • In a stmt of a 'do' block: + var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String)) In the expression: do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String)) putMVar var (show :: forall b. Show b => b -> String) + In an equation for ‘foo’: + foo + = do var <- newEmptyMVar :: + IO (MVar (forall a. Show a => a -> String)) + putMVar var (show :: forall b. Show b => b -> String) diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.hs b/testsuite/tests/typecheck/should_fail/tcfail174.hs index c3328ea4e7..226a9ee36e 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail174.hs +++ b/testsuite/tests/typecheck/should_fail/tcfail174.hs @@ -6,12 +6,16 @@ data Capture a = Base a | Capture (Capture (forall x . x -> a)) g :: Capture (forall a . a -> a) -g = Base id -- Fails; need a rigid signature on 'id' +g = Base id + -- Fails; need a rigid signature on 'id' -- Actually, succeeds now, with visible type application -- Disagree: should not succeed because it instantiates -- Base with a forall type + -- May 20: succeeds with Quick Look --- This function should definitely be rejected, with or without type signature + +-- h should definitely be rejected, +-- with (h2) or without (h1) type signature h1 = Capture g diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr index 5747a270ef..8ac8d3f9d5 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr @@ -1,29 +1,21 @@ -tcfail174.hs:9:5: error: - • Couldn't match type: a0 -> a0 - with: forall a. a -> a - Expected: Capture (forall a. a -> a) - Actual: Capture (a0 -> a0) - • In the expression: Base id - In an equation for ‘g’: g = Base id - -tcfail174.hs:16:14: error: +tcfail174.hs:20:14: error: • Couldn't match type ‘a1’ with ‘a’ Expected: Capture (forall x. x -> a) Actual: Capture (forall a. a -> a) ‘a1’ is a rigid type variable bound by the type a -> a - at tcfail174.hs:16:1-14 + at tcfail174.hs:20:1-14 ‘a’ is a rigid type variable bound by the inferred type of h1 :: Capture a - at tcfail174.hs:16:1-14 + at tcfail174.hs:20:1-14 • In the first argument of ‘Capture’, namely ‘g’ In the expression: Capture g In an equation for ‘h1’: h1 = Capture g • Relevant bindings include - h1 :: Capture a (bound at tcfail174.hs:16:1) + h1 :: Capture a (bound at tcfail174.hs:20:1) -tcfail174.hs:19:14: error: +tcfail174.hs:23:14: error: • Couldn't match type ‘a’ with ‘b’ Expected: Capture (forall x. x -> b) Actual: Capture (forall a. a -> a) @@ -33,9 +25,9 @@ tcfail174.hs:19:14: error: ‘b’ is a rigid type variable bound by the type signature for: h2 :: forall b. Capture b - at tcfail174.hs:18:1-15 + at tcfail174.hs:22:1-15 • In the first argument of ‘Capture’, namely ‘g’ In the expression: Capture g In an equation for ‘h2’: h2 = Capture g • Relevant bindings include - h2 :: Capture b (bound at tcfail174.hs:19:1) + h2 :: Capture b (bound at tcfail174.hs:23:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail204.stderr b/testsuite/tests/typecheck/should_fail/tcfail204.stderr index 8083ffce60..a1ab99c445 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail204.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail204.stderr @@ -2,7 +2,7 @@ tcfail204.hs:10:7: error: [-Wtype-defaults (in -Wall), -Werror=type-defaults] • Defaulting the following constraints to type ‘Double’ (RealFrac a0) - arising from a use of ‘ceiling’ at tcfail204.hs:10:7-17 + arising from a use of ‘ceiling’ at tcfail204.hs:10:7-13 (Fractional a0) arising from the literal ‘6.3’ at tcfail204.hs:10:15-17 • In the expression: ceiling 6.3 diff --git a/testsuite/tests/typecheck/should_fail/tcfail218.stderr b/testsuite/tests/typecheck/should_fail/tcfail218.stderr index efb6c4c9d3..f591b09b2a 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail218.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail218.stderr @@ -1,11 +1,11 @@ -tcfail218.hs:16:5: - Overlapping instances for C [a] Bool arising from a use of ‘foo’ - Matching instances: - instance C [a] b -- Defined at tcfail218.hs:8:29 - instance C [Int] Bool -- Defined at tcfail218.hs:7:29 - (The choice depends on the instantiation of ‘a’ - To pick the first instance above, use IncoherentInstances - when compiling the other instance declarations) - In the expression: foo - In an equation for ‘x’: x = foo +tcfail218.hs:16:5: error: + • Overlapping instances for C [a] Bool arising from a use of ‘foo’ + Matching instances: + instance C [a] b -- Defined at tcfail218.hs:8:29 + instance C [Int] Bool -- Defined at tcfail218.hs:7:29 + (The choice depends on the instantiation of ‘a’ + To pick the first instance above, use IncoherentInstances + when compiling the other instance declarations) + • In the expression: foo + In an equation for ‘x’: x = foo diff --git a/testsuite/tests/typecheck/should_fail/too-many.hs b/testsuite/tests/typecheck/should_fail/too-many.hs new file mode 100644 index 0000000000..e3a4e2ba04 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/too-many.hs @@ -0,0 +1,18 @@ +module TooMany where + +foo :: (Int -> Int -> Bool) -> Int +foo = error "urk" + +f1 :: Int -> Int -> Int -> Bool +f1 = f1 + +g1 = foo (f1 2 3) + -- Here is is sensible to report + -- f1 is applied to too many arguments + +f2 :: Int -> Bool +f2 = f2 + +g2 = foo (f2 2) + -- Here is is /not/ sensible to report + -- f2 is applied to too many arguments diff --git a/testsuite/tests/typecheck/should_fail/too-many.stderr b/testsuite/tests/typecheck/should_fail/too-many.stderr new file mode 100644 index 0000000000..01e50050ff --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/too-many.stderr @@ -0,0 +1,16 @@ + +too-many.hs:9:11: error: + • Couldn't match type ‘Bool’ with ‘Int -> Bool’ + Expected: Int -> Int -> Bool + Actual: Int -> Bool + • Possible cause: ‘f1’ is applied to too many arguments + In the first argument of ‘foo’, namely ‘(f1 2 3)’ + In the expression: foo (f1 2 3) + In an equation for ‘g1’: g1 = foo (f1 2 3) + +too-many.hs:16:11: error: + • Couldn't match expected type ‘Int -> Int -> Bool’ + with actual type ‘Bool’ + • In the first argument of ‘foo’, namely ‘(f2 2)’ + In the expression: foo (f2 2) + In an equation for ‘g2’: g2 = foo (f2 2) diff --git a/testsuite/tests/typecheck/should_run/T9497a-run.stderr b/testsuite/tests/typecheck/should_run/T9497a-run.stderr index 6461d98b10..7f05844778 100644 --- a/testsuite/tests/typecheck/should_run/T9497a-run.stderr +++ b/testsuite/tests/typecheck/should_run/T9497a-run.stderr @@ -1,8 +1,7 @@ T9497a-run: T9497a-run.hs:2:8: error: • Found hole: _main :: IO () Or perhaps ‘_main’ is mis-spelled, or not in scope - • In the expression: _main - In an equation for ‘main’: main = _main + • In an equation for ‘main’: main = _main • Relevant bindings include main :: IO () (bound at T9497a-run.hs:2:1) Valid hole fits include diff --git a/testsuite/tests/typecheck/should_run/T9497b-run.stderr b/testsuite/tests/typecheck/should_run/T9497b-run.stderr index a73b71981c..e6155ddae5 100644 --- a/testsuite/tests/typecheck/should_run/T9497b-run.stderr +++ b/testsuite/tests/typecheck/should_run/T9497b-run.stderr @@ -1,8 +1,7 @@ T9497b-run: T9497b-run.hs:2:8: error: • Found hole: _main :: IO () Or perhaps ‘_main’ is mis-spelled, or not in scope - • In the expression: _main - In an equation for ‘main’: main = _main + • In an equation for ‘main’: main = _main • Relevant bindings include main :: IO () (bound at T9497b-run.hs:2:1) Valid hole fits include diff --git a/testsuite/tests/typecheck/should_run/T9497c-run.stderr b/testsuite/tests/typecheck/should_run/T9497c-run.stderr index 8666900b4e..6ce2781031 100644 --- a/testsuite/tests/typecheck/should_run/T9497c-run.stderr +++ b/testsuite/tests/typecheck/should_run/T9497c-run.stderr @@ -1,8 +1,7 @@ T9497c-run: T9497c-run.hs:2:8: error: • Found hole: _main :: IO () Or perhaps ‘_main’ is mis-spelled, or not in scope - • In the expression: _main - In an equation for ‘main’: main = _main + • In an equation for ‘main’: main = _main • Relevant bindings include main :: IO () (bound at T9497c-run.hs:2:1) Valid hole fits include diff --git a/testsuite/tests/typecheck/should_run/tcrun042.hs b/testsuite/tests/typecheck/should_run/tcrun042.hs index 30c67601ed..82add262b1 100644 --- a/testsuite/tests/typecheck/should_run/tcrun042.hs +++ b/testsuite/tests/typecheck/should_run/tcrun042.hs @@ -22,4 +22,5 @@ e = (,"Hello" ++ "World",) dropFunction :: (a, String, forall c. c -> c -> c) -> (a, String, Int) dropFunction (x, y, z) = (x, y, z 10 20) -main = print (dropFunction $ e "Meh" (flip const), dropFunction $ e 10 const) +main = print ( dropFunction (e "Meh" (flip const)) + , dropFunction (e 10 const)) diff --git a/testsuite/tests/warnings/should_compile/PluralS.stderr b/testsuite/tests/warnings/should_compile/PluralS.stderr index 42c81daf5f..53ed5c4633 100644 --- a/testsuite/tests/warnings/should_compile/PluralS.stderr +++ b/testsuite/tests/warnings/should_compile/PluralS.stderr @@ -8,7 +8,7 @@ PluralS.hs:15:17: warning: [-Wtype-defaults (in -Wall)] PluralS.hs:17:24: warning: [-Wtype-defaults (in -Wall)] • Defaulting the following constraints to type ‘Integer’ - (Show a0) arising from a use of ‘show’ at PluralS.hs:17:24-31 + (Show a0) arising from a use of ‘show’ at PluralS.hs:17:24-27 (Num a0) arising from the literal ‘123’ at PluralS.hs:17:29-31 • In the expression: show 123 In an equation for ‘defaultingNumAndShow’: |