diff options
59 files changed, 400 insertions, 682 deletions
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index dca692ec83..d29fa4a9f9 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -3992,7 +3992,8 @@ wWarningFlagsDeps = [ flagSpec "hi-shadowing" Opt_WarnHiShadows, flagSpec "inaccessible-code" Opt_WarnInaccessibleCode, flagSpec "implicit-prelude" Opt_WarnImplicitPrelude, - flagSpec "implicit-kind-vars" Opt_WarnImplicitKindVars, + depFlagSpec "implicit-kind-vars" Opt_WarnImplicitKindVars + "it is now an error", flagSpec "incomplete-patterns" Opt_WarnIncompletePatterns, flagSpec "incomplete-record-updates" Opt_WarnIncompletePatternsRecUpd, flagSpec "incomplete-uni-patterns" Opt_WarnIncompleteUniPatterns, @@ -4830,7 +4831,6 @@ minusWcompatOpts = [ Opt_WarnMissingMonadFailInstances , Opt_WarnSemigroup , Opt_WarnNonCanonicalMonoidInstances - , Opt_WarnImplicitKindVars , Opt_WarnStarIsType ] diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index 0699f80858..5155f3ab84 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -727,15 +727,11 @@ rnFamInstEqn doc mb_cls rhs_kvars ; let pat_kity_vars_with_dups = extractHsTyArgRdrKiTyVarsDup pats -- Use the "...Dups" form because it's needed -- below to report unsed binder on the LHS - ; let pat_kity_vars = rmDupsInRdrTyVars pat_kity_vars_with_dups - - -- all pat vars not explicitly bound (see extractHsTvBndrs) - ; let mb_imp_kity_vars = extractHsTvBndrs <$> mb_bndrs <*> pure pat_kity_vars - imp_vars = case mb_imp_kity_vars of - -- kind vars are the only ones free if we have an explicit forall - Just nbnd_kity_vars -> freeKiTyVarsKindVars nbnd_kity_vars - -- all pattern vars are free otherwise - Nothing -> freeKiTyVarsAllVars pat_kity_vars + + -- Implicitly bound variables, empty if we have an explicit 'forall' according + -- to the "forall-or-nothing" rule. + ; let imp_vars | isNothing mb_bndrs = nubL pat_kity_vars_with_dups + | otherwise = [] ; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars ; let bndrs = fromMaybe [] mb_bndrs @@ -766,7 +762,7 @@ rnFamInstEqn doc mb_cls rhs_kvars -- See Note [Unused type variables in family instances] ; let groups :: [NonEmpty (Located RdrName)] groups = equivClasses cmpLocated $ - freeKiTyVarsAllVars pat_kity_vars_with_dups + pat_kity_vars_with_dups ; nms_dups <- mapM (lookupOccRn . unLoc) $ [ tv | (tv :| (_:_)) <- groups ] -- Add to the used variables diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index 8e390f0e17..499fd74bd9 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -26,14 +26,11 @@ module RnTypes ( -- Binding related stuff bindLHsTyVarBndr, bindLHsTyVarBndrs, rnImplicitBndrs, bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames, - extractFilteredRdrTyVars, extractFilteredRdrTyVarsDups, extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars, - extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars, - extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars, + extractHsTysRdrTyVarsDups, extractRdrKindSigVars, extractDataDefnKindVars, extractHsTvBndrs, extractHsTyArgRdrKiTyVarsDup, - freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars, - elemRdr + nubL, elemRdr ) where import GhcPrelude @@ -127,7 +124,7 @@ rn_hs_sig_wc_type scoping ctxt (HsWC { hswc_body = HsIB { hsib_body = hs_ty }}) thing_inside = do { free_vars <- extractFilteredRdrTyVarsDups hs_ty - ; (tv_rdrs, nwc_rdrs') <- partition_nwcs free_vars + ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars ; let nwc_rdrs = nubL nwc_rdrs' bind_free_tvs = case scoping of AlwaysBind -> True @@ -148,7 +145,7 @@ rn_hs_sig_wc_type _ _ (XHsWildCardBndrs _) _ rnHsWcType :: HsDocContext -> LHsWcType GhcPs -> RnM (LHsWcType GhcRn, FreeVars) rnHsWcType ctxt (HsWC { hswc_body = hs_ty }) = do { free_vars <- extractFilteredRdrTyVars hs_ty - ; (_, nwc_rdrs) <- partition_nwcs free_vars + ; (nwc_rdrs, _) <- partition_nwcs free_vars ; (wcs, hs_ty', fvs) <- rnWcBody ctxt nwc_rdrs hs_ty ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = hs_ty' } ; return (sig_ty', fvs) } @@ -251,9 +248,7 @@ extraConstraintWildCardsAllowed env -- NB: this includes named wildcards, which look like perfectly -- ordinary type variables at this point extractFilteredRdrTyVars :: LHsType GhcPs -> RnM FreeKiTyVarsNoDups -extractFilteredRdrTyVars hs_ty - = do { rdr_env <- getLocalRdrEnv - ; return (filterInScope rdr_env (extractHsTyRdrTyVars hs_ty)) } +extractFilteredRdrTyVars hs_ty = filterInScopeM (extractHsTyRdrTyVars hs_ty) -- | Finds free type and kind variables in a type, -- with duplicates, but @@ -261,22 +256,20 @@ extractFilteredRdrTyVars hs_ty -- NB: this includes named wildcards, which look like perfectly -- ordinary type variables at this point extractFilteredRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups -extractFilteredRdrTyVarsDups hs_ty - = do { rdr_env <- getLocalRdrEnv - ; return (filterInScope rdr_env (extractHsTyRdrTyVarsDups hs_ty)) } +extractFilteredRdrTyVarsDups hs_ty = filterInScopeM (extractHsTyRdrTyVarsDups hs_ty) -- | When the NamedWildCards extension is enabled, partition_nwcs -- removes type variables that start with an underscore from the -- FreeKiTyVars in the argument and returns them in a separate list. -- When the extension is disabled, the function returns the argument -- and empty list. See Note [Renaming named wild cards] -partition_nwcs :: FreeKiTyVars -> RnM (FreeKiTyVars, [Located RdrName]) -partition_nwcs free_vars@(FKTV { fktv_tys = tys }) - = do { wildcards_enabled <- fmap (xopt LangExt.NamedWildCards) getDynFlags - ; let (nwcs, no_nwcs) | wildcards_enabled = partition is_wildcard tys - | otherwise = ([], tys) - free_vars' = free_vars { fktv_tys = no_nwcs } - ; return (free_vars', nwcs) } +partition_nwcs :: FreeKiTyVars -> RnM ([Located RdrName], FreeKiTyVars) +partition_nwcs free_vars + = do { wildcards_enabled <- xoptM LangExt.NamedWildCards + ; return $ + if wildcards_enabled + then partition is_wildcard free_vars + else ([], free_vars) } where is_wildcard :: Located RdrName -> Bool is_wildcard rdr = startsWithUnderscore (rdrNameOcc (unLoc rdr)) @@ -326,51 +319,20 @@ rnImplicitBndrs :: Bool -- True <=> bring into scope any free type variables -> ([Name] -> RnM (a, FreeVars)) -> RnM (a, FreeVars) rnImplicitBndrs bind_free_tvs - fvs_with_dups@(FKTV { fktv_kis = kvs_with_dups - , fktv_tys = tvs_with_dups }) + fvs_with_dups thing_inside - = do { let FKTV kvs tvs = rmDupsInRdrTyVars fvs_with_dups - real_tvs | bind_free_tvs = tvs + = do { let fvs = nubL fvs_with_dups + real_fvs | bind_free_tvs = fvs | otherwise = [] - -- We always bind over free /kind/ variables. - -- Bind free /type/ variables only if there is no - -- explicit forall. E.g. - -- f :: Proxy (a :: k) -> b - -- Quantify over {k} and {a,b} - -- g :: forall a. Proxy (a :: k) -> b - -- Quantify over {k} and {} - -- Note that we always do the implicit kind-quantification - -- but, rather arbitrarily, we switch off the type-quantification - -- if there is an explicit forall - - ; traceRn "rnImplicitBndrs" (vcat [ ppr kvs, ppr tvs, ppr real_tvs ]) - - ; whenWOptM Opt_WarnImplicitKindVars $ - unless (bind_free_tvs || null kvs) $ - addWarnAt (Reason Opt_WarnImplicitKindVars) (getLoc (head kvs)) $ - implicit_kind_vars_msg kvs - ; loc <- getSrcSpanM - -- NB: kinds before tvs, as mandated by - -- Note [Ordering of implicit variables] - ; vars <- mapM (newLocalBndrRn . cL loc . unLoc) (kvs ++ real_tvs) + ; traceRn "rnImplicitBndrs" $ + vcat [ ppr fvs_with_dups, ppr fvs, ppr real_fvs ] - ; traceRn "checkMixedVars2" $ - vcat [ text "kvs_with_dups" <+> ppr kvs_with_dups - , text "tvs_with_dups" <+> ppr tvs_with_dups ] + ; loc <- getSrcSpanM + ; vars <- mapM (newLocalBndrRn . cL loc . unLoc) real_fvs ; bindLocalNamesFV vars $ thing_inside vars } - where - implicit_kind_vars_msg kvs = - vcat [ text "An explicit" <+> quotes (text "forall") <+> - text "was used, but the following kind variables" <+> - text "are not quantified:" <+> - hsep (punctuate comma (map (quotes . ppr) kvs)) - , text "Despite this fact, GHC will introduce them into scope," <+> - text "but it will stop doing so in the future." - , text "Suggested fix: add" <+> - quotes (text "forall" <+> hsep (map ppr kvs) <> char '.') ] {- ****************************************************** * * @@ -1474,8 +1436,7 @@ opTyErr op overall_ty Note [Kind and type-variable binders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In a type signature we may implicitly bind type variable and, more -recently, kind variables. For example: +In a type signature we may implicitly bind type/kind variables. For example: * f :: a -> a f = ... Here we need to find the free type variables of (a -> a), @@ -1493,42 +1454,11 @@ recently, kind variables. For example: * type instance F (T (a :: Maybe k)) = ...a...k... Here we want to constrain the kind of 'a', and bind 'k'. -In general we want to walk over a type, and find - * Its free type variables - * The free kind variables of any kind signatures in the type - -Hence we return a pair (kind-vars, type vars) -(See Note [HsBSig binder lists] in HsTypes.) -Moreover, we preserve the left-to-right order of the first occurrence of each -variable, while preserving dependency order. -(See Note [Ordering of implicit variables].) - -Most clients of this code just want to know the kind/type vars, without -duplicates. The function rmDupsInRdrTyVars removes duplicates. That function -also makes sure that no variable is reported as both a kind var and -a type var, preferring kind vars. Why kind vars? Consider this: - - foo :: forall (a :: k). Proxy k -> Proxy a -> ... +To do that, we need to walk over a type and find its free type/kind variables. +We preserve the left-to-right order of each variable occurrence. +See Note [Ordering of implicit variables]. -Should that be accepted? - -Normally, if a type signature has an explicit forall, it must list *all* -tyvars mentioned in the type. But there's an exception for tyvars mentioned in -a kind, as k is above. Note that k is also used "as a type variable", as the -argument to the first Proxy. So, do we consider k to be type-variable-like and -require it in the forall? Or do we consider k to be kind-variable-like and not -require it? - -It's not just in type signatures: kind variables are implicitly brought into -scope in a variety of places. Should vars used at both the type level and kind -level be treated this way? - -GHC indeed allows kind variables to be brought into scope implicitly even when -the kind variable is also used as a type variable. Thus, we must prefer to keep -a variable listed as a kind var in rmDupsInRdrTyVars. If we kept it as a type -var, then this would prevent it from being implicitly quantified (see -rnImplicitBndrs). In the `foo` example above, that would have the consequence -of the k in Proxy k being reported as out of scope. +Clients of this code can remove duplicates with nubL. Note [Ordering of implicit variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1558,30 +1488,98 @@ See Note [ScopedSort] in Type. Implicitly bound variables are collected by any function which returns a FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably -includes the `extract-` family of functions (extractHsTysRdrTyVars, +includes the `extract-` family of functions (extractHsTysRdrTyVarsDups, extractHsTyVarBndrsKVs, etc.). These functions thus promise to keep left-to-right ordering. -Look for pointers to this note to see the places where the action happens. - -Note that we also maintain this ordering in kind signatures. Even though -there's no visible kind application (yet), having implicit variables be -quantified in left-to-right order in kind signatures is nice since: - -* It's consistent with the treatment for type signatures. -* It can affect how types are displayed with -fprint-explicit-kinds (see - #15568 for an example), which is a situation where knowing the order in - which implicit variables are quantified can be useful. -* In the event that visible kind application is implemented, the order in - which we would expect implicit variables to be ordered in kinds will have - already been established. + +Note [Implicit quantification in type synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We typically bind type/kind variables implicitly when they are in a kind +annotation on the LHS, for example: + + data Proxy (a :: k) = Proxy + type KindOf (a :: k) = k + +Here 'k' is in the kind annotation of a type variable binding, KindedTyVar, and +we want to implicitly quantify over it. This is easy: just extract all free +variables from the kind signature. That's what we do in extract_hs_tv_bndrs_kvs + +By contrast, on the RHS we can't simply collect *all* free variables. Which of +the following are allowed? + + type TySyn1 = a :: Type + type TySyn2 = 'Nothing :: Maybe a + type TySyn3 = 'Just ('Nothing :: Maybe a) + type TySyn4 = 'Left a :: Either Type a + +After some design deliberations (see non-taken alternatives below), the answer +is to reject TySyn1 and TySyn3, but allow TySyn2 and TySyn4, at least for now. +We implicitly quantify over free variables of the outermost kind signature, if +one exists: + + * In TySyn1, the outermost kind signature is (:: Type), and it does not have + any free variables. + * In TySyn2, the outermost kind signature is (:: Maybe a), it contains a + free variable 'a', which we implicitly quantify over. + * In TySyn3, there is no outermost kind signature. The (:: Maybe a) signature + is hidden inside 'Just. + * In TySyn4, the outermost kind signature is (:: Either Type a), it contains + a free variable 'a', which we implicitly quantify over. That is why we can + also use it to the left of the double colon: 'Left a + +The logic resides in extractHsTyRdrTyVarsKindVars. We use it both for type +synonyms and type family instances. + +This is something of a stopgap solution until we can explicitly bind invisible +type/kind variables: + + type TySyn3 :: forall a. Maybe a + type TySyn3 @a = 'Just ('Nothing :: Maybe a) + +Note [Implicit quantification in type synonyms: non-taken alternatives] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Alternative I: No quantification +-------------------------------- +We could offer no implicit quantification on the RHS, accepting none of the +TySyn<N> examples. The user would have to bind the variables explicitly: + + type TySyn1 a = a :: Type + type TySyn2 a = 'Nothing :: Maybe a + type TySyn3 a = 'Just ('Nothing :: Maybe a) + type TySyn4 a = 'Left a :: Either Type a + +However, this would mean that one would have to specify 'a' at call sites every +time, which could be undesired. + +Alternative II: Indiscriminate quantification +--------------------------------------------- +We could implicitly quantify over all free variables on the RHS just like we do +on the LHS. Then we would infer the following kinds: + + TySyn1 :: forall {a}. Type + TySyn2 :: forall {a}. Maybe a + TySyn3 :: forall {a}. Maybe (Maybe a) + TySyn4 :: forall {a}. Either Type a + +This would work fine for TySyn<2,3,4>, but TySyn1 is clearly bogus: the variable +is free-floating, not fixed by anything. + +Alternative III: reportFloatingKvs +---------------------------------- +We could augment Alternative II by hunting down free-floating variables during +type checking. While viable, this would mean we'd end up accepting this: + + data Prox k (a :: k) + type T = Prox k + -} -- See Note [Kind and type-variable binders] -- These lists are guaranteed to preserve left-to-right ordering of -- the types the variables were extracted from. See also -- Note [Ordering of implicit variables]. -data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName] - , fktv_tys :: [Located RdrName] } +type FreeKiTyVars = [Located RdrName] -- | A 'FreeKiTyVars' list that is allowed to have duplicate variables. type FreeKiTyVarsWithDups = FreeKiTyVars @@ -1589,94 +1587,70 @@ type FreeKiTyVarsWithDups = FreeKiTyVars -- | A 'FreeKiTyVars' list that contains no duplicate variables. type FreeKiTyVarsNoDups = FreeKiTyVars -instance Outputable FreeKiTyVars where - ppr (FKTV { fktv_kis = kis, fktv_tys = tys}) = ppr (kis, tys) - -emptyFKTV :: FreeKiTyVarsNoDups -emptyFKTV = FKTV { fktv_kis = [], fktv_tys = [] } - -freeKiTyVarsAllVars :: FreeKiTyVars -> [Located RdrName] -freeKiTyVarsAllVars (FKTV { fktv_kis = kvs, fktv_tys = tvs }) = kvs ++ tvs - -freeKiTyVarsKindVars :: FreeKiTyVars -> [Located RdrName] -freeKiTyVarsKindVars = fktv_kis - -freeKiTyVarsTypeVars :: FreeKiTyVars -> [Located RdrName] -freeKiTyVarsTypeVars = fktv_tys - filterInScope :: LocalRdrEnv -> FreeKiTyVars -> FreeKiTyVars -filterInScope rdr_env (FKTV { fktv_kis = kis, fktv_tys = tys }) - = FKTV { fktv_kis = filterOut in_scope kis - , fktv_tys = filterOut in_scope tys } - where - in_scope = inScope rdr_env . unLoc +filterInScope rdr_env = filterOut (inScope rdr_env . unLoc) + +filterInScopeM :: FreeKiTyVars -> RnM FreeKiTyVars +filterInScopeM vars + = do { rdr_env <- getLocalRdrEnv + ; return (filterInScope rdr_env vars) } inScope :: LocalRdrEnv -> RdrName -> Bool inScope rdr_env rdr = rdr `elemLocalRdrEnv` rdr_env --- | 'extractHsTyRdrTyVars' finds the --- free (kind, type) variables of an 'HsType' --- or the free (sort, kind) variables of an 'HsKind'. --- It's used when making the @forall@s explicit. --- Does not return any wildcards. --- When the same name occurs multiple times in the types, only the first --- occurrence is returned. --- See Note [Kind and type-variable binders] - - extract_tyarg :: LHsTypeArg GhcPs -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_tyarg (HsValArg ty) acc = extract_lty TypeLevel ty acc -extract_tyarg (HsTypeArg _ ki) acc = extract_lty KindLevel ki acc +extract_tyarg (HsValArg ty) acc = extract_lty ty acc +extract_tyarg (HsTypeArg _ ki) acc = extract_lty ki acc extract_tyarg (HsArgPar _) acc = acc extract_tyargs :: [LHsTypeArg GhcPs] -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups extract_tyargs args acc = foldr extract_tyarg acc args extractHsTyArgRdrKiTyVarsDup :: [LHsTypeArg GhcPs] -> FreeKiTyVarsWithDups -extractHsTyArgRdrKiTyVarsDup args = extract_tyargs args emptyFKTV +extractHsTyArgRdrKiTyVarsDup args + = extract_tyargs args [] +-- | 'extractHsTyRdrTyVars' finds the type/kind variables +-- of a HsType/HsKind. +-- It's used when making the @forall@s explicit. +-- When the same name occurs multiple times in the types, only the first +-- occurrence is returned. +-- See Note [Kind and type-variable binders] extractHsTyRdrTyVars :: LHsType GhcPs -> FreeKiTyVarsNoDups extractHsTyRdrTyVars ty - = rmDupsInRdrTyVars (extractHsTyRdrTyVarsDups ty) + = nubL (extractHsTyRdrTyVarsDups ty) --- | 'extractHsTyRdrTyVarsDups' find the --- free (kind, type) variables of an 'HsType' --- or the free (sort, kind) variables of an 'HsKind'. +-- | 'extractHsTyRdrTyVarsDups' finds the type/kind variables +-- of a HsType/HsKind. -- It's used when making the @forall@s explicit. --- Does not return any wildcards. -- When the same name occurs multiple times in the types, all occurrences -- are returned. extractHsTyRdrTyVarsDups :: LHsType GhcPs -> FreeKiTyVarsWithDups extractHsTyRdrTyVarsDups ty - = extract_lty TypeLevel ty emptyFKTV + = extract_lty ty [] --- | Extracts the free kind variables (but not the type variables) of an --- 'HsType'. Does not return any wildcards. +-- | Extracts the free type/kind variables from the kind signature of a HsType. +-- This is used to implicitly quantify over @k@ in @type T = Nothing :: Maybe k@. -- When the same name occurs multiple times in the type, only the first -- occurrence is returned, and the left-to-right order of variables is -- preserved. -- See Note [Kind and type-variable binders] and --- Note [Ordering of implicit variables]. -extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> [Located RdrName] -extractHsTyRdrTyVarsKindVars ty - = freeKiTyVarsKindVars (extractHsTyRdrTyVars ty) - --- | Extracts free type and kind variables from types in a list. --- When the same name occurs multiple times in the types, only the first --- occurrence is returned and the rest is filtered out. --- See Note [Kind and type-variable binders] -extractHsTysRdrTyVars :: [LHsType GhcPs] -> FreeKiTyVarsNoDups -extractHsTysRdrTyVars tys - = rmDupsInRdrTyVars (extractHsTysRdrTyVarsDups tys) +-- Note [Ordering of implicit variables] and +-- Note [Implicit quantification in type synonyms]. +extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> FreeKiTyVarsNoDups +extractHsTyRdrTyVarsKindVars (unLoc -> ty) = + case ty of + HsParTy _ ty -> extractHsTyRdrTyVarsKindVars ty + HsKindSig _ _ ki -> extractHsTyRdrTyVars ki + _ -> [] -- | Extracts free type and kind variables from types in a list. -- When the same name occurs multiple times in the types, all occurrences -- are returned. extractHsTysRdrTyVarsDups :: [LHsType GhcPs] -> FreeKiTyVarsWithDups extractHsTysRdrTyVarsDups tys - = extract_ltys TypeLevel tys emptyFKTV + = extract_ltys tys [] -extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> [Located RdrName] -- Returns the free kind variables of any explictly-kinded binders, returning -- variable occurrences in left-to-right order. -- See Note [Ordering of implicit variables]. @@ -1684,124 +1658,76 @@ extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> [Located RdrName] -- However duplicates are removed -- E.g. given [k1, a:k1, b:k2] -- the function returns [k1,k2], even though k1 is bound here +extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> FreeKiTyVarsNoDups extractHsTyVarBndrsKVs tv_bndrs = nubL (extract_hs_tv_bndrs_kvs tv_bndrs) --- | Removes multiple occurrences of the same name from FreeKiTyVars. If a --- variable occurs as both a kind and a type variable, only keep the occurrence --- as a kind variable. --- See also Note [Kind and type-variable binders] -rmDupsInRdrTyVars :: FreeKiTyVarsWithDups -> FreeKiTyVarsNoDups -rmDupsInRdrTyVars (FKTV { fktv_kis = kis, fktv_tys = tys }) - = FKTV { fktv_kis = kis' - , fktv_tys = nubL (filterOut (`elemRdr` kis') tys) } - where - kis' = nubL kis - -extractRdrKindSigVars :: LFamilyResultSig GhcPs -> [Located RdrName] -- Returns the free kind variables in a type family result signature, returning -- variable occurrences in left-to-right order. -- See Note [Ordering of implicit variables]. +extractRdrKindSigVars :: LFamilyResultSig GhcPs -> [Located RdrName] extractRdrKindSigVars (dL->L _ resultSig) - | KindSig _ k <- resultSig = kindRdrNameFromSig k - | TyVarSig _ (dL->L _ (KindedTyVar _ _ k)) <- resultSig = kindRdrNameFromSig k + | KindSig _ k <- resultSig = extractHsTyRdrTyVars k + | TyVarSig _ (dL->L _ (KindedTyVar _ _ k)) <- resultSig = extractHsTyRdrTyVars k | otherwise = [] - where - kindRdrNameFromSig k = freeKiTyVarsAllVars (extractHsTyRdrTyVars k) -extractDataDefnKindVars :: HsDataDefn GhcPs -> [Located RdrName] --- Get the scoped kind variables mentioned free in the constructor decls --- Eg: data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) --- Here k should scope over the whole definition +-- Get type/kind variables mentioned in the kind signature, preserving +-- left-to-right order and without duplicates: -- --- However, do NOT collect free kind vars from the deriving clauses: --- Eg: (Trac #14331) class C p q --- data D = D deriving ( C (a :: k) ) --- Here k should /not/ scope over the whole definition. We intend --- this to elaborate to: --- class C @k1 @k2 (p::k1) (q::k2) --- data D = D --- instance forall k (a::k). C @k @* a D where ... +-- * data T a (b :: k1) :: k2 -> k1 -> k2 -> Type -- result: [k2,k1] +-- * data T a (b :: k1) -- result: [] -- --- This returns variable occurrences in left-to-right order. -- See Note [Ordering of implicit variables]. -extractDataDefnKindVars (HsDataDefn { dd_ctxt = ctxt, dd_kindSig = ksig - , dd_cons = cons }) - = (nubL . freeKiTyVarsKindVars) $ - (extract_lctxt TypeLevel ctxt $ - extract_mb extract_lkind ksig $ - foldr (extract_con . unLoc) emptyFKTV cons) - where - extract_con (ConDeclGADT { }) acc = acc - extract_con (ConDeclH98 { con_ex_tvs = ex_tvs - , con_mb_cxt = ctxt, con_args = args }) acc - = extract_hs_tv_bndrs ex_tvs acc $ - extract_mlctxt ctxt $ - extract_ltys TypeLevel (hsConDeclArgTys args) emptyFKTV - extract_con (XConDecl { }) _ = panic "extractDataDefnKindVars" +extractDataDefnKindVars :: HsDataDefn GhcPs -> FreeKiTyVarsNoDups +extractDataDefnKindVars (HsDataDefn { dd_kindSig = ksig }) + = maybe [] extractHsTyRdrTyVars ksig extractDataDefnKindVars (XHsDataDefn _) = panic "extractDataDefnKindVars" -extract_mlctxt :: Maybe (LHsContext GhcPs) - -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_mlctxt Nothing acc = acc -extract_mlctxt (Just ctxt) acc = extract_lctxt TypeLevel ctxt acc - -extract_lctxt :: TypeOrKind - -> LHsContext GhcPs +extract_lctxt :: LHsContext GhcPs -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_lctxt t_or_k ctxt = extract_ltys t_or_k (unLoc ctxt) +extract_lctxt ctxt = extract_ltys (unLoc ctxt) -extract_ltys :: TypeOrKind - -> [LHsType GhcPs] +extract_ltys :: [LHsType GhcPs] -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_ltys t_or_k tys acc = foldr (extract_lty t_or_k) acc tys +extract_ltys tys acc = foldr extract_lty acc tys -extract_mb :: (a -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups) - -> Maybe a - -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_mb _ Nothing acc = acc -extract_mb f (Just x) acc = f x acc - -extract_lkind :: LHsType GhcPs -> FreeKiTyVars -> FreeKiTyVars -extract_lkind = extract_lty KindLevel - -extract_lty :: TypeOrKind -> LHsType GhcPs +extract_lty :: LHsType GhcPs -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_lty t_or_k (dL->L _ ty) acc +extract_lty (dL->L _ ty) acc = case ty of - HsTyVar _ _ ltv -> extract_tv t_or_k ltv acc - HsBangTy _ _ ty -> extract_lty t_or_k ty acc - HsRecTy _ flds -> foldr (extract_lty t_or_k + HsTyVar _ _ ltv -> extract_tv ltv acc + HsBangTy _ _ ty -> extract_lty ty acc + HsRecTy _ flds -> foldr (extract_lty . cd_fld_type . unLoc) acc flds - HsAppTy _ ty1 ty2 -> extract_lty t_or_k ty1 $ - extract_lty t_or_k ty2 acc - HsAppKindTy _ ty k -> extract_lty t_or_k ty $ - extract_lty KindLevel k acc - HsListTy _ ty -> extract_lty t_or_k ty acc - HsTupleTy _ _ tys -> extract_ltys t_or_k tys acc - HsSumTy _ tys -> extract_ltys t_or_k tys acc - HsFunTy _ ty1 ty2 -> extract_lty t_or_k ty1 $ - extract_lty t_or_k ty2 acc - HsIParamTy _ _ ty -> extract_lty t_or_k ty acc - HsOpTy _ ty1 tv ty2 -> extract_tv t_or_k tv $ - extract_lty t_or_k ty1 $ - extract_lty t_or_k ty2 acc - HsParTy _ ty -> extract_lty t_or_k ty acc + HsAppTy _ ty1 ty2 -> extract_lty ty1 $ + extract_lty ty2 acc + HsAppKindTy _ ty k -> extract_lty ty $ + extract_lty k acc + HsListTy _ ty -> extract_lty ty acc + HsTupleTy _ _ tys -> extract_ltys tys acc + HsSumTy _ tys -> extract_ltys tys acc + HsFunTy _ ty1 ty2 -> extract_lty ty1 $ + extract_lty ty2 acc + HsIParamTy _ _ ty -> extract_lty ty acc + HsOpTy _ ty1 tv ty2 -> extract_tv tv $ + extract_lty ty1 $ + extract_lty ty2 acc + HsParTy _ ty -> extract_lty ty acc HsSpliceTy {} -> acc -- Type splices mention no tvs - HsDocTy _ ty _ -> extract_lty t_or_k ty acc - HsExplicitListTy _ _ tys -> extract_ltys t_or_k tys acc - HsExplicitTupleTy _ tys -> extract_ltys t_or_k tys acc + HsDocTy _ ty _ -> extract_lty ty acc + HsExplicitListTy _ _ tys -> extract_ltys tys acc + HsExplicitTupleTy _ tys -> extract_ltys tys acc HsTyLit _ _ -> acc HsStarTy _ _ -> acc - HsKindSig _ ty ki -> extract_lty t_or_k ty $ - extract_lkind ki acc + HsKindSig _ ty ki -> extract_lty ty $ + extract_lty ki acc HsForAllTy { hst_bndrs = tvs, hst_body = ty } -> extract_hs_tv_bndrs tvs acc $ - extract_lty t_or_k ty emptyFKTV + extract_lty ty [] HsQualTy { hst_ctxt = ctxt, hst_body = ty } - -> extract_lctxt t_or_k ctxt $ - extract_lty t_or_k ty acc + -> extract_lctxt ctxt $ + extract_lty ty acc XHsType {} -> acc -- We deal with these separately in rnLHsTypeWithWildCards HsWildCardTy {} -> acc @@ -1810,7 +1736,7 @@ extractHsTvBndrs :: [LHsTyVarBndr GhcPs] -> FreeKiTyVarsWithDups -- Free in body -> FreeKiTyVarsWithDups -- Free in result extractHsTvBndrs tv_bndrs body_fvs - = extract_hs_tv_bndrs tv_bndrs emptyFKTV body_fvs + = extract_hs_tv_bndrs tv_bndrs [] body_fvs extract_hs_tv_bndrs :: [LHsTyVarBndr GhcPs] -> FreeKiTyVarsWithDups -- Accumulator @@ -1820,27 +1746,14 @@ extract_hs_tv_bndrs :: [LHsTyVarBndr GhcPs] -- 'a' is bound by the forall -- 'b' is a free type variable -- 'e' is a free kind variable -extract_hs_tv_bndrs tv_bndrs - (FKTV { fktv_kis = acc_kvs, fktv_tys = acc_tvs }) -- Accumulator - (FKTV { fktv_kis = body_kvs, fktv_tys = body_tvs }) -- Free in the body - | null tv_bndrs - = FKTV { fktv_kis = body_kvs ++ acc_kvs - , fktv_tys = body_tvs ++ acc_tvs } - | otherwise - = FKTV { fktv_kis = filterOut (`elemRdr` tv_bndr_rdrs) all_kv_occs - -- NB: delete all tv_bndr_rdrs from bndr_kvs as well - -- as body_kvs; see Note [Kind variable scoping] - ++ acc_kvs - , fktv_tys = filterOut (`elemRdr` tv_bndr_rdrs) body_tvs ++ acc_tvs } +extract_hs_tv_bndrs tv_bndrs acc_vars body_vars + | null tv_bndrs = body_vars ++ acc_vars + | otherwise = filterOut (`elemRdr` tv_bndr_rdrs) (bndr_vars ++ body_vars) ++ acc_vars + -- NB: delete all tv_bndr_rdrs from bndr_vars as well as body_vars. + -- See Note [Kind variable scoping] where - bndr_kvs = extract_hs_tv_bndrs_kvs tv_bndrs - - tv_bndr_rdrs, all_kv_occs :: [Located RdrName] + bndr_vars = extract_hs_tv_bndrs_kvs tv_bndrs tv_bndr_rdrs = map hsLTyVarLocName tv_bndrs - all_kv_occs = bndr_kvs ++ body_kvs - -- We must include both kind variables from the binding as well - -- as the body of the `forall` type. - -- See Note [Variables used as both types and kinds]. extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> [Located RdrName] -- Returns the free kind variables of any explictly-kinded binders, returning @@ -1850,17 +1763,14 @@ extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> [Located RdrName] -- Duplicates are /not/ removed -- E.g. given [k1, a:k1, b:k2] -- the function returns [k1,k2], even though k1 is bound here -extract_hs_tv_bndrs_kvs tv_bndrs - = freeKiTyVarsKindVars $ -- There will /be/ no free tyvars! - foldr extract_lkind emptyFKTV +extract_hs_tv_bndrs_kvs tv_bndrs = + foldr extract_lty [] [k | (dL->L _ (KindedTyVar _ _ k)) <- tv_bndrs] -extract_tv :: TypeOrKind -> Located RdrName - -> FreeKiTyVarsWithDups -> FreeKiTyVarsWithDups -extract_tv t_or_k ltv@(dL->L _ tv) acc@(FKTV kvs tvs) - | not (isRdrTyVar tv) = acc - | isTypeLevel t_or_k = FKTV { fktv_kis = kvs, fktv_tys = ltv : tvs } - | otherwise = FKTV { fktv_kis = ltv : kvs, fktv_tys = tvs } +extract_tv :: Located RdrName + -> [Located RdrName] -> [Located RdrName] +extract_tv tv acc = + if isRdrTyVar (unLoc tv) then tv:acc else acc -- Deletes duplicates in a list of Located things. -- diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 467c60465a..ef038e119b 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -47,7 +47,6 @@ module TcHsType ( typeLevelMode, kindLevelMode, kindGeneralize, checkExpectedKind_pp, - reportFloatingKvs, -- Sort-checking kinds tcLHsKindSig, badKindSig, @@ -1871,13 +1870,6 @@ kcLHsQTyVars_Cusk name flav -- doesn't work, we catch it here, before an error cascade ; checkValidTelescope tycon - -- If any of the specified tyvars aren't actually mentioned in a binder's - -- kind (or the return kind), then we're in the CUSK case from - -- Note [Free-floating kind vars] - ; let unmentioned_kvs = filterOut (`elemVarSet` mentioned_kv_set) specified - ; reportFloatingKvs name flav (map binderVar final_tc_binders) unmentioned_kvs - - ; traceTc "kcLHsQTyVars: cusk" $ vcat [ text "name" <+> ppr name , text "kv_ns" <+> ppr kv_ns @@ -2889,8 +2881,6 @@ promotionErr name err NoDataKindsTC -> text "perhaps you intended to use DataKinds" NoDataKindsDC -> text "perhaps you intended to use DataKinds" PatSynPE -> text "pattern synonyms cannot be promoted" - PatSynExPE -> sep [ text "the existential variables of a pattern synonym" - , text "signature do not scope over the pattern" ] _ -> text "it is defined and used in the same recursive group" {- @@ -2919,112 +2909,6 @@ badPatTyVarTvs sig_ty bad_tvs -} -{- Note [Free-floating kind vars] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - - data S a = MkS (Proxy (a :: k)) - -According to the rules around implicitly-bound kind variables, -that k scopes over the whole declaration. The renamer grabs -it and adds it to the hsq_implicits field of the HsQTyVars of the -tycon. So we get - S :: forall {k}. k -> Type - -That's fine. But consider this variant: - data T = MkT (forall (a :: k). Proxy a) - -- from test ghci/scripts/T7873 - -This is not an existential datatype, but a higher-rank one (the forall -to the right of MkT). Again, 'k' scopes over the whole declaration, -but we do not want to get - T :: forall {k}. Type -Why not? Because the kind variable isn't fixed by anything. For -a variable like k to be implicit, it needs to be mentioned in the kind -of a tycon tyvar. But it isn't. - -Rejecting T depends on whether or not the datatype has a CUSK. - -Non-CUSK (handled in TcTyClsDecls.kcTyClGroup (generalise)): - When generalising the TyCon we check that every Specified 'k' - appears free in the kind of the TyCon; that is, in the kind of - one of its Required arguments, or the result kind. - -CUSK (handled in TcHsType.kcLHsQTyVars, the CUSK case): - When we determine the tycon's final, never-to-be-changed kind - in kcLHsQTyVars, we check to make sure all implicitly-bound kind - vars are indeed mentioned in a kind somewhere. If not, error. - -We also perform free-floating kind var analysis for type family instances -(see #13985). Here is an interesting example: - - type family T :: k - type instance T = (Nothing :: Maybe a) - -Upon a cursory glance, it may appear that the kind variable `a` is -free-floating above, since there are no (visible) LHS patterns in `T`. However, -there is an *invisible* pattern due to the return kind, so inside of GHC, the -instance looks closer to this: - - type family T @k :: k - type instance T @(Maybe a) = (Nothing :: Maybe a) - -Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in -fact not free-floating. Contrast that with this example: - - type instance T = Proxy (Nothing :: Maybe a) - -This would looks like this inside of GHC: - - type instance T @(*) = Proxy (Nothing :: Maybe a) - -So this time, `a` is neither bound by a visible nor invisible type pattern on -the LHS, so it would be reported as free-floating. - -Finally, here's one more brain-teaser (from #9574). In the example below: - - class Funct f where - type Codomain f :: * - instance Funct ('KProxy :: KProxy o) where - type Codomain 'KProxy = NatTr (Proxy :: o -> *) - -As it turns out, `o` is not free-floating in this example. That is because `o` -bound by the kind signature of the LHS type pattern 'KProxy. To make this more -obvious, one can also write the instance like so: - - instance Funct ('KProxy :: KProxy o) where - type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *) --} - --- See Note [Free-floating kind vars] -reportFloatingKvs :: Name -- of the tycon - -> TyConFlavour -- What sort of TyCon it is - -> [TcTyVar] -- all tyvars, not necessarily zonked - -> [TcTyVar] -- floating tyvars - -> TcM () -reportFloatingKvs tycon_name flav all_tvs bad_tvs - = unless (null bad_tvs) $ -- don't bother zonking if there's no error - do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs - ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs - ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs - tidy_bad_tvs = map (tidyTyCoVarOcc tidy_env) bad_tvs - ; mapM_ (report tidy_all_tvs) tidy_bad_tvs } - where - report tidy_all_tvs tidy_bad_tv - = addErr $ - vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+> - text "is implicitly bound in" <+> ppr flav - , quotes (ppr tycon_name) <> comma <+> - text "but does not appear as the kind of any" - , text "of its type variables. Perhaps you meant" - , text "to bind it explicitly somewhere?" - , ppWhen (not (null tidy_all_tvs)) $ - hang (text "Type variables with inferred kinds:") - 2 (ppr_tv_bndrs tidy_all_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, 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 diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index d46ade1028..50721dc67a 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -384,9 +384,6 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(dL->L _ name), psb_args = details ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys ) pushLevelAndCaptureConstraints $ tcExtendTyVarEnv univ_tvs $ - tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE) - | ex_tv <- extra_ex] $ - -- See Note [Pattern synonym existentials do not scope] tcPat PatSyn lpat (mkCheckExpType pat_ty) $ do { let in_scope = mkInScopeSet (mkVarSet univ_tvs) empty_subst = mkEmptyTCvSubst in_scope @@ -451,54 +448,6 @@ This should work. But in the matcher we must match against MkT, and then instantiate its argument 'x', to get a function of type (Int -> Int). Equality is not enough! Trac #13752 was an example. -Note [Pattern synonym existentials do not scope] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this (Trac #14498): - pattern SS :: forall (t :: k). () => - => forall (a :: kk -> k) (n :: kk). - => TypeRep n -> TypeRep t - pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n) - -Here 'k' is implicitly bound in the signature, but (with --XScopedTypeVariables) it does still scope over the pattern-synonym -definition. But what about 'kk', which is oexistential? It too is -implicitly bound in the signature; should it too scope? And if so, -what type variable is it bound to? - -The trouble is that the type variable to which it is bound is itself -only brought into scope in part the pattern, so it makes no sense for -'kk' to scope over the whole pattern. See the discussion on -Trac #14498, esp comment:16ff. Here is a simpler example: - data T where { MkT :: x -> (x->Int) -> T } - pattern P :: () => forall x. x -> (x->Int) -> T - pattern P a b = (MkT a b, True) - -Here it would make no sense to mention 'x' in the True pattern, -like this: - pattern P a b = (MkT a b, True :: x) - -The 'x' only makes sense "under" the MkT pattern. Conclusion: the -existential type variables of a pattern-synonym signature should not -scope. - -But it's not that easy to implement, because we don't know -exactly what the existentials /are/ until we get to type checking. -(See Note [The pattern-synonym signature splitting rule], and -the partition of implicit_tvs in tcCheckPatSynDecl.) - -So we do this: - -- The reaner brings all the implicitly-bound kind variables into - scope, without trying to distinguish universal from existential - -- tcCheckPatSynDecl uses tcExtendKindEnvList to bind the - implicitly-bound existentials to - APromotionErr PatSynExPE - It's not really a promotion error, but it's a way to bind the Name - (which the renamer has not complained about) to something that, when - looked up, will cause a complaint (in this case - TcHsType.promotionErr) - Note [The pattern-synonym signature splitting rule] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 797a421956..9cf338b9d0 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -1107,9 +1107,6 @@ data PromotionErr | PatSynPE -- Pattern synonyms -- See Note [Don't promote pattern synonyms] in TcEnv - | PatSynExPE -- Pattern synonym existential type variable - -- See Note [Pattern synonym existentials do not scope] in TcPatSyn - | RecDataConPE -- Data constructor in a recursive loop -- See Note [Recursion and promoting data constructors] in TcTyClsDecls | NoDataKindsTC -- -XDataKinds not enabled (for a tycon) @@ -1303,7 +1300,6 @@ instance Outputable PromotionErr where ppr ClassPE = text "ClassPE" ppr TyConPE = text "TyConPE" ppr PatSynPE = text "PatSynPE" - ppr PatSynExPE = text "PatSynExPE" ppr FamDataConPE = text "FamDataConPE" ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE" <+> parens (ppr pred) @@ -1322,7 +1318,6 @@ pprPECategory :: PromotionErr -> SDoc pprPECategory ClassPE = text "Class" pprPECategory TyConPE = text "Type constructor" pprPECategory PatSynPE = text "Pattern synonym" -pprPECategory PatSynExPE = text "Pattern synonym existential" pprPECategory FamDataConPE = text "Data constructor" pprPECategory ConstrainedDataConPE{} = text "Data constructor" pprPECategory RecDataConPE = text "Data constructor" diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index 121193d6e2..631c777ab7 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -1252,7 +1252,7 @@ reifyInstances th_nm th_tys ; rdr_ty <- cvt loc (mkThAppTs (TH.ConT th_nm) th_tys) -- #9262 says to bring vars into scope, like in HsForAllTy case -- of rnHsTyKi - ; let tv_rdrs = freeKiTyVarsAllVars (extractHsTyRdrTyVars rdr_ty) + ; let tv_rdrs = extractHsTyRdrTyVars rdr_ty -- Rename to HsType Name ; ((tv_names, rn_ty), _fvs) <- checkNoErrs $ -- If there are out-of-scope Names here, then we diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 28b692f2e8..eb8a066529 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -537,7 +537,6 @@ generaliseTcTyCon tc = setSrcSpan (getSrcSpan tc) $ addTyConCtxt tc $ do { let tc_name = tyConName tc - tc_flav = tyConFlavour tc tc_res_kind = tyConResKind tc tc_tvs = tyConTyVars tc @@ -610,21 +609,13 @@ generaliseTcTyCon tc , text "required_tcbs =" <+> ppr required_tcbs , text "final_tcbs =" <+> ppr final_tcbs ] - -- Step 8: check for floating kind vars - -- See Note [Free-floating kind vars] - -- They are easily identified by the fact that they - -- have not been skolemised by quantifyTyVars - ; let floating_specified = filter isTyVarTyVar scoped_tvs - ; reportFloatingKvs tc_name tc_flav - scoped_tvs floating_specified - - -- Step 9: Check for duplicates + -- Step 8: Check for duplicates -- E.g. data SameKind (a::k) (b::k) -- data T (a::k1) (b::k2) = MkT (SameKind a b) -- Here k1 and k2 start as TyVarTvs, and get unified with each other ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_tv_pairs) - -- Step 10: Check for validity. + -- Step 9: Check for validity. -- We do this here because we're about to put the tycon into -- the environment, and we don't want anything malformed in the -- environment. diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst index cf67246abf..cfe07deb81 100644 --- a/docs/users_guide/8.10.1-notes.rst +++ b/docs/users_guide/8.10.1-notes.rst @@ -16,6 +16,34 @@ Full details Language ~~~~~~~~ +- Kind variables are no longer implicitly quantified when an explicit ``forall`` is used, see + `GHC proposal #24 + <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__. + :ghc-flag:`-Wimplicit-kind-vars` is now obsolete. + +- Kind variables are no longer implicitly quantified in constructor declarations: :: + + data T a = T1 (S (a :: k) | forall (b::k). T2 (S b) -- no longer accepted + data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b) -- still accepted + +- Implicitly quantified kind variables are no longer put in front of other variables: :: + + f :: Proxy (a :: k) -> Proxy (b :: j) + + ghci> :t +v f -- old order: + f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b + + ghci> :t +v f -- new order: + f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b + + This is a breaking change for users of :extension:`TypeApplications`. + +- In type synonyms and type family equations, free variables on the RHS are no longer + implicitly quantified unless used in an outermost kind annotation: :: + + type T = Just (Nothing :: Maybe a) -- no longer accepted + type T = Just Nothing :: Maybe (Maybe a) -- still accepted + Compiler ~~~~~~~~ diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index eae0283f6c..9ba8fa2daf 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -7574,16 +7574,16 @@ instance for ``GMap`` is :: In this example, the declaration has only one variant. In general, it can be any number. -When :extension:`ExplicitForAll` is enabled, type or kind variables used on +When :extension:`ExplicitForAll` is enabled, type and kind variables used on the left hand side can be explicitly bound. For example: :: data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool -When an explicit ``forall`` is present, all *type* variables mentioned which -are not already in scope must be bound by the ``forall``. Kind variables will -be implicitly bound if necessary, for example: :: +When an explicit ``forall`` is present, *all* type and kind variables mentioned +which are not already in scope must be bound by the ``forall``: - data instance forall (a :: k). F a = FOtherwise + data instance forall (a :: k). F a = FOtherwise -- rejected: k not in scope + data instance forall k (a :: k). F a = FOtherwise -- accepted When the flag :ghc-flag:`-Wunused-type-patterns` is enabled, type variables that are mentioned in the patterns on the left hand side, but not @@ -9184,17 +9184,74 @@ a type variable ``a`` of kind ``k``. In general, there is no limit to how deeply nested this sort of dependency can work. However, the dependency must be well-scoped: ``forall (a :: k) k. ...`` is an error. -For backward compatibility, kind variables *do not* need to be bound explicitly, -even if the type starts with ``forall``. +Implicit quantification in type synonyms and type family instances +------------------------------------------------------------------ -Accordingly, the rule for kind quantification in higher-rank contexts has -changed slightly. In GHC 7, if a kind variable was mentioned for the first -time in the kind of a variable bound in a non-top-level ``forall``, the kind -variable was bound there, too. -That is, in ``f :: (forall (a :: k). ...) -> ...``, the ``k`` was bound -by the same ``forall`` as the ``a``. In GHC 8, however, all kind variables -mentioned in a type are bound at the outermost level. If you want one bound -in a higher-rank ``forall``, include it explicitly. +Consider the scoping rules for type synonyms and type family instances, such as +these:: + + type TS a (b :: k) = <rhs> + type instance TF a (b :: k) = <rhs> + +The basic principle is that all variables mentioned on the right hand side +``<rhs>`` must be bound on the left hand side:: + + type TS a (b :: k) = (k, a, Proxy b) -- accepted + type TS a (b :: k) = (k, a, Proxy b, z) -- rejected: z not in scope + +But there is one exception: free variables mentioned in the outermost kind +signature on the right hand side are quantified implicitly. Thus, in the +following example the variables ``a``, ``b``, and ``k`` are all in scope on the +right hand side of ``S``:: + + type S a b = <rhs> :: k -> k + +The reason for this exception is that there may be no other way to bind ``k``. +For example, suppose we wanted ``S`` to have the the following kind with an +*invisible* parameter ``k``:: + + S :: forall k. Type -> Type -> k -> k + +In this case, we could not simply bind ``k`` on the left-hand side, as ``k`` +would become a *visible* parameter:: + + type S k a b = <rhs> :: k -> k + S :: forall k -> Type -> Type -> k -> k + +Note that we only look at the *outermost* kind signature to decide which +variables to quantify implicitly. As a counter-example, consider ``M1``: :: + + type M1 = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + +Here, the kind signature is hidden inside ``'Just``, and there is no outermost +kind signature. We can fix this example by providing an outermost kind signature: :: + + type M2 = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k) + +Here, ``k`` is brought into scope by ``:: Maybe (Maybe k)``. + +A kind signature is considered to be outermost regardless of redundant +parentheses: :: + + type P = 'Nothing :: Maybe a -- accepted + type P = ((('Nothing :: Maybe a))) -- accepted + +Closed type family instances are subject to the same rules: :: + + type family F where + F = 'Nothing :: Maybe k -- accepted + + type family F where + F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + + type family F where + F = 'Just ('Nothing :: Maybe k) :: Maybe (Maybe k) -- accepted + + type family F :: Maybe (Maybe k) where + F = 'Just ('Nothing :: Maybe k) -- rejected: k not in scope + + type family F :: Maybe (Maybe k) where + F @k = 'Just ('Nothing :: Maybe k) -- accepted Kind-indexed GADTs ------------------ @@ -10832,19 +10889,6 @@ the rules in the subtler cases: - If an identifier's type has a ``forall``, then the order of type variables as written in the ``forall`` is retained. -- If the type signature includes any kind annotations (either on variable - binders or as annotations on types), any variables used in kind - annotations come before any variables never used in kind annotations. - This rule is not recursive: if there is an annotation within an annotation, - then the variables used therein are on equal footing. Examples:: - - f :: Proxy (a :: k) -> Proxy (b :: j) -> () - -- as if f :: forall k j a b. ... - - g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> () - -- as if g :: forall j k b a. ... - -- NB: k is in a kind annotation within a kind annotation - - If any of the variables depend on other variables (that is, if some of the variables are *kind* variables), the variables are reordered so that kind variables come before type variables, preserving the @@ -10854,13 +10898,11 @@ the rules in the subtler cases: h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> () -- as if h :: forall j k a b. ... - In this example, all of ``a``, ``j``, and ``k`` are considered kind - variables and will always be placed before ``b``, a lowly type variable. - (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears - lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first, - because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k`` - are not reordered with respect to each other, even though doing so would - not violate dependency conditions. + In this example, ``a`` depends on ``j`` and ``k``, and ``b`` depends on ``a``. + Even though ``a`` appears lexically before ``j`` and ``k``, ``j`` and ``k`` + are quantified first, because ``a`` depends on ``j`` and ``k``. Note further + that ``j`` and ``k`` are not reordered with respect to each other, even + though doing so would not violate dependency conditions. A "stable topological sort" here, we mean that we perform this algorithm (which we call *ScopedSort*): diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst index c392ab38df..9f9e4d948d 100644 --- a/docs/users_guide/using-warnings.rst +++ b/docs/users_guide/using-warnings.rst @@ -123,7 +123,6 @@ The following flags are simple ways to select standard "packages" of warnings: * :ghc-flag:`-Wmissing-monadfail-instances` * :ghc-flag:`-Wsemigroup` * :ghc-flag:`-Wnoncanonical-monoid-instances` - * :ghc-flag:`-Wimplicit-kind-vars` * :ghc-flag:`-Wstar-is-type` .. ghc-flag:: -Wno-compat @@ -776,58 +775,6 @@ of ``-W(no-)*``. This warning is off by default. -.. ghc-flag:: -Wimplicit-kind-vars - :shortdesc: warn when kind variables are brought into scope implicitly despite - the "forall-or-nothing" rule - :type: dynamic - :reverse: -Wno-implicit-kind-vars - :category: - - :since: 8.6 - - `GHC proposal #24 - <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst>`__ - prescribes to treat kind variables and type variables identically in - ``forall``, removing the legacy distinction between them. - - Consider the following examples: :: - - f :: Proxy a -> Proxy b -> () - g :: forall a b. Proxy a -> Proxy b -> () - - ``f`` does not use an explicit ``forall``, so type variables ``a`` and ``b`` - are brought into scope implicitly. ``g`` quantifies both ``a`` and ``b`` - explicitly. Both ``f`` and ``g`` work today and will continue to work in the - future because they adhere to the "forall-or-nothing" rule: either all type - variables in a function definition are introduced explicitly or implicitly, - there is no middle ground. - - A violation of the "forall-or-nothing" rule looks like this: :: - - m :: forall a. Proxy a -> Proxy b -> () - - ``m`` does not introduce one of the variables, ``b``, and thus is rejected. - - However, consider the following example: :: - - n :: forall a. Proxy (a :: k) -> () - - While ``n`` uses ``k`` without introducing it and thus violates the rule, it - is currently accepted. This is because ``k`` in ``n`` is considered a kind - variable, as it occurs in a kind signature. In reality, the line between - type variables and kind variables is blurry, as the following example - demonstrates: :: - - kindOf :: forall a. Proxy (a :: k) -> Proxy k - - In ``kindOf``, the ``k`` variable is used both in a kind position and a type - position. Currently, ``kindOf`` happens to be accepted as well. - - In a future release of GHC, both ``n`` and ``kindOf`` will be rejected per - the "forall-or-nothing" rule. This warning, being part of the - :ghc-flag:`-Wcompat` option group, allows to detect this before the actual - breaking change takes place. - .. ghc-flag:: -Wincomplete-patterns :shortdesc: warn when a pattern match could fail :type: dynamic diff --git a/testsuite/tests/codeGen/should_fail/T13233.hs b/testsuite/tests/codeGen/should_fail/T13233.hs index 1facb77914..f24fc03bfb 100644 --- a/testsuite/tests/codeGen/should_fail/T13233.hs +++ b/testsuite/tests/codeGen/should_fail/T13233.hs @@ -8,9 +8,9 @@ module Bug where import GHC.Exts (TYPE, RuntimeRep, Weak#, State#, RealWorld, mkWeak# ) class Foo (a :: TYPE rep) where - bar :: forall (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b + bar :: forall rep2 (b :: TYPE rep2). (a -> a -> b) -> a -> a -> b -baz :: forall (a :: TYPE rep). Foo a => a -> a -> (# a, a #) +baz :: forall rep (a :: TYPE rep). Foo a => a -> a -> (# a, a #) baz = bar (#,#) obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) diff --git a/testsuite/tests/dependent/should_compile/T15264.stderr b/testsuite/tests/dependent/should_compile/T15264.stderr deleted file mode 100644 index 222d686513..0000000000 --- a/testsuite/tests/dependent/should_compile/T15264.stderr +++ /dev/null @@ -1,10 +0,0 @@ - -T15264.hs:8:22: warning: [-Wimplicit-kind-vars (in -Wcompat)] - An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k’ - Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future. - Suggested fix: add ‘forall k.’ - -T15264.hs:11:22: warning: [-Wimplicit-kind-vars (in -Wcompat)] - An explicit ‘forall’ was used, but the following kind variables are not quantified: ‘k1’, ‘k2’ - Despite this fact, GHC will introduce them into scope, but it will stop doing so in the future. - Suggested fix: add ‘forall k1 k2.’ diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index fa39c9a69a..ca5f436174 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -48,7 +48,6 @@ test('T14066a', normal, compile, ['']) test('T14749', normal, compile, ['']) test('T14845_compile', normal, compile, ['']) test('T14991', normal, compile, ['']) -test('T15264', normal, compile, ['']) test('DkNameRes', normal, compile, ['']) test('T15346', normal, compile, ['']) test('T15419', normal, compile, ['']) diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs index b12adbd8e3..e33fdf110e 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs @@ -10,5 +10,5 @@ data SameKind :: k -> k -> * foo :: forall a k (b :: k). SameKind a b foo = undefined -bar :: forall a (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d +bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d bar = undefined diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr index 55a484910c..a8c4b689ae 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr @@ -5,9 +5,9 @@ BadTelescope2.hs:10:8: error: k (a :: k) (b :: k) • In the type signature: foo :: forall a k (b :: k). SameKind a b -BadTelescope2.hs:13:70: error: - • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’ +BadTelescope2.hs:13:81: error: + • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’ • In the second argument of ‘SameKind’, namely ‘d’ In the type signature: - bar :: forall a (c :: Proxy b) (d :: Proxy a). + bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d diff --git a/testsuite/tests/dependent/should_compile/T15264.hs b/testsuite/tests/dependent/should_fail/T15264.hs index f3dec42564..394c53a013 100644 --- a/testsuite/tests/dependent/should_compile/T15264.hs +++ b/testsuite/tests/dependent/should_fail/T15264.hs @@ -1,5 +1,4 @@ {-# LANGUAGE ExplicitForAll, PolyKinds #-} -{-# OPTIONS -Wcompat -Wno-error=implicit-kind-vars #-} module T15264 where diff --git a/testsuite/tests/dependent/should_fail/T15264.stderr b/testsuite/tests/dependent/should_fail/T15264.stderr new file mode 100644 index 0000000000..6d5f597823 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15264.stderr @@ -0,0 +1,6 @@ + +T15264.hs:7:22: error: Not in scope: type variable ‘k’ + +T15264.hs:10:22: error: Not in scope: type variable ‘k1’ + +T15264.hs:10:32: error: Not in scope: type variable ‘k2’ diff --git a/testsuite/tests/dependent/should_fail/T15825.hs b/testsuite/tests/dependent/should_fail/T15825.hs index 01227a8696..651525b21d 100644 --- a/testsuite/tests/dependent/should_fail/T15825.hs +++ b/testsuite/tests/dependent/should_fail/T15825.hs @@ -10,5 +10,5 @@ module T15825 where type C k = (forall (x::k). *) -class X (a :: *) -instance forall (a :: C k). X (a :: *) +class X (a :: *) +instance forall k (a :: C k). X (a :: *) diff --git a/testsuite/tests/dependent/should_fail/T15825.stderr b/testsuite/tests/dependent/should_fail/T15825.stderr index d64cab0494..97582ba952 100644 --- a/testsuite/tests/dependent/should_fail/T15825.stderr +++ b/testsuite/tests/dependent/should_fail/T15825.stderr @@ -1,5 +1,5 @@ -T15825.hs:14:29: error: +T15825.hs:14:31: error: • Illegal type synonym family application ‘GHC.Types.Any @k’ in instance: X (a @(GHC.Types.Any @k)) diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index f1272200ba..4b258cc065 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -39,3 +39,4 @@ test('T15743c', normal, compile_fail, ['']) test('T15743d', normal, compile_fail, ['']) test('T15825', normal, compile_fail, ['']) test('T15859', normal, compile_fail, ['']) +test('T15264', normal, compile_fail, ['']) diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr index b4759714c2..8ec10322c8 100644 --- a/testsuite/tests/ghci/scripts/T7873.stderr +++ b/testsuite/tests/ghci/scripts/T7873.stderr @@ -1,8 +1,2 @@ -<interactive>:2:1: error: - • Kind variable ‘k’ is implicitly bound in data type - ‘D1’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? - Type variables with inferred kinds: (k :: *) - • In the data type declaration for ‘D1’ +<interactive>:2:32: error: Not in scope: type variable ‘k’ diff --git a/testsuite/tests/ghci/scripts/T9293.stdout b/testsuite/tests/ghci/scripts/T9293.stdout index 6d140bc9f7..87b950654d 100644 --- a/testsuite/tests/ghci/scripts/T9293.stdout +++ b/testsuite/tests/ghci/scripts/T9293.stdout @@ -13,7 +13,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -37,7 +36,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -60,7 +58,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -85,7 +82,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances diff --git a/testsuite/tests/ghci/scripts/ghci024.stdout b/testsuite/tests/ghci/scripts/ghci024.stdout index 863184ad49..138da30075 100644 --- a/testsuite/tests/ghci/scripts/ghci024.stdout +++ b/testsuite/tests/ghci/scripts/ghci024.stdout @@ -14,7 +14,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances diff --git a/testsuite/tests/ghci/scripts/ghci057.stdout b/testsuite/tests/ghci/scripts/ghci057.stdout index 6d140bc9f7..87b950654d 100644 --- a/testsuite/tests/ghci/scripts/ghci057.stdout +++ b/testsuite/tests/ghci/scripts/ghci057.stdout @@ -13,7 +13,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -37,7 +36,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -60,7 +58,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances @@ -85,7 +82,6 @@ other dynamic, non-language, flag settings: -fimplicit-import-qualified -fshow-warning-groups warning settings: - -Wimplicit-kind-vars -Wmissing-monadfail-instances -Wsemigroup -Wnoncanonical-monoid-instances diff --git a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs index 067127cf8a..c16e4e0156 100644 --- a/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs +++ b/testsuite/tests/indexed-types/should_compile/ExplicitForAllFams1.hs @@ -26,6 +26,6 @@ type family H a b where -- More tests type family D a b where - forall (a :: Type -> Type) (b :: a Int) (c :: k). D (Proxy b) (Proxy c) = () + forall (a :: Type -> Type) (b :: a Int) k (c :: k). D (Proxy b) (Proxy c) = () forall (a :: Bool) (b :: Proxy a). D (Proxy b) () = Int forall (a :: Type). D a a = Maybe a diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index d6cfe26b40..9a0c6b8e6e 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -287,8 +287,8 @@ (NoExt) (DataFamInstDecl (HsIB - [{Name: k} - ,{Name: a}] + [{Name: a} + ,{Name: k}] (FamEqn (NoExt) ({ DumpRenamedAst.hs:18:18-20 } diff --git a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr index 1563a2eb23..d07ce73230 100644 --- a/testsuite/tests/partial-sigs/should_compile/T15039a.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T15039a.stderr @@ -27,7 +27,7 @@ T15039a.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’ Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by the type signature for: - ex3 :: forall k a (b :: k). Dict (a ~~ b) -> () + ex3 :: forall a k (b :: k). Dict (a ~~ b) -> () at T15039a.hs:24:1-43 • In a pattern type signature: _ In the pattern: Dict :: _ diff --git a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr index c28b94879b..8f9c2c8a45 100644 --- a/testsuite/tests/partial-sigs/should_compile/T15039b.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T15039b.stderr @@ -28,7 +28,7 @@ T15039b.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)] standing for ‘Dict ((a :: *) ~~ (b :: k))’ Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by the type signature for: - ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> () + ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> () at T15039b.hs:24:1-43 • In a pattern type signature: _ In the pattern: Dict :: _ diff --git a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr index 40c126f061..261a82e91a 100644 --- a/testsuite/tests/partial-sigs/should_compile/T15039c.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T15039c.stderr @@ -27,7 +27,7 @@ T15039c.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)] • Found type wildcard ‘_’ standing for ‘Dict (a ~~ b)’ Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by the type signature for: - ex3 :: forall k a (b :: k). Dict (a ~~ b) -> () + ex3 :: forall a k (b :: k). Dict (a ~~ b) -> () at T15039c.hs:24:1-43 • In a pattern type signature: _ In the pattern: Dict :: _ diff --git a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr index cca94416b8..8548356001 100644 --- a/testsuite/tests/partial-sigs/should_compile/T15039d.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T15039d.stderr @@ -29,7 +29,7 @@ T15039d.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)] standing for ‘Dict ((a :: *) ~~ (b :: k))’ Where: ‘a’, ‘k’, ‘b’ are rigid type variables bound by the type signature for: - ex3 :: forall k a (b :: k). Dict ((a :: *) ~~ (b :: k)) -> () + ex3 :: forall a k (b :: k). Dict ((a :: *) ~~ (b :: k)) -> () at T15039d.hs:24:1-43 • In a pattern type signature: _ In the pattern: Dict :: _ diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.hs b/testsuite/tests/partial-sigs/should_compile/T16334.hs new file mode 100644 index 0000000000..c01ef5cc16 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T16334.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE NamedWildCards, PartialTypeSignatures, PolyKinds, NoStarIsType #-} + +module T16334 where + +k :: (Int :: _t) +k = 42 diff --git a/testsuite/tests/partial-sigs/should_compile/T16334.stderr b/testsuite/tests/partial-sigs/should_compile/T16334.stderr new file mode 100644 index 0000000000..83429e0d33 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T16334.stderr @@ -0,0 +1,4 @@ + +T16334.hs:5:14: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found type wildcard ‘_t’ standing for ‘Type’ + • In the type signature: k :: (Int :: _t) diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T index d6eaa7727a..3e62552a20 100644 --- a/testsuite/tests/partial-sigs/should_compile/all.T +++ b/testsuite/tests/partial-sigs/should_compile/all.T @@ -89,3 +89,4 @@ test('T15039b', normal, compile, ['-fprint-explicit-kinds']) test('T15039c', normal, compile, ['-fprint-equality-relations']) test('T15039d', normal, compile, ['-fprint-explicit-kinds -fprint-equality-relations']) +test('T16334', normal, compile, ['']) diff --git a/testsuite/tests/patsyn/should_fail/T14498.hs b/testsuite/tests/patsyn/should_compile/T14498.hs index 0744310aee..b7f7db4d8a 100644 --- a/testsuite/tests/patsyn/should_fail/T14498.hs +++ b/testsuite/tests/patsyn/should_compile/T14498.hs @@ -23,9 +23,9 @@ type SN = (TypeRep :: N -> Type) pattern SO = (Typeable :: TypeRep (O::N)) pattern SS :: - forall (t :: k'). + forall k' (t :: k'). () - => forall (a :: kk -> k') (n :: kk). + => forall kk (a :: kk -> k') (n :: kk). (t ~ a n) => TypeRep n -> TypeRep t diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 54775a80a2..6eb9e2db8a 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -76,3 +76,4 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])], test('T14326', normal, compile, ['']) test('T14394', normal, ghci_script, ['T14394.script']) test('T14552', normal, compile, ['']) +test('T14498', normal, compile, ['']) diff --git a/testsuite/tests/patsyn/should_fail/T14507.hs b/testsuite/tests/patsyn/should_fail/T14507.hs index b36425ced6..9599b73c77 100644 --- a/testsuite/tests/patsyn/should_fail/T14507.hs +++ b/testsuite/tests/patsyn/should_fail/T14507.hs @@ -13,7 +13,7 @@ foo rep = error "urk" type family SING :: k -> Type where SING = (TypeRep :: Bool -> Type) -pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk) +pattern RepN :: forall kk (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk) pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk , tr :: TypeRep (a::Bool))) diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T index 7cdef908a6..5431e8b76a 100644 --- a/testsuite/tests/patsyn/should_fail/all.T +++ b/testsuite/tests/patsyn/should_fail/all.T @@ -40,7 +40,6 @@ test('T13470', normal, compile_fail, ['']) test('T14112', normal, compile_fail, ['']) test('T14114', normal, compile_fail, ['']) test('T14380', normal, compile_fail, ['']) -test('T14498', normal, compile_fail, ['']) test('T14507', normal, compile_fail, ['-dsuppress-uniques']) test('T15289', normal, compile_fail, ['']) test('T15685', normal, compile_fail, ['']) diff --git a/testsuite/tests/polykinds/BadKindVar.hs b/testsuite/tests/polykinds/BadKindVar.hs index c24657f3d2..9275d453c5 100644 --- a/testsuite/tests/polykinds/BadKindVar.hs +++ b/testsuite/tests/polykinds/BadKindVar.hs @@ -5,5 +5,5 @@ module Foo where import Data.Proxy -- Should be illegal without PolyKinds -f :: forall (a :: k). Proxy a +f :: forall k (a :: k). Proxy a f = f diff --git a/testsuite/tests/polykinds/BadKindVar.stderr b/testsuite/tests/polykinds/BadKindVar.stderr index beeed2b3c8..3312350602 100644 --- a/testsuite/tests/polykinds/BadKindVar.stderr +++ b/testsuite/tests/polykinds/BadKindVar.stderr @@ -1,5 +1,5 @@ -BadKindVar.hs:8:19: error: +BadKindVar.hs:8:21: error: Unexpected kind variable ‘k’ Perhaps you intended to use PolyKinds In the type signature for ‘f’ diff --git a/testsuite/tests/polykinds/KindVarOrder.script b/testsuite/tests/polykinds/KindVarOrder.script new file mode 100644 index 0000000000..c4b4165dcf --- /dev/null +++ b/testsuite/tests/polykinds/KindVarOrder.script @@ -0,0 +1,9 @@ +:set -XPolyKinds -XDataKinds +import Data.Kind (Type) +data Proxy (a :: k) +f :: Proxy (a :: k) -> Proxy (b :: j) -> (); f = f +g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> (); g = g +h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> (); h = h +:t +v f +:t +v g +:t +v h diff --git a/testsuite/tests/polykinds/KindVarOrder.stdout b/testsuite/tests/polykinds/KindVarOrder.stdout new file mode 100644 index 0000000000..66a950dc23 --- /dev/null +++ b/testsuite/tests/polykinds/KindVarOrder.stdout @@ -0,0 +1,5 @@ +f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b -> () +g :: forall j (b :: j) k (a :: Proxy Proxy). + Proxy b -> Proxy a -> () +h :: forall j k (a :: (j, k)) (b :: Proxy a). + Proxy a -> Proxy b -> () diff --git a/testsuite/tests/polykinds/T10503.hs b/testsuite/tests/polykinds/T10503.hs index 2cc1ee717e..2b9900652f 100644 --- a/testsuite/tests/polykinds/T10503.hs +++ b/testsuite/tests/polykinds/T10503.hs @@ -5,5 +5,5 @@ data Proxy p = Proxy data KProxy (a :: *) = KProxy -h :: forall r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r +h :: forall k r . (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r h = undefined diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr index 9fb87e9be7..a47a872253 100644 --- a/testsuite/tests/polykinds/T10503.stderr +++ b/testsuite/tests/polykinds/T10503.stderr @@ -4,14 +4,14 @@ T10503.hs:8:6: error: from the context: Proxy 'KProxy ~ Proxy 'KProxy bound by a type expected by the context: (Proxy 'KProxy ~ Proxy 'KProxy) => r - at T10503.hs:8:6-85 + at T10503.hs:8:6-87 ‘k’ is a rigid type variable bound by the type signature for: h :: forall k r. ((Proxy 'KProxy ~ Proxy 'KProxy) => r) -> r - at T10503.hs:8:6-85 + at T10503.hs:8:6-87 • In the ambiguity check for ‘h’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: - h :: forall r. + h :: forall k r. (Proxy ('KProxy :: KProxy k) ~ Proxy ('KProxy :: KProxy *) => r) -> r diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr index 2df92c34da..ba07f3cda1 100644 --- a/testsuite/tests/polykinds/T13985.stderr +++ b/testsuite/tests/polykinds/T13985.stderr @@ -1,28 +1,10 @@ -T13985.hs:13:41: error: - • Type variable ‘k’ is mentioned in the RHS, - but not bound on the LHS of the family instance - • In the data instance declaration for ‘Fam’ +T13985.hs:13:41: error: Not in scope: type variable ‘k’ -T13985.hs:16:43: error: - • Type variable ‘a’ is mentioned in the RHS, - but not bound on the LHS of the family instance - • In the type instance declaration for ‘T’ +T13985.hs:16:43: error: Not in scope: type variable ‘a’ -T13985.hs:23:26: error: - • Type variable ‘k’ is mentioned in the RHS, - but not bound on the LHS of the family instance - • In the data instance declaration for ‘CD’ - In the instance declaration for ‘C Type’ +T13985.hs:23:26: error: Not in scope: type variable ‘k’ -T13985.hs:24:37: error: - • Type variable ‘a’ is mentioned in the RHS, - but not bound on the LHS of the family instance - • In the type instance declaration for ‘CT’ - In the instance declaration for ‘C Type’ +T13985.hs:24:37: error: Not in scope: type variable ‘a’ -T13985.hs:28:39: error: - • Type variable ‘x’ is mentioned in the RHS, - but not bound on the LHS of the family instance - • In the default type instance declaration for ‘ZT’ - In the class declaration for ‘Z’ +T13985.hs:28:39: error: Not in scope: type variable ‘x’ diff --git a/testsuite/tests/polykinds/T14561.hs b/testsuite/tests/polykinds/T14561.hs index 7b1f17e08e..8c74ab4740 100644 --- a/testsuite/tests/polykinds/T14561.hs +++ b/testsuite/tests/polykinds/T14561.hs @@ -8,7 +8,7 @@ module T14561 where import GHC.Types import GHC.Prim -badId :: forall (a :: TYPE r). a -> a +badId :: forall r (a :: TYPE r). a -> a badId = unsafeCoerce# -- Un-saturated application of a levity-polymorphic -- function that must be eta-expanded diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs index bdc05dd6df..aefa12b59e 100644 --- a/testsuite/tests/polykinds/T14563.hs +++ b/testsuite/tests/polykinds/T14563.hs @@ -5,5 +5,5 @@ import GHC.Types (TYPE) import Data.Kind data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where - Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. + Lan :: forall rep rep' xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. (g xx -> a) -> h xx -> Lan g h a diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 43d81c5e1e..6e8384542f 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -23,13 +23,13 @@ T14846.hs:38:8: error: In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:12: error: - • Couldn't match kind ‘k3’ with ‘Struct cls2’ - ‘k3’ is a rigid type variable bound by + • 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 cls0 :: Struct cls -> Constraint - cls1 :: k3 -> Constraint + cls1 :: k4 -> Constraint • In the expression: struct :: AStruct (Structured a cls) In the expression: case struct :: AStruct (Structured a cls) of In an equation for ‘i’: @@ -38,12 +38,12 @@ T14846.hs:39:12: error: i :: Hom riki a a (bound at T14846.hs:39:3) T14846.hs:39:31: error: - • Couldn't match kind ‘k3’ with ‘Struct cls2’ - ‘k3’ is a rigid type variable bound by + • 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 - cls1 :: k3 -> Constraint + cls1 :: k4 -> Constraint cls0 :: Struct cls -> Constraint Expected kind ‘Struct cls0’, but ‘Structured a cls’ has kind ‘Struct cls1’ diff --git a/testsuite/tests/polykinds/T14887a.hs b/testsuite/tests/polykinds/T14887a.hs index 2e5cf02212..4179862cad 100644 --- a/testsuite/tests/polykinds/T14887a.hs +++ b/testsuite/tests/polykinds/T14887a.hs @@ -1,16 +1,10 @@ {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeInType #-} -{-# OPTIONS_GHC -Wno-partial-type-signatures -Wno-implicit-kind-vars #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} module Bug where import Data.Proxy -f1 :: forall (x :: a). Proxy (x :: _) --- This one has an implicitly-quantified kind var 'a', which --- we will stop accepting in the future, under the forall-or-nothing --- rule. Hence -Wno-implicit-kind-vars -f1 = Proxy - f2 :: forall a (x :: a). Proxy (x :: _) f2 = Proxy diff --git a/testsuite/tests/polykinds/T8616.hs b/testsuite/tests/polykinds/T8616.hs index 47e31bcc94..e8f4c682bf 100644 --- a/testsuite/tests/polykinds/T8616.hs +++ b/testsuite/tests/polykinds/T8616.hs @@ -4,11 +4,11 @@ module T8616 where import Data.Proxy import GHC.Exts -withSomeSing :: forall (kproxy :: k). Proxy kproxy +withSomeSing :: forall k (kproxy :: k). Proxy kproxy withSomeSing = undefined :: (Any :: k) -- The 'k' is bought into scope by the type signature -- This is a type error, but should not crash GHC -foo = (undefined :: Proxy (a :: k)) :: forall (a :: k). Proxy a +foo = (undefined :: Proxy (a :: k)) :: forall k (a :: k). Proxy a -- Again, the 'k' is bought into scope by the type signature - -- No type error though
\ No newline at end of file + -- No type error though diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index f9e5132a34..4341b3051a 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -4,7 +4,7 @@ T8616.hs:8:16: error: ‘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 + at T8616.hs:7:1-52 When matching types a0 :: * Any :: k diff --git a/testsuite/tests/polykinds/T9144.hs b/testsuite/tests/polykinds/T9144.hs index 0a9ef08afa..85e1b24dbe 100644 --- a/testsuite/tests/polykinds/T9144.hs +++ b/testsuite/tests/polykinds/T9144.hs @@ -8,7 +8,7 @@ import GHC.TypeLits data family Sing (a :: k) data SomeSing :: KProxy k -> * where - SomeSing :: forall (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k) + SomeSing :: forall k (a :: k). Sing a -> SomeSing ('KProxy :: KProxy k) class kproxy ~ 'KProxy => SingKind (kproxy :: KProxy k) where fromSing :: forall (a :: k). Sing a -> DemoteRep ('KProxy :: KProxy k) diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 8a885b39a5..1cfb2aa424 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -206,3 +206,4 @@ test('T14887a', normal, compile, ['']) test('T14847', normal, compile, ['']) test('T15795', normal, compile, ['']) test('T15795a', normal, compile, ['']) +test('KindVarOrder', normal, ghci_script, ['KindVarOrder.script']) diff --git a/testsuite/tests/typecheck/should_compile/T13343.hs b/testsuite/tests/typecheck/should_compile/T13343.hs index fcff9db1a4..2f3f120c72 100644 --- a/testsuite/tests/typecheck/should_compile/T13343.hs +++ b/testsuite/tests/typecheck/should_compile/T13343.hs @@ -4,6 +4,6 @@ module Bug where import GHC.Exts -type Bad = forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1 +type Bad = (forall (v1 :: RuntimeRep) (a1 :: TYPE v). a1) :: TYPE v -- should be accepted because GHC will generalize over v. Note v /= v1. diff --git a/testsuite/tests/typecheck/should_fail/T12973.hs b/testsuite/tests/typecheck/should_fail/T12973.hs index b0a33a8213..765e02f34b 100644 --- a/testsuite/tests/typecheck/should_fail/T12973.hs +++ b/testsuite/tests/typecheck/should_fail/T12973.hs @@ -9,7 +9,7 @@ class Num (a :: TYPE r) where (+) :: a -> a -> a fromInteger :: P.Integer -> a -foo :: forall (a :: TYPE r). Num a => a +foo :: forall r (a :: TYPE r). Num a => a foo = 3 + 4 diff --git a/testsuite/tests/typecheck/should_fail/T13983.stderr b/testsuite/tests/typecheck/should_fail/T13983.stderr index d1b2fe067b..aba88bc9f2 100644 --- a/testsuite/tests/typecheck/should_fail/T13983.stderr +++ b/testsuite/tests/typecheck/should_fail/T13983.stderr @@ -1,8 +1,2 @@ -T13983.hs:7:1: error: - • Kind variable ‘k’ is implicitly bound in type synonym - ‘Wat’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it explicitly somewhere? - Type variables with inferred kinds: (k :: *) - • In the type synonym declaration for ‘Wat’ +T13983.hs:7:25: error: Not in scope: type variable ‘k’ diff --git a/testsuite/tests/typecheck/should_fail/T15629.hs b/testsuite/tests/typecheck/should_fail/T15629.hs index fdbba60ccc..6d1d0b8897 100644 --- a/testsuite/tests/typecheck/should_fail/T15629.hs +++ b/testsuite/tests/typecheck/should_fail/T15629.hs @@ -23,5 +23,5 @@ sg _ _ = Proxy f :: forall (x :: Type). Proxy x -> () f _ = () where - g :: forall ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) + g :: forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) g = sg Proxy Proxy diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr index ce77bb04a3..a0e0f42286 100644 --- a/testsuite/tests/typecheck/should_fail/T15629.stderr +++ b/testsuite/tests/typecheck/should_fail/T15629.stderr @@ -1,12 +1,12 @@ -T15629.hs:26:35: error: +T15629.hs:26:37: error: • Expected kind ‘x1 ~> F x1 ab1’, but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z’ • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’ In the first argument of ‘Proxy’, namely ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’ In the type signature: - g :: forall ab. + g :: forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) T15629.hs:27:9: error: @@ -14,11 +14,11 @@ T15629.hs:27:9: error: ‘ab1’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) - at T15629.hs:26:5-82 + at T15629.hs:26:5-84 ‘z’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) - at T15629.hs:26:5-82 + at T15629.hs:26:5-84 When matching types f0 :: x ~> F x ab F1Sym :: TyFun x1 (F x1 z) -> * @@ -31,7 +31,7 @@ T15629.hs:27:9: error: = () where g :: - forall ab. + forall z ab. Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) g = sg Proxy Proxy • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/T15797.hs b/testsuite/tests/typecheck/should_fail/T15797.hs index eadd8cb972..925674fecf 100644 --- a/testsuite/tests/typecheck/should_fail/T15797.hs +++ b/testsuite/tests/typecheck/should_fail/T15797.hs @@ -13,7 +13,7 @@ import Data.Kind class Ríki (obj :: Type) where type Obj :: obj -> Constraint - type Obj = Bæ @obj + type Obj = Bæ @k :: k -> Constraint class Bæ (a :: k) instance Bæ @k (a :: k) |