diff options
62 files changed, 621 insertions, 415 deletions
diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs index bb3c46ba47..5b74487c5d 100644 --- a/compiler/deSugar/DsMeta.hs +++ b/compiler/deSugar/DsMeta.hs @@ -204,7 +204,7 @@ get_scoped_tvs (L _ signature) -- Both implicit and explicit quantified variables -- We need the implicit ones for f :: forall (a::k). blah -- here 'k' scopes too - | HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_vars } + | HsIB { hsib_ext = implicit_vars , hsib_body = hs_ty } <- sig , (explicit_vars, _) <- splitLHsForAllTy hs_ty = implicit_vars ++ map hsLTyVarName explicit_vars @@ -544,7 +544,7 @@ repTyFamInstD decl@(TyFamInstDecl { tfid_eqn = eqn }) ; repTySynInst tc eqn1 } repTyFamEqn :: TyFamInstEqn GhcRn -> DsM (Core TH.TySynEqnQ) -repTyFamEqn (HsIB { hsib_ext = HsIBRn { hsib_vars = var_names } +repTyFamEqn (HsIB { hsib_ext = var_names , hsib_body = FamEqn { feqn_pats = tys , feqn_rhs = rhs }}) = do { let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn @@ -561,7 +561,7 @@ repTyFamEqn (HsIB _ (XFamEqn _)) = panic "repTyFamEqn" repDataFamInstD :: DataFamInstDecl GhcRn -> DsM (Core TH.DecQ) repDataFamInstD (DataFamInstDecl { dfid_eqn = - (HsIB { hsib_ext = HsIBRn { hsib_vars = var_names } + (HsIB { hsib_ext = var_names , hsib_body = FamEqn { feqn_tycon = tc_name , feqn_pats = tys , feqn_rhs = defn }})}) @@ -651,7 +651,7 @@ repRuleD (L _ (XRuleDecl _)) = panic "repRuleD" ruleBndrNames :: LRuleBndr GhcRn -> [Name] ruleBndrNames (L _ (RuleBndr _ n)) = [unLoc n] ruleBndrNames (L _ (RuleBndrSig _ n sig)) - | HsWC { hswc_body = HsIB { hsib_ext = HsIBRn { hsib_vars = vars } }} <- sig + | HsWC { hswc_body = HsIB { hsib_ext = vars }} <- sig = unLoc n : vars ruleBndrNames (L _ (RuleBndrSig _ _ (HsWC _ (XHsImplicitBndrs _)))) = panic "ruleBndrNames" @@ -1042,7 +1042,7 @@ repContext ctxt = do preds <- repList typeQTyConName repLTy ctxt repCtxt preds repHsSigType :: LHsSigType GhcRn -> DsM (Core TH.TypeQ) -repHsSigType (HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_tvs } +repHsSigType (HsIB { hsib_ext = implicit_tvs , hsib_body = body }) | (explicit_tvs, ctxt, ty) <- splitLHsSigmaTy body = addSimpleTyVarBinds implicit_tvs $ diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs index 8c5387ddb2..3939f57adb 100644 --- a/compiler/hsSyn/HsTypes.hs +++ b/compiler/hsSyn/HsTypes.hs @@ -20,7 +20,7 @@ module HsTypes ( HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind, HsTyVarBndr(..), LHsTyVarBndr, LHsQTyVars(..), HsQTvsRn(..), - HsImplicitBndrs(..), HsIBRn(..), + HsImplicitBndrs(..), HsWildCardBndrs(..), LHsSigType, LHsSigWcType, LHsWcType, HsTupleSort(..), @@ -332,23 +332,18 @@ isEmptyLHsQTvs _ = False -- | Haskell Implicit Binders data HsImplicitBndrs pass thing -- See Note [HsType binders] - = HsIB { hsib_ext :: XHsIB pass thing + = HsIB { hsib_ext :: XHsIB pass thing -- after renamer: [Name] + -- Implicitly-bound kind & type vars + -- Order is important; see + -- Note [Ordering of implicit variables] + , hsib_body :: thing -- Main payload (type or list of types) } | XHsImplicitBndrs (XXHsImplicitBndrs pass thing) -data HsIBRn - = HsIBRn { hsib_vars :: [Name] -- Implicitly-bound kind & type vars - -- Order is important; see - -- Note [Ordering of implicit variables] - , hsib_closed :: Bool -- Taking the hsib_vars into account, - -- is the payload closed? Used in - -- TcHsType.decideKindGeneralisationPlan - } deriving Data - type instance XHsIB GhcPs _ = NoExt -type instance XHsIB GhcRn _ = HsIBRn -type instance XHsIB GhcTc _ = HsIBRn +type instance XHsIB GhcRn _ = [Name] +type instance XHsIB GhcTc _ = [Name] type instance XXHsImplicitBndrs (GhcPass _) _ = NoExt @@ -429,9 +424,7 @@ mkHsWildCardBndrs x = HsWC { hswc_body = x -- Add empty binders. This is a bit suspicious; what if -- the wrapped thing had free type variables? mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs GhcRn thing -mkEmptyImplicitBndrs x = HsIB { hsib_ext = HsIBRn - { hsib_vars = [] - , hsib_closed = False } +mkEmptyImplicitBndrs x = HsIB { hsib_ext = [] , hsib_body = x } mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs GhcRn thing @@ -928,7 +921,7 @@ hsWcScopedTvs :: LHsSigWcType GhcRn -> [Name] -- because they scope in the same way hsWcScopedTvs sig_ty | HsWC { hswc_ext = nwcs, hswc_body = sig_ty1 } <- sig_ty - , HsIB { hsib_ext = HsIBRn { hsib_vars = vars} + , HsIB { hsib_ext = vars , hsib_body = sig_ty2 } <- sig_ty1 = case sig_ty2 of L _ (HsForAllTy { hst_bndrs = tvs }) -> vars ++ nwcs ++ @@ -942,7 +935,7 @@ hsWcScopedTvs (XHsWildCardBndrs _) = panic "hsWcScopedTvs" hsScopedTvs :: LHsSigType GhcRn -> [Name] -- Same as hsWcScopedTvs, but for a LHsSigType hsScopedTvs sig_ty - | HsIB { hsib_ext = HsIBRn { hsib_vars = vars } + | HsIB { hsib_ext = vars , hsib_body = sig_ty2 } <- sig_ty , L _ (HsForAllTy { hst_bndrs = tvs }) <- sig_ty2 = vars ++ map hsLTyVarName tvs @@ -1132,7 +1125,7 @@ splitLHsQualTy body = (noLoc [], body) splitLHsInstDeclTy :: LHsSigType GhcRn -> ([Name], LHsContext GhcRn, LHsType GhcRn) -- Split up an instance decl type, returning the pieces -splitLHsInstDeclTy (HsIB { hsib_ext = HsIBRn { hsib_vars = itkvs } +splitLHsInstDeclTy (HsIB { hsib_ext = itkvs , hsib_body = inst_ty }) | (tvs, cxt, body_ty) <- splitLHsSigmaTy inst_ty = (itkvs ++ map hsLTyVarName tvs, cxt, body_ty) diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index 33e7c7d2b6..beb7c5b705 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -765,8 +765,7 @@ rnFamInstEqn doc mb_cls rhs_kvars all_fvs = fvs `addOneFV` unLoc tycon' -- type instance => use, hence addOneFV - ; return (HsIB { hsib_ext = HsIBRn { hsib_vars = all_ibs - , hsib_closed = True } + ; return (HsIB { hsib_ext = all_ibs , hsib_body = FamEqn { feqn_ext = noExt , feqn_tycon = tycon' @@ -1691,7 +1690,7 @@ rnLDerivStrategy doc mds thing_inside NewtypeStrategy -> boring_case (L loc NewtypeStrategy) ViaStrategy via_ty -> do (via_ty', fvs1) <- rnHsSigType doc via_ty - let HsIB { hsib_ext = HsIBRn { hsib_vars = via_imp_tvs } + let HsIB { hsib_ext = via_imp_tvs , hsib_body = via_body } = via_ty' (via_exp_tv_bndrs, _, _) = splitLHsSigmaTy via_body via_exp_tvs = map hsLTyVarName via_exp_tv_bndrs diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index a9e02dc5a5..e5f51660da 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -127,7 +127,8 @@ rn_hs_sig_wc_type always_bind_free_tvs ctxt ; rnImplicitBndrs bind_free_tvs tv_rdrs $ \ vars -> do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = ib_ty' } - ib_ty' = mk_implicit_bndrs vars hs_ty' fvs1 + ib_ty' = HsIB { hsib_ext = vars + , hsib_body = hs_ty' } ; (res, fvs2) <- thing_inside sig_ty' ; return (res, fvs1 `plusFV` fvs2) } } rn_hs_sig_wc_type _ _ (HsWC _ (XHsImplicitBndrs _)) _ @@ -300,7 +301,9 @@ rnHsSigType ctx (HsIB { hsib_body = hs_ty }) ; vars <- extractFilteredRdrTyVarsDups hs_ty ; rnImplicitBndrs (not (isLHsForAllTy hs_ty)) vars $ \ vars -> do { (body', fvs) <- rnLHsType ctx hs_ty - ; return ( mk_implicit_bndrs vars body' fvs, fvs ) } } + ; return ( HsIB { hsib_ext = vars + , hsib_body = body' } + , fvs ) } } rnHsSigType _ (XHsImplicitBndrs _) = panic "rnHsSigType" rnImplicitBndrs :: Bool -- True <=> bring into scope any free type variables @@ -367,18 +370,6 @@ rnLHsInstType :: SDoc -> LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars) -- Do not try to decompose the inst_ty in case it is malformed rnLHsInstType doc inst_ty = rnHsSigType (GenericCtx doc) inst_ty -mk_implicit_bndrs :: [Name] -- implicitly bound - -> a -- payload - -> FreeVars -- FreeVars of payload - -> HsImplicitBndrs GhcRn a -mk_implicit_bndrs vars body fvs - = HsIB { hsib_ext = HsIBRn - { hsib_vars = vars - , hsib_closed = nameSetAll (not . isTyVarName) (vars `delFVs` fvs) } - , hsib_body = body } - - - {- ****************************************************** * * LHsType and HsType diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 37bfa18192..6f749fc60f 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -713,17 +713,14 @@ tcStandaloneDerivInstType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM ([TyVar], DerivContext, Class, [Type]) tcStandaloneDerivInstType ctxt - (HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = HsIBRn - { hsib_vars = vars - , hsib_closed = closed } + (HsWC { hswc_body = deriv_ty@(HsIB { hsib_ext = vars , hsib_body = deriv_ty_body })}) | (tvs, theta, rho) <- splitLHsSigmaTy deriv_ty_body , L _ [wc_pred] <- theta , L _ (HsWildCardTy (AnonWildCard (L wc_span _))) <- ignoreParens wc_pred = do (deriv_tvs, _deriv_theta, deriv_cls, deriv_inst_tys) <- tcHsClsInstType ctxt $ - HsIB { hsib_ext = HsIBRn { hsib_vars = vars - , hsib_closed = closed } + HsIB { hsib_ext = vars , hsib_body = L (getLoc deriv_ty_body) $ HsForAllTy { hst_bndrs = tvs diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs index a5a900410f..8f4e1076ca 100644 --- a/compiler/typecheck/TcEnv.hs +++ b/compiler/typecheck/TcEnv.hs @@ -614,8 +614,10 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things tvs _other -> tvs `unionVarSet` id_tvs where - id_tvs = tyCoVarsOfType (idType id) - is_closed_type = not (anyVarSet isTyVar id_tvs) + id_ty = idType id + id_tvs = tyCoVarsOfType id_ty + id_co_tvs = closeOverKinds (coVarsOfType id_ty) + is_closed_type = not (anyVarSet isTyVar (id_tvs `minusVarSet` id_co_tvs)) -- We only care about being closed wrt /type/ variables -- E.g. a top-level binding might have a type like -- foo :: t |> co diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index efdda06fe3..4188303860 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -38,6 +38,7 @@ module TcHsType ( tcHsLiftedTypeNC, tcHsOpenTypeNC, tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType, tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps, + failIfEmitsConstraints, solveEqualities, -- useful re-export typeLevelMode, kindLevelMode, @@ -69,6 +70,7 @@ import TcUnify import TcIface import TcSimplify import TcHsSyn +import TcErrors ( reportAllUnsolved ) import TcType import Inst ( tcInstTyBinders, tcInstTyBinder ) import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig @@ -178,7 +180,7 @@ tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty) kcHsSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM () kcHsSigType skol_info names (HsIB { hsib_body = hs_ty - , hsib_ext = HsIBRn { hsib_vars = sig_vars }}) + , hsib_ext = sig_vars }) = addSigCtxt (funsSigCtxt names) hs_ty $ discardResult $ tcImplicitTKBndrs skol_info sig_vars $ @@ -205,10 +207,7 @@ tcHsSigType ctxt sig_ty -- of kind * in a Template Haskell quote eg [t| Maybe |] -- Generalise here: see Note [Kind generalisation] - ; do_kind_gen <- decideKindGeneralisationPlan sig_ty - ; ty <- if do_kind_gen - then tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType - else tc_hs_sig_type skol_info sig_ty kind + ; ty <- tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType ; checkValidType ctxt ty ; traceTc "end tcHsSigType }" (ppr ty) @@ -222,38 +221,23 @@ tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type -- and then kind-generalizes. -- This will never emit constraints, as it uses solveEqualities interally. -- No validity checking or zonking -tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext - = HsIBRn { hsib_vars = sig_vars } +tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext = sig_vars , hsib_body = hs_ty }) kind - = do { (tkvs, ty) <- solveEqualities $ - tcImplicitTKBndrs skol_info sig_vars $ - tc_lhs_type typeLevelMode hs_ty kind - -- NB the call to solveEqualities, which unifies all those - -- kind variables floating about, immediately prior to - -- kind generalisation - - ; ty1 <- zonkPromoteType $ mkSpecForAllTys tkvs ty - ; kvs <- kindGeneralize ty1 + = do { ((tkvs, ty), wanted) <- captureConstraints $ + tcImplicitTKBndrs skol_info sig_vars $ + tc_lhs_type typeLevelMode hs_ty kind + -- Any remaining variables (unsolved in the solveLocalEqualities in the + -- tcImplicitTKBndrs) + -- should be in the global tyvars, and therefore won't be quantified + -- over. + + ; let ty1 = mkSpecForAllTys tkvs ty + ; kvs <- kindGeneralizeLocal wanted ty1 + ; emitConstraints wanted -- we still need to solve these ; return (mkInvForAllTys kvs ty1) } tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen" -tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type --- Kind-check/desugar a 'LHsSigType', but does not solve --- the equalities that arise from doing so; instead it may --- emit kind-equality constraints into the monad --- Zonking, but no validity checking -tc_hs_sig_type skol_info (HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars } - , hsib_body = hs_ty }) kind - = do { (tkvs, ty) <- tcImplicitTKBndrs skol_info sig_vars $ - tc_lhs_type typeLevelMode hs_ty kind - - -- need to promote any remaining metavariables; test case: - -- dependent/should_fail/T14066e. - ; zonkPromoteType (mkSpecForAllTys tkvs ty) } - -tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type" - ----------------- tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind])) -- Like tcHsSigType, but for the ...deriving( C t1 ty2 ) clause @@ -330,7 +314,14 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt -- Like tcHsSigType, but for a class instance declaration tcHsClsInstType user_ctxt hs_inst_ty = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $ - do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind + {- We want to fail here if the tc_hs_sig_type_and_gen emits constraints. + First off, we know we'll never solve the constraints, as classes are + always at top level, and their constraints do not inform the kind checking + of method types. So failing isn't wrong. Yet, the reason we do it is + to avoid the validity checker from seeing unsolved coercion holes in + types. Much better just to report the kind error directly. -} + do { inst_ty <- failIfEmitsConstraints $ + tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind ; inst_ty <- zonkTcTypeToType emptyZonkEnv inst_ty ; checkValidInstance user_ctxt hs_inst_ty inst_ty } @@ -345,6 +336,12 @@ tcHsTypeApp wc_ty kind -- signature so we want to solve its equalities right now tcWildCardBinders sig_wcs $ \ _ -> tcCheckLHsType hs_ty kind + -- We must promote here. Ex: + -- f :: forall a. a + -- g = f @(forall b. Proxy b -> ()) @Int ... + -- After when processing the @Int, we'll have to check its kind + -- against the as-yet-unknown kind of b. This check causes an assertion + -- failure if we don't promote. ; ty <- zonkPromoteType ty ; checkValidType TypeAppCtxt ty ; return ty } @@ -392,50 +389,7 @@ tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty) where mode = allowUnsaturated typeLevelMode ---------------------------- --- | Should we generalise the kind of this type signature? --- We *should* generalise if the type is closed --- or if NoMonoLocalBinds is set. Otherwise, nope. --- See Note [Kind generalisation plan] -decideKindGeneralisationPlan :: LHsSigType GhcRn -> TcM Bool -decideKindGeneralisationPlan sig_ty@(HsIB { hsib_ext - = HsIBRn { hsib_closed = closed } }) - = do { mono_locals <- xoptM LangExt.MonoLocalBinds - ; let should_gen = not mono_locals || closed - ; traceTc "decideKindGeneralisationPlan" - (ppr sig_ty $$ text "should gen?" <+> ppr should_gen) - ; return should_gen } -decideKindGeneralisationPlan(XHsImplicitBndrs _) - = panic "decideKindGeneralisationPlan" - -{- Note [Kind generalisation plan] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When should we do kind-generalisation for user-written type signature? -Answer: we use the same rule as for value bindings: - - * We always kind-generalise if the type signature is closed - * Additionally, we attempt to generalise if we have NoMonoLocalBinds - -Trac #13337 shows the problem if we kind-generalise an open type (i.e. -one that mentions in-scope type variable - foo :: forall k (a :: k) proxy. (Typeable k, Typeable a) - => proxy a -> String - foo _ = case eqT :: Maybe (k :~: Type) of - Nothing -> ... - Just Refl -> case eqT :: Maybe (a :~: Int) of ... - -In the expression type sig on the last line, we have (a :: k) -but (Int :: Type). Since (:~:) is kind-homogeneous, this requires -k ~ *, which is true in the Refl branch of the outer case. - -That equality will be solved if we allow it to float out to the -implication constraint for the Refl match, but not not if we aggressively -attempt to solve all equalities the moment they occur; that is, when -checking (Maybe (a :~: Int)). (NB: solveEqualities fails unless it -solves all the kind equalities, which is the right thing at top level.) - -So here the right thing is simply not to do kind generalisation! - +{- ************************************************************************ * * Type-checking modes @@ -1495,9 +1449,10 @@ Checking a user-written signature requires several steps: 1. Generate constraints. 2. Solve constraints. - 3. Zonk and promote tyvars. - 4. (Optional) Kind-generalize. - 5. Check validity. + 3. Zonk. + 4. Promote tyvars and/or kind-generalize. + 5. Zonk. + 6. Check validity. There may be some surprises in here: @@ -1507,12 +1462,34 @@ to get these in the right order (see Note [Keeping scoped variables in order: Implicit]). Additionally, solving is necessary in order to kind-generalize correctly. -Step 3 requires *promoting* type variables. If there are any foralls -in a type, the TcLevel will be bumped within the forall. This might -lead to the generation of matavars with a high level. If we don't promote, -we violate MetaTvInv of Note [TcLevel and untouchable type variables] +In Step 4, 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 every being visible +in the surrounding context, we must obey the following dictum: + + Every metavariable in a type must either be + (A) promoted, or + (B) generalized. + +If a variable is generalized, then it becomes a skolem and no longer +has a proper TcLevel. (I'm ignoring the TcLevel on a skolem here, as +it's not really in play here.) On the other hand, if it is not +generalized (because we're not generalizing the construct -- e.g., pattern +sig -- or because the metavars are constrained -- see kindGeneralizeLocal) +we need to promote to (MetaTvInv) of Note [TcLevel and untouchable type variables] in TcType. +After promoting/generalizing, we need to zonk *again* because both +promoting and generalizing fill in metavariables. + +To avoid the double-zonk, we do two things: + 1. zonkPromoteType and friends zonk and promote at the same time. + Accordingly, the function does setps 3-5 all at once, preventing + the need for multiple traversals. + + 2. kindGeneralize does not require a zonked type -- it zonks as it + gathers free variables. So this way effectively sidesteps step 3. + -} tcWildCardBinders :: [Name] @@ -1921,14 +1898,36 @@ kindGeneralize :: TcType -> TcM [KindVar] -- Quantify the free kind variables of a kind or type -- In the latter case the type is closed, so it has no free -- type variables. So in both cases, all the free vars are kind vars --- Input must be zonked. +-- Input needn't be zonked. -- NB: You must call solveEqualities or solveLocalEqualities before -- kind generalization -kindGeneralize kind_or_type - = do { let kvs = tyCoVarsOfTypeDSet kind_or_type - dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet } +kindGeneralize = kindGeneralizeLocal emptyWC + +-- | This variant of 'kindGeneralize' refuses to generalize over any +-- variables free in the given WantedConstraints. Instead, it promotes +-- these variables into an outer TcLevel. See also +-- Note [Promoting unification variables] in TcSimplify +kindGeneralizeLocal :: WantedConstraints -> TcType -> TcM [KindVar] +kindGeneralizeLocal wanted kind_or_type + = do { + -- This bit is very much like decideMonoTyVars in TcSimplify, + -- 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) + ; (_, constrained) <- promoteTyVarSet constrained + + -- NB: zonk here, after promotion + ; kvs <- zonkTcTypeAndFV kind_or_type + ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet } + ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked - ; quantifyTyVars gbl_tvs dvs } + ; traceTc "kindGeneralizeLocal" (vcat [ ppr wanted + , ppr kind_or_type + , ppr constrained + , ppr dvs ]) + + ; quantifyTyVars (gbl_tvs `unionVarSet` constrained) dvs } {- Note [Kind generalisation] @@ -2268,7 +2267,7 @@ tcHsPartialSigType -- See Note [Recipe for checking a signature] tcHsPartialSigType ctxt sig_ty | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty - , HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs } + , HsIB { hsib_ext = implicit_hs_tvs , hsib_body = hs_ty } <- ib_ty , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty = addSigCtxt ctxt hs_ty $ @@ -2392,7 +2391,7 @@ tcHsPatSigType :: UserTypeCtxt -- See Note [Recipe for checking a signature] tcHsPatSigType ctxt sig_ty | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty - , HsIB { hsib_ext = HsIBRn { hsib_vars = sig_vars} + , HsIB { hsib_ext = sig_vars , hsib_body = hs_ty } <- ib_ty = addSigCtxt ctxt hs_ty $ do { sig_tkvs <- mapM new_implicit_tv sig_vars @@ -2406,6 +2405,9 @@ tcHsPatSigType ctxt sig_ty -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty -- contains a forall). Promote these. + -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ... + -- When we instantiate x, we have to compare the kind of the argument + -- to a's kind, which will be a metavariable. ; sig_ty <- zonkPromoteType sig_ty ; checkValidType ctxt sig_ty @@ -2582,7 +2584,7 @@ unifyKinds rn_tys act_kinds -- to make sure that any free meta-tyvars in the type are promoted to the -- current TcLevel. (They might be at a higher level due to the level-bumping -- in tcExplicitTKBndrs, for example.) This function both zonks *and* --- promotes. +-- promotes. Why at the same time? See Note [Recipe for checking a signature] zonkPromoteType :: TcType -> TcM TcType zonkPromoteType = mapType zonkPromoteMapper () @@ -2618,10 +2620,8 @@ zonkPromoteTcTyVar tv = do { let ref = metaTyVarRef tv ; contents <- readTcRef ref ; case contents of - Flexi -> do { promoted <- promoteTyVar tv - ; if promoted - then zonkPromoteTcTyVar tv -- read it again - else mkTyVarTy <$> zonkPromoteTyCoVarKind tv } + Flexi -> do { (_, promoted_tv) <- promoteTyVar tv + ; mkTyVarTy <$> zonkPromoteTyCoVarKind promoted_tv } Indirect ty -> zonkPromoteType ty } | isTcTyVar tv && isSkolemTyVar tv -- NB: isSkolemTyVar says "True" to pure TyVars @@ -2667,6 +2667,7 @@ tcLHsKindSig ctxt hs_kind = do { kind <- solveLocalEqualities $ tc_lhs_kind kindLevelMode hs_kind ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind) + -- No generalization, so we must promote ; kind <- zonkPromoteType kind -- This zonk is very important in the case of higher rank kinds -- E.g. Trac #13879 f :: forall (p :: forall z (y::z). <blah>). @@ -2762,3 +2763,14 @@ reportFloatingKvs tycon_name flav all_tvs bad_tvs ppr_tv_bndrs tvs = sep (map pp_tv tvs) pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv)) + +-- | If the inner action emits constraints, reports them as errors and fails; +-- 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 + = do { (res, lie) <- captureConstraints thing_inside + ; reportAllUnsolved lie + ; return res + } diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index 9a94365233..cd6aec729b 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -588,9 +588,8 @@ tcDataFamInstDecl :: Maybe ClsInstInfo -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo) -- "newtype instance" and "data instance" tcDataFamInstDecl mb_clsinfo - (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext - = HsIBRn { hsib_vars = tv_names } - , hsib_body = + (L loc decl@(DataFamInstDecl { dfid_eqn = HsIB { hsib_ext = tv_names + , hsib_body = FamEqn { feqn_pats = pats , feqn_tycon = fam_tc_name , feqn_fixity = fixity diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 58138eb631..80929d12d4 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -1307,6 +1307,8 @@ a \/\a in the final result but all the occurrences of a will be zonked to () -- variables free in anything (term-level or type-level) in scope. We thus -- don't have to worry about clashes with things that are not in scope, because -- if they are reachable, then they'll be returned here. +-- NB: This is closed over kinds, so it can return unification variables mentioned +-- in the kinds of in-scope tyvars. tcGetGlobalTyCoVars :: TcM TcTyVarSet tcGetGlobalTyCoVars = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index c8e168dea7..4449d67c29 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -391,14 +391,14 @@ tcRnSrcDecls :: Bool -- False => no 'module M(..) where' header at all -> TcM TcGblEnv tcRnSrcDecls explicit_mod_hdr decls = do { -- Do all the declarations - ; ((tcg_env, tcl_env), lie) <- captureTopConstraints $ - do { (tcg_env, tcl_env) <- tc_rn_src_decls decls + ; (tcg_env, tcl_env, lie) <- tc_rn_src_decls decls - -- Check for the 'main' declaration - -- Must do this inside the captureTopConstraints - ; tcg_env <- setEnvs (tcg_env, tcl_env) $ - checkMain explicit_mod_hdr - ; return (tcg_env, tcl_env) } + -- Check for the 'main' declaration + -- Must do this inside the captureTopConstraints + ; (tcg_env, lie_main) <- setEnvs (tcg_env, tcl_env) $ + -- always set envs *before* captureTopConstraints + captureTopConstraints $ + checkMain explicit_mod_hdr ; setEnvs (tcg_env, tcl_env) $ do { @@ -412,7 +412,7 @@ tcRnSrcDecls explicit_mod_hdr decls -- * the local env exposes the local Ids to simplifyTop, -- so that we get better error messages (monomorphism restriction) ; new_ev_binds <- {-# SCC "simplifyTop" #-} - simplifyTop lie + simplifyTop (lie `andWC` lie_main) -- Emit Typeable bindings ; tcg_env <- mkTypeableBinds @@ -470,16 +470,17 @@ run_th_modfinalizers = do then getEnvs else do writeTcRef th_modfinalizers_var [] - (envs, lie) <- captureTopConstraints $ do - sequence_ th_modfinalizers - -- Finalizers can add top-level declarations with addTopDecls. - tc_rn_src_decls [] - setEnvs envs $ do + (_, lie_th) <- captureTopConstraints $ + sequence_ th_modfinalizers + -- Finalizers can add top-level declarations with addTopDecls, so + -- we have to run tc_rn_src_decls to get them + (tcg_env, tcl_env, lie_top_decls) <- tc_rn_src_decls [] + setEnvs (tcg_env, tcl_env) $ do -- Subsequent rounds of finalizers run after any new constraints are -- simplified, or some types might not be complete when using reify -- (see #12777). new_ev_binds <- {-# SCC "simplifyTop2" #-} - simplifyTop lie + simplifyTop (lie_th `andWC` lie_top_decls) updGblEnv (\tcg_env -> tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds } ) @@ -487,9 +488,10 @@ run_th_modfinalizers = do run_th_modfinalizers tc_rn_src_decls :: [LHsDecl GhcPs] - -> TcM (TcGblEnv, TcLclEnv) + -> TcM (TcGblEnv, TcLclEnv, WantedConstraints) -- Loops around dealing with each top level inter-splice group -- in turn, until it's dealt with the entire module +-- Never emits constraints; calls captureTopConstraints internally tc_rn_src_decls ds = {-# SCC "tc_rn_src_decls" #-} do { (first_group, group_tail) <- findSplice ds @@ -534,13 +536,17 @@ tc_rn_src_decls ds } -- Type check all declarations - ; (tcg_env, tcl_env) <- setGblEnv tcg_env $ - tcTopSrcDecls rn_decls + -- NB: set the env **before** captureTopConstraints so that error messages + -- get reported w.r.t. the right GlobalRdrEnv. It is for this reason that + -- the captureTopConstraints must go here, not in tcRnSrcDecls. + ; ((tcg_env, tcl_env), lie1) <- setGblEnv tcg_env $ + captureTopConstraints $ + tcTopSrcDecls rn_decls -- If there is no splice, we're nearly done ; setEnvs (tcg_env, tcl_env) $ case group_tail of - { Nothing -> return (tcg_env, tcl_env) + { Nothing -> return (tcg_env, tcl_env, lie1) -- If there's a splice, we must carry on ; Just (SpliceDecl _ (L loc splice) _, rest_ds) -> @@ -551,8 +557,11 @@ tc_rn_src_decls ds splice) -- Glue them on the front of the remaining decls and loop - ; setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $ - tc_rn_src_decls (spliced_decls ++ rest_ds) + ; (tcg_env, tcl_env, lie2) <- + setGblEnv (tcg_env `addTcgDUs` usesOnly splice_fvs) $ + tc_rn_src_decls (spliced_decls ++ rest_ds) + + ; return (tcg_env, tcl_env, lie1 `andWC` lie2) } ; Just (XSpliceDecl _, _) -> panic "tc_rn_src_decls" } @@ -583,8 +592,9 @@ tcRnHsBootDecls hsc_src decls <- rnTopSrcDecls first_group -- The empty list is for extra dependencies coming from .hs-boot files -- See Note [Extra dependencies from .hs-boot files] in RnSource - ; (gbl_env, lie) <- captureTopConstraints $ setGblEnv tcg_env $ do { - + ; (gbl_env, lie) <- setGblEnv tcg_env $ captureTopConstraints $ do { + -- NB: setGblEnv **before** captureTopConstraints so that + -- if the latter reports errors, it knows what's in scope -- Check for illegal declarations ; case group_tail of diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index 13b5e7ad48..4f4d9b0f82 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -303,12 +303,12 @@ tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo -- See Note [Pattern synonym signatures] -- See Note [Recipe for checking a signature] in TcHsType tcPatSynSig name sig_ty - | HsIB { hsib_ext = HsIBRn { hsib_vars = implicit_hs_tvs } + | HsIB { hsib_ext = implicit_hs_tvs , hsib_body = hs_ty } <- sig_ty , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty , (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTy hs_ty1 = do { (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty)))) - <- -- NB: tcImplicitTKBndrs calls solveEqualities + <- -- NB: tcImplicitTKBndrs calls solveLocalEqualities tcImplicitTKBndrs skol_info implicit_hs_tvs $ tcExplicitTKBndrs skol_info univ_hs_tvs $ tcExplicitTKBndrs skol_info ex_hs_tvs $ @@ -319,9 +319,8 @@ tcPatSynSig name sig_ty -- e.g. pattern Zero <- 0# (Trac #12094) ; return (req, prov, body_ty) } - ; ungen_patsyn_ty <- zonkPromoteType $ - build_patsyn_type [] implicit_tvs univ_tvs req - ex_tvs prov body_ty + ; let ungen_patsyn_ty = build_patsyn_type [] implicit_tvs univ_tvs req + ex_tvs prov body_ty -- Kind generalisation ; kvs <- kindGeneralize ungen_patsyn_ty diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 5856c0f14b..7ea19b4e6c 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -5,12 +5,14 @@ module TcSimplify( growThetaTyVars, simplifyAmbiguityCheck, simplifyDefault, - simplifyTop, simplifyTopImplic, captureTopConstraints, + simplifyTop, simplifyTopImplic, simplifyInteractive, solveEqualities, solveLocalEqualities, simplifyWantedsTcM, tcCheckSatisfiability, + captureTopConstraints, + simpl_top, promoteTyVar, @@ -76,6 +78,8 @@ captureTopConstraints :: TcM a -> TcM (a, WantedConstraints) -- generates plus the constraints produced by static forms inside. -- If it fails with an exception, it reports any insolubles -- (out of scope variables) before doing so +-- NB: bring any environments into scope before calling this, so that +-- the reportUnsolved has access to the most complete GlobalRdrEnv captureTopConstraints thing_inside = do { static_wc_var <- TcM.newTcRef emptyWC ; ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $ @@ -1027,7 +1031,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates = do { -- Promote any tyvars that we cannot generalise -- See Note [Promote momomorphic tyvars] ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) - ; prom <- promoteTyVarSet mono_tvs + ; (prom, _) <- promoteTyVarSet mono_tvs -- Default any kind/levity vars ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} @@ -1909,10 +1913,11 @@ we'll get more Givens (a unification is like adding a Given) to allow the implication to make progress. -} -promoteTyVar :: TcTyVar -> TcM Bool +promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar) -- When we float a constraint out of an implication we must restore -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in 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 @@ -1920,14 +1925,16 @@ promoteTyVar 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 } + ; return (True, rhs_tv) } + else return (False, tv) } -- Returns whether or not *any* tyvar is defaulted -promoteTyVarSet :: TcTyVarSet -> TcM Bool +promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet) promoteTyVarSet tvs - = or <$> mapM promoteTyVar (nonDetEltsUniqSet tvs) - -- non-determinism is OK because order of promotion doesn't matter + = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs) + -- non-determinism is OK because order of promotion doesn't matter + + ; return (or bools, mkVarSet tyvars) } promoteTyVarTcS :: TcTyVar -> TcS () -- When we float a constraint out of an implication we must restore diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 5e50dac3f3..b0d68152f6 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -1180,7 +1180,7 @@ reifyInstances th_nm th_tys do { (rn_ty, fvs) <- rnLHsType doc rdr_ty ; return ((tv_names, rn_ty), fvs) } ; (_tvs, ty) - <- solveEqualities $ + <- failIfEmitsConstraints $ -- avoid error cascade if there are unsolved tcImplicitTKBndrs ReifySkol tv_names $ fst <$> tcLHsType rn_ty ; ty <- zonkTcTypeToType emptyZonkEnv ty diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 8a3b7c7946..cd80be649c 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1399,7 +1399,7 @@ but it works. ------------------------- kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM () kcTyFamInstEqn tc_fam_tc - (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names } + (L loc (HsIB { hsib_ext = tv_names , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name , feqn_pats = pats , feqn_rhs = hs_ty }})) @@ -1452,7 +1452,7 @@ tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn -- Needs to be here, not in TcInstDcls, because closed families -- (typechecked here) have TyFamInstEqns tcTyFamInstEqn fam_tc mb_clsinfo - (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names } + (L loc (HsIB { hsib_ext = tv_names , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name , feqn_pats = pats , feqn_rhs = hs_ty }})) @@ -1960,7 +1960,8 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl skol_info = DataConSkol name ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts))) - <- solveEqualities $ + <- failIfEmitsConstraints $ -- we won't get another crack, and we don't + -- want an error cascade tcImplicitTKBndrs skol_info implicit_tkv_nms $ tcExplicitTKBndrs skol_info explicit_tkv_nms $ do { ctxt <- tcHsMbContext cxt diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 1dc60e7312..7c9ef67837 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -2095,6 +2095,7 @@ checkValidTelescope tvbs user_tyvars extra -} -- Free variables of a type, retaining repetitions, and expanding synonyms +-- This ignores coercions, as coercions aren't user-written fvType :: Type -> [TyCoVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty fvType (TyVarTy tv) = [tv] @@ -2105,42 +2106,12 @@ fvType (FunTy arg res) = fvType arg ++ fvType res fvType (ForAllTy (TvBndr tv _) ty) = fvType (tyVarKind tv) ++ filter (/= tv) (fvType ty) -fvType (CastTy ty co) = fvType ty ++ fvCo co -fvType (CoercionTy co) = fvCo co +fvType (CastTy ty _) = fvType ty +fvType (CoercionTy {}) = [] fvTypes :: [Type] -> [TyVar] fvTypes tys = concat (map fvType tys) -fvMCo :: MCoercion -> [TyCoVar] -fvMCo MRefl = [] -fvMCo (MCo co) = fvCo co - -fvCo :: Coercion -> [TyCoVar] -fvCo (Refl ty) = fvType ty -fvCo (GRefl _ ty mco) = fvType ty ++ fvMCo mco -fvCo (TyConAppCo _ _ args) = concatMap fvCo args -fvCo (AppCo co arg) = fvCo co ++ fvCo arg -fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h -fvCo (FunCo _ co1 co2) = fvCo co1 ++ fvCo co2 -fvCo (CoVarCo v) = [v] -fvCo (AxiomInstCo _ _ args) = concatMap fvCo args -fvCo (UnivCo p _ t1 t2) = fvProv p ++ fvType t1 ++ fvType t2 -fvCo (SymCo co) = fvCo co -fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2 -fvCo (NthCo _ _ co) = fvCo co -fvCo (LRCo _ co) = fvCo co -fvCo (InstCo co arg) = fvCo co ++ fvCo arg -fvCo (KindCo co) = fvCo co -fvCo (SubCo co) = fvCo co -fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs -fvCo (HoleCo h) = pprPanic "fvCo falls into a hole" (ppr h) - -fvProv :: UnivCoProvenance -> [TyCoVar] -fvProv UnsafeCoerceProv = [] -fvProv (PhantomProv co) = fvCo co -fvProv (ProofIrrelProv co) = fvCo co -fvProv (PluginProv _) = [] - sizeType :: Type -> Int -- Size of a type: the number of variables and constructors sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty @@ -2151,7 +2122,7 @@ sizeType (AppTy fun arg) = sizeType fun + sizeType arg sizeType (FunTy arg res) = sizeType arg + sizeType res + 1 sizeType (ForAllTy _ ty) = sizeType ty sizeType (CastTy ty _) = sizeType ty -sizeType (CoercionTy _) = 1 +sizeType (CoercionTy _) = 0 sizeTypes :: [Type] -> Int sizeTypes = foldr ((+) . sizeType) 0 diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 3ea4f61741..fd3d1dfff7 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -2247,6 +2247,34 @@ sym (ForAllCo tv h g) ==> ForAllCo tv (sym h) (sym g[tv |-> tv |> sym h]) +Note [Substituting in a coercion hole] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +It seems highly suspicious to be substituting in a coercion that still +has coercion holes. Yet, this can happen in a situation like this: + + f :: forall k. k :~: Type -> () + f Refl = let x :: forall (a :: k). [a] -> ... + x = ... + +When we check x's type signature, we require that k ~ Type. We indeed +know this due to the Refl pattern match, but the eager unifier can't +make use of givens. So, when we're done looking at x's type, a coercion +hole will remain. Then, when we're checking x's definition, we skolemise +x's type (in order to, e.g., bring the scoped type variable `a` into scope). +This requires performing a substitution for the fresh skolem variables. + +This subsitution needs to affect the kind of the coercion hole, too -- +otherwise, the kind will have an out-of-scope variable in it. More problematically +in practice (we won't actually notice the out-of-scope variable ever), skolems +in the kind might have too high a level, triggering a failure to uphold the +invariant that no free variables in a type have a higher level than the +ambient level in the type checker. In the event of having free variables in the +hole's kind, I'm pretty sure we'll always have an erroneous program, so we +don't need to worry what will happen when the hole gets filled in. After all, +a hole relating a locally-bound type variable will be unable to be solved. This +is why it's OK not to look through the IORef of a coercion hole during +substitution. + -} -- | Type substitution, see 'zipTvSubst' @@ -2511,19 +2539,17 @@ subst_co subst co go (SubCo co) = mkSubCo $! (go co) go (AxiomRuleCo c cs) = let cs1 = map go cs in cs1 `seqList` AxiomRuleCo c cs1 - go (HoleCo h) = HoleCo h - -- NB: this last case is a little suspicious, but we need it. Originally, - -- there was a panic here, but it triggered from deeplySkolemise. Because - -- we only skolemise tyvars that are manually bound, this operation makes - -- sense, even over a coercion with holes. We don't need to substitute - -- in the type of the coHoleCoVar because it wouldn't makes sense to have - -- forall a. ....(ty |> {hole_cv::a}).... + go (HoleCo h) = HoleCo $! go_hole h go_prov UnsafeCoerceProv = UnsafeCoerceProv go_prov (PhantomProv kco) = PhantomProv (go kco) go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) go_prov p@(PluginProv _) = p + -- See Note [Substituting in a coercion hole] + go_hole h@(CoercionHole { ch_co_var = cv }) + = h { ch_co_var = updateVarType go_ty cv } + substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion) substForAllCoBndr subst = substForAllCoBndrUsing False (substCo subst) subst diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 5d1c0b30cb..d5cdf71ed0 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -10559,49 +10559,6 @@ and :extension:`GADTs`. You can switch it off again with :extension:`NoMonoLocalBinds <-XMonoLocalBinds>` but type inference becomes less predictable if you do so. (Read the papers!) -.. _kind-generalisation: - -Kind generalisation -------------------- - -Just as :extension:`MonoLocalBinds` places limitations on when the *type* of a -*term* is generalised (see :ref:`mono-local-binds`), it also limits when the -*kind* of a *type signature* is generalised. Here is an example involving -:ref:`type signatures on instance declarations <instance-sigs>`: :: - - data Proxy a = Proxy - newtype Tagged s b = Tagged b - - class C b where - c :: forall (s :: k). Tagged s b - - instance C (Proxy a) where - c :: forall s. Tagged s (Proxy a) - c = Tagged Proxy - -With :extension:`MonoLocalBinds` enabled, this ``C (Proxy a)`` instance will -fail to typecheck. The reason is that the type signature for ``c`` captures -``a``, an outer-scoped type variable, which means the type signature is not -closed. Therefore, the inferred kind for ``s`` will *not* be generalised, and -as a result, it will fail to unify with the kind variable ``k`` which is -specified in the declaration of ``c``. This can be worked around by specifying -an explicit kind variable for ``s``, e.g., :: - - instance C (Proxy a) where - c :: forall (s :: k). Tagged s (Proxy a) - c = Tagged Proxy - -or, alternatively: :: - - instance C (Proxy a) where - c :: forall k (s :: k). Tagged s (Proxy a) - c = Tagged Proxy - -This declarations are equivalent using Haskell's implicit "add implicit -foralls" rules (see :ref:`implicit-quantification`). The implicit foralls rules -are purely syntactic and are quite separate from the kind generalisation -described here. - .. _visible-type-application: Visible type application diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_compile/T14066h.hs index a20ae30958..df3db1c15d 100644 --- a/testsuite/tests/dependent/should_fail/T14066h.hs +++ b/testsuite/tests/dependent/should_compile/T14066h.hs @@ -7,5 +7,5 @@ import Data.Proxy f :: forall b. b -> (Proxy Int, Proxy Maybe) f x = (fst y :: Proxy Int, fst y :: Proxy Maybe) where - y :: (Proxy a, b) -- MonoLocalBinds means this won't generalize over the kind of a + y :: (Proxy a, b) -- this generalizes over the kind of a y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index 4e096c1f71..418fba2d85 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -53,3 +53,4 @@ test('T15264', normal, compile, ['']) test('DkNameRes', normal, compile, ['']) test('T15346', normal, compile, ['']) test('T15419', normal, compile, ['']) +test('T14066h', normal, compile, ['']) diff --git a/testsuite/tests/dependent/should_fail/DepFail1.stderr b/testsuite/tests/dependent/should_fail/DepFail1.stderr index 630f010fa3..a8e64d4e0c 100644 --- a/testsuite/tests/dependent/should_fail/DepFail1.stderr +++ b/testsuite/tests/dependent/should_fail/DepFail1.stderr @@ -2,11 +2,25 @@ DepFail1.hs:7:6: error: • Expecting one more argument to ‘Proxy Bool’ Expected a type, but ‘Proxy Bool’ has kind ‘Bool -> *’ - • In the type signature: - z :: Proxy Bool + • In the type signature: z :: Proxy Bool + +DepFail1.hs:8:5: error: + • Couldn't match expected type ‘Proxy Bool’ + with actual type ‘Proxy k0 a1’ + • In the expression: P + In an equation for ‘z’: z = P DepFail1.hs:10:16: error: • Expected kind ‘Int’, but ‘Bool’ has kind ‘*’ • In the second argument of ‘Proxy’, namely ‘Bool’ - In the type signature: - a :: Proxy Int Bool + In the type signature: a :: Proxy Int Bool + +DepFail1.hs:11:5: error: + • Couldn't match kind ‘*’ with ‘Int’ + When matching types + a0 :: Int + Bool :: * + Expected type: Proxy Int Bool + Actual type: Proxy Int a0 + • In the expression: P + In an equation for ‘a’: a = P diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr index 0ae1710bf0..3e8bef6858 100644 --- a/testsuite/tests/dependent/should_fail/T13895.stderr +++ b/testsuite/tests/dependent/should_fail/T13895.stderr @@ -1,4 +1,28 @@ +T13895.hs:8:14: error: + • Could not deduce (Typeable (t dict0)) + from the context: (Data a, Typeable (t dict)) + bound by the type signature for: + dataCast1 :: forall k (dict :: Typeable k) (dict1 :: Typeable + *) a (c :: * + -> *) (t :: forall k1. + Typeable + k1 => + k1 + -> *). + (Data a, Typeable (t dict)) => + (forall d. Data d => c (t dict1 d)) -> Maybe (c a) + at T13895.hs:(8,14)-(14,24) + The type variable ‘dict0’ is ambiguous + • In the ambiguity check for ‘dataCast1’ + To defer the ambiguity check to use sites, enable AllowAmbiguousTypes + In the type signature: + dataCast1 :: forall (a :: Type). + Data a => + forall (c :: Type -> Type) + (t :: forall (k :: Type). Typeable k => k -> Type). + Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a) + T13895.hs:12:23: error: • Illegal constraint in a kind: Typeable k0 • In the first argument of ‘Typeable’, namely ‘t’ diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr index cd0142f5c1..e5179e510b 100644 --- a/testsuite/tests/dependent/should_fail/T14066.stderr +++ b/testsuite/tests/dependent/should_fail/T14066.stderr @@ -1,6 +1,6 @@ T14066.hs:15:59: error: - • Expected kind ‘k0’, but ‘b’ has kind ‘k’ + • Expected kind ‘k’, but ‘b’ has kind ‘k1’ • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: g :: forall k (b :: k). SameKind a b In the expression: @@ -8,4 +8,6 @@ T14066.hs:15:59: error: g :: forall k (b :: k). SameKind a b g = undefined in () - • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4) + • Relevant bindings include + x :: Proxy a (bound at T14066.hs:15:4) + f :: Proxy a -> () (bound at T14066.hs:15:1) diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index 504ca5a80e..193c74d193 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,6 +1,15 @@ T14066e.hs:13:59: error: - • Expected kind ‘c’, but ‘b'’ has kind ‘k0’ + • Couldn't match kind ‘k1’ with ‘*’ + ‘k1’ is a rigid type variable bound by + the type signature for: + j :: forall k k1 (c :: k1) (b :: k). + Proxy a -> Proxy b -> Proxy c -> Proxy b + at T14066e.hs:12:5-61 + When matching kinds + k :: * + c :: k1 + Expected kind ‘c’, but ‘b'’ has kind ‘k’ • In the first argument of ‘Proxy’, namely ‘(b' :: c')’ In an expression type signature: Proxy (b' :: c') In the expression: (p1 :: Proxy (b' :: c')) diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr deleted file mode 100644 index bfd33693b6..0000000000 --- a/testsuite/tests/dependent/should_fail/T14066h.stderr +++ /dev/null @@ -1,16 +0,0 @@ - -T14066h.hs:8:28: error: - • Couldn't match kind ‘* -> *’ with ‘*’ - When matching types - a0 :: * - Maybe :: * -> * - Expected type: Proxy Maybe - Actual type: Proxy a0 - • In the expression: fst y :: Proxy Maybe - In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe) - In an equation for ‘f’: - f x - = (fst y :: Proxy Int, fst y :: Proxy Maybe) - where - y :: (Proxy a, b) - y = (Proxy, x) diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 593b7787a1..0f7129020e 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -26,7 +26,6 @@ test('T14066d', normal, compile_fail, ['']) test('T14066e', normal, compile_fail, ['']) test('T14066f', normal, compile_fail, ['']) test('T14066g', normal, compile_fail, ['']) -test('T14066h', normal, compile_fail, ['']) test('T14845_fail1', normal, compile_fail, ['']) test('T14845_fail2', normal, compile_fail, ['']) test('InferDependency', normal, compile_fail, ['']) diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index a1c412bd7d..2c1a0ec7df 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -125,10 +125,8 @@ (Just [({ DumpRenamedAst.hs:9:3-36 } (HsIB - (HsIBRn - [{Name: a} - ,{Name: as}] - (True)) + [{Name: a} + ,{Name: as}] (FamEqn (NoExt) ({ DumpRenamedAst.hs:9:3-8 } @@ -183,9 +181,7 @@ {Name: as})))))))))))) ,({ DumpRenamedAst.hs:10:3-24 } (HsIB - (HsIBRn - [] - (True)) + [] (FamEqn (NoExt) ({ DumpRenamedAst.hs:10:3-8 } @@ -285,10 +281,8 @@ (NoExt) (DataFamInstDecl (HsIB - (HsIBRn - [{Name: k} - ,{Name: a}] - (True)) + [{Name: k} + ,{Name: a}] (FamEqn (NoExt) ({ DumpRenamedAst.hs:15:18-20 } diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr index ea687c3247..a3b40c1222 100644 --- a/testsuite/tests/polykinds/T11142.stderr +++ b/testsuite/tests/polykinds/T11142.stderr @@ -1,6 +1,17 @@ T11142.hs:9:49: error: - • Expected kind ‘k’, but ‘b’ has kind ‘k0’ + • Expected kind ‘k1’, but ‘b’ has kind ‘k0’ • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: foo :: forall b. (forall k (a :: k). SameKind a b) -> () + +T11142.hs:10:7: error: + • Cannot instantiate unification variable ‘a0’ + with a type involving foralls: + (forall k1 (a :: k1). SameKind a b) -> () + GHC doesn't yet support impredicative polymorphism + • In the expression: undefined + In an equation for ‘foo’: foo = undefined + • Relevant bindings include + foo :: (forall k1 (a :: k1). SameKind a b) -> () + (bound at T11142.hs:10:1) diff --git a/testsuite/tests/polykinds/T11516.hs b/testsuite/tests/polykinds/T11516.hs index 3b19a997f9..66feeec387 100644 --- a/testsuite/tests/polykinds/T11516.hs +++ b/testsuite/tests/polykinds/T11516.hs @@ -3,6 +3,7 @@ {-# language ConstraintKinds #-} {-# language FlexibleInstances #-} {-# language FunctionalDependencies #-} +{-# language UndecidableInstances #-} import GHC.Exts (Constraint) diff --git a/testsuite/tests/polykinds/T11516.stderr b/testsuite/tests/polykinds/T11516.stderr index 5db11c8f83..5f8083309c 100644 --- a/testsuite/tests/polykinds/T11516.stderr +++ b/testsuite/tests/polykinds/T11516.stderr @@ -1,5 +1,5 @@ -T11516.hs:11:16: error: +T11516.hs:12:16: error: • Expected kind ‘i0 -> i0 -> *’, but ‘()’ has kind ‘*’ • In the first argument of ‘Varpi’, namely ‘()’ In the instance declaration for ‘Varpi (->) (->) (Either f)’ diff --git a/testsuite/tests/polykinds/T11520.hs b/testsuite/tests/polykinds/T11520.hs index eef999d4ba..9c1d4fe1be 100644 --- a/testsuite/tests/polykinds/T11520.hs +++ b/testsuite/tests/polykinds/T11520.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses #-} +{-# LANGUAGE RankNTypes, PolyKinds, GADTs, UndecidableSuperClasses, UndecidableInstances #-} module T11520 where diff --git a/testsuite/tests/polykinds/T11520.stderr b/testsuite/tests/polykinds/T11520.stderr index 11a81baf62..75147e6a00 100644 --- a/testsuite/tests/polykinds/T11520.stderr +++ b/testsuite/tests/polykinds/T11520.stderr @@ -1,4 +1,8 @@ +T11520.hs:15:57: error: + • Illegal type synonym family application in instance: Compose f g + • In the instance declaration for ‘Typeable (Compose f g)’ + T11520.hs:15:77: error: • Expected kind ‘k20 -> k10’, but ‘g’ has kind ‘k’ • In the second argument of ‘Compose’, namely ‘g’ diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr index 43f762221e..27123a8bc8 100644 --- a/testsuite/tests/polykinds/T12593.stderr +++ b/testsuite/tests/polykinds/T12593.stderr @@ -10,7 +10,7 @@ T12593.hs:12:31: error: • Expecting one more argument to ‘k’ Expected a type, but ‘k’ has kind - ‘(((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *) + ‘(((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) -> Constraint’ • In the kind ‘k’ In the type signature: @@ -22,7 +22,7 @@ T12593.hs:12:40: error: • Expecting two more arguments to ‘k1’ Expected a type, but ‘k1’ has kind - ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’ + ‘((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *’ • In the kind ‘k1’ In the type signature: run :: k2 q => @@ -31,13 +31,13 @@ T12593.hs:12:40: error: T12593.hs:12:47: error: • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint) - -> (k2 -> k3 -> *) -> *) + -> (k3 -> k4 -> *) -> *) -> Constraint’ with ‘*’ When matching kinds - k2 :: * - k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *) - -> Constraint + k3 :: * + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint • In the first argument of ‘p’, namely ‘c’ In the type signature: run :: k2 q => @@ -46,11 +46,11 @@ T12593.hs:12:47: error: T12593.hs:12:49: error: • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) - -> (k2 -> k3 -> *) -> *’ + -> (k3 -> k4 -> *) -> *’ with ‘*’ When matching kinds - k3 :: * - k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> * + k4 :: * + k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> * • In the second argument of ‘p’, namely ‘d’ In the type signature: run :: k2 q => @@ -59,13 +59,13 @@ T12593.hs:12:49: error: T12593.hs:12:56: error: • Couldn't match kind ‘(((k0 -> k1 -> *) -> Constraint) - -> (k2 -> k3 -> *) -> *) + -> (k3 -> k4 -> *) -> *) -> Constraint’ with ‘*’ When matching kinds k0 :: * - k :: (((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *) - -> Constraint + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint • In the first argument of ‘q’, namely ‘c’ In the type signature: run :: k2 q => @@ -74,13 +74,43 @@ T12593.hs:12:56: error: T12593.hs:12:58: error: • Couldn't match kind ‘((k0 -> k1 -> *) -> Constraint) - -> (k2 -> k3 -> *) -> *’ + -> (k3 -> k4 -> *) -> *’ with ‘*’ When matching kinds k1 :: * - k4 :: ((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> * + k7 :: ((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> * • In the second argument of ‘q’, namely ‘d’ 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:14:6: error: + • Couldn't match type ‘Free k2 p0’ with ‘Free k6 k7 k8 p’ + Expected type: Free k6 k7 k8 p a b + Actual type: Free k2 p0 a b + • In the pattern: Free cat + In an equation for ‘run’: run (Free cat) = cat + • Relevant bindings include + run :: Free k6 k7 k8 p a b + -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + (bound at T12593.hs:14:1) + +T12593.hs:14:18: error: + • Couldn't match kind ‘*’ + with ‘(((k3 -> k4 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint’ + When matching kinds + k0 :: * + k6 :: (((k0 -> k1 -> *) -> Constraint) -> (k3 -> k4 -> *) -> *) + -> Constraint + • In the expression: cat + In an equation for ‘run’: run (Free cat) = cat + • Relevant bindings include + cat :: forall (q :: k0 -> k1 -> *). + k2 q => + (forall (c :: k0) (d :: k1). p0 c d -> q c d) -> q a b + (bound at T12593.hs:14:11) + run :: Free k6 k7 k8 p a b + -> (forall (c :: k6) (d :: k7). p c d -> q c d) -> q a b + (bound at T12593.hs:14:1) diff --git a/testsuite/tests/polykinds/T13555.stderr b/testsuite/tests/polykinds/T13555.stderr deleted file mode 100644 index 3d2492e23d..0000000000 --- a/testsuite/tests/polykinds/T13555.stderr +++ /dev/null @@ -1,20 +0,0 @@ - -T13555.hs:25:14: error: - • Couldn't match type ‘k2’ with ‘k0’ - ‘k2’ is a rigid type variable bound by - the type signature for: - crtInfo :: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - at T13555.hs:25:14-79 - Expected type: TaggedT m Maybe (CRTInfo (GF fp d)) - Actual type: TaggedT m0 Maybe (CRTInfo (GF fp d)) - • When checking that instance signature for ‘crtInfo’ - is more general than its signature in the class - Instance sig: forall (m :: k0). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - Class sig: forall k2 (m :: k2). - Reflects m Int => - TaggedT m Maybe (CRTInfo (GF fp d)) - In the instance declaration for ‘CRTrans Maybe (GF fp d)’ diff --git a/testsuite/tests/polykinds/T14520.hs b/testsuite/tests/polykinds/T14520.hs index 23e903773b..44dc2ee18d 100644 --- a/testsuite/tests/polykinds/T14520.hs +++ b/testsuite/tests/polykinds/T14520.hs @@ -1,4 +1,4 @@ -{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators #-} +{-# Language DataKinds, PolyKinds, TypeFamilies, TypeOperators, AllowAmbiguousTypes #-} module T14520 where diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr index e19d834b95..07042fde92 100644 --- a/testsuite/tests/polykinds/T14520.stderr +++ b/testsuite/tests/polykinds/T14520.stderr @@ -1,5 +1,6 @@ T14520.hs:15:24: error: - • Expected kind ‘bat w w’, but ‘Id’ has kind ‘XXX (XXX kat0 b0) b0’ + • Expected kind ‘bat w w’, + but ‘Id’ has kind ‘XXX * a0 (XXX (a0 ~>> *) a0 kat0 b0) b0’ • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’ In the type signature: sId :: Sing w -> Sing (Id :: bat w w) diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 3abdb88d2f..1d852031d9 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -13,10 +13,11 @@ T14846.hs:38:8: error: ríki a a at T14846.hs:38:8-48 Expected type: ríki a a - Actual type: Hom riki a0 a0 + Actual type: Hom riki a a • When checking that instance signature for ‘i’ is more general than its signature in the class - Instance sig: forall (xx :: k0) (a :: Struct cls0). + Instance sig: forall k1 (cls :: k1 + -> Constraint) k2 (xx :: k2) (a :: Struct cls). StructI xx a => Hom riki a a Class sig: forall k1 (cls :: k1 @@ -31,15 +32,15 @@ T14846.hs:38:8: error: In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:31: error: - • Couldn't match kind ‘k4’ with ‘Struct cls0’ + • Couldn't match kind ‘k4’ with ‘Struct cls2’ ‘k4’ is a rigid type variable bound by the instance declaration at T14846.hs:37:10-65 When matching kinds - cls :: k4 -> Constraint - cls1 :: Struct cls0 -> Constraint - Expected kind ‘Struct cls1’, - but ‘Structured a cls’ has kind ‘Struct cls’ + cls1 :: k4 -> Constraint + cls0 :: Struct cls -> Constraint + Expected kind ‘Struct cls0’, + but ‘Structured a cls’ has kind ‘Struct cls1’ • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’ In an expression type signature: AStruct (Structured a cls) In the expression: struct :: AStruct (Structured a cls) diff --git a/testsuite/tests/polykinds/T7224.stderr b/testsuite/tests/polykinds/T7224.stderr index daab1c40a9..774a4bce69 100644 --- a/testsuite/tests/polykinds/T7224.stderr +++ b/testsuite/tests/polykinds/T7224.stderr @@ -2,6 +2,12 @@ T7224.hs:6:19: error: • Expected kind ‘i’, but ‘i’ has kind ‘*’ • In the first argument of ‘m’, namely ‘i’ + In the type signature: ret' :: a -> m i i a + In the class declaration for ‘PMonad'’ + +T7224.hs:7:14: error: + • Expected kind ‘i’, but ‘i’ has kind ‘*’ + • In the first argument of ‘m’, namely ‘i’ In the type signature: - ret' :: a -> m i i a + bind' :: m i j a -> (a -> m j k b) -> m i k b In the class declaration for ‘PMonad'’ diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index 6249bf7b62..9aa4ab50d9 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -1,8 +1,14 @@ -T8616.hs:8:29: error: - • Expected a type, but ‘(Any :: k)’ has kind ‘k’ - • In an expression type signature: (Any :: k) - In the expression: undefined :: (Any :: k) +T8616.hs:8:16: error: + • Couldn't match kind ‘k’ with ‘*’ + ‘k’ is a rigid type variable bound by + the type signature for: + withSomeSing :: forall k (kproxy :: k). Proxy kproxy + at T8616.hs:7:1-50 + When matching types + a0 :: * + 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/all.T b/testsuite/tests/polykinds/all.T index 425e57a946..de46acfc3a 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -161,7 +161,7 @@ test('T13394a', normal, compile, ['']) test('T13394', normal, compile, ['']) test('T13371', normal, compile, ['']) test('T13393', normal, compile_fail, ['']) -test('T13555', normal, compile_fail, ['']) +test('T13555', normal, compile, ['']) test('T13659', normal, compile_fail, ['']) test('T13625', normal, compile_fail, ['']) test('T13985', normal, compile_fail, ['']) @@ -176,7 +176,7 @@ test('T14450', normal, compile_fail, ['']) test('T14172', normal, multimod_compile_fail, ['T14172.hs','-v0']) test('T14174', normal, compile_fail, ['']) test('T14174a', normal, compile, ['']) -test('T14520', normal, compile_fail, ['']) +test('T14520', normal, compile_fail, ['-fprint-explicit-kinds']) test('T11203', normal, compile_fail, ['']) test('T14555', normal, compile_fail, ['-fprint-explicit-runtime-reps']) test('T14563', normal, compile_fail, ['-fprint-explicit-runtime-reps']) diff --git a/testsuite/tests/rename/should_fail/T5951.stderr b/testsuite/tests/rename/should_fail/T5951.stderr index 8fda353b33..a6969971ab 100644 --- a/testsuite/tests/rename/should_fail/T5951.stderr +++ b/testsuite/tests/rename/should_fail/T5951.stderr @@ -4,6 +4,10 @@ T5951.hs:8:8: error: Expected a constraint, but ‘A’ has kind ‘* -> Constraint’ • In the instance declaration for ‘B => C’ +T5951.hs:8:8: error: + • Instance head is not headed by a class: C + • In the instance declaration for ‘B => C’ + T5951.hs:9:8: error: • Expecting one more argument to ‘B’ Expected a constraint, but ‘B’ has kind ‘* -> Constraint’ diff --git a/testsuite/tests/rename/should_fail/rnfail026.hs b/testsuite/tests/rename/should_fail/rnfail026.hs index d09d9fc22f..2d22df20d4 100644 --- a/testsuite/tests/rename/should_fail/rnfail026.hs +++ b/testsuite/tests/rename/should_fail/rnfail026.hs @@ -1,6 +1,6 @@ {-# LANGUAGE RankNTypes, FlexibleInstances #-} --- This one made ghc-4.08 crash +-- This one made ghc-4.08 crash -- rename/RnEnv.lhs:239: Non-exhaustive patterns in function get_tycon_key -- The type in the Monad instance is utterly bogus, of course @@ -9,11 +9,12 @@ module ShouldCompile ( Set ) where data Set a = Set [a] deriving (Eq, Ord, Read, Show) - +{- instance Functor Set where f `fmap` (Set xs) = Set $ f `fmap` xs - +-} instance Monad (forall a. Eq a => Set a) where return x = Set [x] - -instance Eq (forall a. [a]) where +{- +instance Eq (forall a. [a]) where +-} diff --git a/testsuite/tests/rename/should_fail/rnfail026.stderr b/testsuite/tests/rename/should_fail/rnfail026.stderr index 8bd80b1b58..79b07c4d24 100644 --- a/testsuite/tests/rename/should_fail/rnfail026.stderr +++ b/testsuite/tests/rename/should_fail/rnfail026.stderr @@ -1,10 +1,10 @@ +rnfail026.hs:16:10: error: + • Illegal polymorphic type: forall a. Eq a => Set a + • In the instance declaration for ‘Monad (forall a. Eq a => Set a)’ + rnfail026.hs:16:27: error: • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’ • In the first argument of ‘Monad’, namely ‘(forall a. Eq a => Set a)’ In the instance declaration for ‘Monad (forall a. Eq a => Set a)’ - -rnfail026.hs:19:10: error: - • Illegal polymorphic type: forall a. [a] - • In the instance declaration for ‘Eq (forall a. [a])’ diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr index b698bc1004..4bfc53a78e 100644 --- a/testsuite/tests/th/T5358.stderr +++ b/testsuite/tests/th/T5358.stderr @@ -1,24 +1,4 @@ -T5358.hs:10:13: error: - • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’ - • The function ‘T5358.t1’ is applied to one argument, - but its type ‘Int’ has none - In the first argument of ‘(==)’, namely ‘T5358.t1 x’ - In the expression: T5358.t1 x == T5358.t2 x - • Relevant bindings include - x :: t (bound at T5358.hs:10:9) - T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1) - -T5358.hs:10:21: error: - • Couldn't match expected type ‘t -> a0’ with actual type ‘Int’ - • The function ‘T5358.t2’ is applied to one argument, - but its type ‘Int’ has none - In the second argument of ‘(==)’, namely ‘T5358.t2 x’ - In the expression: T5358.t1 x == T5358.t2 x - • Relevant bindings include - x :: t (bound at T5358.hs:10:9) - T5358.prop_x1 :: t -> Bool (bound at T5358.hs:10:1) - T5358.hs:14:12: error: • Exception when trying to run compile-time code: runTest called error: forall (t_0 :: *) . t_0 -> GHC.Types.Bool diff --git a/testsuite/tests/typecheck/should_compile/T15141.hs b/testsuite/tests/typecheck/should_compile/T15141.hs new file mode 100644 index 0000000000..c0cb5d8488 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T15141.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies, + ScopedTypeVariables, TypeOperators, GADTs, + DataKinds #-} + +module T15141 where + +import Data.Type.Equality +import Data.Proxy + +type family F a = r | r -> a where + F () = Bool + +data Wumpus where + Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus + +f :: forall k (a :: k). k :~: Bool -> () +f Refl = let x :: Proxy ('Unify a b) + x = undefined + in () + +{- +We want this situation: + +forall[1] k[1]. + [G] k ~ Bool + forall [2] ... . [W] k ~ F kappa[2] + +where the inner wanted can be solved only by taking the outer +given into account. This means that the wanted needs to be floated out. +More germane to this bug, we need *not* to generalize over kappa. + +The code above builds this scenario fairly exactly, and indeed fails +without the logic in kindGeneralize that excludes constrained variables +from generalization. +-} diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 2fb5429715..1857ba814e 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -646,3 +646,4 @@ test('T15431', normal, compile, ['']) test('T15431a', normal, compile, ['']) test('T15428', normal, compile, ['']) test('T15412', normal, compile, ['']) +test('T15141', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_fail/T11112.stderr b/testsuite/tests/typecheck/should_fail/T11112.stderr index ec2154c8ce..304078158e 100644 --- a/testsuite/tests/typecheck/should_fail/T11112.stderr +++ b/testsuite/tests/typecheck/should_fail/T11112.stderr @@ -1,5 +1,13 @@ T11112.hs:3:9: error: • Expected a type, but ‘Ord s’ has kind ‘Constraint’ - • In the type signature: - sort :: Ord s -> [s] -> [s] + • In the type signature: sort :: Ord s -> [s] -> [s] + +T11112.hs:4:11: error: + • Couldn't match expected type ‘[s] -> [s]’ + with actual type ‘Ord s’ + • In the expression: xs + In an equation for ‘sort’: sort xs = xs + • Relevant bindings include + xs :: Ord s (bound at T11112.hs:4:6) + sort :: Ord s => [s] -> [s] (bound at T11112.hs:4:1) diff --git a/testsuite/tests/typecheck/should_fail/T11563.stderr b/testsuite/tests/typecheck/should_fail/T11563.stderr index 27eca84816..1283c33983 100644 --- a/testsuite/tests/typecheck/should_fail/T11563.stderr +++ b/testsuite/tests/typecheck/should_fail/T11563.stderr @@ -1,4 +1,10 @@ +T11563.hs:5:10: error: + • Variable ‘s’ occurs more often + in the constraint ‘C s’ than in the instance head ‘C T’ + (Use UndecidableInstances to permit this) + • In the instance declaration for ‘C T’ + T11563.hs:5:19: error: • Expecting one more argument to ‘T’ Expected a type, but ‘T’ has kind ‘* -> *’ diff --git a/testsuite/tests/typecheck/should_fail/T14232.stderr b/testsuite/tests/typecheck/should_fail/T14232.stderr index a497be7b19..1ca41f0bd5 100644 --- a/testsuite/tests/typecheck/should_fail/T14232.stderr +++ b/testsuite/tests/typecheck/should_fail/T14232.stderr @@ -2,3 +2,16 @@ T14232.hs:3:6: error: • Expected kind ‘* -> *’, but ‘String -> a’ has kind ‘*’ • In the type signature: f :: (String -> a) String -> a + +T14232.hs:4:9: error: + • Couldn't match type ‘String -> a’ with ‘(->) t0’ + Expected type: t0 -> [Char] + Actual type: (String -> a) String + • The function ‘g’ is applied to one argument, + but its type ‘(String -> a) String’ has none + In the expression: g s + In an equation for ‘f’: f g s = g s + • Relevant bindings include + s :: t0 (bound at T14232.hs:4:5) + g :: (String -> a) String (bound at T14232.hs:4:3) + f :: (String -> a) String -> a (bound at T14232.hs:4:1) diff --git a/testsuite/tests/typecheck/should_fail/T1633.stderr b/testsuite/tests/typecheck/should_fail/T1633.stderr index 300e6c3def..5d9dcc44f5 100644 --- a/testsuite/tests/typecheck/should_fail/T1633.stderr +++ b/testsuite/tests/typecheck/should_fail/T1633.stderr @@ -1,5 +1,5 @@ T1633.hs:8:18: error: - Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’ - In the first argument of ‘Functor’, namely ‘Bool’ - In the instance declaration for ‘Functor Bool’ + • Expected kind ‘* -> *’, but ‘Bool’ has kind ‘*’ + • In the first argument of ‘Functor’, namely ‘Bool’ + In the instance declaration for ‘Functor Bool’ diff --git a/testsuite/tests/typecheck/should_fail/T2994.stderr b/testsuite/tests/typecheck/should_fail/T2994.stderr index 7f20acf5aa..09b36165a6 100644 --- a/testsuite/tests/typecheck/should_fail/T2994.stderr +++ b/testsuite/tests/typecheck/should_fail/T2994.stderr @@ -5,12 +5,20 @@ T2994.hs:11:10: error: but ‘MonadReader Int’ has kind ‘* -> Constraint’ • In the instance declaration for ‘MonadReader Int’ +T2994.hs:11:10: error: + • Instance head is not headed by a class: MonadReader Int + • In the instance declaration for ‘MonadReader Int’ + T2994.hs:13:10: error: • Expecting one more argument to ‘MonadReader (Reader' r)’ Expected a constraint, but ‘MonadReader (Reader' r)’ has kind ‘* -> Constraint’ • In the instance declaration for ‘MonadReader (Reader' r)’ +T2994.hs:13:10: error: + • Instance head is not headed by a class: MonadReader (Reader' r) + • In the instance declaration for ‘MonadReader (Reader' r)’ + T2994.hs:13:23: error: • Expecting one more argument to ‘Reader' r’ Expected a type, but ‘Reader' r’ has kind ‘* -> *’ @@ -21,3 +29,8 @@ T2994.hs:15:10: error: • Expected kind ‘(* -> *) -> Constraint’, but ‘MonadReader r r’ has kind ‘Constraint’ • In the instance declaration for ‘MonadReader r r (Reader' r)’ + +T2994.hs:15:10: error: + • Instance head is not headed by a class: + MonadReader r r (Reader' r) + • In the instance declaration for ‘MonadReader r r (Reader' r)’ diff --git a/testsuite/tests/typecheck/should_fail/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr index 0fdb88b313..eeb2c051f2 100644 --- a/testsuite/tests/typecheck/should_fail/T3540.stderr +++ b/testsuite/tests/typecheck/should_fail/T3540.stderr @@ -3,6 +3,16 @@ T3540.hs:4:12: error: • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’ • In the type signature: thing :: (a ~ Int) +T3540.hs:5:9: error: + • Couldn't match kind ‘Constraint’ with ‘*’ + When matching types + a0 :: * + a ~ Int :: Constraint + • In the expression: undefined + In an equation for ‘thing’: thing = undefined + • Relevant bindings include + thing :: a ~ Int (bound at T3540.hs:5:1) + T3540.hs:7:20: error: • Expected a type, but ‘a ~ Int’ has kind ‘Constraint’ • In the type signature: thing1 :: Int -> (a ~ Int) diff --git a/testsuite/tests/typecheck/should_fail/T7778.stderr b/testsuite/tests/typecheck/should_fail/T7778.stderr index a0f10fcd92..1993b772e0 100644 --- a/testsuite/tests/typecheck/should_fail/T7778.stderr +++ b/testsuite/tests/typecheck/should_fail/T7778.stderr @@ -1,4 +1,10 @@ +T7778.hs:3:6: error: + • Illegal qualified type: Num Int => Num + A constraint must be a monotype + Perhaps you intended to use QuantifiedConstraints + • In the type signature: v :: ((Num Int => Num) ()) => () + T7778.hs:3:7: error: • Expected kind ‘* -> Constraint’, but ‘Num Int => Num’ has kind ‘*’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail057.stderr b/testsuite/tests/typecheck/should_fail/tcfail057.stderr index 945c81c1cd..9ddffeb28b 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail057.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail057.stderr @@ -1,5 +1,13 @@ tcfail057.hs:5:7: error: • Expected a type, but ‘RealFrac a’ has kind ‘Constraint’ - • In the type signature: - f :: (RealFrac a) -> a -> a + • In the type signature: f :: (RealFrac a) -> a -> a + +tcfail057.hs:6:7: error: + • Couldn't match expected type ‘a -> a’ + with actual type ‘RealFrac a’ + • In the expression: x + In an equation for ‘f’: f x = x + • Relevant bindings include + x :: RealFrac a (bound at tcfail057.hs:6:3) + f :: RealFrac a => a -> a (bound at tcfail057.hs:6:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail058.stderr b/testsuite/tests/typecheck/should_fail/tcfail058.stderr index 478aa7f467..5150637cb9 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail058.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail058.stderr @@ -2,5 +2,24 @@ tcfail058.hs:6:7: error: • Expecting one more argument to ‘Array a’ Expected a constraint, but ‘Array a’ has kind ‘* -> *’ - • In the type signature: - f :: (Array a) => a -> b + • In the type signature: f :: (Array a) => a -> b + +tcfail058.hs:7:7: error: + • Could not deduce: a ~ b + from the context: Array a + bound by the type signature for: + f :: forall a b. Array a => a -> b + at tcfail058.hs:6:1-24 + ‘a’ is a rigid type variable bound by + the type signature for: + f :: forall a b. Array a => a -> b + at tcfail058.hs:6:1-24 + ‘b’ is a rigid type variable bound by + the type signature for: + f :: forall a b. Array a => a -> b + at tcfail058.hs:6:1-24 + • In the expression: x + In an equation for ‘f’: f x = x + • Relevant bindings include + x :: a (bound at tcfail058.hs:7:3) + f :: a -> b (bound at tcfail058.hs:7:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail063.stderr b/testsuite/tests/typecheck/should_fail/tcfail063.stderr index 935390e436..7dd1e9ce02 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail063.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail063.stderr @@ -2,5 +2,21 @@ tcfail063.hs:6:9: error: • Expecting one more argument to ‘Num’ Expected a constraint, but ‘Num’ has kind ‘* -> Constraint’ - • In the type signature: - moby :: Num => Int -> a -> Int + • In the type signature: moby :: Num => Int -> a -> Int + +tcfail063.hs:7:14: error: + • Could not deduce: a ~ Int + from the context: Num + bound by the type signature for: + moby :: forall a. Num => Int -> a -> Int + at tcfail063.hs:6:1-30 + ‘a’ is a rigid type variable bound by + the type signature for: + moby :: forall a. Num => Int -> a -> Int + at tcfail063.hs:6:1-30 + • In the second argument of ‘(+)’, namely ‘y’ + In the expression: x + y + In an equation for ‘moby’: moby x y = x + y + • Relevant bindings include + y :: a (bound at tcfail063.hs:7:8) + moby :: Int -> a -> Int (bound at tcfail063.hs:7:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail078.stderr b/testsuite/tests/typecheck/should_fail/tcfail078.stderr index 014d589bf6..a0816a746c 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail078.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail078.stderr @@ -2,3 +2,16 @@ tcfail078.hs:5:6: error: • Expected kind ‘* -> Constraint’, but ‘Integer’ has kind ‘*’ • In the type signature: f :: Integer i => i + +tcfail078.hs:6:19: error: + • Could not deduce (Num i) arising from the literal ‘0’ + from the context: Integer i + bound by the type signature for: + f :: forall i. Integer i => i + at tcfail078.hs:5:1-19 + Possible fix: + add (Num i) to the context of + the type signature for: + f :: forall i. Integer i => i + • In the expression: 0 + In an equation for ‘f’: f = 0 diff --git a/testsuite/tests/typecheck/should_fail/tcfail113.stderr b/testsuite/tests/typecheck/should_fail/tcfail113.stderr index fbdffa5ab9..80c97d2737 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail113.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail113.stderr @@ -4,11 +4,32 @@ tcfail113.hs:12:7: error: Expected a type, but ‘Maybe’ has kind ‘* -> *’ • In the type signature: f :: [Maybe] +tcfail113.hs:13:1: error: + • Couldn't match expected type ‘[Maybe]’ + with actual type ‘p1 -> p1’ + • The equation(s) for ‘f’ have one argument, + but its type ‘[Maybe]’ has none + • Relevant bindings include + f :: [Maybe] (bound at tcfail113.hs:13:1) + tcfail113.hs:15:8: error: • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’ • In the first argument of ‘T’, namely ‘Int’ In the type signature: g :: T Int +tcfail113.hs:16:1: error: + • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’ + • The equation(s) for ‘g’ have one argument, + but its type ‘T Int’ has none + • Relevant bindings include g :: T Int (bound at tcfail113.hs:16:1) + tcfail113.hs:18:6: error: • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’ • In the type signature: h :: Int Int + +tcfail113.hs:19:1: error: + • Couldn't match type ‘Int’ with ‘(->) Int’ + Expected type: Int Int + Actual type: Int -> Int + • The equation(s) for ‘h’ have one argument, + but its type ‘Int Int’ has none diff --git a/testsuite/tests/typecheck/should_fail/tcfail158.stderr b/testsuite/tests/typecheck/should_fail/tcfail158.stderr index 12f8a4e8df..995be74380 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail158.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail158.stderr @@ -1,6 +1,3 @@ -tcfail158.hs:14:19: error: - • Expecting one more argument to ‘Val v’ - Expected a type, but ‘Val v’ has kind ‘* -> *’ - • In the type signature: - bar :: forall v. Val v +tcfail158.hs:1:1: error: + The IO action ‘main’ is not defined in module ‘Main’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail160.stderr b/testsuite/tests/typecheck/should_fail/tcfail160.stderr index 46a7640cf9..400b2bf5a4 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail160.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail160.stderr @@ -2,5 +2,10 @@ tcfail160.hs:7:8: error: • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’ • In the first argument of ‘T’, namely ‘Int’ - In the type signature: - g :: T Int + In the type signature: g :: T Int + +tcfail160.hs:8:1: error: + • Couldn't match expected type ‘T Int’ with actual type ‘p0 -> p0’ + • The equation(s) for ‘g’ have one argument, + but its type ‘T Int’ has none + • Relevant bindings include g :: T Int (bound at tcfail160.hs:8:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail161.stderr b/testsuite/tests/typecheck/should_fail/tcfail161.stderr index ce783bb5ab..89042d1d20 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail161.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail161.stderr @@ -2,5 +2,12 @@ tcfail161.hs:5:7: error: • Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘* -> *’ - • In the type signature: - f :: [Maybe] + • In the type signature: f :: [Maybe] + +tcfail161.hs:6:1: error: + • Couldn't match expected type ‘[Maybe]’ + with actual type ‘p0 -> p0’ + • The equation(s) for ‘f’ have one argument, + but its type ‘[Maybe]’ has none + • Relevant bindings include + f :: [Maybe] (bound at tcfail161.hs:6:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr index 8eb7e6e57f..8ceab3e931 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr @@ -2,21 +2,31 @@ tcfail212.hs:10:7: error: • Expecting one more argument to ‘Maybe’ Expected a type, but ‘Maybe’ has kind ‘* -> *’ - • In the type signature: - f :: (Maybe, Either Int) + • In the type signature: f :: (Maybe, Either Int) tcfail212.hs:10:14: error: • Expecting one more argument to ‘Either Int’ Expected a type, but ‘Either Int’ has kind ‘* -> *’ - • In the type signature: - f :: (Maybe, Either Int) + • In the type signature: f :: (Maybe, Either Int) + +tcfail212.hs:11:6: error: + • Couldn't match expected type ‘Maybe’ + with actual type ‘Maybe Integer’ + • In the expression: Just 1 + In the expression: (Just 1, Left 1) + In an equation for ‘f’: f = (Just 1, Left 1) + +tcfail212.hs:11:14: error: + • Couldn't match expected type ‘Either Int’ + with actual type ‘Either Integer b0’ + • In the expression: Left 1 + In the expression: (Just 1, Left 1) + In an equation for ‘f’: f = (Just 1, Left 1) tcfail212.hs:13:7: error: • Expecting a lifted type, but ‘Int#’ is unlifted - • In the type signature: - g :: (Int#, Int#) + • In the type signature: g :: (Int#, Int#) tcfail212.hs:13:13: error: • Expecting a lifted type, but ‘Int#’ is unlifted - • In the type signature: - g :: (Int#, Int#) + • In the type signature: g :: (Int#, Int#) diff --git a/utils/haddock b/utils/haddock -Subproject 612f44f9a582b1f7c8a9ba709651bce83692b60 +Subproject a264b6b3e41dd42946110afcf5000341e5fb3a6 |