diff options
| author | Tobias Dammers <tdammers@gmail.com> | 2018-09-13 09:56:02 +0200 |
|---|---|---|
| committer | Richard Eisenberg <rae@cs.brynmawr.edu> | 2018-10-28 23:17:47 -0400 |
| commit | 5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3 (patch) | |
| tree | 41449e2a558385d2b290d0005fec353e6c9c88dd | |
| parent | e8a652f65318cf60e856f7c2777a003eba10ddc6 (diff) | |
| download | haskell-5e45ad10ffca1ad175b10f6ef3327e1ed8ba25f3.tar.gz | |
Finish fix for #14880.
The real change that fixes the ticket is described in
Note [Naughty quantification candidates] in TcMType.
Fixing this required reworking candidateQTyVarsOfType, the function
that extracts free variables as candidates for quantification.
One consequence is that we now must be more careful when quantifying:
any skolems around must be quantified manually, and quantifyTyVars
will now only quantify over metavariables. This makes good sense,
as skolems are generally user-written and are listed in the AST.
As a bonus, we now have more control over the ordering of such
skolems.
Along the way, this commit fixes #15711 and refines the fix
to #14552 (by accepted a program that was previously rejected,
as we can now accept that program by zapping variables to Any).
This commit also does a fair amount of rejiggering kind inference
of datatypes. Notably, we now can skip the generalization step
in kcTyClGroup for types with CUSKs, because we get the
kind right the first time. This commit also thus fixes #15743 and
#15592, which both concern datatype kind generalisation.
(#15591 is also very relevant.) For this aspect of the commit, see
Note [Required, Specified, and Inferred in types] in TcTyClsDecls.
Test cases: dependent/should_fail/T14880{,-2},
dependent/should_fail/T15743[cd]
dependent/should_compile/T15743{,e}
ghci/scripts/T15743b
polykinds/T15592
dependent/should_fail/T15591[bc]
ghci/scripts/T15591
86 files changed, 1601 insertions, 951 deletions
diff --git a/compiler/basicTypes/Var.hs b/compiler/basicTypes/Var.hs index 2009b6c764..a23132eb66 100644 --- a/compiler/basicTypes/Var.hs +++ b/compiler/basicTypes/Var.hs @@ -405,6 +405,23 @@ sameVis Required _ = False sameVis _ Required = False sameVis _ _ = True +instance Outputable ArgFlag where + ppr Required = text "[req]" + ppr Specified = text "[spec]" + ppr Inferred = text "[infrd]" + +instance Binary ArgFlag where + put_ bh Required = putByte bh 0 + put_ bh Specified = putByte bh 1 + put_ bh Inferred = putByte bh 2 + + get bh = do + h <- getByte bh + case h of + 0 -> return Required + 1 -> return Specified + _ -> return Inferred + {- ********************************************************************* * * * VarBndr, TyCoVarBinder @@ -469,6 +486,19 @@ mkTyVarBinders vis = map (mkTyVarBinder vis) isTyVarBinder :: TyCoVarBinder -> Bool isTyVarBinder (Bndr v _) = isTyVar v +instance Outputable tv => Outputable (VarBndr tv ArgFlag) where + ppr (Bndr v Required) = ppr v + ppr (Bndr v Specified) = char '@' <> ppr v + ppr (Bndr v Inferred) = braces (ppr v) + +instance (Binary tv, Binary vis) => Binary (VarBndr tv vis) where + put_ bh (Bndr tv vis) = do { put_ bh tv; put_ bh vis } + + get bh = do { tv <- get bh; vis <- get bh; return (Bndr tv vis) } + +instance NamedThing tv => NamedThing (VarBndr tv flag) where + getName (Bndr tv _) = getName tv + {- ************************************************************************ * * @@ -524,35 +554,6 @@ tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var <+> dcolon <+> pprKind ( setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar setTcTyVarDetails tv details = tv { tc_tv_details = details } -------------------------------------- -instance Outputable tv => Outputable (VarBndr tv ArgFlag) where - ppr (Bndr v Required) = ppr v - ppr (Bndr v Specified) = char '@' <> ppr v - ppr (Bndr v Inferred) = braces (ppr v) - -instance Outputable ArgFlag where - ppr Required = text "[req]" - ppr Specified = text "[spec]" - ppr Inferred = text "[infrd]" - -instance (Binary tv, Binary vis) => Binary (VarBndr tv vis) where - put_ bh (Bndr tv vis) = do { put_ bh tv; put_ bh vis } - - get bh = do { tv <- get bh; vis <- get bh; return (Bndr tv vis) } - - -instance Binary ArgFlag where - put_ bh Required = putByte bh 0 - put_ bh Specified = putByte bh 1 - put_ bh Inferred = putByte bh 2 - - get bh = do - h <- getByte bh - case h of - 0 -> return Required - 1 -> return Specified - _ -> return Inferred - {- %************************************************************************ %* * diff --git a/compiler/basicTypes/VarSet.hs b/compiler/basicTypes/VarSet.hs index ac3c545b2a..52faab5799 100644 --- a/compiler/basicTypes/VarSet.hs +++ b/compiler/basicTypes/VarSet.hs @@ -237,6 +237,7 @@ unitDVarSet = unitUniqDSet mkDVarSet :: [Var] -> DVarSet mkDVarSet = mkUniqDSet +-- The new element always goes to the right of existing ones. extendDVarSet :: DVarSet -> Var -> DVarSet extendDVarSet = addOneToUniqDSet diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index a425ad249e..8a7d3b4f6a 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -101,7 +101,7 @@ sortQuantVars :: [Var] -> [Var] sortQuantVars vs = sorted_tcvs ++ ids where (tcvs, ids) = partition (isTyVar <||> isCoVar) vs - sorted_tcvs = toposortTyVars tcvs + sorted_tcvs = scopedSort tcvs -- | Bind a binding group over an expression, using a @let@ or @case@ as -- appropriate (see "CoreSyn#let_app_invariant") diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index f2ff5dd623..447fea4871 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -862,7 +862,7 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs -- Add extra tyvar binders: Note [Free tyvars in rule LHS] -- and extra dict binders: Note [Free dictionaries in rule LHS] mk_extra_bndrs fn_id args - = toposortTyVars unbound_tvs ++ unbound_dicts + = scopedSort unbound_tvs ++ unbound_dicts where unbound_tvs = [ v | v <- unbound_vars, isTyVar v ] unbound_dicts = [ mkLocalId (localiseName (idName d)) (idType d) diff --git a/compiler/main/HscTypes.hs b/compiler/main/HscTypes.hs index 445c496253..bb89c58344 100644 --- a/compiler/main/HscTypes.hs +++ b/compiler/main/HscTypes.hs @@ -2015,8 +2015,8 @@ tyThingParent_maybe (AConLike cl) = case cl of RealDataCon dc -> Just (ATyCon (dataConTyCon dc)) PatSynCon{} -> Nothing tyThingParent_maybe (ATyCon tc) = case tyConAssoc_maybe tc of - Just cls -> Just (ATyCon (classTyCon cls)) - Nothing -> Nothing + Just tc -> Just (ATyCon tc) + Nothing -> Nothing tyThingParent_maybe (AnId id) = case idDetails id of RecSelId { sel_tycon = RecSelData tc } -> Just (ATyCon tc) diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot index b777fa187b..8cc83d7ac7 100644 --- a/compiler/prelude/TysWiredIn.hs-boot +++ b/compiler/prelude/TysWiredIn.hs-boot @@ -14,6 +14,8 @@ mkBoxedTupleTy :: [Type] -> Type coercibleTyCon, heqTyCon :: TyCon +unitTy :: Type + liftedTypeKind :: Kind constraintKind :: Kind diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index abdaaae7e2..f9ce0199c2 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -827,7 +827,7 @@ bindHsQTyVars :: forall a b. -> (LHsQTyVars GhcRn -> Bool -> RnM (b, FreeVars)) -- The Bool is True <=> all kind variables used in the -- kind signature are bound on the left. Reason: - -- the TypeInType clause of Note [Complete user-supplied + -- the last clause of Note [CUSKs: Complete user-supplied -- kind signatures] in HsDecls -> RnM (b, FreeVars) @@ -840,7 +840,6 @@ bindHsQTyVars :: forall a b. bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside = do { let hs_tv_bndrs = hsQTvExplicit hsq_bndrs bndr_kv_occs = extractHsTyVarBndrsKVs hs_tv_bndrs - ; rdr_env <- getLocalRdrEnv ; let -- See Note [bindHsQTyVars examples] for what -- all these various things are doing @@ -850,8 +849,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside -- Make sure to list the binder kvs before the -- body kvs, as mandated by -- Note [Ordering of implicit variables] - implicit_kvs = filter_occs rdr_env bndrs kv_occs - -- Deleting bndrs: See Note [Kind-variable ordering] + implicit_kvs = filter_occs bndrs kv_occs -- dep_bndrs is the subset of bndrs that are dependent -- i.e. appear in bndr/body_kv_occs -- Can't use implicit_kvs because we've deleted bndrs from that! @@ -879,17 +877,15 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside all_bound_on_lhs } } where - filter_occs :: LocalRdrEnv -- In scope - -> [Located RdrName] -- Bound here + filter_occs :: [Located RdrName] -- Bound here -> [Located RdrName] -- Potential implicit binders -> [Located RdrName] -- Final implicit binders -- Filter out any potential implicit binders that are either - -- already in scope, or are explicitly bound here - filter_occs rdr_env bndrs occs + -- already in scope, or are explicitly bound in the same HsQTyVars + filter_occs bndrs occs = filterOut is_in_scope occs where - is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ) - || locc `elemRdr` bndrs + is_in_scope locc = locc `elemRdr` bndrs {- Note [bindHsQTyVars examples] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1586,9 +1582,8 @@ must come after any variables mentioned in their kinds. typeRep :: Typeable a => TypeRep (a :: k) -- forall k a. ... The k comes first because a depends on k, even though the k appears later than -the a in the code. Thus, GHC does a *stable topological sort* on the variables. -By "stable", we mean that any two variables who do not depend on each other -preserve their existing left-to-right ordering. +the a in the code. Thus, GHC does ScopedSort on the variables. +See Note [ScopedSort] in Type. Implicitly bound variables are collected by any function which returns a FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably diff --git a/compiler/simplCore/SetLevels.hs b/compiler/simplCore/SetLevels.hs index b8212c72f3..009f7a818b 100644 --- a/compiler/simplCore/SetLevels.hs +++ b/compiler/simplCore/SetLevels.hs @@ -87,8 +87,7 @@ import Literal ( litIsTrivial ) import Demand ( StrictSig, Demand, isStrictDmd, splitStrictSig, increaseStrictSigArity ) import Name ( getOccName, mkSystemVarName ) import OccName ( occNameString ) -import Type ( Type, mkLamTypes, splitTyConApp_maybe, tyCoVarsOfType ) -import TyCoRep ( closeOverKindsDSet ) +import Type ( Type, mkLamTypes, splitTyConApp_maybe, tyCoVarsOfType, closeOverKindsDSet ) import BasicTypes ( Arity, RecFlag(..), isRec ) import DataCon ( dataConOrigResTy ) import TysWiredIn diff --git a/compiler/simplCore/SimplUtils.hs b/compiler/simplCore/SimplUtils.hs index ca1b9bd23d..d4726abf59 100644 --- a/compiler/simplCore/SimplUtils.hs +++ b/compiler/simplCore/SimplUtils.hs @@ -1763,7 +1763,7 @@ abstractFloats dflags top_lvl main_tvs floats body rhs' = CoreSubst.substExpr (text "abstract_floats2") subst rhs -- tvs_here: see Note [Which type variables to abstract over] - tvs_here = toposortTyVars $ + tvs_here = scopedSort $ filter (`elemVarSet` main_tv_set) $ closeOverKindsList $ exprSomeFreeVarsList isTyVar rhs' @@ -1791,7 +1791,7 @@ abstractFloats dflags top_lvl main_tvs floats body -- If you ever want to be more selective, remember this bizarre case too: -- x::a = x -- Here, we must abstract 'x' over 'a'. - tvs_here = toposortTyVars main_tvs + tvs_here = scopedSort main_tvs mk_poly1 :: [TyVar] -> Id -> SimplM (Id, CoreExpr) mk_poly1 tvs_here var diff --git a/compiler/specialise/SpecConstr.hs b/compiler/specialise/SpecConstr.hs index f6d27ccba5..b07e480ff5 100644 --- a/compiler/specialise/SpecConstr.hs +++ b/compiler/specialise/SpecConstr.hs @@ -2091,7 +2091,7 @@ callToPats env bndr_occs call@(Call _ args con_env) -- See Note [Shadowing] at the top (ktvs, ids) = partition isTyVar qvars - qvars' = toposortTyVars ktvs ++ map sanitise ids + qvars' = scopedSort ktvs ++ map sanitise ids -- Order into kind variables, type variables, term variables -- The kind of a type variable may mention a kind variable -- and the type of a term variable may mention a type variable diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 8f1f7ba5f6..5825232574 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -168,7 +168,13 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) -- Note [Linting type synonym applications]. case lintTypes dflags tcvs' (rhs':lhs') of Nothing -> pure () - Just fail_msg -> pprPanic "Core Lint error" fail_msg + Just fail_msg -> pprPanic "Core Lint error" (vcat [ fail_msg + , ppr fam_tc + , ppr subst + , ppr tvs' + , ppr cvs' + , ppr lhs' + , ppr rhs' ]) ; return (FamInst { fi_fam = tyConName fam_tc , fi_flavor = flavor , fi_tcs = roughMatchTcs lhs @@ -893,7 +899,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn has_kinds = not $ isEmptyVarSet invis_vars doc = sep [ what <+> text "variable" <> - pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . toposortTyVars) + pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort) , text "cannot be inferred from the right-hand side." ] what = case (has_types, has_kinds) of (True, True) -> text "Type and kind" diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs index 118a219af6..fe29c3d1d0 100644 --- a/compiler/typecheck/TcClassDcl.hs +++ b/compiler/typecheck/TcClassDcl.hs @@ -514,8 +514,8 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs) rhs' = substTyUnchecked subst' rhs_ty tcv' = tyCoVarsOfTypesList pat_tys' (tv', cv') = partition isTyVar tcv' - tvs' = toposortTyVars tv' - cvs' = toposortTyVars cv' + tvs' = scopedSort tv' + cvs' = scopedSort cv' ; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys' ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' cvs' fam_tc pat_tys' rhs' diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 6f749fc60f..bb9c76ba61 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -815,7 +815,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred final_tkvs = tyCoVarsOfTypesWellScoped $ final_cls_tys ++ final_tc_args - ; let tkvs = toposortTyVars $ fvVarList $ + ; let tkvs = scopedSort $ fvVarList $ unionFV (tyCoFVsOfTypes tc_args_to_keep) (FV.mkFVs deriv_tvs) Just kind_subst = mb_match diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 951107bbcf..1fd98f1aa5 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -485,7 +485,7 @@ reportBadTelescope ctxt env (Just telescope) skols text "are out of dependency order. Perhaps try this ordering:") 2 (pprTyVars sorted_tvs) - sorted_tvs = toposortTyVars skols + sorted_tvs = scopedSort skols reportBadTelescope _ _ Nothing skols = pprPanic "reportBadTelescope" (ppr skols) diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index b3a4d536d1..84147c6b64 100644 --- a/compiler/typecheck/TcGenDeriv.hs +++ b/compiler/typecheck/TcGenDeriv.hs @@ -1840,8 +1840,8 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty rep_rhs_ty = mkTyConApp fam_tc rep_rhs_tys rep_tcvs = tyCoVarsOfTypesList rep_lhs_tys (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs - rep_tvs' = toposortTyVars rep_tvs - rep_cvs' = toposortTyVars rep_cvs + rep_tvs' = scopedSort rep_tvs + rep_cvs' = scopedSort rep_cvs pp_lhs = ppr (mkTyConApp fam_tc rep_lhs_tys) -- Same as inst_tys, but with the last argument type replaced by the diff --git a/compiler/typecheck/TcGenGenerics.hs b/compiler/typecheck/TcGenGenerics.hs index 9da94280ce..6372c66912 100644 --- a/compiler/typecheck/TcGenGenerics.hs +++ b/compiler/typecheck/TcGenGenerics.hs @@ -434,8 +434,8 @@ tc_mkRepFamInsts gk tycon inst_tys = repTy' = substTy subst repTy tcv' = tyCoVarsOfTypeList inst_ty (tv', cv') = partition isTyVar tcv' - tvs' = toposortTyVars tv' - cvs' = toposortTyVars cv' + tvs' = scopedSort tv' + cvs' = scopedSort cv' axiom = mkSingleCoAxiom Nominal rep_name tvs' cvs' fam_tc inst_tys repTy' diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index a2016888c2..f5fedc9d51 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -423,7 +423,7 @@ zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar) -- This guarantees to return a TyVar (not a TcTyVar) -- then we add it to the envt, so all occurrences are replaced zonkTyBndrX env tv - = ASSERT( isImmutableTyVar tv ) + = ASSERT2( isImmutableTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) ) do { ki <- zonkTcTypeToTypeX env (tyVarKind tv) -- Internal names tidy up better, for iface files. ; let tv' = mkTyVar (tyVarName tv) ki diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 2194fa08fa..3706c236c6 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -53,7 +53,10 @@ module TcHsType ( zonkPromoteType, -- Pattern type signatures - tcHsPatSigType, tcPatSig, funAppCtxt + tcHsPatSigType, tcPatSig, + + -- Error messages + funAppCtxt, addTyConFlavCtxt ) where #include "HsVersions.h" @@ -1368,7 +1371,7 @@ as a degenerate case of some (pi (x :: t) -> s) and then this will all get more permissive. Note [Kind generalisation and TyVarTvs] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider data T (a :: k1) x = MkT (S a ()) data S (b :: k2) y = MkS (T b ()) @@ -1383,7 +1386,7 @@ in TcBinds. There are some wrinkles * We always want to kind-generalise over TyVarTvs, and /not/ default - them to Type. Another way to say this is: a SigTV should /never/ + them to Type. Another way to say this is: a TyVarTv should /never/ stand for a type, even via defaulting. Hence the check in TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's another example (Trac #14555): @@ -1396,12 +1399,22 @@ There are some wrinkles data SameKind :: k -> k -> * data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) Here we will unify k1 with k2, but this time doing so is an error, - because k1 and k2 are bound in the same delcaration. + because k1 and k2 are bound in the same declaration. - We sort this out using findDupTyVarTvs, in TcTyClTyVars; very much + We sort this out using findDupTyVarTvs, in TcHsType.tcTyClTyVars; very much as we do with partial type signatures in mk_psig_qtvs in TcBinds.chooseInferredQuantifiers +* Even the Required arguments should be made into TyVarTvs, not skolems. + Consider + + data T k (a :: k) + + Here, k is a Required, dependent variable. For uniformity, it is helpful + to have k be a TyVarTv, in parallel with other dependent variables. + (This is key in the call to quantifyTyVars in kcTyClGroup, where quantifyTyVars + expects not to see unknown skolems.) + Note [Keeping scoped variables in order: Explicit] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When the user writes `forall a b c. blah`, we bring a, b, and c into @@ -1432,7 +1445,7 @@ signature), we need to come up with some ordering on these variables. This is done by bumping the TcLevel, bringing the tyvars into scope, and then type-checking the thing_inside. The constraints are all wrapped in an implication, which is then solved. Finally, we can -zonk all the binders and then order them with toposortTyVars. +zonk all the binders and then order them with scopedSort. It's critical to solve before zonking and ordering in order to uncover any unifications. You might worry that this eager solving could cause @@ -1468,8 +1481,9 @@ raise the TcLevel. To avoid these variables from ever being visible in the surrounding context, we must obey the following dictum: Every metavariable in a type must either be - (A) promoted, or - (B) generalized. + (A) promoted + (B) generalized, or + (C) zapped to Any 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 @@ -1479,6 +1493,8 @@ sig -- or because the metavars are constrained -- see kindGeneralizeLocal) we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables] in TcType. +For more about (C), see Note [Naughty quantification candidates] in TcMType. + After promoting/generalizing, we need to zonk *again* because both promoting and generalizing fill in metavariables. @@ -1514,69 +1530,93 @@ tcWildCardBinders wc_names thing_inside kcLHsQTyVars :: Name -- ^ of the thing being checked -> TyConFlavour -- ^ What sort of 'TyCon' is being checked -> Bool -- ^ True <=> the decl being checked has a CUSK - -> [(Name, TyVar)] -- ^ If the thing being checked is associated - -- with a class, this is the class's scoped - -- type variables. Empty otherwise. -> LHsQTyVars GhcRn -> TcM Kind -- ^ The result kind -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon -kcLHsQTyVars name flav cusk parent_tv_prs +kcLHsQTyVars name flav cusk user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns , hsq_dependent = dep_names } , hsq_explicit = hs_tvs }) thing_inside | cusk - = do { (scoped_kvs, (tc_tvs, res_kind)) + -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls + = addTyConFlavCtxt name flav $ + do { (scoped_kvs, (tc_tvs, res_kind)) <- solveEqualities $ tcImplicitQTKBndrs skol_info kv_ns $ kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside - -- Now, because we're in a CUSK, quantify over the mentioned - -- kind vars, in dependency order. - ; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs - ; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $ - mkTyConKind tc_binders_unzonked res_kind) - ; let -- Any type variables bound by the parent class that are specified - -- in this declaration (associated with the class). We single - -- these out because we want to bind these first in this - -- declaration's kind. - -- See Note [Kind variable ordering for associated types]. - reused_from_parent_tv_prs = - filter (\(_, tv) -> tv `elemDVarSet` dv_kvs dvs - || tv `elemDVarSet` dv_tvs dvs) parent_tv_prs - reused_from_parent_tvs = map snd reused_from_parent_tv_prs - ; qkvs <- quantifyTyVars (mkVarSet reused_from_parent_tvs) dvs - -- don't call tcGetGlobalTyCoVars. For associated types, it gets the - -- tyvars from the enclosing class -- but that's wrong. We *do* want - -- to quantify over those tyvars. - - ; scoped_kvs <- mapM zonkTcTyVarToTyVar scoped_kvs - ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs - ; res_kind <- zonkTcType res_kind - ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs - - -- If any of the scoped_kvs aren't actually mentioned in a binder's + ; let class_tc_binders + | Just class_tc <- tyConFlavourAssoc_maybe flav + = tyConBinders class_tc -- class has a CUSK, so these are zonked + -- and fully settled + | otherwise + = [] + + class_tv_set = mkVarSet (binderVars class_tc_binders) + local_specified = filterOut (`elemVarSet` class_tv_set) scoped_kvs + -- NB: local_specified are guaranteed to be in a well-scoped + -- order because of tcImplicitQTKBndrs + + -- NB: candidateQTyVarsOfType is OK with unzonked input + ; candidates <- candidateQTyVarsOfType class_tv_set $ + mkSpecForAllTys local_specified $ + mkSpecForAllTys tc_tvs $ + res_kind + -- The type above is a bit wrong, in that we're using foralls for all + -- the tc_tvs, even those that aren't dependent. This is OK, though, + -- because we're building the type only to extract the variables to + -- quantify. We use mk_tc_binder below to get this right. + + ; local_inferred <- quantifyTyVars class_tv_set candidates + + ; local_specified <- mapM zonkTyCoVarKind local_specified + ; tc_tvs <- mapM zonkTyCoVarKind tc_tvs + ; res_kind <- zonkTcType res_kind + + ; let dep_tv_set = tyCoVarsOfTypes (res_kind : map tyVarKind tc_tvs) + local_tcbs = concat [ mkNamedTyConBinders Inferred local_inferred + , mkNamedTyConBinders Specified local_specified + , map (mkRequiredTyConBinder dep_tv_set) tc_tvs ] + + free_class_tv_set = tyCoVarsOfTypes (res_kind : map binderType local_tcbs) + `delVarSetList` map binderVar local_tcbs + + used_class_tcbs = filter ((`elemVarSet` free_class_tv_set) . binderVar) + class_tc_binders + + -- Suppose we have class C k where type F (x :: k). We can't have + -- k *required* in F, so it becomes Specified + to_invis_tcb tcb + | Required <- tyConBinderArgFlag tcb + = mkNamedTyConBinder Specified (binderVar tcb) + | otherwise + = tcb + + used_class_tcbs_invis = map to_invis_tcb used_class_tcbs + + all_tcbs = used_class_tcbs_invis ++ local_tcbs + + -- If the ordering from + -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls + -- doesn't work, we catch it here, before an error cascade + ; checkValidTelescope all_tcbs (ppr user_tyvars) + + -- If any of the all_kvs 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 all_tc_tvs = scoped_kvs ++ tc_tvs - all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind) - all_tc_tvs - `unionVarSet` tyCoVarsOfType res_kind - unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs) - scoped_kvs - ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs - - ; let all_scoped_kvs = reused_from_parent_tvs ++ scoped_kvs - final_binders = map (mkNamedTyConBinder Inferred) qkvs - ++ map (mkNamedTyConBinder Specified) all_scoped_kvs - ++ tc_binders - all_tv_prs = reused_from_parent_tv_prs ++ - mkTyVarNamePairs (scoped_kvs ++ tc_tvs) - tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind - all_tv_prs flav - -- the tvs contain the binders already - -- in scope from an enclosing class, but - -- re-adding tvs to the env't doesn't cause - -- harm + ; let all_kvs = concat [ map binderVar used_class_tcbs_invis + , local_inferred + , local_specified ] + + all_mentioned_tvs = dep_tv_set `unionVarSet` + tyCoVarsOfTypes (map tyVarKind all_kvs) + + unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs) all_kvs + ; reportFloatingKvs name flav (map binderVar all_tcbs) unmentioned_kvs + + ; let all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) + tycon = mkTcTyCon name (ppr user_tyvars) all_tcbs res_kind + all_tv_prs True {- it is generalised -} flav ; traceTc "kcLHsQTyVars: cusk" $ vcat [ text "name" <+> ppr name @@ -1584,17 +1624,11 @@ kcLHsQTyVars name flav cusk parent_tv_prs , text "hs_tvs" <+> ppr hs_tvs , text "dep_names" <+> ppr dep_names , text "scoped_kvs" <+> ppr scoped_kvs - , text "reused_from_parent_tv_prs" - <+> ppr reused_from_parent_tv_prs , text "tc_tvs" <+> ppr tc_tvs , text "res_kind" <+> ppr res_kind - , text "dvs" <+> ppr dvs - , text "qkvs" <+> ppr qkvs - , text "all_scoped_kvs" <+> ppr all_scoped_kvs - , text "tc_binders" <+> ppr tc_binders - , text "final_binders" <+> ppr final_binders - , text "mkTyConKind final_binders res_kind" - <+> ppr (mkTyConKind final_binders res_kind) + , text "all_tcbs" <+> ppr all_tcbs + , text "mkTyConKind all_tcbs res_kind" + <+> ppr (mkTyConKind all_tcbs res_kind) , text "all_tv_prs" <+> ppr all_tv_prs ] ; return tycon } @@ -1607,10 +1641,15 @@ kcLHsQTyVars name flav cusk parent_tv_prs kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they - -- must remain lined up with the binders + -- might unify with kind vars in other types in a mutually + -- recursive group. See Note [Kind generalisation and TyVarTvs] tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs + -- Also, note that tc_binders has the tyvars from only the + -- user-written tyvarbinders. See S1 in Note [How TcTyCons work] + -- in TcTyClsDecls tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind (mkTyVarNamePairs (scoped_kvs ++ tc_tvs)) + False -- not yet generalised flav ; traceTc "kcLHsQTyVars: not-cusk" $ @@ -1629,7 +1668,7 @@ kcLHsQTyVars name flav cusk parent_tv_prs | otherwise = mkAnonTyConBinder tv -kcLHsQTyVars _ _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" +kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" kcLHsQTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope -> Bool -- True <=> Default un-annotated tyvar @@ -1679,7 +1718,7 @@ kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing -- Open type/data families default their variables -- variables to kind *. But don't default in-scope -- class tyvars, of course - ; tv <- newSkolemTyVar name kind + ; tv <- new_tv name kind ; return (tv, False) } } kc_hs_tv (KindedTyVar _ lname@(L _ name) lhs_kind) @@ -1691,11 +1730,18 @@ kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing unifyKind (Just (HsTyVar noExt NotPromoted lname)) kind (tyVarKind tv) ; return (tv, True) } - _ -> do { tv <- newSkolemTyVar name kind + _ -> do { tv <- new_tv name kind ; return (tv, False) } } kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv" + + new_tv :: Name -> Kind -> TcM TcTyVar + new_tv + | cusk = newSkolemTyVar + | otherwise = newTyVarTyVar + -- Third wrinkle in Note [Kind generalisation and TyVarTvs] + {- Note [Kind-checking tyvar binders for associated types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When kind-checking the type-variable binders for associated @@ -1762,10 +1808,13 @@ kcImplicitTKBndrs :: [Name] -- of the vars -> TcM ([TcTyVar], a) -- returns the tyvars created -- these are *not* dependency ordered kcImplicitTKBndrs var_ns thing_inside - = do { tkvs <- mapM newFlexiKindedTyVarTyVar var_ns - ; result <- tcExtendTyVarEnv tkvs thing_inside - ; return (tkvs, result) } - + -- NB: Just use tyvars that are in scope, if any. Otherwise, we + -- get #15711, where GHC forgets that a variable used in an associated + -- type is the same as the one used in the enclosing class + = do { tkvs_pairs <- mapM (newFlexiKindedQTyVar newTyVarTyVar) var_ns + ; let tkvs_to_scope = [ tkv | (tkv, True) <- tkvs_pairs ] + ; result <- tcExtendTyVarEnv tkvs_to_scope thing_inside + ; return (map fst tkvs_pairs, result) } tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs :: SkolemInfo @@ -1774,7 +1823,8 @@ tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs -> TcM ([TcTyVar], a) tcImplicitTKBndrs = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedTyVarTyVar -tcImplicitQTKBndrs = tcImplicitTKBndrsX newFlexiKindedQTyVar +tcImplicitQTKBndrs = tcImplicitTKBndrsX + (\nm -> fst <$> newFlexiKindedQTyVar newSkolemTyVar nm) tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function -> SkolemInfo @@ -1809,19 +1859,20 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside -- do a stable topological sort, following -- Note [Ordering of implicit variables] in RnTypes - ; let final_tvs = toposortTyVars skol_tvs + ; let final_tvs = scopedSort skol_tvs ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs) ; return (final_tvs, result) } -newFlexiKindedQTyVar :: Name -> TcM TcTyVar --- Make a new skolem for an implicit binder in a type/class/type +newFlexiKindedQTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM (TcTyVar, Bool) +-- Make a new tyvar for an implicit binder in a type/class/type -- instance declaration, with a flexi-kind -- But check for in-scope-ness, and if so return that instead -newFlexiKindedQTyVar name +-- Returns True as second return value iff this created a real new tyvar +newFlexiKindedQTyVar mk_tv name = do { mb_tv <- tcLookupLcl_maybe name ; case mb_tv of - Just (ATyVar _ tv) -> return tv - _ -> newFlexiKindedSkolemTyVar name } + Just (ATyVar _ tv) -> return (tv, False) + _ -> (, True) <$> newFlexiKindedTyVar mk_tv name } newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar newFlexiKindedTyVar new_tv name @@ -1981,17 +2032,21 @@ kindGeneralizeLocal wanted kind_or_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 + ; let mono_tvs = gbl_tvs `unionVarSet` constrained + + -- use the "Kind" variant here, as any types we see + -- here will already have all type variables quantified; + -- thus, every free variable is really a kv, never a tv. + ; dvs <- candidateQTyVarsOfKind mono_tvs kind_or_type + ; traceTc "kindGeneralizeLocal" (vcat [ ppr wanted , ppr kind_or_type , ppr constrained + , ppr mono_tvs , ppr dvs ]) - ; quantifyTyVars (gbl_tvs `unionVarSet` constrained) dvs } + ; quantifyTyVars mono_tvs dvs } {- Note [Kind generalisation] @@ -2819,3 +2874,9 @@ failIfEmitsConstraints thing_inside ; reportAllUnsolved lie ; return res } + +-- | Add a "In the data declaration for T" or some such. +addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a +addTyConFlavCtxt name flav + = addErrCtxt $ hsep [ text "In the", ppr flav + , text "declaration for", quotes (ppr name) ] diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index c9d9dd0ab6..ba2fd7588e 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -648,7 +648,7 @@ tcDataFamInstDecl mb_clsinfo ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) -> do { let ty_binders = full_tcbs `chkAppend` extra_tcbs ; data_cons <- tcConDecls rec_rep_tc - (ty_binders, orig_res_ty) cons + ty_binders orig_res_ty cons ; tc_rhs <- case new_or_data of DataType -> return (mkDataTyConRhs data_cons) NewType -> ASSERT( not (null data_cons) ) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index fb5f1b515a..c3786e20bf 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -25,7 +25,7 @@ module TcMType ( newFmvTyVar, newFskTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, - newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar, + newMetaDetails, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- -- Expected types @@ -67,10 +67,11 @@ module TcMType ( zonkTcTyVarToTyVar, zonkTyVarTyVarPairs, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkTyCoVarsAndFVList, - zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars, + candidateQTyVarsOfType, candidateQTyVarsOfKind, + candidateQTyVarsOfTypes, CandidatesQTvs(..), zonkQuantifiedTyVar, defaultTyVar, quantifyTyVars, - zonkTcTyCoVarBndr, zonkTcTyVarBinder, + zonkTcTyCoVarBndr, zonkTyConBinders, zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, @@ -93,6 +94,7 @@ import GhcPrelude import TyCoRep import TcType import Type +import TyCon import Coercion import Class import Var @@ -119,8 +121,9 @@ import qualified GHC.LanguageExtensions as LangExt import Control.Monad import Maybes -import Data.List ( mapAccumL ) +import Data.List ( mapAccumL, partition ) import Control.Arrow ( second ) +import qualified Data.Semigroup as Semi {- ************************************************************************ @@ -703,16 +706,23 @@ readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTyVarRef tyvar) +isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type) +isFilledMetaTyVar_maybe tv + | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv + = do { cts <- readTcRef ref + ; case cts of + Indirect ty -> return (Just ty) + Flexi -> return Nothing } + | otherwise + = return Nothing + isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable -isFilledMetaTyVar tv - | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv - = do { details <- readMutVar ref - ; return (isIndirect details) } - | otherwise = return False +isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv isUnfilledMetaTyVar :: TyVar -> TcM Bool -- True of a un-filled-in (Flexi) meta type variable +-- NB: Not the opposite of isFilledMetaTyVar isUnfilledMetaTyVar tv | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv = do { details <- readMutVar ref @@ -794,7 +804,6 @@ writeMetaTyVarRef tyvar ref ty double_upd_msg details = hang (text "Double update of meta tyvar") 2 (ppr tyvar $$ ppr details) - {- Note [Level check when unifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When unifying @@ -961,6 +970,291 @@ newMetaTyVarTyAtLevel tc_lvl kind {- ********************************************************************* * * + Finding variables to quantify over +* * +********************************************************************* -} + +data CandidatesQTvs -- See Note [Dependent type variables] + -- See Note [CandidatesQTvs determinism and order] + -- NB: All variables stored here are MetaTvs. No exceptions. + = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) + , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) + -- A variable may appear in both sets + -- E.g. T k (x::k) The first occurrence of k makes it + -- show up in dv_tvs, the second in dv_kvs + -- See Note [Dependent type variables] + , dv_cvs :: CoVarSet + -- These are covars. We will *not* quantify over these, but + -- we must make sure also not to quantify over any cv's kinds, + -- so we include them here as further direction for quantifyTyVars + } + +instance Semi.Semigroup CandidatesQTvs where + (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 }) + <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 }) + = DV { dv_kvs = kv1 `unionDVarSet` kv2 + , dv_tvs = tv1 `unionDVarSet` tv2 + , dv_cvs = cv1 `unionVarSet` cv2 } + +instance Monoid CandidatesQTvs where + mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet } + mappend = (Semi.<>) + +instance Outputable CandidatesQTvs where + ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) + = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs + , text "dv_tvs =" <+> ppr tvs + , text "dv_cvs =" <+> ppr cvs ]) + +closeOverKindsCQTvs :: TyCoVarSet -- globals + -> CandidatesQTvs -> TcM CandidatesQTvs +-- Don't close the covars; this is done in quantifyTyVars. Note that +-- closing over the CoVars would introduce tyvars into the CoVarSet. +closeOverKindsCQTvs gbl_tvs dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) + = do { let all_kinds = map tyVarKind (dVarSetElems (kvs `unionDVarSet` tvs)) + ; foldlM (collect_cand_qtvs True gbl_tvs) dv all_kinds } + +{- Note [Dependent type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In Haskell type inference we quantify over type variables; but we only +quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds +we default the kind variables to *. + +So, to support this defaulting, and only for that reason, when +collecting the free vars of a type, prior to quantifying, we must keep +the type and kind variables separate. + +But what does that mean in a system where kind variables /are/ type +variables? It's a fairly arbitrary distinction based on how the +variables appear: + + - "Kind variables" appear in the kind of some other free variable + + These are the ones we default to * if -XPolyKinds is off + + - "Type variables" are all free vars that are not kind variables + +E.g. In the type T k (a::k) + 'k' is a kind variable, because it occurs in the kind of 'a', + even though it also appears at "top level" of the type + 'a' is a type variable, because it doesn't + +We gather these variables using a CandidatesQTvs record: + DV { dv_kvs: Variables free in the kind of a free type variable + or of a forall-bound type variable + , dv_tvs: Variables sytactically free in the type } + +So: dv_kvs are the kind variables of the type + (dv_tvs - dv_kvs) are the type variable of the type + +Note that + +* A variable can occur in both. + T k (x::k) The first occurrence of k makes it + show up in dv_tvs, the second in dv_kvs + +* We include any coercion variables in the "dependent", + "kind-variable" set because we never quantify over them. + +* The "kind variables" might depend on each other; e.g + (k1 :: k2), (k2 :: *) + The "type variables" do not depend on each other; if + one did, it'd be classified as a kind variable! + +Note [CandidatesQTvs determinism and order] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Determinism: when we quantify over type variables we decide the + order in which they appear in the final type. Because the order of + type variables in the type can end up in the interface file and + affects some optimizations like worker-wrapper, we want this order to + be deterministic. + + To achieve that we use deterministic sets of variables that can be + converted to lists in a deterministic order. For more information + about deterministic sets see Note [Deterministic UniqFM] in UniqDFM. + +* Order: as well as being deterministic, we use an + accumulating-parameter style for candidateQTyVarsOfType so that we + add variables one at a time, left to right. That means we tend to + produce the variables in left-to-right order. This is just to make + it bit more predicatable for the programmer. + +Note [Naughty quantification candidates] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#14880, dependent/should_compile/T14880-2) + + forall arg. ... (alpha[tau]:arg) ... + +We have a metavariable alpha whose kind is a locally bound (skolem) variable. +This can arise while type-checking a user-written type signature +(see the test case for the full code). According to +Note [Recipe for checking a signature] in TcHsType, we try to solve +all constraints that arise during checking before looking to kind-generalize. +However, in the case above, this solving pass does not unify alpha, because +it is utterly unconstrained. The question is: what to do with alpha? + +We can't generalize it, because it would have to be generalized *after* +arg, and implicit generalization always goes before explicit generalization. +We can't simply leave it be, because this type is about to go into the +typing environment (as the type of some let-bound variable, say), and then +chaos erupts when we try to instantiate. In any case, we'll never learn +anything more about alpha anyway. + +So, we zap it, eagerly, to Any. We don't have to do this eager zapping +in terms (say, in `length []`) because terms are never re-examined before +the final zonk (which zaps any lingering metavariables to Any). + +The right time to do this eager zapping is during generalization, when +every metavariable is either (A) promoted, (B) generalized, or (C) zapped +(according again to Note [Recipe for checking a signature] in TcHsType). + +Accordingly, when quantifyTyVars is skolemizing the variables to quantify, +these naughty ones are zapped to Any. We identify the naughty ones by +looking for out-of-scope tyvars in the candidate tyvars' kinds, where +we assume that all in-scope tyvars are in the gbl_tvs passed to quantifyTyVars. +In the example above, we would have `alpha` in the CandidatesQTvs, but +`arg` wouldn't be in the gbl_tvs. Hence, alpha is naughty, and zapped to +Any. Naughty variables are discovered by is_naughty_tv in quantifyTyVars. + +-} + +-- | Gathers free variables to use as quantification candidates (in +-- 'quantifyTyVars'). This might output the same var +-- in both sets, if it's used in both a type and a kind. +-- See Note [CandidatesQTvs determinism and order] +-- See Note [Dependent type variables] +candidateQTyVarsOfType :: TcTyVarSet -- zonked set of global/mono tyvars + -> TcType -- not necessarily zonked + -> TcM CandidatesQTvs +candidateQTyVarsOfType gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<< + collect_cand_qtvs False gbl_tvs mempty ty + +-- | Like 'candidateQTyVarsOfType', but consider every free variable +-- to be dependent. This is appropriate when generalizing a *kind*, +-- instead of a type. (That way, -XNoPolyKinds will default the variables +-- to Type.) +candidateQTyVarsOfKind :: TcTyVarSet -- zonked set of global/mono tyvars + -> TcKind -- not necessarily zonked + -> TcM CandidatesQTvs +candidateQTyVarsOfKind gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<< + collect_cand_qtvs True gbl_tvs mempty ty + +collect_cand_qtvs :: Bool -- True <=> consider every fv in Type to be dependent + -> VarSet -- bound variables (both locally bound and globally bound) + -> CandidatesQTvs -> Type -> TcM CandidatesQTvs +collect_cand_qtvs is_dep bound dvs ty + = go dvs ty + where + go dv (AppTy t1 t2) = foldlM go dv [t1, t2] + go dv (TyConApp _ tys) = foldlM go dv tys + go dv (FunTy arg res) = foldlM go dv [arg, res] + go dv (LitTy {}) = return dv + go dv (CastTy ty co) = do dv1 <- go dv ty + collect_cand_qtvs_co bound dv1 co + go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co + + go dv (TyVarTy tv) + | is_bound tv + = return dv + + | isImmutableTyVar tv + = WARN(True, (sep [ text "Note [Naughty quantification candidates] skolem:" + , ppr tv <+> dcolon <+> ppr (tyVarKind tv) ])) + return dv -- This happens when processing kinds of variables affected by + -- Note [Naughty quantification candidates] + -- NB: CandidatesQTvs stores only MetaTvs, so don't store an + -- immutable tyvar here. + + | otherwise + = ASSERT2( isMetaTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) $$ ppr ty $$ ppr bound ) + do { m_contents <- isFilledMetaTyVar_maybe tv + ; case m_contents of + Just ind_ty -> go dv ind_ty + + Nothing -> return $ insert_tv dv tv } + + go dv (ForAllTy (Bndr tv _) ty) + = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv) + ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty } + + is_bound tv = tv `elemVarSet` bound + + insert_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv + | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv } + | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv } + -- You might be tempted (like I was) to use unitDVarSet and mappend here. + -- However, the union algorithm for deterministic sets depends on (roughly) + -- the size of the sets. The elements from the smaller set end up to the + -- right of the elements from the larger one. When sets are equal, the + -- left-hand argument to `mappend` goes to the right of the right-hand + -- argument. In our case, if we use unitDVarSet and mappend, we learn that + -- the free variables of (a -> b -> c -> d) are [b, a, c, d], and we then + -- quantify over them in that order. (The a comes after the b because we + -- union the singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter, + -- the size criterion works to our advantage.) This is just annoying to + -- users, so I use `extendDVarSet`, which unambiguously puts the new element + -- to the right. Note that the unitDVarSet/mappend implementation would not + -- be wrong against any specification -- just suboptimal and confounding to users. + +collect_cand_qtvs_co :: VarSet -- bound variables + -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs +collect_cand_qtvs_co bound = go_co + where + go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty + go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty + go_mco dv1 mco + go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos + go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos + go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos + go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov + dv2 <- collect_cand_qtvs True bound dv1 t1 + collect_cand_qtvs True bound dv2 t2 + go_co dv (SymCo co) = go_co dv co + go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (NthCo _ _ co) = go_co dv co + go_co dv (LRCo _ co) = go_co dv co + go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (KindCo co) = go_co dv co + go_co dv (SubCo co) = go_co dv co + + go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole + case m_co of + Just co -> go_co dv co + Nothing -> return $ insert_cv dv (coHoleCoVar hole) + + go_co dv (CoVarCo cv) + | is_bound cv + = return dv + | otherwise + = return $ insert_cv dv cv + + go_co dv (ForAllCo tcv kind_co co) + = do { dv1 <- go_co dv kind_co + ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co } + + go_mco dv MRefl = return dv + go_mco dv (MCo co) = go_co dv co + + go_prov dv UnsafeCoerceProv = return dv + go_prov dv (PhantomProv co) = go_co dv co + go_prov dv (ProofIrrelProv co) = go_co dv co + go_prov dv (PluginProv _) = return dv + + insert_cv dv@(DV { dv_cvs = cvs }) cv + = dv { dv_cvs = cvs `extendVarSet` cv } + + is_bound tv = tv `elemVarSet` bound + +-- | Like 'splitDepVarsOfType', but over a list of types +candidateQTyVarsOfTypes :: TyCoVarSet -- zonked global ty/covars + -> [Type] -> TcM CandidatesQTvs +candidateQTyVarsOfTypes gbl_tvs tys = closeOverKindsCQTvs gbl_tvs =<< + foldlM (collect_cand_qtvs False gbl_tvs) mempty tys + +{- ********************************************************************* +* * Quantification * * ************************************************************************ @@ -988,7 +1282,7 @@ has free vars {f,a}, but we must add 'k' as well! Hence step (2). With -XPolyKinds, it treats both classes of variables identically. * quantifyTyVars never quantifies over - - a coercion variable + - a coercion variable (or any tv mentioned in the kind of a covar) - a runtime-rep variable Note [quantifyTyVars determinism] @@ -1007,52 +1301,61 @@ Note [Deterministic UniqFM] in UniqDFM. quantifyTyVars :: TcTyCoVarSet -- Global tvs; already zonked - -> CandidatesQTvs -- See Note [Dependent type variables] in TcType + -> CandidatesQTvs -- See Note [Dependent type variables] -- Already zonked -> TcM [TcTyVar] -- See Note [quantifyTyVars] -- Can be given a mixture of TcTyVars and TyVars, in the case of -- associated type declarations. Also accepts covars, but *never* returns any. - -quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) - = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs]) - ; let dep_kvs = dVarSetElemsWellScoped $ - dep_tkvs `dVarSetMinusVarSet` gbl_tvs +quantifyTyVars gbl_tvs + dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars }) + = do { traceTc "quantifyTyVars 1" (vcat [ppr dvs, ppr gbl_tvs]) + ; let mono_tvs = gbl_tvs `unionVarSet` closeOverKinds covars + -- NB: All variables in the kind of a covar must not be + -- quantified over, as we don't quantify over the covar. + + dep_kvs = dVarSetElemsWellScoped $ + dep_tkvs `dVarSetMinusVarSet` mono_tvs -- dVarSetElemsWellScoped: put the kind variables into -- well-scoped order. -- E.g. [k, (a::k)] not the other way roud nondep_tvs = dVarSetElems $ (nondep_tkvs `minusDVarSet` dep_tkvs) - `dVarSetMinusVarSet` gbl_tvs - -- See Note [Dependent type variables] in TcType + `dVarSetMinusVarSet` mono_tvs + -- See Note [Dependent type variables] -- The `minus` dep_tkvs removes any kind-level vars -- e.g. T k (a::k) Since k appear in a kind it'll -- be in dv_kvs, and is dependent. So remove it from -- dv_tvs which will also contain k -- No worry about dependent covars here; -- they are all in dep_tkvs - -- No worry about scoping, because these are all - -- type variables -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV + -- See Note [Naughty quantification candidates] + (naughty_deps, final_dep_kvs) = partition (is_naughty_tv mono_tvs) dep_kvs + (naughty_nondeps, final_nondep_tvs) = partition (is_naughty_tv mono_tvs) nondep_tvs + + ; mapM_ zap_naughty_tv (naughty_deps ++ naughty_nondeps) + -- In the non-PolyKinds case, default the kind variables -- to *, and zonk the tyvars as usual. Notice that this -- may make quantifyTyVars return a shorter list -- than it was passed, but that's ok ; poly_kinds <- xoptM LangExt.PolyKinds - ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs - ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs + ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) final_dep_kvs + ; nondep_tvs' <- mapMaybeM (zonk_quant False) final_nondep_tvs ; let final_qtvs = dep_kvs' ++ nondep_tvs' -- Because of the order, any kind variables -- mentioned in the kinds of the nondep_tvs' -- now refer to the dep_kvs' - ; traceTc "quantifyTyVars" - (vcat [ text "globals:" <+> ppr gbl_tvs - , text "nondep:" <+> pprTyVars nondep_tvs - , text "dep:" <+> pprTyVars dep_kvs - , text "dep_kvs'" <+> pprTyVars dep_kvs' + ; traceTc "quantifyTyVars 2" + (vcat [ text "globals:" <+> ppr gbl_tvs + , text "mono_tvs:" <+> ppr mono_tvs + , text "nondep:" <+> pprTyVars nondep_tvs + , text "dep:" <+> pprTyVars dep_kvs + , text "dep_kvs'" <+> pprTyVars dep_kvs' , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ]) -- We should never quantify over coercion variables; check this @@ -1061,6 +1364,11 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) ; return final_qtvs } where + -- See Note [Naughty quantification candidates] + is_naughty_tv mono_tvs tv + = anyVarSet (isSkolemTyVar <&&> (not . (`elemVarSet` mono_tvs))) $ + tyCoVarsOfType (tyVarKind tv) + -- zonk_quant returns a tyvar if it should be quantified over; -- otherwise, it returns Nothing. The latter case happens for -- * Kind variables, with -XNoPolyKinds: don't quantify over these @@ -1080,6 +1388,10 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) False -> do { tv <- zonkQuantifiedTyVar tkv ; return (Just tv) } } + zap_naughty_tv tv + = WARN(True, text "naughty quantification candidate: " <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)) + writeMetaTyVar tv (anyTypeOfKind (tyVarKind tv)) + zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables @@ -1162,7 +1474,7 @@ skolemiseUnboundMetaTyVar tv ; kind <- zonkTcType (tyVarKind tv) ; let uniq = getUnique tv -- NB: Use same Unique as original tyvar. This is - -- important for TcHsType.splitTelescopeTvs to work properly + -- convenient in reading dumps, but is otherwise inessential. tv_name = getOccName tv final_name = mkInternalName uniq tv_name span @@ -1352,15 +1664,6 @@ zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet zonkTcTypeAndFV ty = tyCoVarsOfTypeDSet <$> zonkTcType ty --- | Zonk a type and call 'candidateQTyVarsOfType' on it. -zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs -zonkTcTypeAndSplitDepVars ty - = candidateQTyVarsOfType <$> zonkTcType ty - -zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs -zonkTcTypesAndSplitDepVars tys - = candidateQTyVarsOfTypes <$> mapM zonkTcType tys - zonkTyCoVar :: TyCoVar -> TcM TcType -- Works on TyVars and TcTyVars zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv @@ -1409,8 +1712,8 @@ zonkImplication implic@(Implic { ic_skols = skols , ic_given = given , ic_wanted = wanted , ic_info = info }) - = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds! - -- as Trac #7230 showed + = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds! + -- as Trac #7230 showed ; given' <- mapM zonkEvVar given ; info' <- zonkSkolemInfo info ; wanted' <- zonkWCRec wanted @@ -1552,7 +1855,7 @@ zonkTcTypeMapper = TyCoMapper , tcm_tyvar = const zonkTcTyVar , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv) , tcm_hole = hole - , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv + , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv , tcm_tycon = return } where hole :: () -> CoercionHole -> TcM Coercion @@ -1583,17 +1886,25 @@ zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar -- unification variables. zonkTcTyCoVarBndr tyvar | isTyVarTyVar tyvar - = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" <$> zonkTcTyVar tyvar + -- We want to preserve the binding location of the original TyVarTv. + -- This is important for error messages. If we don't do this, then + -- we get bad locations in, e.g., typecheck/should_fail/T2688 + = do { zonked_ty <- zonkTcTyVar tyvar + ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty + zonked_name = getName zonked_tyvar + reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar) + ; return (setTyVarName zonked_tyvar reloc'd_name) } | otherwise - -- can't use isCoVar, because it looks at a TyCon. Argh. - = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar ) - updateTyVarKindM zonkTcType tyvar - -zonkTcTyVarBinder :: VarBndr TcTyVar vis -> TcM (VarBndr TcTyVar vis) -zonkTcTyVarBinder (Bndr tv vis) - = do { tv' <- zonkTcTyCoVarBndr tv - ; return (Bndr tv' vis) } + = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar ) + zonkTyCoVarKind tyvar + +zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder] +zonkTyConBinders = mapM zonk1 + where + zonk1 (Bndr tv vis) + = do { tv' <- zonkTcTyCoVarBndr tv + ; return (Bndr tv' vis) } zonkTcTyVar :: TcTyVar -> TcM TcType -- Simply look through all Flexis diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index e86ff3c34b..4a770b563d 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -164,13 +164,6 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details (prov_theta, prov_evs) = unzip (mapMaybe mkProvEvidence filtered_prov_dicts) - -- Report bad universal type variables - -- See Note [Type variables whose kind is captured] - ; let bad_tvs = [ tv | tv <- univ_tvs - , tyCoVarsOfType (tyVarKind tv) - `intersectsVarSet` ex_tv_set ] - ; mapM_ (badUnivTvErr ex_tvs) bad_tvs - -- Report coercions that esacpe -- See Note [Coercions that escape] ; args <- mapM zonkId args @@ -217,20 +210,6 @@ mkProvEvidence ev_id pred = evVarPred ev_id eq_con_args = [evId ev_id] -badUnivTvErr :: [TyVar] -> TyVar -> TcM () --- See Note [Type variables whose kind is captured] -badUnivTvErr ex_tvs bad_tv - = addErrTc $ - vcat [ text "Universal type variable" <+> quotes (ppr bad_tv) - <+> text "has existentially bound kind:" - , nest 2 (ppr_with_kind bad_tv) - , hang (text "Existentially-bound variables:") - 2 (vcat (map ppr_with_kind ex_tvs)) - , text "Probable fix: give the pattern synonym a type signature" - ] - where - ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) - dependentArgErr :: (Id, DTyCoVarSet) -> TcM () -- See Note [Coercions that escape] dependentArgErr (arg, bad_cos) @@ -293,37 +272,6 @@ marginally less efficient, if the builder/martcher are not inlined. See also Note [Lift equality constaints when quantifying] in TcType -Note [Type variables whose kind is captured] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data AST a = Sym [a] - class Prj s where { prj :: [a] -> Maybe (s a) - pattern P x <= Sym (prj -> Just x) - -Here we get a matcher with this type - $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r - -No problem. But note that 's' is not fixed by the type of the -pattern (AST a), nor is it existentially bound. It's really only -fixed by the type of the continuation. - -Trac #14552 showed that this can go wrong if the kind of 's' mentions -existentially bound variables. We obviously can't make a type like - $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r) - -> r -> r -But neither is 's' itself existentially bound, so the forall (s::k->*) -can't go in the inner forall either. (What would the matcher apply -the continuation to?) - -So we just fail in this case, with a pretty terrible error message. -Maybe we could do better, but I can't see how. (It'd be possible to -default 's' to (Any k), but that probably isn't what the user wanted, -and it not straightforward to implement, because by the time we see -the problem, simplifyInfer has already skolemised 's'.) - -This stuff can only happen in the presence of view patterns, with -PolyKinds, so it's a bit of a corner case. - Note [Coercions that escape] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Trac #14507 showed an example where the inferred type of the matcher diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index 56f3f07a44..4bcd203a2b 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -86,8 +86,8 @@ tcRule (HsRule { rd_ext = ext ; (stuff,_) <- pushTcLevelM $ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs - ; let (id_bndrs, lhs', lhs_wanted - , rhs', rhs_wanted, rule_ty, tc_lvl) = stuff + ; let (tv_bndrs, id_bndrs, lhs', lhs_wanted + , rhs', rhs_wanted, rule_ty, tc_lvl) = stuff ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname , ppr lhs_wanted @@ -110,14 +110,16 @@ tcRule (HsRule { rd_ext = ext -- during zonking (see TcHsSyn.zonkRule) ; let tpl_ids = lhs_evs ++ id_bndrs - ; forall_tkvs <- zonkTcTypesAndSplitDepVars $ - rule_ty : map idType tpl_ids ; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level -- monomorphic bindings from the MR; test tc111 + ; forall_tkvs <- candidateQTyVarsOfTypes gbls $ + map (mkSpecForAllTys tv_bndrs) $ -- don't quantify over lexical tyvars + rule_ty : map idType tpl_ids ; qtkvs <- quantifyTyVars gbls forall_tkvs ; traceTc "tcRule" (vcat [ pprFullRuleName rname , ppr forall_tkvs , ppr qtkvs + , ppr tv_bndrs , ppr rule_ty , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] ]) @@ -127,10 +129,11 @@ tcRule (HsRule { rd_ext = ext -- For the LHS constraints we must solve the remaining constraints -- (a) so that we report insoluble ones -- (b) so that we bind any soluble ones - ; let skol_info = RuleSkol name - ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs + ; let all_qtkvs = qtkvs ++ tv_bndrs + skol_info = RuleSkol name + ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs lhs_evs residual_lhs_wanted - ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs + ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs lhs_evs rhs_wanted ; emitImplications (lhs_implic `unionBags` rhs_implic) @@ -138,14 +141,15 @@ tcRule (HsRule { rd_ext = ext , rd_name = rname , rd_act = act , rd_tyvs = ty_bndrs -- preserved for ppr-ing - , rd_tmvs = map (noLoc . RuleBndr noExt . noLoc) (qtkvs ++ tpl_ids) + , rd_tmvs = map (noLoc . RuleBndr noExt . noLoc) (all_qtkvs ++ tpl_ids) , rd_lhs = mkHsDictLet lhs_binds lhs' , rd_rhs = mkHsDictLet rhs_binds rhs' } } tcRule (XRuleDecl _) = panic "tcRule" generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] -> LHsExpr GhcRn -> LHsExpr GhcRn - -> TcM ( [TcId] + -> TcM ( [TyVar] + , [TcId] , LHsExpr GhcTc, WantedConstraints , LHsExpr GhcTc, WantedConstraints , TcType @@ -166,9 +170,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs ; (rhs', rhs_wanted) <- captureConstraints $ tcMonoExpr rhs (mkCheckExpType rule_ty) ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted - ; return (id_bndrs, lhs', all_lhs_wanted - , rhs', rhs_wanted, rule_ty, lvl) } } - -- Slightly curious that tv_bndrs is not returned + ; return (tv_bndrs, id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty, lvl) } } -- See Note [TcLevel in type checking rules] tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 43e8512d82..68a514fbd9 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -105,7 +105,7 @@ module TcSMonad ( zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo, zonkTyCoVarsAndFVList, zonkSimples, zonkWC, - zonkTcTyCoVarBndr, + zonkTyCoVarKind, -- References newTcRef, readTcRef, writeTcRef, updTcRef, @@ -3095,14 +3095,7 @@ pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type) -isFilledMetaTyVar_maybe tv - = case tcTyVarDetails tv of - MetaTv { mtv_ref = ref } - -> do { cts <- readTcRef ref - ; case cts of - Indirect ty -> return (Just ty) - Flexi -> return Nothing } - _ -> return Nothing +isFilledMetaTyVar_maybe tv = wrapTcS (TcM.isFilledMetaTyVar_maybe tv) isFilledMetaTyVar :: TcTyVar -> TcS Bool isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv) @@ -3131,8 +3124,8 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts) zonkWC :: WantedConstraints -> TcS WantedConstraints zonkWC wc = wrapTcS (TcM.zonkWC wc) -zonkTcTyCoVarBndr :: TcTyCoVar -> TcS TcTyCoVar -zonkTcTyCoVarBndr tv = wrapTcS (TcM.zonkTcTyCoVarBndr tv) +zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar +zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv) {- ********************************************************************* * * diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index ada91786c0..f7a41e58bf 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -349,9 +349,9 @@ tcPatSynSig name sig_ty -- These are /signatures/ so we zonk to squeeze out any kind -- unification variables. Do this after kindGeneralize which may -- default kind variables to *. - ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs - ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs - ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs + ; implicit_tvs <- mapM zonkTyCoVarKind implicit_tvs + ; univ_tvs <- mapM zonkTyCoVarKind univ_tvs + ; ex_tvs <- mapM zonkTyCoVarKind ex_tvs ; req <- zonkTcTypes req ; prov <- zonkTcTypes prov ; body_ty <- zonkTcType body_ty diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 562340f0da..6ef62c80a8 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -674,7 +674,7 @@ simplifyInfer :: TcLevel -- Used when generating the constraints simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds | isEmptyWC wanteds = do { gbl_tvs <- tcGetGlobalTyCoVars - ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus) + ; dep_vars <- candidateQTyVarsOfTypes gbl_tvs (map snd name_taus) ; qtkvs <- quantifyTyVars gbl_tvs dep_vars ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs) ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) } @@ -1083,8 +1083,12 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates ; (prom, _) <- promoteTyVarSet mono_tvs -- Default any kind/levity vars - ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} - = candidateQTyVarsOfTypes candidates + ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} + <- candidateQTyVarsOfTypes mono_tvs candidates + -- any covars should already be handled by + -- the logic in decideMonoTyVars, which looks at + -- the constraints generated + ; poly_kinds <- xoptM LangExt.PolyKinds ; default_kvs <- mapM (default_one poly_kinds True) (dVarSetElems cand_kvs) @@ -1150,11 +1154,10 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces -- them in that order, so that the final qtvs quantifies in the same -- order as the partial signatures do (Trac #13524) - ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} - = candidateQTyVarsOfTypes $ - psig_tys ++ candidates ++ tau_tys - pick = (`dVarSetIntersectVarSet` grown_tcvs) - dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } + ; dv@DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes mono_tvs $ + psig_tys ++ candidates ++ tau_tys + ; let pick = (`dVarSetIntersectVarSet` grown_tcvs) + dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } ; traceTc "decideQuantifiedTyVars" (vcat [ text "seed_tys =" <+> ppr seed_tys @@ -1696,7 +1699,7 @@ checkBadTelescope :: Implication -> TcS Bool checkBadTelescope (Implic { ic_telescope = m_telescope , ic_skols = skols }) | isJust m_telescope - = do{ skols <- mapM TcS.zonkTcTyCoVarBndr skols + = do{ skols <- mapM TcS.zonkTyCoVarKind skols ; return (go emptyVarSet (reverse skols))} | otherwise diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index ea1299825f..5725cfd703 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -73,7 +73,6 @@ import BasicTypes import qualified GHC.LanguageExtensions as LangExt import Control.Monad -import Control.Monad.Zip import Data.List import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.Set as Set @@ -346,11 +345,15 @@ TcTyCons are used for two distinct purposes of parameters written to the tycon) to get an initial shape of the tycon's kind. We record that shape in a TcTyCon. + For CUSK tycons, the TcTyCon has the final, generalised kind. + For non-CUSK tycons, the TcTyCon has as its tyConBinders only + the explicit arguments given -- no kind variables, etc. + S2) Then, using these initial kinds, we kind-check the body of the tycon (class methods, data constructors, etc.), filling in the metavariables in the tycon's initial kind. - S3) We then generalize to get the tycon's final, fixed + S3) We then generalize to get the (non-CUSK) tycon's final, fixed kind. Finally, once this has happened for all tycons in a mutually recursive group, we can desugar the lot. @@ -390,35 +393,6 @@ TcTyCons are used for two distinct purposes See also Note [Type checking recursive type and class declarations]. -Note [Check telescope again during generalisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The telescope check before kind generalisation is useful to catch something -like this: - - data T a k = MkT (Proxy (a :: k)) - -Clearly, the k has to come first. Checking for this problem must come before -kind generalisation, as described in Note [Generalisation for type constructors] - -However, we have to check again *after* kind generalisation, to catch something -like this: - - data SameKind :: k -> k -> Type -- to force unification - data S a (b :: a) (d :: SameKind c b) - -Note that c has no explicit binding site. As such, it's quantified by kind -generalisation. (Note that kcHsTyVarBndrs does not return such variables -as binders in its returned TcTyCon.) The user-written part of this telescope -is well-ordered; no earlier variables depend on later ones. However, after -kind generalisation, we put c up front, like so: - - data S {c :: a} a (b :: a) (d :: SameKind c b) - -We now have a problem. We could detect this problem just by looking at the -free vars of the kinds of the generalised variables (the kvs), but we get -such a nice error message out of checkValidTelescope that it seems like the -right thing to do. - Note [Type environment evolution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As we typecheck a group of declarations the type environment evolves. @@ -532,9 +506,17 @@ kcTyClGroup decls tcExtendKindEnvWithTyCons initial_tcs $ mapM_ kcLTyClDecl decls - -- Step 3: generalisation + -- Step 3: skolemisation -- Kind checking done for this group - -- Now we have to kind generalize the flexis + -- Now we have to kind skolemise the flexis + ; candidates <- gather_quant_candidates initial_tcs + ; _ <- quantifyTyVars emptyVarSet candidates + -- We'll get the actual vars to quantify over later. + + -- Step 4: generalisation + -- Finally, go through each tycon and give it its final kind, + -- with all the required, specified, and inferred variables + -- in order. ; poly_tcs <- mapAndReportM generalise initial_tcs ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs) @@ -544,123 +526,219 @@ kcTyClGroup decls ppr_tc_kinds tcs = vcat (map pp_tc tcs) pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc) - generalise :: TcTyCon -> TcM TcTyCon - -- For polymorphic things this is a no-op - generalise tc - = setSrcSpan (getSrcSpan tc) $ - addTyConCtxt tc $ - do { let name = tyConName tc - ; tc_binders <- mapM zonkTcTyVarBinder (tyConBinders tc) - ; tc_res_kind <- zonkTcType (tyConResKind tc) - ; let scoped_tvs = tcTyConScopedTyVars tc - user_tyvars = tcTyConUserTyVars tc - tc_tyvars = binderVars tc_binders - - -- See Note [checkValidDependency] - ; checkValidDependency tc_binders tc_res_kind - - -- See Note [Generalisation for type constructors] - ; let kvs_to_gen = tyCoVarsOfTypesDSet (tc_res_kind : map tyVarKind tc_tyvars) - `delDVarSetList` tc_tyvars - dvs = DV { dv_kvs = kvs_to_gen, dv_tvs = emptyDVarSet } - ; kvs <- quantifyTyVars emptyVarSet dvs - - -- See Note [Work out final tyConBinders] - ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs - ; let (specified_kvs, inferred_kvs) = partition is_specified kvs - user_specified_tkvs = mkVarSet (map snd scoped_tvs') - is_specified kv = kv `elemVarSet` user_specified_tkvs - all_binders = mkNamedTyConBinders Inferred inferred_kvs ++ - mkNamedTyConBinders Specified specified_kvs ++ - tc_binders - - ; (env, all_binders') <- zonkTyVarBinders all_binders - ; tc_res_kind' <- zonkTcTypeToTypeX env tc_res_kind - - -- See Note [Check telescope again during generalisation] - ; checkValidTelescope all_binders user_tyvars - - -- Make sure tc_kind' has the final, zonked kind variables - ; traceTc "Generalise kind" $ - vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind) - , ppr kvs, ppr all_binders, ppr tc_res_kind - , ppr all_binders', ppr tc_res_kind' - , ppr scoped_tvs ] - - ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind' - scoped_tvs' - (tyConFlavour tc)) } + gather_quant_candidates :: [TcTyCon] -> TcM CandidatesQTvs + gather_quant_candidates tcs = mconcat <$> mapM gather1 tcs -{- Note [Generalisation for type constructors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider test T14066g: - data SameKind :: k -> k -> Type - -We find that the Specified variable has kind (c :: a). We always -put Specified variables before Required ones, so we should reject. - - -Now that we can mix type and kind variables, there are an awful lot of -ways to shoot yourself in the foot. Here are some. - -data SameKind :: k -> k -> * -- just to force unification - -1. data T1 a k (b :: k) (x :: SameKind a b) + gather1 :: TcTyCon -> TcM CandidatesQTvs + gather1 tc + | tcTyConIsPoly tc -- these don't need generalisation + = return mempty - The problem here is that we discover that a and b should have the same - kind. But this kind mentions k, which is bound *after* a. - (Testcase: dependent/should_fail/BadTelescope) - -2. data Q a (b :: a) (d :: SameKind c b) - - Note that c is not bound; it is Specified, not Required. Yet its - kind mentions a. Because we have a nice rule that all Specified - variables come before Required ones this is bogus. (We could - probably figure out to put c between a and b. But I think this is - doing users a disservice, in the long run.) (Testcase: - dependent/should_fail/BadTelescope4) - - So, when finding the free vars to generalise, we should look at the - kinds of all Q's binders, plus its result kind, and delete Q's - binders, leaving just {c}. We should NOT try to short-cut by taking - the free vars of the half-baked kind - (forall a. a -> SameKind c b -> *) - because since 'c' is free we also think 'a' (another 'a'!) is - free in that kind. - -To catch these dependency errors, we call checkValidTelescope during -kind-checking datatype declarations. + | otherwise + = do { tc_binders <- zonkTyConBinders (tyConBinders tc) + ; tc_res_kind <- zonkTcType (tyConResKind tc) -See Note [Keeping scoped variables in order: Explicit] for how this -check works for `forall x y z.` written in a type. --} + ; let tvs = mkDVarSet $ map binderVar tc_binders + kvs = tyCoVarsOfTypesDSet (tc_res_kind : map binderType tc_binders) + `minusDVarSet` tvs -{- Note [Work out final tyConBinders] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data T f (a::k1) b = MkT (f a b) (T f a b) + ; return (mempty { dv_kvs = kvs, dv_tvs = tvs }) } -We should get - T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> * + generalise :: TcTyCon -> TcM TcTyCon + generalise tc + | tcTyConIsPoly tc + = return tc -- nothing to do here; we already have the final kind + -- This is just an optimization; generalising is a no-op -Note that: - * k1 is Specified, because it appears in a user-written kind - * k2 is Inferred, because it doesn't appear at all in the - original declaration + | otherwise + -- See Note [Required, Specified, and Inferred for types] + = do { -- Step 0: get the tyvars from the enclosing class (if any) + (all_class_tctvs, class_scoped_tvs) <- get_class_tvs tc + + -- Step 1: gather all the free variables + ; tc_tvs <- mapM zonkTcTyCoVarBndr (map binderVar (tyConBinders tc)) + ; tc_res_kind <- zonkTcType (tyConResKind tc) + ; scoped_tv_pairs <- zonkTyVarTyVarPairs (tcTyConScopedTyVars tc) + + ; let all_fvs = tyCoVarsOfTypesDSet (tc_res_kind : map tyVarKind tc_tvs) + scoped_tvs = map snd scoped_tv_pairs + + ; MASSERT( all ((== Required) . tyConBinderArgFlag) (tyConBinders tc) ) + + -- Step 2: Select out the Required arguments; that is, the tc_binders + ; let no_req_fvs = all_fvs `delDVarSetList` tc_tvs + + -- Step 3: partition remaining variables into class variables and + -- local variables (matters only for associated types) + (class_fvs, local_fvs) + = partitionDVarSet (`elemDVarSet` all_class_tctvs) no_req_fvs + + -- Step 4: For each set so far, use the set to select the scoped_tvs. + -- We take from the scoped_tvs to preserve order. These tvs will become + -- the Specified ones. + class_specified = filter (`elemDVarSet` class_fvs) class_scoped_tvs + local_specified = filter (`elemDVarSet` local_fvs) scoped_tvs + + -- Step 5: Order the specified variables by ScopedSort + -- See Note [ScopedSort] in Type + class_specified_sorted = scopedSort class_specified + local_specified_sorted = scopedSort local_specified + + -- Step 6: Remove the Specified ones from the fv sets. These are the + -- Inferred ones. + class_inferred_set = class_fvs `delDVarSetList` class_specified_sorted + local_inferred_set = local_fvs `delDVarSetList` local_specified_sorted + + class_inferred = dVarSetElemsWellScoped class_inferred_set + local_inferred = dVarSetElemsWellScoped local_inferred_set + + -- Step 7: Make the TyConBinders. + class_inferred_tcbs = mkNamedTyConBinders Inferred class_inferred + class_specified_tcbs = mkNamedTyConBinders Specified class_specified_sorted + local_inferred_tcbs = mkNamedTyConBinders Inferred local_inferred + local_specified_tcbs = mkNamedTyConBinders Specified local_specified_sorted + + mk_req_tcb tv + | tv `elemDVarSet` all_fvs = mkNamedTyConBinder Required tv + | otherwise = mkAnonTyConBinder tv + + required_tcbs = map mk_req_tcb tc_tvs + + -- Step 8: Assemble the final list. + final_tcbs = concat [ class_inferred_tcbs + , class_specified_tcbs + , local_inferred_tcbs + , local_specified_tcbs + , required_tcbs ] + + -- 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. + ; let user_tyvars = tcTyConUserTyVars tc + ; setSrcSpan (getSrcSpan tc) $ + addTyConCtxt tc $ + checkValidTelescope final_tcbs user_tyvars + + -- Step 10: Make the result TcTyCon + ; let name = tyConName tc + ; traceTc "Generalise kind" $ + vcat [ text "name =" <+> ppr name + , text "all_class_tctvs =" <+> ppr all_class_tctvs + , text "class_scoped_tvs =" <+> ppr class_scoped_tvs + , text "tc_tvs =" <+> ppr tc_tvs + , text "tc_res_kind =" <+> ppr tc_res_kind + , text "scoped_tvs =" <+> ppr scoped_tvs + , text "class_inferred_tcbs =" <+> ppr class_inferred_tcbs + , text "class_specified_tcbs =" <+> ppr class_specified_tcbs + , text "local_inferred_tcbs =" <+> ppr local_inferred_tcbs + , text "local_specified_tcbs =" <+> ppr local_specified_tcbs + , text "required_tcbs =" <+> ppr required_tcbs ] + ; return $ mkTcTyCon name user_tyvars final_tcbs tc_res_kind scoped_tv_pairs + True {- it's generalised now -} (tyConFlavour tc) } + + get_class_tvs :: TcTyCon -> TcM (DTyCoVarSet, [TcTyVar]) + -- returns all tyConTyVars of the enclosing class, as well as its + -- scoped type variables. Both are zonked. + get_class_tvs at_tc + | Just class_tc <- tyConAssoc_maybe at_tc + = do { -- We can't just call tyConTyVars, because the enclosing class + -- hasn't been generalised yet + tc_binders <- zonkTyConBinders (tyConBinders class_tc) + ; tc_res_kind <- zonkTcType (tyConResKind class_tc) + ; scoped_tvs <- mapM zonkTcTyVarToTyVar (map snd (tcTyConScopedTyVars class_tc)) + + ; return ( tyCoVarsOfTypesDSet (tc_res_kind : map binderType tc_binders) + `extendDVarSetList` tyConTyVars class_tc + , scoped_tvs ) } -However, at this point in kcTyClGroup, the tc_binders are -simply [f, a, b], the user-written argumennts to the TyCon. -(Why? Because that's what we need for the recursive uses in -T's RHS.) + | otherwise + = return (emptyDVarSet, []) -So kindGeneralize will generalise over /both/ k1 /and/ k2. -Yet we must distinguish them, and we must put the Inferred -ones first. How can we tell the difference? Well, the -Specified variables will be among the tyConScopedTyVars of -the TcTyCon. +{- Note [Required, Specified, and Inferred for types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have some design choices in how we classify the tyvars bound +in a type declaration. (Here, I use "type" to refer to any TyClDecl.) +Much of the debate is memorialized in #15743. This Note documents +the final conclusion. + +First, a reminder: + * a Required argument is one that must be provided at every call site + * a Specified argument is one that can be inferred at call sites, but + may be instantiated with visible type application + * an Inferred argument is one that must be inferred at call sites; it + is unavailable for use with visible type application. + +Why have Inferred at all? Because we just can't make user-facing promises +about the ordering of some variables. These might swizzle around even between +minor released. By forbidding visible type application, we ensure users +aren't caught unawares. See also +Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. + +When inferring the ordering of variables (that is, for those +variables that he user has not specified the order with an explicit `forall`) +we use the following order: + + 1. Inferred variables from an enclosing class (associated types only) + 2. Specified variables from an enclosing class (associated types only) + 3. Inferred variables not from an enclosing class + 4. Specified variables not from an enclosing class + 5. Required variables before a top-level :: + 6. All variables after a top-level :: + +If this ordering does not make a valid telescope, we reject the definition. + +This idea is implemented in the generalise function within kcTyClGroup (for +declarations without CUSKs), and in kcLHsQTyVars (for declarations with +CUSKs). Note that neither definition worries about point (6) above, as this +is nicely handled by not mangling the res_kind. (Mangling res_kinds is done +*after* all this stuff, in tcDataDefn's call to tcDataKindSig.) We can +easily tell Inferred apart from Specified by looking at the scoped tyvars; +Specified are always included there. + +One other small open question here: how to classify variables from an +enclosing class? Here is an example: + + class C (a :: k) where + type F a + +In the kind of F, should k be Inferred or Specified? Currently, we mark +it as Specified, as we can commit to an ordering, based on the ordering +of class variables in the enclosing class declaration. If k were not mentioned +in the class head, then it would be Inferred. The alternative to this +approach is to make the Inferred/Specified distinction locally, by just +looking at the declaration for F. This lowers the availability of type +application, but makes the reasoning more local. However, this alternative +also disagrees with the treatment for methods, where all class variables +are Specified, regardless of whether or not the variable is mentioned in the +method type. + +A few points of motivation for the ordering above: + +* We put the class variables before the local variables in a nod to the + treatment for class methods, where class variables (and the class constraint) + come first. While this is an unforced design decision, it never rejects + more declarations, as class variables can never depend on local variables. + +* We rigidly require the ordering above, even though we could be much more + permissive. Relevant musings are at + https://ghc.haskell.org/trac/ghc/ticket/15743#comment:7 + The bottom line conclusion is that, if the user wants a different ordering, + then can specify it themselves, and it is better to be predictable and dumb + than clever and capricious. + + I (Richard) conjecture we could be fully permissive, allowing all classes + of variables to intermix. We would have to augment ScopedSort to refuse to + reorder Required variables (or check that it wouldn't have). But this would + allow more programs. See #15743 for examples. Interestingly, Idris seems + to allow this intermixing. The intermixing would be fully specified, in that + we can be sure that inference wouldn't change between versions. However, + would users be able to predict it? That I cannot answer. + +Test cases (and tickets) relevant to these design decisions: + T15591* + T15592* + T15743* -Hence partitioning by is_specified. See Trac #15592 for -some discussion. -} -------------- @@ -721,12 +799,12 @@ getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon] getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) = do { let cusk = hsDeclHasCusk decl - ; tycon <- kcLHsQTyVars name ClassFlavour cusk [] ktvs $ + ; tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $ return constraintKind ; let parent_tv_prs = tcTyConScopedTyVars tycon -- See Note [Don't process associated types in kcLHsQTyVars] ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $ - getFamDeclInitialKinds (Just (cusk, parent_tv_prs)) ats + getFamDeclInitialKinds (Just tycon) ats ; return (tycon : inner_tcs) } getInitialKind decl@(DataDecl { tcdLName = L _ name @@ -735,7 +813,7 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name , dd_ND = new_or_data } }) = do { tycon <- kcLHsQTyVars name (newOrDataToFlavour new_or_data) - (hsDeclHasCusk decl) [] ktvs $ + (hsDeclHasCusk decl) ktvs $ case m_sig of Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig Nothing -> return liftedTypeKind @@ -749,7 +827,7 @@ getInitialKind decl@(SynDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdRhs = rhs }) = do { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) - [] ktvs $ + ktvs $ case kind_annotation rhs of Nothing -> newMetaKindVar Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig @@ -766,47 +844,38 @@ getInitialKind (XTyClDecl _) = panic "getInitialKind" --------------------------------- getFamDeclInitialKinds - :: Maybe (Bool, [(Name, TyVar)]) - -- ^ If this family declaration is associated with a class, this is - -- @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of - -- the associated class and @cls_tv_prs@ contains the class's scoped - -- type variables. + :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any -> [LFamilyDecl GhcRn] -> TcM [TcTyCon] -getFamDeclInitialKinds mb_parent_info decls - = mapM (addLocM (getFamDeclInitialKind mb_parent_info)) decls +getFamDeclInitialKinds mb_parent_tycon decls + = mapM (addLocM (getFamDeclInitialKind mb_parent_tycon)) decls getFamDeclInitialKind - :: Maybe (Bool, [(Name, TyVar)]) - -- ^ If this family declaration is associated with a class, this is - -- @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of - -- the associated class and @cls_tv_prs@ contains the class's scoped - -- type variables. + :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any -> FamilyDecl GhcRn -> TcM TcTyCon -getFamDeclInitialKind mb_parent_info +getFamDeclInitialKind mb_parent_tycon decl@(FamilyDecl { fdLName = L _ name , fdTyVars = ktvs , fdResultSig = L _ resultSig , fdInfo = info }) - = do { tycon <- kcLHsQTyVars name flav cusk parent_tv_prs ktvs $ - case resultSig of - KindSig _ ki -> tcLHsKindSig ctxt ki - TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki - _ -- open type families have * return kind by default - | tcFlavourIsOpen flav -> return liftedTypeKind + = kcLHsQTyVars name flav cusk ktvs $ + case resultSig of + KindSig _ ki -> tcLHsKindSig ctxt ki + TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki + _ -- open type families have * return kind by default + | tcFlavourIsOpen flav -> return liftedTypeKind -- closed type families have their return kind inferred -- by default - | otherwise -> newMetaKindVar - ; return tycon } + | otherwise -> newMetaKindVar where - (mb_cusk, mb_parent_tv_prs) = munzip mb_parent_info - cusk = famDeclHasCusk mb_cusk decl - parent_tv_prs = mb_parent_tv_prs `orElse` [] + mb_cusk = tcTyConIsPoly <$> mb_parent_tycon + cusk = famDeclHasCusk mb_cusk decl flav = case info of - DataFamily -> DataFamilyFlavour (isJust mb_cusk) - OpenTypeFamily -> OpenTypeFamilyFlavour (isJust mb_cusk) - ClosedTypeFamily _ -> ClosedTypeFamilyFlavour + DataFamily -> DataFamilyFlavour mb_parent_tycon + OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon + ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) + ClosedTypeFamilyFlavour ctxt = TyFamResKindCtxt name getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind" @@ -815,7 +884,7 @@ kcLTyClDecl :: LTyClDecl GhcRn -> TcM () -- See Note [Kind checking for type and class decls] kcLTyClDecl (L loc decl) | hsDeclHasCusk decl -- See Note [Skip decls with CUSKs in kcLTyClDecl] - = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name) + = traceTc "kcTyClDecl skipped due to cusk:" (ppr tc_name) | otherwise = setSrcSpan loc $ @@ -1373,7 +1442,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na -- Process the equations, creating CoAxBranches ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind - [] ClosedTypeFamilyFlavour + [] False {- this doesn't matter here -} + ClosedTypeFamilyFlavour ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns -- Do not attempt to drop equations dominated by earlier @@ -1488,7 +1558,7 @@ tcDataDefn roles_info ; tycon <- fixM $ \ tycon -> do { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs)) - ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons + ; data_cons <- tcConDecls tycon final_bndrs res_ty cons ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons ; tc_rep_nm <- newTyConRepName tc_name ; return (mkAlgTyCon tc_name @@ -1558,7 +1628,8 @@ kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn" kcTyFamEqnRhs :: Maybe ClsInstInfo -> LHsType GhcRn -- ^ Eqn RHS -> TcKind -- ^ Inferred kind of left-hand side - -> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side + -> TcM ([TcTyVar], [TcType], TcKind) + -- ^ New pattern skolems, New pats, inst'ed kind of left-hand side kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away. (new_pats, insted_lhs_ki) @@ -1573,7 +1644,8 @@ kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki - ; return (new_pats, insted_lhs_ki) } + ; return ([], new_pats, insted_lhs_ki) } + -- we never introduce new skolems here where mb_kind_env = thdOf3 <$> mb_clsinfo @@ -1600,7 +1672,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo ; pats' <- zonkTcTypesToTypesX ze pats ; traceTc "tcTyFamInstEqn 3" (ppr eqn_tc_name <+> ppr pats $$ ppr rhs_ty) ; rhs_ty' <- zonkTcTypeToTypeX ze rhs_ty - ; traceTc "tcTyFamInstEqn 4" (ppr fam_tc <+> pprTyVars tvs') + ; traceTc "tcTyFamInstEqn 4 }" (ppr fam_tc <+> pprTyVars tvs') ; return (mkCoAxBranch tvs' [] pats' rhs_ty' (map (const Nominal) tvs') loc) } @@ -1611,12 +1683,12 @@ kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars -- (associated types only) -> DataFamInstDecl GhcRn -> TcKind -- ^ the kind of the tycon applied to pats - -> TcM ([TcType], TcKind) + -> TcM ([TcTyVar], [TcType], TcKind) -- ^ the kind signature might force instantiation - -- of the tycon; this returns any extra args and the inst'ed kind + -- of the tycon; this returns any extra skolems, args and the inst'ed kind -- See Note [Instantiating a family tycon] -- Used for 'data instance' only --- Ordinary 'data' is handled by kcTyClDec +-- Ordinary 'data' is handled by kcTyClDecl kcDataDefn mb_kind_env (DataFamInstDecl { dfid_eqn = HsIB { hsib_body = FamEqn { feqn_tycon = fam_name @@ -1643,8 +1715,6 @@ kcDataDefn mb_kind_env ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise - -- we don't need to do anything substantive with the tvs' because the - -- quantifyTyVars in tcFamTyPats will catch them. ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind tv_prs = zip (map tyVarName tvs_to_skolemise) tvs' @@ -1665,7 +1735,7 @@ kcDataDefn mb_kind_env ; rhs_ki <- zonkTcType rhs_ki ; MASSERT( lhs_ki `tcEqType` rhs_ki ) } - ; return (new_args, lhs_ki) } + ; return (tvs', new_args, lhs_ki) } where bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats) pp_fam_app = pprFamInstLHS fam_name mb_bndrs pats fixity (unLoc ctxt) mb_kind @@ -1699,12 +1769,8 @@ to instantiate the k. With data family instances, this problem can be even more intricate, due to Note [Arity of data families] in FamInstEnv. See indexed-types/should_compile/T12369 for an example. -So, the kind-checker must return both the new args (that is, Type -(Type -> Type) for the equations above) and the instantiated kind. - -Because we don't need this information in the kind-checking phase of -checking closed type families, we don't require these extra pieces of -information in tc_fam_ty_pats. +So, the kind-checker must return the new skolems and args (that is, Type +or (Type -> Type) for the equations above) and the instantiated kind. Note [Failing early in kcDataDefn] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1747,7 +1813,7 @@ tcFamTyPats :: TyCon -> [Name] -- Implicitly bound kind/type variable names -> Maybe [LHsTyVarBndr GhcRn] -> HsTyPats GhcRn -- Type patterns - -> (TcKind -> TcM ([TcType], TcKind)) + -> (TcKind -> TcM ([TcTyVar], [TcType], TcKind)) -- kind-checker for RHS -- See Note [Instantiating a family tycon] -> ( [TcTyVar] -- Kind and type variables @@ -1781,7 +1847,7 @@ tcFamTyPats fam_tc mb_clsinfo wrongNumberOfParmsErr vis_arity -- report only explicit arguments - ; (imp_tvs, (exp_tvs, (typats, (more_typats, res_kind)))) + ; (imp_tvs, (exp_tvs, (typats, (more_tyvars, more_typats, res_kind)))) <- solveEqualities $ -- See Note [Constraints in patterns] tcImplicitQTKBndrs FamInstSkol imp_vars $ tcExplicitTKBndrs FamInstSkol (fromMaybe [] mb_expl_bndrs) $ @@ -1822,9 +1888,26 @@ tcFamTyPats fam_tc mb_clsinfo -- them into skolems, so that we don't subsequently -- replace a meta kind var with (Any *) -- Very like kindGeneralize - ; let all_pats = typats `chkAppend` more_typats - ; vars <- zonkTcTypesAndSplitDepVars all_pats + ; let all_pats = typats `chkAppend` more_typats + fam_app = mkTyConApp fam_tc all_pats + + user_tvs = exp_tvs ++ imp_tvs `chkAppend` more_tyvars + + -- the user_tvs might have quantified kind variables from + -- an enclosing class/instance; make sure to bring these into scope + extra_tvs = case mb_clsinfo of + Nothing -> [] + Just (_, inst_tvs, _) -> + filter (`elemVarSet` tyCoVarsOfType (mkSpecForAllTys user_tvs fam_app)) + inst_tvs + + all_tvs = extra_tvs ++ user_tvs + + -- the user_tvs are already bound in the pats; don't quantify over these again. + ; vars <- candidateQTyVarsOfType emptyVarSet $ + mkSpecForAllTys all_tvs fam_app ; qtkvs <- quantifyTyVars emptyVarSet vars + ; let all_qtkvs = qtkvs ++ all_tvs ; when debugIsOn $ do { all_pats <- mapM zonkTcType all_pats @@ -1838,26 +1921,27 @@ tcFamTyPats fam_tc mb_clsinfo $$ ppr all_pats $$ ppr qtkvs) -- See Note [Free-floating kind vars] in TcHsType - ; let all_mentioned_tvs = mkVarSet qtkvs - -- qtkvs has all the tyvars bound by LHS - -- type patterns - unmentioned_imp_tvs = filterOut (`elemVarSet` all_mentioned_tvs) imp_tvs + ; lhs_tvs <- zonkTcTypeAndFV fam_app + ; let unmentioned_tvs = filterOut (`elemDVarSet` lhs_tvs) imp_tvs -- If there are tyvars left over, we can -- assume they're free-floating, since they -- aren't bound by a type pattern + -- Recall that user are those lexically + -- used in the equation. As skolems, they + -- don't need zonking. ; checkNoErrs $ reportFloatingKvs fam_name flav - qtkvs unmentioned_imp_tvs + (dVarSetElemsWellScoped lhs_tvs) unmentioned_tvs -- Error if exp_tvs contains anything that is still unused. -- See Note [Unused explicitly bound variables in a family pattern] - ; let unmentioned_exp_tvs = filterOut (`elemVarSet` all_mentioned_tvs) exp_tvs + ; let unmentioned_exp_tvs = filterOut (`elemDVarSet` lhs_tvs) exp_tvs ; checkNoErrs $ mapM_ (unusedExplicitForAllErr . Var.varName) unmentioned_exp_tvs - ; scopeTyVars FamInstSkol qtkvs $ + ; scopeTyVars FamInstSkol all_qtkvs $ -- Extend envt with TcTyVars not TyVars, because the -- kind checking etc done by thing_inside does not expect -- to encounter TyVars; it expects TcTyVars - thing_inside qtkvs all_pats res_kind } + thing_inside all_qtkvs all_pats res_kind } where fam_name = tyConName fam_tc flav = tyConFlavour fam_tc @@ -2019,11 +2103,11 @@ consUseGadtSyntax _ = False -- All constructors have same shape ----------------------------------- -tcConDecls :: KnotTied TyCon -> ([KnotTied TyConBinder], KnotTied Type) +tcConDecls :: KnotTied TyCon -> [KnotTied TyConBinder] -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon] -- Why both the tycon tyvars and binders? Because the tyvars -- have all the names and the binders have the visibilities. -tcConDecls rep_tycon (tmpl_bndrs, res_tmpl) +tcConDecls rep_tycon tmpl_bndrs res_tmpl = concatMapM $ addLocM $ tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl -- It's important that we pay for tag allocation here, once per TyCon, @@ -2203,7 +2287,7 @@ quantifyConDecl :: TcTyCoVarSet -- outer tvs, not to be quantified over; zonked -> TcType -> TcM [TcTyVar] quantifyConDecl gbl_tvs ty = do { ty <- zonkTcType ty - ; let fvs = candidateQTyVarsOfType ty + ; fvs <- candidateQTyVarsOfType gbl_tvs ty ; quantifyTyVars gbl_tvs fvs } tcConIsInfixH98 :: Name @@ -2311,8 +2395,7 @@ rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result -- data instance T [a] b c ... -- gives template ([a,b,c], T [a] b c) -- Type must be of kind *! - -> [TyVar] -- The constructor's user-written, inferred - -- type variables + -> [TyVar] -- The constructor's inferred type variables -> [TyVar] -- The constructor's user-written, specified -- type variables -> KnotTied Type -- res_ty type must be of kind * @@ -3363,75 +3446,6 @@ For example: data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a } -Note [checkValidDependency] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - - data Proxy k (a :: k) - data Proxy2 k a = P (Proxy k a) - -(This is test dependent/should_fail/InferDependency.) While it seems GHC can -figure out the dependency between the arguments to Proxy2, this case errors. -The problem is that when we build the initial kind (getInitialKind) for -a tycon, we need to decide whether an argument is dependent or not. At first, -I thought we could just assume that *all* arguments are dependent, and then -patch it up later. However, this causes problems in error messages (where -tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification -(where we try to unify kappa ~ forall (a :: k) -> blah, failing because the -RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out -(say, by storing the dependency flag in a mutable cell and by avoiding -these fancy kinds in error messages depending on the extension in effect) -but it doesn't seem worth it. - -So: we choose the dependency for each argument variable once and for all -in getInitialKind. This means that any dependency must be lexically manifest. - -checkValidDependency checks to make sure that no lexically non-dependent -argument actually appears in a kind. Note the example above, where the k -in Proxy2 is a dependent argument, but this fact is not lexically -manifest. checkValidDependency will reject. This function must be called -*before* kind generalization, because kind generalization works with -the result of mkTyConKind, which will think that Proxy2's kind is -Type -> k -> Type, where k is unbound. (It won't use a forall for a -"non-dependent" argument k.) --} - --- | See Note [checkValidDependency] -checkValidDependency :: [TyConBinder] -- zonked - -> TcKind -- zonked (result kind) - -> TcM () -checkValidDependency binders res_kind - = go (tyCoVarsOfType res_kind) (reverse binders) - where - go :: TyCoVarSet -- fvs from scope - -> [TyConBinder] -- binders, in reverse order - -> TcM () - go _ [] = return () -- all set - go fvs (tcb : tcbs) - | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs - = do { setSrcSpan (getSrcSpan tcb_var) $ - addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+> - text "is used dependently." - , text "Any dependent arguments must be obviously so, not inferred" - , text "by the type-checker." - , hang (text "Inferred argument kinds:") - 2 (vcat (map pp_binder binders)) - , text "Suggestion: use" <+> quotes (ppr tcb_var) <+> - text "in a kind to make the dependency clearer." ]) - ; go new_fvs tcbs } - - | otherwise - = go new_fvs tcbs - where - new_fvs = fvs `delVarSet` tcb_var - `unionVarSet` tyCoVarsOfType tcb_kind - - tcb_var = binderVar tcb - tcb_kind = tyVarKind tcb_var - - pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderType binder) - -{- ************************************************************************ * * Checking role validity @@ -3813,13 +3827,10 @@ incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+> (text "Use IncoherentInstances to allow this; bad role found") addTyConCtxt :: TyCon -> TcM a -> TcM a -addTyConCtxt tc - = addErrCtxt ctxt +addTyConCtxt tc = addTyConFlavCtxt name flav where name = getName tc - flav = ppr (tyConFlavour tc) - ctxt = hsep [ text "In the", flav - , text "declaration for", quotes (ppr name) ] + flav = tyConFlavour tc addRoleAnnotCtxt :: Name -> TcM a -> TcM a addRoleAnnotCtxt name diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 8fcdde1dad..2ddb4c4604 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -104,7 +104,6 @@ module TcType ( -- * Finding "exact" (non-dead) type variables exactTyCoVarsOfType, exactTyCoVarsOfTypes, - candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..), anyRewritableTyVar, --------------------------------- @@ -181,7 +180,7 @@ module TcType ( pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred, pprTCvBndr, pprTCvBndrs, - TypeSize, sizeType, sizeTypes, toposortTyVars, + TypeSize, sizeType, sizeTypes, scopedSort, --------------------------------- -- argument visibility @@ -225,11 +224,10 @@ import FastString import ErrUtils( Validity(..), MsgDoc, isValid ) import qualified GHC.LanguageExtensions as LangExt -import Data.List ( mapAccumL ) +import Data.List ( mapAccumL, foldl' ) import Data.Functor.Identity( Identity(..) ) import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) -import qualified Data.Semigroup as Semi {- ************************************************************************ @@ -1007,149 +1005,6 @@ would re-occur and we end up with an infinite loop in which each kicks out the other (Trac #14363). -} -{- ********************************************************************* -* * - Type and kind variables in a type -* * -********************************************************************* -} - -data CandidatesQTvs -- See Note [Dependent type variables] - -- See Note [CandidatesQTvs determinism and order] - = DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent) - , dv_tvs :: DTyVarSet -- "type" variables (non-dependent) - -- A variable may appear in both sets - -- E.g. T k (x::k) The first occurrence of k makes it - -- show up in dv_tvs, the second in dv_kvs - -- See Note [Dependent type variables] - } - -instance Semi.Semigroup CandidatesQTvs where - (DV { dv_kvs = kv1, dv_tvs = tv1 }) <> (DV { dv_kvs = kv2, dv_tvs = tv2 }) - = DV { dv_kvs = kv1 `unionDVarSet` kv2 - , dv_tvs = tv1 `unionDVarSet` tv2} - -instance Monoid CandidatesQTvs where - mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet } - mappend = (Semi.<>) - -instance Outputable CandidatesQTvs where - ppr (DV {dv_kvs = kvs, dv_tvs = tvs }) - = text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs - , text "dv_tvs =" <+> ppr tvs ]) - -{- Note [Dependent type variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In Haskell type inference we quantify over type variables; but we only -quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds -we default the kind variables to *. - -So, to support this defaulting, and only for that reason, when -collecting the free vars of a type, prior to quantifying, we must keep -the type and kind variables separate. - -But what does that mean in a system where kind variables /are/ type -variables? It's a fairly arbitrary distinction based on how the -variables appear: - - - "Kind variables" appear in the kind of some other free variable - PLUS any free coercion variables - - These are the ones we default to * if -XPolyKinds is off - - - "Type variables" are all free vars that are not kind variables - -E.g. In the type T k (a::k) - 'k' is a kind variable, because it occurs in the kind of 'a', - even though it also appears at "top level" of the type - 'a' is a type variable, because it doesn't - -We gather these variables using a CandidatesQTvs record: - DV { dv_kvs: Variables free in the kind of a free type variable - or of a forall-bound type variable - , dv_tvs: Variables sytactically free in the type } - -So: dv_kvs are the kind variables of the type - (dv_tvs - dv_kvs) are the type variable of the type - -Note that - -* A variable can occur in both. - T k (x::k) The first occurrence of k makes it - show up in dv_tvs, the second in dv_kvs - -* We include any coercion variables in the "dependent", - "kind-variable" set because we never quantify over them. - -* Both sets are un-ordered, of course. - -* The "kind variables" might depend on each other; e.g - (k1 :: k2), (k2 :: *) - The "type variables" do not depend on each other; if - one did, it'd be classified as a kind variable! - -Note [CandidatesQTvs determinism and order] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* Determinism: when we quantify over type variables we decide the - order in which they appear in the final type. Because the order of - type variables in the type can end up in the interface file and - affects some optimizations like worker-wrapper, we want this order to - be deterministic. - - To achieve that we use deterministic sets of variables that can be - converted to lists in a deterministic order. For more information - about deterministic sets see Note [Deterministic UniqFM] in UniqDFM. - -* Order: as well as being deterministic, we use an - accumulating-parameter style for candidateQTyVarsOfType so that we - add variables one at a time, left to right. That means we tend to - produce the variables in left-to-right order. This is just to make - it bit more predicatable for the programmer. --} - --- | Worker for 'splitDepVarsOfType'. This might output the same var --- in both sets, if it's used in both a type and a kind. --- See Note [CandidatesQTvs determinism and order] --- See Note [Dependent type variables] -candidateQTyVarsOfType :: Type -> CandidatesQTvs -candidateQTyVarsOfType = split_dvs emptyVarSet mempty - -split_dvs :: VarSet -> CandidatesQTvs -> Type -> CandidatesQTvs -split_dvs bound dvs ty - = go dvs ty - where - go dv (AppTy t1 t2) = go (go dv t1) t2 - go dv (TyConApp _ tys) = foldl' go dv tys - go dv (FunTy arg res) = go (go dv arg) res - go dv (LitTy {}) = dv - go dv (CastTy ty co) = go dv ty `mappend` go_co co - go dv (CoercionTy co) = dv `mappend` go_co co - - go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv) - | tv `elemVarSet` bound - = dv - | otherwise - = DV { dv_kvs = kvs `unionDVarSet` - kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv)) - , dv_tvs = tvs `extendDVarSet` tv } - - go dv (ForAllTy (Bndr tv _) ty) - = DV { dv_kvs = kvs `unionDVarSet` - kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv)) - , dv_tvs = tvs } - where - DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty - - go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co) - , dv_tvs = emptyDVarSet } - - kill_bound free - | isEmptyVarSet bound = free - | otherwise = free `dVarSetMinusVarSet` bound - --- | Like 'splitDepVarsOfType', but over a list of types -candidateQTyVarsOfTypes :: [Type] -> CandidatesQTvs -candidateQTyVarsOfTypes = foldl' (split_dvs emptyVarSet) mempty - {- ************************************************************************ * * diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 936eed842f..f9aad513b7 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1779,7 +1779,8 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat = do { -- Check that the associated type indeed comes from this class -- See [Mismatched class methods and associated type families] -- in TcInstDecls. - checkTc (Just clas == tyConAssoc_maybe fam_tc) + + checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc) (badATErr (className clas) (tyConName fam_tc)) -- Check type args first (more comprehensible) @@ -1789,9 +1790,9 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat ; checkTcM (all check_arg kind_shapes) (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds) - ; traceTc "cfi" (vcat [ ppr inst_tvs - , ppr arg_shapes - , ppr mini_env ]) } + ; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs + , ppr arg_shapes + , ppr mini_env ]) } where arg_shapes :: [AssocInstArgShape] arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty) @@ -2062,6 +2063,33 @@ famPatErr fam_tc tvs pats Telescope checking * * ************************************************************************ + +Note [Bad telescopes] +~~~~~~~~~~~~~~~~~~~~~ +Now that we can mix type and kind variables, there are an awful lot of +ways to shoot yourself in the foot. Here are some. + + data SameKind :: k -> k -> * -- just to force unification + +1. data T1 a k (b :: k) (x :: SameKind a b) + +The problem here is that we discover that a and b should have the same +kind. But this kind mentions k, which is bound *after* a. +(Testcase: dependent/should_fail/BadTelescope) + +2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) + +Note that b is not bound. Yet its kind mentions a. Because we have +a nice rule that all implicitly bound variables come before others, +this is bogus. + +To catch these errors, we call checkValidTelescope during kind-checking +datatype declarations. See also +Note [Required, Specified, and Inferred for types] in TcTyClsDecls. + +Note [Keeping scoped variables in order: Explicit] discusses how this +check works for `forall x y z.` written in a type. + -} -- | Check a list of binders to see if they make a valid telescope. @@ -2089,7 +2117,7 @@ checkValidTelescope tvbs user_tyvars , extra ] where tvs = binderVars tvbs - (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (toposortTyVars tvs) + (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (scopedSort tvs) (_, bad_tvbs) = foldl add_one (mkVarSet tvs, []) tvbs @@ -2106,11 +2134,11 @@ checkValidTelescope tvbs user_tyvars fkvs = tyCoVarsOfType (tyVarKind tv) bad' = bad_bndrs `delVarSet` tv - extra | all (isVisibleArgFlag . tyConBinderArgFlag) bad_tvbs - = empty - | otherwise - = text "NB: Implicitly declared variables come before others." - + extra + | any isInvisibleTyConBinder tvbs + = text "NB: Implicitly declared variables come before others." + | otherwise + = empty {- ************************************************************************ diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index ef894d8d57..1c0d5f9dd2 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -79,7 +79,6 @@ module TyCoRep ( tyCoVarsOfType, tyCoVarsOfTypeDSet, tyCoVarsOfTypes, tyCoVarsOfTypesDSet, tyCoFVsBndr, tyCoFVsOfType, tyCoVarsOfTypeList, tyCoFVsOfTypes, tyCoVarsOfTypesList, - closeOverKindsDSet, closeOverKindsFV, closeOverKindsList, closeOverKinds, coVarsOfType, coVarsOfTypes, coVarsOfCo, coVarsOfCos, tyCoVarsOfCo, tyCoVarsOfCos, @@ -156,7 +155,7 @@ import {-# SOURCE #-} DataCon( dataConFullSig import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy, mkCastTy , tyCoVarsOfTypeWellScoped , tyCoVarsOfTypesWellScoped - , toposortTyVars + , scopedSort , coreView ) -- Transitively pulls in a LOT of stuff, better to break the loop @@ -564,7 +563,7 @@ Pi-types: * A dependent compile-time-only polytype, written with forall, e.g. forall (a:*). ty - represented as ForAllTy (TvBndr a v) ty + represented as ForAllTy (Bndr a v) ty Both Pi-types classify terms/types that take an argument. In other words, if `x` is either a function or a polytype, `x arg` makes sense @@ -684,6 +683,8 @@ Here Foo's TyConBinders are and its kind prints as Foo :: forall a -> forall b. (a -> b -> Type) -> Type +See also Note [Required, Specified, and Inferred for types] in TcTyClsDecls + ---- Printing ----- We print forall types with enough syntax to tell you their visibility @@ -2052,32 +2053,6 @@ almost_devoid_co_var_of_types (ty:tys) cv = almost_devoid_co_var_of_type ty cv && almost_devoid_co_var_of_types tys cv -------------- Closing over kinds ----------------- - --- | Add the kind variables free in the kinds of the tyvars in the given set. --- Returns a non-deterministic set. -closeOverKinds :: TyVarSet -> TyVarSet -closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet - -- It's OK to use nonDetEltsUniqSet here because we immediately forget - -- about the ordering by returning a set. - --- | Given a list of tyvars returns a deterministic FV computation that --- returns the given tyvars with the kind variables free in the kinds of the --- given tyvars. -closeOverKindsFV :: [TyVar] -> FV -closeOverKindsFV tvs = - mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs - --- | Add the kind variables free in the kinds of the tyvars in the given set. --- Returns a deterministically ordered list. -closeOverKindsList :: [TyVar] -> [TyVar] -closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs - --- | Add the kind variables free in the kinds of the tyvars in the given set. --- Returns a deterministic set. -closeOverKindsDSet :: DTyVarSet -> DTyVarSet -closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems - ------------- Injective free vars ----------------- -- | Returns the free variables of a 'TyConBinder' that are in injective @@ -3196,7 +3171,7 @@ tidyToIfaceCo :: Coercion -> IfaceCoercion tidyToIfaceCo co = toIfaceCoercionX (mkVarSet free_tcvs) (tidyCo env co) where env = tidyFreeTyCoVars emptyTidyEnv free_tcvs - free_tcvs = toposortTyVars $ tyCoVarsOfCoList co + free_tcvs = scopedSort $ tyCoVarsOfCoList co ------------ pprClassPred :: Class -> [Type] -> SDoc diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 6f53bc3c98..c96cb6beb8 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -19,6 +19,7 @@ module TyCon( -- * TyConBinder TyConBinder, TyConBndrVis(..), TyConTyCoBinder, mkNamedTyConBinder, mkNamedTyConBinders, + mkRequiredTyConBinder, mkAnonTyConBinder, mkAnonTyConBinders, tyConBinderArgFlag, tyConBndrVisArgFlag, isNamedTyConBinder, isVisibleTyConBinder, isInvisibleTyConBinder, @@ -65,7 +66,7 @@ module TyCon( isBuiltInSynFamTyCon_maybe, isUnliftedTyCon, isGadtSyntaxTyCon, isInjectiveTyCon, isGenerativeTyCon, isGenInjAlgRhs, - isTyConAssoc, tyConAssoc_maybe, + isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe, isImplicitTyCon, isTyConWithSrcDataCons, isTcTyCon, isTcLevPoly, @@ -97,7 +98,7 @@ module TyCon( algTcFields, tyConRuntimeRepInfo, tyConBinders, tyConResKind, tyConTyVarBinders, - tcTyConScopedTyVars, tcTyConUserTyVars, + tcTyConScopedTyVars, tcTyConUserTyVars, tcTyConIsPoly, mkTyConTagMap, -- ** Manipulating TyCons @@ -140,6 +141,7 @@ import {-# SOURCE #-} DataCon ( DataCon, dataConExTyCoVars, dataConFieldLabel import Binary import Var +import VarSet import Class import BasicTypes import DynFlags @@ -308,7 +310,7 @@ See also Note [Wrappers for data instance tycons] in MkId.hs Note [Associated families and their parent class] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ *Associated* families are just like *non-associated* families, except -that they have a famTcParent field of (Just cls), which identifies the +that they have a famTcParent field of (Just cls_tc), which identifies the parent class. However there is an important sharing relationship between @@ -422,6 +424,15 @@ mkNamedTyConBinders :: ArgFlag -> [TyVar] -> [TyConBinder] -- The odd argument order supports currying mkNamedTyConBinders vis tvs = map (mkNamedTyConBinder vis) tvs +-- | Make a Required TyConBinder. It chooses between NamedTCB and +-- AnonTCB based on whether the tv is mentioned in the dependent set +mkRequiredTyConBinder :: TyCoVarSet -- these are used dependently + -> TyVar + -> TyConBinder +mkRequiredTyConBinder dep_set tv + | tv `elemVarSet` dep_set = mkNamedTyConBinder Required tv + | otherwise = mkAnonTyConBinder tv + tyConBinderArgFlag :: TyConBinder -> ArgFlag tyConBinderArgFlag (Bndr _ vis) = tyConBndrVisArgFlag vis @@ -768,8 +779,8 @@ data TyCon -- abstract, built-in. See comments for -- FamTyConFlav - famTcParent :: Maybe Class, -- ^ For *associated* type/data families - -- The class in whose declaration the family is declared + famTcParent :: Maybe TyCon, -- ^ For *associated* type/data families + -- The class tycon in which the family is declared -- See Note [Associated families and their parent class] famTcInj :: Injectivity -- ^ is this a type family injective in @@ -839,8 +850,13 @@ data TyCon tcTyConScopedTyVars :: [(Name,TyVar)], -- ^ Scoped tyvars over the tycon's body -- See Note [How TcTyCons work] in TcTyClsDecls - -- Order does *not* matter. + -- Order *does* matter: for TcTyCons with a CUSK, + -- it's the correct dependency order. For TcTyCons + -- without a CUSK, it's the original left-to-right + -- that the user wrote. Nec'y for getting Specified + -- variables in the right order. tcTyConUserTyVars :: SDoc, -- ^ Original, user-written tycon tyvars + tcTyConIsPoly :: Bool, -- ^ Is this TcTyCon already generalized? tcTyConFlavour :: TyConFlavour -- ^ What sort of 'TyCon' this represents. @@ -1558,9 +1574,10 @@ mkTcTyCon :: Name -> Kind -- ^ /result/ kind only -> [(Name,TcTyVar)] -- ^ Scoped type variables; -- see Note [How TcTyCons work] in TcTyClsDecls + -> Bool -- ^ Is this TcTyCon generalised already? -> TyConFlavour -- ^ What sort of 'TyCon' this represents -> TyCon -mkTcTyCon name tyvars binders res_kind scoped_tvs flav +mkTcTyCon name tyvars binders res_kind scoped_tvs poly flav = TcTyCon { tyConUnique = getUnique name , tyConName = name , tyConTyVars = binderVars binders @@ -1569,6 +1586,7 @@ mkTcTyCon name tyvars binders res_kind scoped_tvs flav , tyConKind = mkTyConKind binders res_kind , tyConArity = length binders , tcTyConScopedTyVars = scoped_tvs + , tcTyConIsPoly = poly , tcTyConFlavour = flav , tcTyConUserTyVars = tyvars } @@ -1648,7 +1666,7 @@ mkFamilyTyCon name binders res_kind resVar flav parent inj , tyConTyVars = binderVars binders , famTcResVar = resVar , famTcFlav = flav - , famTcParent = parent + , famTcParent = classTyCon <$> parent , famTcInj = inj } @@ -1690,6 +1708,7 @@ makeRecoveryTyCon tc = mkTcTyCon (tyConName tc) empty (tyConBinders tc) (tyConResKind tc) [{- no scoped vars -}] + True (tyConFlavour tc) -- | Does this 'TyCon' represent something that cannot be defined in Haskell? @@ -1975,14 +1994,19 @@ isDataFamFlav :: FamTyConFlav -> Bool isDataFamFlav (DataFamilyTyCon {}) = True -- Data family isDataFamFlav _ = False -- Type synonym family --- | Are we able to extract information 'TyVar' to class argument list --- mapping from a given 'TyCon'? +-- | Is this TyCon for an associated type? isTyConAssoc :: TyCon -> Bool -isTyConAssoc tc = isJust (tyConAssoc_maybe tc) +isTyConAssoc = isJust . tyConAssoc_maybe + +-- | Get the enclosing class TyCon (if there is one) for the given TyCon. +tyConAssoc_maybe :: TyCon -> Maybe TyCon +tyConAssoc_maybe = tyConFlavourAssoc_maybe . tyConFlavour -tyConAssoc_maybe :: TyCon -> Maybe Class -tyConAssoc_maybe (FamilyTyCon { famTcParent = mb_cls }) = mb_cls -tyConAssoc_maybe _ = Nothing +-- | Get the enclosing class TyCon (if there is one) for the given TyConFlavour +tyConFlavourAssoc_maybe :: TyConFlavour -> Maybe TyCon +tyConFlavourAssoc_maybe (DataFamilyFlavour mb_parent) = mb_parent +tyConFlavourAssoc_maybe (OpenTypeFamilyFlavour mb_parent) = mb_parent +tyConFlavourAssoc_maybe _ = Nothing -- The unit tycon didn't used to be classed as a tuple tycon -- but I thought that was silly so I've undone it @@ -2416,8 +2440,8 @@ data TyConFlavour | DataTypeFlavour | NewtypeFlavour | AbstractTypeFlavour - | DataFamilyFlavour Bool -- True <=> associated - | OpenTypeFamilyFlavour Bool -- True <=> associated + | DataFamilyFlavour (Maybe TyCon) -- Just tc <=> (tc == associated class) + | OpenTypeFamilyFlavour (Maybe TyCon) -- Just tc <=> (tc == associated class) | ClosedTypeFamilyFlavour | TypeSynonymFlavour | BuiltInTypeFlavour -- ^ e.g., the @(->)@ 'TyCon'. @@ -2434,10 +2458,10 @@ instance Outputable TyConFlavour where go DataTypeFlavour = "data type" go NewtypeFlavour = "newtype" go AbstractTypeFlavour = "abstract type" - go (DataFamilyFlavour True) = "associated data family" - go (DataFamilyFlavour False) = "data family" - go (OpenTypeFamilyFlavour True) = "associated type family" - go (OpenTypeFamilyFlavour False) = "type family" + go (DataFamilyFlavour (Just _)) = "associated data family" + go (DataFamilyFlavour Nothing) = "data family" + go (OpenTypeFamilyFlavour (Just _)) = "associated type family" + go (OpenTypeFamilyFlavour Nothing) = "type family" go ClosedTypeFamilyFlavour = "type family" go TypeSynonymFlavour = "type synonym" go BuiltInTypeFlavour = "built-in type" @@ -2455,8 +2479,8 @@ tyConFlavour (AlgTyCon { algTcParent = parent, algTcRhs = rhs }) AbstractTyCon {} -> AbstractTypeFlavour tyConFlavour (FamilyTyCon { famTcFlav = flav, famTcParent = parent }) = case flav of - DataFamilyTyCon{} -> DataFamilyFlavour (isJust parent) - OpenSynFamilyTyCon -> OpenTypeFamilyFlavour (isJust parent) + DataFamilyTyCon{} -> DataFamilyFlavour parent + OpenSynFamilyTyCon -> OpenTypeFamilyFlavour parent ClosedSynFamilyTyCon{} -> ClosedTypeFamilyFlavour AbstractClosedSynFamilyTyCon -> ClosedTypeFamilyFlavour BuiltInSynFamTyCon{} -> ClosedTypeFamilyFlavour diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 34639202db..5ab434f9ed 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -140,15 +140,18 @@ module Type ( tyCoVarsOfType, tyCoVarsOfTypes, tyCoVarsOfTypeDSet, coVarsOfType, - coVarsOfTypes, closeOverKinds, closeOverKindsList, + coVarsOfTypes, + closeOverKindsDSet, closeOverKindsFV, closeOverKindsList, + closeOverKinds, + noFreeVarsOfType, splitVisVarsOfType, splitVisVarsOfTypes, expandTypeSynonyms, typeSize, occCheckExpand, -- * Well-scoped lists of variables - dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped, - tyCoVarsOfTypesWellScoped, + dVarSetElemsWellScoped, scopedSort, tyCoVarsOfTypeWellScoped, + tyCoVarsOfTypesWellScoped, tyCoVarsOfBindersWellScoped, -- * Type comparison eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX, @@ -239,7 +242,7 @@ import UniqSet import Class import TyCon import TysPrim -import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind +import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy , typeSymbolKind, liftedTypeKind ) import PrelNames import CoAxiom @@ -253,16 +256,16 @@ import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo -- others import Util +import FV import Outputable import FastString import Pair import DynFlags ( gopt_set, GeneralFlag(Opt_PrintExplicitRuntimeReps) ) import ListSetOps -import Digraph import Unique ( nonDetCmpUnique ) import Maybes ( orElse ) -import Data.Maybe ( isJust, mapMaybe ) +import Data.Maybe ( isJust ) import Control.Monad ( guard ) -- $type_classification @@ -2101,6 +2104,41 @@ predTypeEqRel ty Well-scoped tyvars * * ************************************************************************ + +Note [ScopedSort] +~~~~~~~~~~~~~~~~~ +Consider + + foo :: Proxy a -> Proxy (b :: k) -> Proxy (a :: k2) -> () + +This function type is implicitly generalised over [a, b, k, k2]. These +variables will be Specified; that is, they will be available for visible +type application. This is because they are written in the type signature +by the user. + +However, we must ask: what order will they appear in? In cases without +dependency, this is easy: we just use the lexical left-to-right ordering +of first occurrence. With dependency, we cannot get off the hook so +easily. + +We thus state: + + * These variables appear in the order as given by ScopedSort, where + the input to ScopedSort is the left-to-right order of first occurrence. + +Note that this applies only to *implicit* quantification, without a +`forall`. If the user writes a `forall`, then we just use the order given. + +ScopedSort is defined thusly (as proposed in #15743): + * Work left-to-right through the input list, with a cursor. + * If variable v at the cursor is depended on by any earlier variable w, + move v immediately before the leftmost such w. + +INVARIANT: The prefix of variables before the cursor form a valid telescope. + +Note that ScopedSort makes sense only after type inference is done and all +types/kinds are fully settled and zonked. + -} -- | Do a topological sort on a list of tyvars, @@ -2112,24 +2150,47 @@ predTypeEqRel ty -- (that is, doesn't depend on Uniques). -- -- It is also meant to be stable: that is, variables should not --- be reordered unnecessarily. The implementation of this --- has been observed to be stable, though it is not proven to --- be so. See also Note [Ordering of implicit variables] in RnTypes -toposortTyVars :: [TyCoVar] -> [TyCoVar] -toposortTyVars tvs = reverse $ - [ node_payload node | node <- topologicalSortG $ - graphFromEdgedVerticesOrd nodes ] +-- be reordered unnecessarily. This is specified in Note [ScopedSort] +-- See also Note [Ordering of implicit variables] in RnTypes + +scopedSort :: [TyCoVar] -> [TyCoVar] +scopedSort = go [] [] where - var_ids :: VarEnv Int - var_ids = mkVarEnv (zip tvs [1..]) + go :: [TyCoVar] -- already sorted, in reverse order + -> [TyCoVarSet] -- each set contains all the variables which must be placed + -- before the tv corresponding to the set; they are accumulations + -- of the fvs in the sorted tvs' kinds + + -- This list is in 1-to-1 correspondence with the sorted tyvars + -- INVARIANT: + -- all (\tl -> all (`subVarSet` head tl) (tail tl)) (tails fv_list) + -- That is, each set in the list is a superset of all later sets. + + -> [TyCoVar] -- yet to be sorted + -> [TyCoVar] + go acc _fv_list [] = reverse acc + go acc fv_list (tv:tvs) + = go acc' fv_list' tvs + where + (acc', fv_list') = insert tv acc fv_list + + insert :: TyCoVar -- var to insert + -> [TyCoVar] -- sorted list, in reverse order + -> [TyCoVarSet] -- list of fvs, as above + -> ([TyCoVar], [TyCoVarSet]) -- augmented lists + insert tv [] [] = ([tv], [tyCoVarsOfType (tyVarKind tv)]) + insert tv (a:as) (fvs:fvss) + | tv `elemVarSet` fvs + , (as', fvss') <- insert tv as fvss + = (a:as', fvs `unionVarSet` fv_tv : fvss') + + | otherwise + = (tv:a:as, fvs `unionVarSet` fv_tv : fvs : fvss) + where + fv_tv = tyCoVarsOfType (tyVarKind tv) - nodes :: [ Node Int TyVar ] - nodes = [ DigraphNode - tv - (lookupVarEnv_NF var_ids tv) - (mapMaybe (lookupVarEnv var_ids) - (tyCoVarsOfTypeList (tyVarKind tv))) - | tv <- tvs ] + -- lists not in correspondence + insert _ _ _ = panic "scopedSort" -- | Extract a well-scoped list of variables from a deterministic set of -- variables. The result is deterministic. @@ -2138,15 +2199,47 @@ toposortTyVars tvs = reverse $ -- well-scoped list. If you care about the list being well-scoped you also -- most likely care about it being in deterministic order. dVarSetElemsWellScoped :: DVarSet -> [Var] -dVarSetElemsWellScoped = toposortTyVars . dVarSetElems +dVarSetElemsWellScoped = scopedSort . dVarSetElems -- | Get the free vars of a type in scoped order tyCoVarsOfTypeWellScoped :: Type -> [TyVar] -tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList +tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList -- | Get the free vars of types in scoped order tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] -tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList +tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList + +-- | Given the suffix of a telescope, returns the prefix. +-- Ex: given [(k :: j), (a :: Proxy k)], returns [(j :: *)]. +tyCoVarsOfBindersWellScoped :: [TyVar] -> [TyVar] +tyCoVarsOfBindersWellScoped tvs + = tyCoVarsOfTypeWellScoped (mkInvForAllTys tvs unitTy) + +------------- Closing over kinds ----------------- + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a non-deterministic set. +closeOverKinds :: TyVarSet -> TyVarSet +closeOverKinds = fvVarSet . closeOverKindsFV . nonDetEltsUniqSet + -- It's OK to use nonDetEltsUniqSet here because we immediately forget + -- about the ordering by returning a set. + +-- | Given a list of tyvars returns a deterministic FV computation that +-- returns the given tyvars with the kind variables free in the kinds of the +-- given tyvars. +closeOverKindsFV :: [TyVar] -> FV +closeOverKindsFV tvs = + mapUnionFV (tyCoFVsOfType . tyVarKind) tvs `unionFV` mkFVs tvs + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a deterministically ordered list. +closeOverKindsList :: [TyVar] -> [TyVar] +closeOverKindsList tvs = fvVarList $ closeOverKindsFV tvs + +-- | Add the kind variables free in the kinds of the tyvars in the given set. +-- Returns a deterministic set. +closeOverKindsDSet :: DTyVarSet -> DTyVarSet +closeOverKindsDSet = fvDVarSet . closeOverKindsFV . dVarSetElems {- ************************************************************************ diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot index e5db1064d4..c88f92f6ed 100644 --- a/compiler/types/Type.hs-boot +++ b/compiler/types/Type.hs-boot @@ -22,5 +22,5 @@ tcView :: Type -> Maybe Type tyCoVarsOfTypesWellScoped :: [Type] -> [TyCoVar] tyCoVarsOfTypeWellScoped :: Type -> [TyCoVar] -toposortTyVars :: [TyCoVar] -> [TyCoVar] +scopedSort :: [TyCoVar] -> [TyCoVar] splitTyConApp_maybe :: HasDebugCallStack => Type -> Maybe (TyCon, [Type]) diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index cfa10e4196..60bba1289f 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -638,7 +638,7 @@ niFixTCvSubst tenv not_fixpoint = any in_domain range_tvs in_domain tv = tv `elemVarEnv` tenv - free_tvs = toposortTyVars (filterOut in_domain range_tvs) + free_tvs = scopedSort (filterOut in_domain range_tvs) -- See Note [Finding the substitution fixpoint], Step 6 init_in_scope = mkInScopeSet (fvVarSet range_fvs) diff --git a/compiler/utils/UniqDFM.hs b/compiler/utils/UniqDFM.hs index 38bf79df24..82a67f351b 100644 --- a/compiler/utils/UniqDFM.hs +++ b/compiler/utils/UniqDFM.hs @@ -145,9 +145,11 @@ emptyUDFM = UDFM M.empty 0 unitUDFM :: Uniquable key => key -> elt -> UniqDFM elt unitUDFM k v = UDFM (M.singleton (getKey $ getUnique k) (TaggedVal v 0)) 1 +-- The new binding always goes to the right of existing ones addToUDFM :: Uniquable key => UniqDFM elt -> key -> elt -> UniqDFM elt addToUDFM m k v = addToUDFM_Directly m (getUnique k) v +-- The new binding always goes to the right of existing ones addToUDFM_Directly :: UniqDFM elt -> Unique -> elt -> UniqDFM elt addToUDFM_Directly (UDFM m i) u v = UDFM (M.insertWith tf (getKey u) (TaggedVal v i) m) (i + 1) diff --git a/compiler/utils/UniqDSet.hs b/compiler/utils/UniqDSet.hs index 0f81a5bc1a..aa53194331 100644 --- a/compiler/utils/UniqDSet.hs +++ b/compiler/utils/UniqDSet.hs @@ -49,6 +49,7 @@ unitUniqDSet x = unitUDFM x x mkUniqDSet :: Uniquable a => [a] -> UniqDSet a mkUniqDSet = foldl' addOneToUniqDSet emptyUniqDSet +-- The new element always goes to the right of existing ones. addOneToUniqDSet :: Uniquable a => UniqDSet a -> a -> UniqDSet a addOneToUniqDSet set x = addToUDFM set x x diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs index 9523c08ff2..c348f79888 100644 --- a/compiler/utils/Util.hs +++ b/compiler/utils/Util.hs @@ -4,6 +4,7 @@ {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE BangPatterns #-} +{-# LANGUAGE TupleSections #-} -- | Highly random utility functions -- @@ -47,7 +48,7 @@ module Util ( -- * Tuples fstOf3, sndOf3, thdOf3, - firstM, first3M, + firstM, first3M, secondM, fst3, snd3, third3, uncurry3, liftFst, liftSnd, @@ -271,6 +272,9 @@ firstM f (x, y) = liftM (\x' -> (x', y)) (f x) first3M :: Monad m => (a -> m d) -> (a, b, c) -> m (d, b, c) first3M f (x, y, z) = liftM (\x' -> (x', y, z)) (f x) +secondM :: Monad m => (b -> m c) -> (a, b) -> m (a, c) +secondM f (x, y) = (x,) <$> f y + {- ************************************************************************ * * diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index 196350348f..e90854c73d 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -8904,6 +8904,78 @@ This rule has occasionally-surprising consequences (see The kind-polymorphism from the class declaration makes ``D1`` kind-polymorphic, but not so ``D2``; and similarly ``F1``, ``F1``. +.. _inferring-variable-order: + +Inferring the order of variables in a type/class declaration +------------------------------------------------------------ + +It is possible to get intricate dependencies among the type variables +introduced in a type or class declaration. Here is an example:: + + data T a (b :: k) c = MkT (a c) + +After analysing this declaration, GHC will discover that ``a`` and +``c`` can be kind-polymorphic, with ``a :: k2 -> Type`` and +``c :: k2``. We thus infer the following kind:: + + T :: forall {k2 :: Type} (k :: Type). (k2 -> Type) -> k -> k2 -> Type + +Note that ``k2`` is placed *before* ``k``, and that ``k`` is placed *before* +``a``. Also, note that ``k2`` is written here in braces. As explained with +:extension:`TypeApplications` (:ref:`inferred-vs-specified`), +type and kind variables that GHC generalises +over, but not written in the original program, are not available for visible +type application. (These are called *inferred* variables.) +Such variables are written in braces with +:ghc-flag:`-fprint-explicit-foralls` enabled. + +The general principle is this: + + * Variables not available for type application come first. + + * Then come variables the user has written, implicitly brought into scope + in a type variable's kind. + + * Lastly come the normal type variables of a declaration. + + * Variables not given an explicit ordering by the user are sorted according + to ScopedSort (:ref:`ScopedSort`). + +With the ``T`` example above, we could bind ``k`` *after* ``a``; doing so +would not violate dependency concerns. However, it would violate our general +principle, and so ``k`` comes first. + +Sometimes, this ordering does not respect dependency. For example:: + + data T2 k (a :: k) (c :: Proxy '[a, b]) + +It must be that ``a`` and ``b`` have the same kind. Note also that ``b`` +is implicitly declared in ``c``\'s kind. Thus, according to our general +principle, ``b`` must come *before* ``k``. However, ``b`` *depends on* +``k``. We thus reject ``T2`` with a suitable error message. + +In keeping with the way that class methods list their class variables +first, associated types also list class variables before others. This +means that the inferred variables from the class come before the +specified variables from the class, which come before other implicitly +bound variables. Here is an example:: + + class C (a :: k) b where + type F (c :: j) (d :: Proxy m) a b + +We infer these kinds:: + + C :: forall {k2 :: Type} (k :: Type). k -> k2 -> Constraint + F :: forall {k2 :: Type} (k :: Type) + {k3 :: Type} (j :: Type) (m :: k3). + j -> Proxy m -> k -> k2 -> Type + +The "general principle" described here is meant to make all this more +predictable for users. It would not be hard to extend GHC to relax +this principle. If you should want a change here, consider writing +a `proposal <https://github.com/ghc-proposals/ghc-proposals/>`_ to +do so. + .. index:: single: CUSK single: complete user-supplied kind signature @@ -10654,14 +10726,108 @@ is an identifier (the common case), its type is considered known only when the identifier has been given a type signature. If the identifier does not have a type signature, visible type application cannot be used. -Here are the details: +.. _inferred-vs-specified: + +Inferred vs. specified type variables +------------------------------------- + +.. index:: + single: type variable; inferred vs. specified + +GHC tracks a distinction between what we call *inferred* and *specified* +type variables. Only specified type variables are available for instantiation +with visible type application. An example illustrates this well:: + + f :: (Eq b, Eq a) => a -> b -> Bool + f x y = (x == x) && (y == y) + + g x y = (x == x) && (y == y) + +The functions ``f`` and ``g`` have the same body, but only ``f`` is given +a type signature. When GHC is figuring out how to process a visible type application, +it must know what variable to instantiate. It thus must be able to provide +an ordering to the type variables in a function's type. + +If the user has supplied a type signature, as in ``f``, then this is easy: +we just take the ordering from the type signature, going left to right and +using the first occurrence of a variable to choose its position within the +ordering. Thus, the variables in ``f`` will be ``b``, then ``a``. + +In contrast, there is no reliable way to do this for ``g``; we will not know +whether ``Eq a`` or ``Eq b`` will be listed first in the constraint in ``g``\'s +type. In order to have visible type application be robust between releases of +GHC, we thus forbid its use with ``g``. + +We say that the type variables in ``f`` are *specified*, while those in +``g`` are *inferred*. The general rule is this: if the user has written +a type variable in the source program, it is *specified*; if not, it is +*inferred*. + +Thus rule applies in datatype declarations, too. For example, if we have +``data Proxy a = Proxy`` (and :extension:`PolyKinds` is enabled), then +``a`` will be assigned kind ``k``, where ``k`` is a fresh kind variable. +Because ``k`` was not written by the user, it will be unavailable for +type application in the type of the constructor ``Proxy``; only the ``a`` +will be available. + +When :ghc-flag:`-fprint-explicit-foralls` is enabled, inferred variables +are printed in braces. Thus, the type of the data constructor ``Proxy`` +from the previous example would be ``forall {k} (a :: k). Proxy a``. +We can observe this behavior in a GHCi session: :: + + > :set -XTypeApplications -fprint-explicit-foralls + > let myLength1 :: Foldable f => f a -> Int; myLength1 = length + > :type +v myLength1 + myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int + > let myLength2 = length + > :type +v myLength2 + myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int + > :type +v myLength2 @[] + + <interactive>:1:1: error: + • Cannot apply expression of type ‘t0 a0 -> Int’ + to a visible type argument ‘[]’ + • In the expression: myLength2 @[] + +Notice that since ``myLength1`` was defined with an explicit type signature, +:ghci-cmd:`:type +v` reports that all of its type variables are available +for type application. On the other hand, ``myLength2`` was not given a type +signature. As a result, all of its type variables are surrounded with braces, +and trying to use visible type application with ``myLength2`` fails. + +Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead +of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type +that would be inferred for a variable assigned to the expression provided +(that is, the type of ``x`` in ``let x = <expr>``). As we saw above with +``myLength2``, this type will have no variables available to visible type +application. On the other hand, :ghci-cmd:`:type +v` gives you the actual +type of the expression provided. To illustrate this: :: + + > :type myLength1 + myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int + > :type myLength2 + myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int + +Using :ghci-cmd:`:type` might lead one to conclude that none of the type +variables in ``myLength1``'s type signature are available for type +application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v` +if you want the most accurate information with respect to visible type +application properties. + +.. _ScopedSort: + +.. index:: + single: ScopedSort + +Ordering of specified variables +------------------------------- + +In the simple case of the previous section, we can say that specified variables +appear in left-to-right order. However, not all cases are so simple. Here are +the rules in the subtler cases: -- If an identifier's type signature does not include an - explicit ``forall``, the type variable arguments appear - in the left-to-right order in which the variables appear in the type. - So, ``foo :: Monad m => a b -> m (a c)`` - will have its type variables - ordered as ``m, a, b, c``. +- 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 @@ -10680,7 +10846,7 @@ Here are the details: of the variables are *kind* variables), the variables are reordered so that kind variables come before type variables, preserving the left-to-right order as much as possible. That is, GHC performs a - stable topological sort on the variables. Examples:: + stable topological sort on the variables. Example:: h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> () -- as if h :: forall j k a b. ... @@ -10693,10 +10859,12 @@ Here are the details: are not reordered with respect to each other, even though doing so would not violate dependency conditions. -- Visible type application is available to instantiate only user-specified - type variables. This means that in ``data Proxy a = Proxy``, the unmentioned - kind variable used in ``a``'s kind is *not* available for visible type - application. + A "stable topological sort" here, we mean that we perform this algorithm + (which we call *ScopedSort*): + + * Work left-to-right through the input list of type variables, with a cursor. + * If variable ``v`` at the cursor is depended on by any earlier variable ``w``, + move ``v`` immediately before the leftmost such ``w``. - Class methods' type arguments include the class type variables, followed by any variables an individual method is polymorphic @@ -10719,72 +10887,9 @@ Here are the details: necessary to specify :extension:`PartialTypeSignatures` and your code will not generate a warning informing you of the omitted type. -- When printing types with :ghc-flag:`-fprint-explicit-foralls` enabled, - type variables not available for visible type application are printed - in braces. We can observe this behavior in a GHCi session: :: - - > :set -XTypeApplications -fprint-explicit-foralls - > let myLength1 :: Foldable f => f a -> Int; myLength1 = length - > :type +v myLength1 - myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int - > let myLength2 = length - > :type +v myLength2 - myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int - > :type +v myLength2 @[] - - <interactive>:1:1: error: - • Cannot apply expression of type ‘t0 a0 -> Int’ - to a visible type argument ‘[]’ - • In the expression: myLength2 @[] - - Notice that since ``myLength1`` was defined with an explicit type signature, - :ghci-cmd:`:type +v` reports that all of its type variables are available - for type application. On the other hand, ``myLength2`` was not given a type - signature. As a result, all of its type variables are surrounded with braces, - and trying to use visible type application with ``myLength2`` fails. - - Also note the use of :ghci-cmd:`:type +v` in the GHCi session above instead - of :ghci-cmd:`:type`. This is because :ghci-cmd:`:type` gives you the type - that would be inferred for a variable assigned to the expression provided - (that is, the type of ``x`` in ``let x = <expr>``). As we saw above with - ``myLength2``, this type will have no variables available to visible type - application. On the other hand, :ghci-cmd:`:type +v` gives you the actual - type of the expression provided. To illustrate this: :: - - > :type myLength1 - myLength1 :: forall {a} {f :: * -> *}. Foldable f => f a -> Int - > :type myLength2 - myLength2 :: forall {a} {t :: * -> *}. Foldable t => t a -> Int - - Using :ghci-cmd:`:type` might lead one to conclude that none of the type - variables in ``myLength1``'s type signature are available for type - application. This isn't true, however! Be sure to use :ghci-cmd:`:type +v` - if you want the most accurate information with respect to visible type - application properties. - -- Although GHC supports visible *type* applications, it does not yet support - visible *kind* applications. However, GHC does follow similar rules for - quantifying variables in kind signatures as it does for quantifying type - signatures. For instance: :: - - type family F (a :: j) (b :: k) :: l - -- F :: forall j k l. j -> k -> l - - In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l`` - is preserved. - - If a family declaration is associated with a class, then class-bound - variables always come first in the kind of the family. For instance: :: - - class C (a :: Type) where - type T (x :: f a) - -- T :: forall a f. f a -> Type - - Contrast this with the kind of the following top-level family declaration: :: - - type family T2 (x :: f a) - -- T2 :: forall f a. f a -> Type - +The section in this manual on kind polymorphism describes how variables +in type and class declarations are ordered (:ref:`inferring-variable-order`). + .. _implicit-parameters: Implicit parameters diff --git a/docs/users_guide/using.rst b/docs/users_guide/using.rst index 4373a4a8d5..e0807a9620 100644 --- a/docs/users_guide/using.rst +++ b/docs/users_guide/using.rst @@ -764,10 +764,13 @@ messages and in GHCi: ghci> :i Data.Type.Equality.sym Data.Type.Equality.sym :: - forall (k :: BOX) (a :: k) (b :: k). + forall k (a :: k) (b :: k). (a Data.Type.Equality.:~: b) -> b Data.Type.Equality.:~: a -- Defined in Data.Type.Equality + This flag also enables the printing of *inferred* type variables + inside braces. See :ref:`inferred-vs-specified`. + .. ghc-flag:: -fprint-explicit-kinds :shortdesc: Print explicit kind foralls and kind arguments in types. See also :ghc-flag:`-XKindSignatures` @@ -784,10 +787,10 @@ messages and in GHCi: ghci> :set -XPolyKinds ghci> data T a = MkT ghci> :t MkT - MkT :: forall (k :: BOX) (a :: k). T a - ghci> :set -fprint-explicit-foralls + MkT :: forall (k :: Type) (a :: k). T a + ghci> :set -fprint-explicit-kinds ghci> :t MkT - MkT :: forall (k :: BOX) (a :: k). T k a + MkT :: forall (k :: Type) (a :: k). T k a .. ghc-flag:: -fprint-explicit-runtime-reps :shortdesc: Print ``RuntimeRep`` variables in types which are diff --git a/testsuite/tests/dependent/should_fail/InferDependency.hs b/testsuite/tests/dependent/should_compile/InferDependency.hs index c2bec19d44..c2bec19d44 100644 --- a/testsuite/tests/dependent/should_fail/InferDependency.hs +++ b/testsuite/tests/dependent/should_compile/InferDependency.hs diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr index 610e434d6c..906695f3f7 100644 --- a/testsuite/tests/dependent/should_compile/T14066a.stderr +++ b/testsuite/tests/dependent/should_compile/T14066a.stderr @@ -1,5 +1,5 @@ T14066a.hs:13:3: warning: Type family instance equation is overlapped: - forall d c (x :: c) (y :: d). + forall c d (x :: c) (y :: d). Bar x y = Bool -- Defined at T14066a.hs:13:3 diff --git a/testsuite/tests/dependent/should_compile/T14880-2.hs b/testsuite/tests/dependent/should_compile/T14880-2.hs new file mode 100644 index 0000000000..e7057a3f00 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14880-2.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PartialTypeSignatures #-} +module Bug where + +import Data.Kind +import Data.Proxy + +data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type + +quux :: forall arg. Proxy (Foo arg) -> () +quux (_ :: _) = () diff --git a/testsuite/tests/dependent/should_compile/T14880-2.stderr b/testsuite/tests/dependent/should_compile/T14880-2.stderr new file mode 100644 index 0000000000..758924dd41 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14880-2.stderr @@ -0,0 +1,12 @@ + +T14880-2.hs:13:12: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found type wildcard ‘_’ standing for ‘Proxy (Foo arg)’ + Where: ‘arg’ is a rigid type variable bound by + the type signature for: + quux :: forall arg. Proxy (Foo arg) -> () + at T14880-2.hs:12:1-41 + • In a pattern type signature: _ + In the pattern: _ :: _ + In an equation for ‘quux’: quux (_ :: _) = () + • Relevant bindings include + quux :: Proxy (Foo arg) -> () (bound at T14880-2.hs:13:1) diff --git a/testsuite/tests/dependent/should_compile/T14880.hs b/testsuite/tests/dependent/should_compile/T14880.hs new file mode 100644 index 0000000000..91cfb20a4a --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T14880.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeInType #-} +module Bug where + +import Data.Kind +import Data.Proxy + +data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type + +data Bar :: Type -> Type where + MkBar :: forall x arg. + -- Commenting out the line below makes the issue go away + Foo arg ~ Foo arg => + Bar x diff --git a/testsuite/tests/dependent/should_compile/T15743.hs b/testsuite/tests/dependent/should_compile/T15743.hs new file mode 100644 index 0000000000..1ba10aeb9a --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T15743.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies #-} + +module T15743 where + +import Data.Proxy + +data T (b :: Proxy (k2 :: k)) c (a :: k) diff --git a/testsuite/tests/dependent/should_compile/T15743.stderr b/testsuite/tests/dependent/should_compile/T15743.stderr new file mode 100644 index 0000000000..7162a877a2 --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T15743.stderr @@ -0,0 +1,6 @@ +TYPE CONSTRUCTORS + type role T nominal nominal nominal phantom phantom phantom + T :: forall {k1} k2 (k3 :: k2). Proxy k3 -> k1 -> k2 -> * +Dependent modules: [] +Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, + integer-gmp-1.0.2.0] diff --git a/testsuite/tests/dependent/should_compile/T15743e.hs b/testsuite/tests/dependent/should_compile/T15743e.hs new file mode 100644 index 0000000000..37e0cbb2cd --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T15743e.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE RankNTypes, PolyKinds, DataKinds, GADTs #-} + +module T15743e where + +import Data.Proxy +import Data.Kind + +-- NO CUSK. +data T k (a :: k) (b :: Proxy k2) f c :: forall k3. Proxy k3 -> forall (k4 :: k5). Proxy k4 -> Type where + MkT :: f c -> T k a b f c d e + +-- Want: +-- T :: forall {k3} {k7} {k6} (k2 :: k3) (k5 :: Type). +-- forall k -> k -> Proxy k2 -> (k7 -> Type) -> k4 -> +-- forall (k3 :: k6). Proxy k3 -> forall (k4 :: k5). Proxy k4 -> Type +-- +-- + +-- CUSK +data T2 (k :: Type) (a :: k) (b :: Proxy k2) (f :: k7 -> Type) (c :: k7) :: forall k3. Proxy k3 -> forall k5 (k4 :: k5). Proxy k4 -> Type where + MkT2 :: f c -> T2 k a b f c d e diff --git a/testsuite/tests/dependent/should_compile/T15743e.stderr b/testsuite/tests/dependent/should_compile/T15743e.stderr new file mode 100644 index 0000000000..c77bf3849c --- /dev/null +++ b/testsuite/tests/dependent/should_compile/T15743e.stderr @@ -0,0 +1,32 @@ +TYPE CONSTRUCTORS + type role T + nominal nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal phantom + T :: + forall {k1} {k2} {k3} (k4 :: k2) k5. forall k6 -> + k6 + -> Proxy k4 + -> (k3 -> *) + -> k3 + -> forall (k7 :: k1). Proxy k7 -> forall (k8 :: k5). Proxy k8 -> * + type role T2 + nominal nominal nominal nominal nominal phantom phantom representational nominal nominal phantom nominal nominal phantom + T2 :: + forall {k1} {k2} (k3 :: k1) k7. forall k4 -> + k4 + -> Proxy k3 + -> (k7 -> *) + -> k7 + -> forall (k5 :: k2). + Proxy k5 -> forall k6 (k8 :: k6). Proxy k8 -> * +DATA CONSTRUCTORS + MkT2 :: forall {k7} {k1} {k2 :: k1} {k3} {k4 :: k3} {k5} {k6 :: k5} + (f :: k7 -> *) (c :: k7) k8 (a :: k8) (b :: Proxy k2) + (d :: Proxy k4) (e :: Proxy k6). + f c -> T2 k8 a b f c d e + MkT :: forall {k1} {k2} {k3 :: k2} {k4} {k5 :: k4} {k6} {k7 :: k6} + (f :: k1 -> *) (c :: k1) k8 (a :: k8) (b :: Proxy k3) + (d :: Proxy k5) (e :: Proxy k7). + f c -> T k8 a b f c d e +Dependent modules: [] +Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3, + integer-gmp-1.0.2.0] diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T index 1bf6cc7142..16c6d13ba9 100644 --- a/testsuite/tests/dependent/should_compile/all.T +++ b/testsuite/tests/dependent/should_compile/all.T @@ -56,3 +56,8 @@ test('T15419', normal, compile, ['']) test('T14066h', normal, compile, ['']) test('T15666', normal, compile, ['']) test('T15725', normal, compile, ['']) +test('T14880', normal, compile, ['']) +test('T14880-2', normal, compile, ['']) +test('T15743', normal, compile, ['-ddump-types -fprint-explicit-foralls']) +test('InferDependency', normal, compile, ['']) +test('T15743e', normal, compile, ['-ddump-types -fprint-explicit-foralls']) diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr deleted file mode 100644 index cc852ee58c..0000000000 --- a/testsuite/tests/dependent/should_fail/InferDependency.stderr +++ /dev/null @@ -1,10 +0,0 @@ - -InferDependency.hs:6:13: error: - • Type constructor argument ‘k’ is used dependently. - Any dependent arguments must be obviously so, not inferred - by the type-checker. - Inferred argument kinds: - k :: * - a :: k - Suggestion: use ‘k’ in a kind to make the dependency clearer. - • In the data type declaration for ‘Proxy2’ diff --git a/testsuite/tests/dependent/should_fail/SelfDep.stderr b/testsuite/tests/dependent/should_fail/SelfDep.stderr index 8ac4be8c0c..3c90f5444b 100644 --- a/testsuite/tests/dependent/should_fail/SelfDep.stderr +++ b/testsuite/tests/dependent/should_fail/SelfDep.stderr @@ -3,3 +3,4 @@ SelfDep.hs:5:11: error: • Type constructor ‘T’ cannot be used here (it is defined and used in the same recursive group) • In the kind ‘T -> *’ + In the data type declaration for ‘T’ diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr index 3e8bef6858..3ced11a79d 100644 --- a/testsuite/tests/dependent/should_fail/T13895.stderr +++ b/testsuite/tests/dependent/should_fail/T13895.stderr @@ -1,19 +1,15 @@ T13895.hs:8:14: error: - • Could not deduce (Typeable (t dict0)) + • Could not deduce (Typeable (t dict)) 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 - -> *). + dataCast1 :: forall k1 a (c :: * -> *) (t :: forall k2. + Typeable k2 => + k2 -> *). (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 + The type variable ‘k0’ is ambiguous • In the ambiguity check for ‘dataCast1’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature: diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr index 8ece51029b..23b8577a1b 100644 --- a/testsuite/tests/dependent/should_fail/T14066d.stderr +++ b/testsuite/tests/dependent/should_fail/T14066d.stderr @@ -15,7 +15,7 @@ T14066d.hs:11:35: error: In the expression: g y In the expression: (fstOf3 y :: Proxy Maybe, g y) • Relevant bindings include - y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b) + y :: forall k1 k2 (a :: k1) (c :: k2). (Proxy a, Proxy c, b) (bound at T14066d.hs:15:5) x :: b (bound at T14066d.hs:11:3) f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1) diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index 193c74d193..a6bf647bee 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,15 +1,15 @@ T14066e.hs:13:59: error: - • Couldn't match kind ‘k1’ with ‘*’ - ‘k1’ is a rigid type variable bound by + • Couldn't match kind ‘k’ with ‘*’ + ‘k’ is a rigid type variable bound by the type signature for: - j :: forall k k1 (c :: k1) (b :: k). + j :: forall k k1 (c :: k) (b :: k1). 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’ + k1 :: * + c :: k + Expected kind ‘c’, but ‘b'’ has kind ‘k1’ • 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/T15591b.hs b/testsuite/tests/dependent/should_fail/T15591b.hs new file mode 100644 index 0000000000..fb23aca2e5 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15591b.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE PolyKinds, MultiParamTypeClasses, DataKinds, TypeFamilies #-} + +module T15591b where + +import Data.Proxy +import Data.Kind + +class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where + type T4 a c diff --git a/testsuite/tests/dependent/should_fail/T15591b.stderr b/testsuite/tests/dependent/should_fail/T15591b.stderr new file mode 100644 index 0000000000..838ee51c8f --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15591b.stderr @@ -0,0 +1,7 @@ + +T15591b.hs:9:3: error: + • These kind and type variables: a c + are out of dependency order. Perhaps try this ordering: + a (b :: Proxy a) (c :: Proxy b) + NB: Implicitly declared variables come before others. + • In the associated type family declaration for ‘T4’ diff --git a/testsuite/tests/dependent/should_fail/T15591c.hs b/testsuite/tests/dependent/should_fail/T15591c.hs new file mode 100644 index 0000000000..b9fcb9cc96 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15591c.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE PolyKinds, MultiParamTypeClasses, DataKinds, TypeFamilies #-} + +module T15591c where + +import Data.Proxy +import Data.Kind + +class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) where + type T5 c a diff --git a/testsuite/tests/dependent/should_fail/T15591c.stderr b/testsuite/tests/dependent/should_fail/T15591c.stderr new file mode 100644 index 0000000000..2f2b47fc8d --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15591c.stderr @@ -0,0 +1,7 @@ + +T15591c.hs:9:3: error: + • These kind and type variables: c a + are out of dependency order. Perhaps try this ordering: + a (b :: Proxy a) (c :: Proxy b) + NB: Implicitly declared variables come before others. + • In the associated type family declaration for ‘T5’ diff --git a/testsuite/tests/dependent/should_fail/T15743c.hs b/testsuite/tests/dependent/should_fail/T15743c.hs new file mode 100644 index 0000000000..eb8f68349f --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15743c.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE PolyKinds, DataKinds, ExplicitForAll #-} + +module T15743 where + +import Data.Kind +import Data.Proxy + +data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type + +data T k (c :: k) (a :: Proxy c) b (x :: SimilarKind a b) +data T2 k (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr new file mode 100644 index 0000000000..9d28b68998 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15743c.stderr @@ -0,0 +1,16 @@ + +T15743c.hs:10:1: error: + • These kind and type variables: k + (c :: k) + (a :: Proxy c) + b + (x :: SimilarKind a b) + are out of dependency order. Perhaps try this ordering: + k + (d :: k) + (c :: k) + (a :: Proxy c) + (b :: Proxy d) + (x :: SimilarKind a b) + NB: Implicitly declared variables come before others. + • In the data type declaration for ‘T’ diff --git a/testsuite/tests/dependent/should_fail/T15743d.hs b/testsuite/tests/dependent/should_fail/T15743d.hs new file mode 100644 index 0000000000..67d8faebed --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15743d.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE PolyKinds, DataKinds, ExplicitForAll #-} + +module T15743 where + +import Data.Kind +import Data.Proxy + +data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type + +data T2 k (c :: k) (a :: Proxy c) (b :: Proxy d) (x :: SimilarKind a b) diff --git a/testsuite/tests/dependent/should_fail/T15743d.stderr b/testsuite/tests/dependent/should_fail/T15743d.stderr new file mode 100644 index 0000000000..d982d16980 --- /dev/null +++ b/testsuite/tests/dependent/should_fail/T15743d.stderr @@ -0,0 +1,16 @@ + +T15743d.hs:10:1: error: + • These kind and type variables: k + (c :: k) + (a :: Proxy c) + (b :: Proxy d) + (x :: SimilarKind a b) + are out of dependency order. Perhaps try this ordering: + k + (d :: k) + (c :: k) + (a :: Proxy c) + (b :: Proxy d) + (x :: SimilarKind a b) + NB: Implicitly declared variables come before others. + • In the data type declaration for ‘T2’ diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T index 0f7129020e..2b602fa383 100644 --- a/testsuite/tests/dependent/should_fail/all.T +++ b/testsuite/tests/dependent/should_fail/all.T @@ -28,9 +28,12 @@ test('T14066f', normal, compile_fail, ['']) test('T14066g', normal, compile_fail, ['']) test('T14845_fail1', normal, compile_fail, ['']) test('T14845_fail2', normal, compile_fail, ['']) -test('InferDependency', normal, compile_fail, ['']) test('T15245', normal, compile_fail, ['']) test('T15215', normal, compile_fail, ['']) test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds']) test('T15343', normal, compile_fail, ['']) test('T15380', normal, compile_fail, ['']) +test('T15591b', normal, compile_fail, ['']) +test('T15591c', normal, compile_fail, ['']) +test('T15743c', normal, compile_fail, ['']) +test('T15743d', normal, compile_fail, ['']) diff --git a/testsuite/tests/ghci/scripts/T15591.hs b/testsuite/tests/ghci/scripts/T15591.hs index eccf628eed..f333fe0194 100644 --- a/testsuite/tests/ghci/scripts/T15591.hs +++ b/testsuite/tests/ghci/scripts/T15591.hs @@ -1,10 +1,26 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} module Foo where import Data.Kind +import Data.Proxy type family T1 (x :: f (a :: Type)) class C (a :: Type) where type T2 (x :: f a) + +class C2 (a :: Type) (b :: Proxy a) (c :: Proxy b) where + type T3 (x :: Proxy '(a, c)) + +-- no CUSK +class C3 (a :: Type) (b :: Proxy a) (c :: Proxy b) d where + type T4 (x :: Proxy '(a, c)) + +class C4 (a :: Type) b where + type T5 (x :: f a) + +class C5 a where + type T6 (x :: f a) diff --git a/testsuite/tests/ghci/scripts/T15591.script b/testsuite/tests/ghci/scripts/T15591.script index 0afd32e1e6..0e181a960e 100644 --- a/testsuite/tests/ghci/scripts/T15591.script +++ b/testsuite/tests/ghci/scripts/T15591.script @@ -2,3 +2,7 @@ :set -fprint-explicit-foralls :kind T1 :kind T2 +:kind T3 +:kind T4 +:kind T5 +:kind T6 diff --git a/testsuite/tests/ghci/scripts/T15591.stdout b/testsuite/tests/ghci/scripts/T15591.stdout index 28dbd49dc1..b4673d5174 100644 --- a/testsuite/tests/ghci/scripts/T15591.stdout +++ b/testsuite/tests/ghci/scripts/T15591.stdout @@ -1,2 +1,6 @@ T1 :: forall (f :: * -> *) a. f a -> * T2 :: forall a (f :: * -> *). f a -> * +T3 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * +T4 :: forall a (b :: Proxy a) (c :: Proxy b). Proxy '(a, c) -> * +T5 :: forall a (f :: * -> *). f a -> * +T6 :: forall {k} (a :: k) (f :: k -> *). f a -> * diff --git a/testsuite/tests/ghci/scripts/T15743b.hs b/testsuite/tests/ghci/scripts/T15743b.hs new file mode 100644 index 0000000000..2bd5b6b649 --- /dev/null +++ b/testsuite/tests/ghci/scripts/T15743b.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE PolyKinds, TypeFamilies #-} + +module T15743b where + +class C (a :: k) where + type F a (b :: k2) diff --git a/testsuite/tests/ghci/scripts/T15743b.script b/testsuite/tests/ghci/scripts/T15743b.script new file mode 100644 index 0000000000..cb0f6c4a5b --- /dev/null +++ b/testsuite/tests/ghci/scripts/T15743b.script @@ -0,0 +1,3 @@ +:load T15743b.hs +:set -fprint-explicit-foralls +:k F diff --git a/testsuite/tests/ghci/scripts/T15743b.stdout b/testsuite/tests/ghci/scripts/T15743b.stdout new file mode 100644 index 0000000000..03e593e5bd --- /dev/null +++ b/testsuite/tests/ghci/scripts/T15743b.stdout @@ -0,0 +1 @@ +F :: forall k k2. k -> k2 -> * diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr index 9765244f1e..6970eb3d7c 100644 --- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr +++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr @@ -39,7 +39,7 @@ <interactive>:55:41: error: Type family equation violates injectivity annotation. - Kind variable ‘k1’ cannot be inferred from the right-hand side. + Kind variable ‘k2’ cannot be inferred from the right-hand side. Use -fprint-explicit-kinds to see the kind arguments In the type family equation: PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41 diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T index bb3be803ff..97ae8bb26f 100755 --- a/testsuite/tests/ghci/scripts/all.T +++ b/testsuite/tests/ghci/scripts/all.T @@ -287,3 +287,4 @@ test('T15341', normal, ghci_script, ['T15341.script']) test('T15568', normal, ghci_script, ['T15568.script']) test('T15325', normal, ghci_script, ['T15325.script']) test('T15591', normal, ghci_script, ['T15591.script']) +test('T15743b', normal, ghci_script, ['T15743b.script']) diff --git a/testsuite/tests/indexed-types/should_fail/T14175.stderr b/testsuite/tests/indexed-types/should_fail/T14175.stderr index dbadbe1f46..e177036e9e 100644 --- a/testsuite/tests/indexed-types/should_fail/T14175.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14175.stderr @@ -3,3 +3,4 @@ T14175.hs:7:42: error: • Expecting one more argument to ‘k’ Expected a type, but ‘k’ has kind ‘j -> *’ • In the kind ‘k’ + In the type family declaration for ‘PComp’ diff --git a/testsuite/tests/patsyn/should_compile/T14394.stdout b/testsuite/tests/patsyn/should_compile/T14394.stdout index 557b8f4a74..f59f62cb78 100644 --- a/testsuite/tests/patsyn/should_compile/T14394.stdout +++ b/testsuite/tests/patsyn/should_compile/T14394.stdout @@ -1,7 +1,7 @@ pattern Foo :: () => (b ~ a) => a :~~: b -- Defined at <interactive>:5:1 pattern Bar - :: forall k2 k1 (a :: k1) (b :: k2). + :: forall k1 k2 (a :: k1) (b :: k2). () => (k2 ~ k1, b ~~ a) => a :~~: b diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_compile/T14552.hs index a4a7493530..a4a7493530 100644 --- a/testsuite/tests/patsyn/should_fail/T14552.hs +++ b/testsuite/tests/patsyn/should_compile/T14552.hs diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 19c9eaafae..54775a80a2 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -75,3 +75,4 @@ test('T14058', [extra_files(['T14058.hs', 'T14058a.hs'])], multimod_compile, ['T14058', '-v0']) test('T14326', normal, compile, ['']) test('T14394', normal, ghci_script, ['T14394.script']) +test('T14552', normal, compile, ['']) diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr deleted file mode 100644 index 1723b325fa..0000000000 --- a/testsuite/tests/patsyn/should_fail/T14552.stderr +++ /dev/null @@ -1,9 +0,0 @@ - -T14552.hs:22:9: error: - • Universal type variable ‘aa’ has existentially bound kind: - aa :: k - Existentially-bound variables: - k :: * - w :: k --> * - Probable fix: give the pattern synonym a type signature - • In the declaration for pattern synonym ‘FOO’ diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T index 099e9059d9..7cdef908a6 100644 --- a/testsuite/tests/patsyn/should_fail/all.T +++ b/testsuite/tests/patsyn/should_fail/all.T @@ -41,7 +41,6 @@ test('T14112', normal, compile_fail, ['']) test('T14114', normal, compile_fail, ['']) test('T14380', normal, compile_fail, ['']) test('T14498', normal, compile_fail, ['']) -test('T14552', 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/PolyKinds06.stderr b/testsuite/tests/polykinds/PolyKinds06.stderr index d6fa854c8f..e5c9daa8c3 100644 --- a/testsuite/tests/polykinds/PolyKinds06.stderr +++ b/testsuite/tests/polykinds/PolyKinds06.stderr @@ -1,5 +1,6 @@ -PolyKinds06.hs:9:11: - Type constructor ‘A’ cannot be used here - (it is defined and used in the same recursive group) - In the kind ‘A -> *’ +PolyKinds06.hs:9:11: error: + • Type constructor ‘A’ cannot be used here + (it is defined and used in the same recursive group) + • In the kind ‘A -> *’ + In the data type declaration for ‘B’ diff --git a/testsuite/tests/polykinds/T13625.stderr b/testsuite/tests/polykinds/T13625.stderr index 4e0d4b68d6..98208fcde3 100644 --- a/testsuite/tests/polykinds/T13625.stderr +++ b/testsuite/tests/polykinds/T13625.stderr @@ -3,3 +3,4 @@ T13625.hs:5:11: error: • Data constructor ‘Y’ cannot be used here (it is defined and used in the same recursive group) • In the kind ‘Y’ + In the data type declaration for ‘X’ diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 1d852031d9..062dc49e1f 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -3,8 +3,8 @@ T14846.hs:38:8: error: • Couldn't match type ‘ríki’ with ‘Hom riki’ ‘ríki’ is a rigid type variable bound by the type signature for: - i :: forall k5 (cls2 :: k5 - -> Constraint) k6 (xx :: k6) (a :: Struct cls2) (ríki :: Struct + i :: forall k5 k6 (cls2 :: k6 + -> Constraint) (xx :: k5) (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 @@ -16,12 +16,12 @@ T14846.hs:38:8: error: 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 k1 (cls :: k1 - -> Constraint) k2 (xx :: k2) (a :: Struct cls). + Instance sig: forall k1 k2 (cls :: k2 + -> Constraint) (xx :: k1) (a :: Struct cls). StructI xx a => Hom riki a a - Class sig: forall k1 (cls :: k1 - -> Constraint) k2 (xx :: k2) (a :: Struct + Class sig: forall k1 k2 (cls :: k2 + -> Constraint) (xx :: k1) (a :: Struct cls) (ríki :: Struct cls -> Struct @@ -32,12 +32,12 @@ 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 cls2’ - ‘k4’ is a rigid type variable bound by + • Couldn't match kind ‘k3’ with ‘Struct cls2’ + ‘k3’ is a rigid type variable bound by the instance declaration at T14846.hs:37:10-65 When matching kinds - cls1 :: k4 -> Constraint + cls1 :: k3 -> Constraint cls0 :: Struct cls -> Constraint Expected kind ‘Struct cls0’, but ‘Structured a cls’ has kind ‘Struct cls1’ diff --git a/testsuite/tests/polykinds/T15592.hs b/testsuite/tests/polykinds/T15592.hs index 7e81c42565..e351c82bf5 100644 --- a/testsuite/tests/polykinds/T15592.hs +++ b/testsuite/tests/polykinds/T15592.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE TypeInType #-} +{-# LANGUAGE PolyKinds, TypeFamilies #-} {-# OPTIONS_GHC -ddump-types -fprint-explicit-foralls #-} module T15592 where diff --git a/testsuite/tests/polykinds/T7524.stderr b/testsuite/tests/polykinds/T7524.stderr index 2340ce1aa6..26cfe39e8a 100644 --- a/testsuite/tests/polykinds/T7524.stderr +++ b/testsuite/tests/polykinds/T7524.stderr @@ -2,5 +2,5 @@ T7524.hs:5:15: error: Conflicting family instance declarations: forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15 - forall k2 k1 (a :: k1) (b :: k2). + forall k1 k2 (a :: k1) (b :: k2). F a b = Bool -- Defined at T7524.hs:6:15 diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr index 54a32adafd..f5c06a654a 100644 --- a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr +++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr @@ -1,4 +1,14 @@ +ExplicitForAllRules1.hs:45:11: warning: + Forall'd type variable ‘k’ is not bound in RULE lhs + Orig bndrs: [k, a, b, x] + Orig lhs: id @ a x + optimised lhs: id @ a x + Forall'd type variable ‘b’ is not bound in RULE lhs + Orig bndrs: [k, a, b, x] + Orig lhs: id @ a x + optimised lhs: id @ a x + ExplicitForAllRules1.hs:45:31: warning: [-Wunused-foralls (in -Wextra)] Unused quantified type variable ‘b’ in the rule "example7" diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr index cbf67b405f..eb80d3ec80 100644 --- a/testsuite/tests/typecheck/should_fail/T14350.stderr +++ b/testsuite/tests/typecheck/should_fail/T14350.stderr @@ -1,6 +1,6 @@ T14350.hs:59:15: error: - • Couldn't match expected type ‘Proxy a2 + • Couldn't match expected type ‘Proxy a1 -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’ with actual type ‘Sing (f @@ t0)’ • The function ‘applySing’ is applied to three arguments, @@ -8,11 +8,11 @@ T14350.hs:59:15: error: In the expression: applySing f Proxy Proxy In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy • Relevant bindings include - x :: Sing x3 (bound at T14350.hs:59:11) + x :: Sing x (bound at T14350.hs:59:11) g :: Sing g (bound at T14350.hs:59:9) f :: Sing f (bound at T14350.hs:59:7) dcomp :: Sing f - -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy) + -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) (bound at T14350.hs:59:1) T14350.hs:59:27: error: @@ -22,9 +22,9 @@ T14350.hs:59:27: error: In the expression: applySing f Proxy Proxy In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy • Relevant bindings include - x :: Sing x3 (bound at T14350.hs:59:11) + x :: Sing x (bound at T14350.hs:59:11) g :: Sing g (bound at T14350.hs:59:9) f :: Sing f (bound at T14350.hs:59:7) dcomp :: Sing f - -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy) + -> Sing g -> Sing x -> (c @@ 'Proxy) @@ (g @@ 'Proxy) (bound at T14350.hs:59:1) diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr index 0265250dbe..7f7dadd499 100644 --- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr @@ -59,7 +59,7 @@ T6018fail.hs:53:15: error: T6018fail.hs:61:10: error: Type family equation violates injectivity annotation. - Kind variable ‘k1’ cannot be inferred from the right-hand side. + Kind variable ‘k2’ cannot be inferred from the right-hand side. Use -fprint-explicit-kinds to see the kind arguments In the type family equation: PolyKindVarsF '[] = '[] -- Defined at T6018fail.hs:61:10 diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr index 9914842013..e90dce0620 100644 --- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr +++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr @@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error: T6018failclosed.hs:25:5: error: • Type family equation violates injectivity annotation. - Type and kind variables ‘k2’, ‘b’ + Type and kind variables ‘k1’, ‘b’ cannot be inferred from the right-hand side. Use -fprint-explicit-kinds to see the kind arguments In the type family equation: - forall k1 k2 (b :: k2) (c :: k1). + forall k1 k2 (b :: k1) (c :: k2). JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5 • In the equations for closed type family ‘JClosed’ In the type family declaration for ‘JClosed’ diff --git a/testsuite/tests/typecheck/should_fail/T7892.stderr b/testsuite/tests/typecheck/should_fail/T7892.stderr index d6120f936c..fa332c745e 100644 --- a/testsuite/tests/typecheck/should_fail/T7892.stderr +++ b/testsuite/tests/typecheck/should_fail/T7892.stderr @@ -1,2 +1,4 @@ -T7892.hs:5:4: error: Expected kind ‘* -> *’, but ‘f’ has kind ‘*’ +T7892.hs:5:4: error: + • Expected kind ‘* -> *’, but ‘f’ has kind ‘*’ + • In the associated type family declaration for ‘F’ |