Commit 5e45ad10 authored by Tobias Dammers's avatar Tobias Dammers 🦈 Committed by Richard Eisenberg
Browse files

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
parent e8a652f6
...@@ -405,6 +405,23 @@ sameVis Required _ = False ...@@ -405,6 +405,23 @@ sameVis Required _ = False
sameVis _ Required = False sameVis _ Required = False
sameVis _ _ = True 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 * VarBndr, TyCoVarBinder
...@@ -469,6 +486,19 @@ mkTyVarBinders vis = map (mkTyVarBinder vis) ...@@ -469,6 +486,19 @@ mkTyVarBinders vis = map (mkTyVarBinder vis)
isTyVarBinder :: TyCoVarBinder -> Bool isTyVarBinder :: TyCoVarBinder -> Bool
isTyVarBinder (Bndr v _) = isTyVar v 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 ( ...@@ -524,35 +554,6 @@ tcTyVarDetails var = pprPanic "tcTyVarDetails" (ppr var <+> dcolon <+> pprKind (
setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar setTcTyVarDetails :: TyVar -> TcTyVarDetails -> TyVar
setTcTyVarDetails tv details = tv { tc_tv_details = details } 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
{- {-
%************************************************************************ %************************************************************************
%* * %* *
......
...@@ -237,6 +237,7 @@ unitDVarSet = unitUniqDSet ...@@ -237,6 +237,7 @@ unitDVarSet = unitUniqDSet
mkDVarSet :: [Var] -> DVarSet mkDVarSet :: [Var] -> DVarSet
mkDVarSet = mkUniqDSet mkDVarSet = mkUniqDSet
-- The new element always goes to the right of existing ones.
extendDVarSet :: DVarSet -> Var -> DVarSet extendDVarSet :: DVarSet -> Var -> DVarSet
extendDVarSet = addOneToUniqDSet extendDVarSet = addOneToUniqDSet
......
...@@ -101,7 +101,7 @@ sortQuantVars :: [Var] -> [Var] ...@@ -101,7 +101,7 @@ sortQuantVars :: [Var] -> [Var]
sortQuantVars vs = sorted_tcvs ++ ids sortQuantVars vs = sorted_tcvs ++ ids
where where
(tcvs, ids) = partition (isTyVar <||> isCoVar) vs (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 -- | Bind a binding group over an expression, using a @let@ or @case@ as
-- appropriate (see "CoreSyn#let_app_invariant") -- appropriate (see "CoreSyn#let_app_invariant")
......
...@@ -862,7 +862,7 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs ...@@ -862,7 +862,7 @@ decomposeRuleLhs dflags orig_bndrs orig_lhs
-- Add extra tyvar binders: Note [Free tyvars in rule LHS] -- Add extra tyvar binders: Note [Free tyvars in rule LHS]
-- and extra dict binders: Note [Free dictionaries in rule LHS] -- and extra dict binders: Note [Free dictionaries in rule LHS]
mk_extra_bndrs fn_id args mk_extra_bndrs fn_id args
= toposortTyVars unbound_tvs ++ unbound_dicts = scopedSort unbound_tvs ++ unbound_dicts
where where
unbound_tvs = [ v | v <- unbound_vars, isTyVar v ] unbound_tvs = [ v | v <- unbound_vars, isTyVar v ]
unbound_dicts = [ mkLocalId (localiseName (idName d)) (idType d) unbound_dicts = [ mkLocalId (localiseName (idName d)) (idType d)
......
...@@ -2015,8 +2015,8 @@ tyThingParent_maybe (AConLike cl) = case cl of ...@@ -2015,8 +2015,8 @@ tyThingParent_maybe (AConLike cl) = case cl of
RealDataCon dc -> Just (ATyCon (dataConTyCon dc)) RealDataCon dc -> Just (ATyCon (dataConTyCon dc))
PatSynCon{} -> Nothing PatSynCon{} -> Nothing
tyThingParent_maybe (ATyCon tc) = case tyConAssoc_maybe tc of tyThingParent_maybe (ATyCon tc) = case tyConAssoc_maybe tc of
Just cls -> Just (ATyCon (classTyCon cls)) Just tc -> Just (ATyCon tc)
Nothing -> Nothing Nothing -> Nothing
tyThingParent_maybe (AnId id) = case idDetails id of tyThingParent_maybe (AnId id) = case idDetails id of
RecSelId { sel_tycon = RecSelData tc } -> RecSelId { sel_tycon = RecSelData tc } ->
Just (ATyCon tc) Just (ATyCon tc)
......
...@@ -14,6 +14,8 @@ mkBoxedTupleTy :: [Type] -> Type ...@@ -14,6 +14,8 @@ mkBoxedTupleTy :: [Type] -> Type
coercibleTyCon, heqTyCon :: TyCon coercibleTyCon, heqTyCon :: TyCon
unitTy :: Type
liftedTypeKind :: Kind liftedTypeKind :: Kind
constraintKind :: Kind constraintKind :: Kind
......
...@@ -827,7 +827,7 @@ bindHsQTyVars :: forall a b. ...@@ -827,7 +827,7 @@ bindHsQTyVars :: forall a b.
-> (LHsQTyVars GhcRn -> Bool -> RnM (b, FreeVars)) -> (LHsQTyVars GhcRn -> Bool -> RnM (b, FreeVars))
-- The Bool is True <=> all kind variables used in the -- The Bool is True <=> all kind variables used in the
-- kind signature are bound on the left. Reason: -- 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 -- kind signatures] in HsDecls
-> RnM (b, FreeVars) -> RnM (b, FreeVars)
...@@ -840,7 +840,6 @@ bindHsQTyVars :: forall a b. ...@@ -840,7 +840,6 @@ bindHsQTyVars :: forall a b.
bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
= do { let hs_tv_bndrs = hsQTvExplicit hsq_bndrs = do { let hs_tv_bndrs = hsQTvExplicit hsq_bndrs
bndr_kv_occs = extractHsTyVarBndrsKVs hs_tv_bndrs bndr_kv_occs = extractHsTyVarBndrsKVs hs_tv_bndrs
; rdr_env <- getLocalRdrEnv
; let -- See Note [bindHsQTyVars examples] for what ; let -- See Note [bindHsQTyVars examples] for what
-- all these various things are doing -- all these various things are doing
...@@ -850,8 +849,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside ...@@ -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 -- Make sure to list the binder kvs before the
-- body kvs, as mandated by -- body kvs, as mandated by
-- Note [Ordering of implicit variables] -- Note [Ordering of implicit variables]
implicit_kvs = filter_occs rdr_env bndrs kv_occs implicit_kvs = filter_occs bndrs kv_occs
-- Deleting bndrs: See Note [Kind-variable ordering]
-- dep_bndrs is the subset of bndrs that are dependent -- dep_bndrs is the subset of bndrs that are dependent
-- i.e. appear in bndr/body_kv_occs -- i.e. appear in bndr/body_kv_occs
-- Can't use implicit_kvs because we've deleted bndrs from that! -- 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 ...@@ -879,17 +877,15 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
all_bound_on_lhs } } all_bound_on_lhs } }
where where
filter_occs :: LocalRdrEnv -- In scope filter_occs :: [Located RdrName] -- Bound here
-> [Located RdrName] -- Bound here
-> [Located RdrName] -- Potential implicit binders -> [Located RdrName] -- Potential implicit binders
-> [Located RdrName] -- Final implicit binders -> [Located RdrName] -- Final implicit binders
-- Filter out any potential implicit binders that are either -- Filter out any potential implicit binders that are either
-- already in scope, or are explicitly bound here -- already in scope, or are explicitly bound in the same HsQTyVars
filter_occs rdr_env bndrs occs filter_occs bndrs occs
= filterOut is_in_scope occs = filterOut is_in_scope occs
where where
is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ) is_in_scope locc = locc `elemRdr` bndrs
|| locc `elemRdr` bndrs
{- Note [bindHsQTyVars examples] {- Note [bindHsQTyVars examples]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
...@@ -1586,9 +1582,8 @@ must come after any variables mentioned in their kinds. ...@@ -1586,9 +1582,8 @@ must come after any variables mentioned in their kinds.
typeRep :: Typeable a => TypeRep (a :: k) -- forall k a. ... 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 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. the a in the code. Thus, GHC does ScopedSort on the variables.
By "stable", we mean that any two variables who do not depend on each other See Note [ScopedSort] in Type.
preserve their existing left-to-right ordering.
Implicitly bound variables are collected by any function which returns a Implicitly bound variables are collected by any function which returns a
FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably
......
...@@ -87,8 +87,7 @@ import Literal ( litIsTrivial ) ...@@ -87,8 +87,7 @@ import Literal ( litIsTrivial )
import Demand ( StrictSig, Demand, isStrictDmd, splitStrictSig, increaseStrictSigArity ) import Demand ( StrictSig, Demand, isStrictDmd, splitStrictSig, increaseStrictSigArity )
import Name ( getOccName, mkSystemVarName ) import Name ( getOccName, mkSystemVarName )
import OccName ( occNameString ) import OccName ( occNameString )
import Type ( Type, mkLamTypes, splitTyConApp_maybe, tyCoVarsOfType ) import Type ( Type, mkLamTypes, splitTyConApp_maybe, tyCoVarsOfType, closeOverKindsDSet )
import TyCoRep ( closeOverKindsDSet )
import BasicTypes ( Arity, RecFlag(..), isRec ) import BasicTypes ( Arity, RecFlag(..), isRec )
import DataCon ( dataConOrigResTy ) import DataCon ( dataConOrigResTy )
import TysWiredIn import TysWiredIn
......
...@@ -1763,7 +1763,7 @@ abstractFloats dflags top_lvl main_tvs floats body ...@@ -1763,7 +1763,7 @@ abstractFloats dflags top_lvl main_tvs floats body
rhs' = CoreSubst.substExpr (text "abstract_floats2") subst rhs rhs' = CoreSubst.substExpr (text "abstract_floats2") subst rhs
-- tvs_here: see Note [Which type variables to abstract over] -- tvs_here: see Note [Which type variables to abstract over]
tvs_here = toposortTyVars $ tvs_here = scopedSort $
filter (`elemVarSet` main_tv_set) $ filter (`elemVarSet` main_tv_set) $
closeOverKindsList $ closeOverKindsList $
exprSomeFreeVarsList isTyVar rhs' exprSomeFreeVarsList isTyVar rhs'
...@@ -1791,7 +1791,7 @@ abstractFloats dflags top_lvl main_tvs floats body ...@@ -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: -- If you ever want to be more selective, remember this bizarre case too:
-- x::a = x -- x::a = x
-- Here, we must abstract 'x' over 'a'. -- 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 :: [TyVar] -> Id -> SimplM (Id, CoreExpr)
mk_poly1 tvs_here var mk_poly1 tvs_here var
......
...@@ -2091,7 +2091,7 @@ callToPats env bndr_occs call@(Call _ args con_env) ...@@ -2091,7 +2091,7 @@ callToPats env bndr_occs call@(Call _ args con_env)
-- See Note [Shadowing] at the top -- See Note [Shadowing] at the top
(ktvs, ids) = partition isTyVar qvars (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 -- Order into kind variables, type variables, term variables
-- The kind of a type variable may mention a kind variable -- The kind of a type variable may mention a kind variable
-- and the type of a term variable may mention a type variable -- and the type of a term variable may mention a type variable
......
...@@ -168,7 +168,13 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) ...@@ -168,7 +168,13 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
-- Note [Linting type synonym applications]. -- Note [Linting type synonym applications].
case lintTypes dflags tcvs' (rhs':lhs') of case lintTypes dflags tcvs' (rhs':lhs') of
Nothing -> pure () 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 ; return (FamInst { fi_fam = tyConName fam_tc
, fi_flavor = flavor , fi_flavor = flavor
, fi_tcs = roughMatchTcs lhs , fi_tcs = roughMatchTcs lhs
...@@ -893,7 +899,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn ...@@ -893,7 +899,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
has_kinds = not $ isEmptyVarSet invis_vars has_kinds = not $ isEmptyVarSet invis_vars
doc = sep [ what <+> text "variable" <> 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." ] , text "cannot be inferred from the right-hand side." ]
what = case (has_types, has_kinds) of what = case (has_types, has_kinds) of
(True, True) -> text "Type and kind" (True, True) -> text "Type and kind"
......
...@@ -514,8 +514,8 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs) ...@@ -514,8 +514,8 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs)
rhs' = substTyUnchecked subst' rhs_ty rhs' = substTyUnchecked subst' rhs_ty
tcv' = tyCoVarsOfTypesList pat_tys' tcv' = tyCoVarsOfTypesList pat_tys'
(tv', cv') = partition isTyVar tcv' (tv', cv') = partition isTyVar tcv'
tvs' = toposortTyVars tv' tvs' = scopedSort tv'
cvs' = toposortTyVars cv' cvs' = scopedSort cv'
; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys' ; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys'
; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' cvs' ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' cvs'
fam_tc pat_tys' rhs' fam_tc pat_tys' rhs'
......
...@@ -815,7 +815,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred ...@@ -815,7 +815,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
final_tkvs = tyCoVarsOfTypesWellScoped $ final_tkvs = tyCoVarsOfTypesWellScoped $
final_cls_tys ++ final_tc_args final_cls_tys ++ final_tc_args
; let tkvs = toposortTyVars $ fvVarList $ ; let tkvs = scopedSort $ fvVarList $
unionFV (tyCoFVsOfTypes tc_args_to_keep) unionFV (tyCoFVsOfTypes tc_args_to_keep)
(FV.mkFVs deriv_tvs) (FV.mkFVs deriv_tvs)
Just kind_subst = mb_match Just kind_subst = mb_match
......
...@@ -485,7 +485,7 @@ reportBadTelescope ctxt env (Just telescope) skols ...@@ -485,7 +485,7 @@ reportBadTelescope ctxt env (Just telescope) skols
text "are out of dependency order. Perhaps try this ordering:") text "are out of dependency order. Perhaps try this ordering:")
2 (pprTyVars sorted_tvs) 2 (pprTyVars sorted_tvs)
sorted_tvs = toposortTyVars skols sorted_tvs = scopedSort skols
reportBadTelescope _ _ Nothing skols reportBadTelescope _ _ Nothing skols
= pprPanic "reportBadTelescope" (ppr skols) = pprPanic "reportBadTelescope" (ppr skols)
......
...@@ -1840,8 +1840,8 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty ...@@ -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_rhs_ty = mkTyConApp fam_tc rep_rhs_tys
rep_tcvs = tyCoVarsOfTypesList rep_lhs_tys rep_tcvs = tyCoVarsOfTypesList rep_lhs_tys
(rep_tvs, rep_cvs) = partition isTyVar rep_tcvs (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs
rep_tvs' = toposortTyVars rep_tvs rep_tvs' = scopedSort rep_tvs
rep_cvs' = toposortTyVars rep_cvs rep_cvs' = scopedSort rep_cvs
pp_lhs = ppr (mkTyConApp fam_tc rep_lhs_tys) pp_lhs = ppr (mkTyConApp fam_tc rep_lhs_tys)
-- Same as inst_tys, but with the last argument type replaced by the -- Same as inst_tys, but with the last argument type replaced by the
......
...@@ -434,8 +434,8 @@ tc_mkRepFamInsts gk tycon inst_tys = ...@@ -434,8 +434,8 @@ tc_mkRepFamInsts gk tycon inst_tys =
repTy' = substTy subst repTy repTy' = substTy subst repTy
tcv' = tyCoVarsOfTypeList inst_ty tcv' = tyCoVarsOfTypeList inst_ty
(tv', cv') = partition isTyVar tcv' (tv', cv') = partition isTyVar tcv'
tvs' = toposortTyVars tv' tvs' = scopedSort tv'
cvs' = toposortTyVars cv' cvs' = scopedSort cv'
axiom = mkSingleCoAxiom Nominal rep_name tvs' cvs' axiom = mkSingleCoAxiom Nominal rep_name tvs' cvs'
fam_tc inst_tys repTy' fam_tc inst_tys repTy'
......
...@@ -423,7 +423,7 @@ zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar) ...@@ -423,7 +423,7 @@ zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar)
-- This guarantees to return a TyVar (not a TcTyVar) -- This guarantees to return a TyVar (not a TcTyVar)
-- then we add it to the envt, so all occurrences are replaced -- then we add it to the envt, so all occurrences are replaced
zonkTyBndrX env tv zonkTyBndrX env tv
= ASSERT( isImmutableTyVar tv ) = ASSERT2( isImmutableTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) )
do { ki <- zonkTcTypeToTypeX env (tyVarKind tv) do { ki <- zonkTcTypeToTypeX env (tyVarKind tv)
-- Internal names tidy up better, for iface files. -- Internal names tidy up better, for iface files.
; let tv' = mkTyVar (tyVarName tv) ki ; let tv' = mkTyVar (tyVarName tv) ki
......
...@@ -53,7 +53,10 @@ module TcHsType ( ...@@ -53,7 +53,10 @@ module TcHsType (
zonkPromoteType, zonkPromoteType,
-- Pattern type signatures -- Pattern type signatures
tcHsPatSigType, tcPatSig, funAppCtxt tcHsPatSigType, tcPatSig,
-- Error messages
funAppCtxt, addTyConFlavCtxt
) where ) where
#include "HsVersions.h" #include "HsVersions.h"
...@@ -1368,7 +1371,7 @@ as a degenerate case of some (pi (x :: t) -> s) and then this will ...@@ -1368,7 +1371,7 @@ as a degenerate case of some (pi (x :: t) -> s) and then this will
all get more permissive. all get more permissive.
Note [Kind generalisation and TyVarTvs] Note [Kind generalisation and TyVarTvs]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider Consider
data T (a :: k1) x = MkT (S a ()) data T (a :: k1) x = MkT (S a ())
data S (b :: k2) y = MkS (T b ()) data S (b :: k2) y = MkS (T b ())
...@@ -1383,7 +1386,7 @@ in TcBinds. ...@@ -1383,7 +1386,7 @@ in TcBinds.
There are some wrinkles There are some wrinkles
* We always want to kind-generalise over TyVarTvs, and /not/ default * 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 stand for a type, even via defaulting. Hence the check in
TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's
another example (Trac #14555): another example (Trac #14555):
...@@ -1396,12 +1399,22 @@ There are some wrinkles ...@@ -1396,12 +1399,22 @@ There are some wrinkles
data SameKind :: k -> k -> * data SameKind :: k -> k -> *
data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) 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, 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 as we do with partial type signatures in mk_psig_qtvs in
TcBinds.chooseInferredQuantifiers 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] Note [Keeping scoped variables in order: Explicit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user writes `forall a b c. blah`, we bring a, b, and c into 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. ...@@ -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, This is done by bumping the TcLevel, bringing the tyvars into scope,
and then type-checking the thing_inside. The constraints are all and then type-checking the thing_inside. The constraints are all
wrapped in an implication, which is then solved. Finally, we can 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 It's critical to solve before zonking and ordering in order to uncover
any unifications. You might worry that this eager solving could cause 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 ...@@ -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: in the surrounding context, we must obey the following dictum:
Every metavariable in a type must either be Every metavariable in a type must either be
(A) promoted, or (A) promoted
(B) generalized. (B) generalized, or
(C) zapped to Any
If a variable is generalized, then it becomes a skolem and no longer 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 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) ...@@ -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] we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables]
in TcType. in TcType.
For more about (C), see Note [Naughty quantification candidates] in TcMType.
After promoting/generalizing, we need to zonk *again* because both After promoting/generalizing, we need to zonk *again* because both
promoting and generalizing fill in metavariables. promoting and generalizing fill in metavariables.
...@@ -1514,69 +1530,93 @@ tcWildCardBinders wc_names thing_inside ...@@ -1514,69 +1530,93 @@ tcWildCardBinders wc_names thing_inside
kcLHsQTyVars :: Name -- ^ of the thing being checked kcLHsQTyVars :: Name -- ^ of the thing being checked
-> TyConFlavour -- ^ What sort of 'TyCon' is being checked -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
-> Bool -- ^ True <=> the decl being checked has a CUSK -> 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 -> LHsQTyVars GhcRn
-> TcM Kind -- ^ The result kind -> TcM Kind -- ^ The result kind
-> TcM TcTyCon -- ^ A suitably-kinded TcTyCon -> 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 user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
, hsq_dependent = dep_names } , hsq_dependent = dep_names }
, hsq_explicit = hs_tvs }) thing_inside , hsq_explicit = hs_tvs }) thing_inside
| cusk | 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 $ <- solveEqualities $
tcImplicitQTKBndrs skol_info kv_ns $ tcImplicitQTKBndrs skol_info kv_ns $
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
-- Now, because we're in a CUSK, quantify over the mentioned ; let class_tc_binders
-- kind vars, in dependency order. | Just class_tc <- tyConFlavourAssoc_maybe flav
; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs = tyConBinders class_tc -- class has a CUSK, so these are zonked