From c8ecee5587d234f777e9d2d72211d0e972604504 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Tue, 26 Feb 2019 13:19:39 +0000 Subject: Wibbles in response to Richard --- compiler/typecheck/TcHsSyn.hs | 14 ++++--- compiler/typecheck/TcHsType.hs | 14 +++++-- compiler/typecheck/TcMType.hs | 64 ++++++++++++++-------------- compiler/typecheck/TcTyClsDecls.hs | 85 +++++++++++++++++++++++++++++++++----- compiler/types/TyCon.hs | 41 +++++++++++------- 5 files changed, 150 insertions(+), 68 deletions(-) diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index 74f6d86eec..d40b722b6b 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -34,7 +34,7 @@ module TcHsSyn ( zonkTopBndrs, ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv, zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX, - zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrsX, + zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs, zonkTcTypeToType, zonkTcTypeToTypeX, zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkTyVarOcc, @@ -459,13 +459,15 @@ zonkTyVarBinderX env (Bndr tv vis) = do { (env', tv') <- zonkTyBndrX env tv ; return (env', Bndr tv' vis) } -zonkRecTyVarBndrsX :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar]) -zonkRecTyVarBndrsX names tc_tvs +zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar]) +-- This rather specialised function is used in exactly one place. +-- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls. +zonkRecTyVarBndrs names tc_tvs = initZonkEnv $ \ ze -> - fixM $ \ ~(_, new_tvs) -> + fixM $ \ ~(_, rec_new_tvs) -> do { let ze' = extendTyZonkEnvN ze $ zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv)) - tc_tvs new_tvs + tc_tvs rec_new_tvs ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs ; return (ze', new_tvs) } where @@ -475,7 +477,7 @@ zonkRecTyVarBndrsX names tc_tvs vcat [ text "old:" <+> ppr tc_tv <+> dcolon <+> ppr (tyVarKind tc_tv) , text "new:" <+> ppr name <+> dcolon <+> ppr ki ] ; return (mkTyVar name ki) } - + zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc) zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 57623ba925..11cc61ceaf 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -1924,6 +1924,9 @@ kcLHsQTyVars_NonCusk name flav all_tv_prs = (kv_ns `zip` scoped_kvs) ++ (hsLTyVarNames hs_tvs `zip` tc_tvs) + -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification + -- variables, hence the need to zip here. Ditto bindExplicit.. + -- See TcMType Note [Unification variables get fresh Names] tycon = mkTcTyCon name tc_binders res_kind all_tv_prs False -- not yet generalised flav @@ -2085,7 +2088,7 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar newFlexiKindedTyVarTyVar :: Name -> TcM TyVar newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar - -- See Note [Unification variables should have fresh Names] in TcMType + -- See Note [Unification variables get fresh Names] in TcMType -------------------------------------- -- Explicit binders @@ -2127,6 +2130,8 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside -- Extend the environment as we go, in case a binder -- is mentioned in the kind of a later binder -- e.g. forall k (a::k). blah + -- NB: tv's Name may differ from hs_tv's + -- See TcMType Note [Unification variables get fresh Names] ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $ go hs_tvs ; return (tv:tvs, res) } @@ -2215,8 +2220,8 @@ kcLookupTcTyCon nm zonkAndScopedSort :: [TcTyVar] -> TcM [TcTyVar] zonkAndScopedSort spec_tkvs - = do { spec_tkvs <- mapM zonkTcTyCoVarBndr spec_tkvs - -- Use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv + = do { spec_tkvs <- mapM zonkAndSkolemise spec_tkvs + -- Use zonkAndSkolemise because a skol_tv might be a TyVarTv -- Do a stable topological sort, following -- Note [Ordering of implicit variables] in RnTypes @@ -2520,7 +2525,7 @@ tcHsPartialSigType ctxt sig_ty -- we need to promote the TyVarTvs so we don't violate the TcLevel -- invariant ; implicit_tvs <- zonkAndScopedSort implicit_tvs - ; explicit_tvs <- mapM zonkTcTyCoVarBndr explicit_tvs + ; explicit_tvs <- mapM zonkAndSkolemise explicit_tvs ; theta <- mapM zonkTcType theta ; tau <- zonkTcType tau @@ -2638,6 +2643,7 @@ tcHsPatSigType ctxt sig_ty RuleSigCtxt {} -> newSkolemTyVar name kind _ -> newTauTyVar name kind -- See Note [Pattern signature binders] + -- NB: tv's Name may be fresh (in the case of newTauTyVar) ; return (name, tv) } tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType" diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index d0af40e264..c641662689 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -70,9 +70,8 @@ module TcMType ( candidateQTyVarsOfType, candidateQTyVarsOfKind, candidateQTyVarsOfTypes, candidateQTyVarsOfKinds, CandidatesQTvs(..), delCandidates, candidateKindVars, - skolemiseQuantifiedTyVar, defaultTyVar, - quantifyTyVars, - zonkTcTyCoVarBndr, + zonkAndSkolemise, skolemiseQuantifiedTyVar, + defaultTyVar, quantifyTyVars, zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, @@ -681,28 +680,29 @@ cloneMetaTyVarName name At the moment we give a unification variable a System Name, which influences the way it is tidied; see TypeRep.tidyTyVarBndr. -Note [Unification variables should have fresh Names] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Unification variables get fresh Names] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Whenever we allocate a unification variable (MetaTyVar) we give it a fresh name. Trac #16221 is a very tricky case that illustrates why this is important: - data T0 a = forall k2 (b :: k2). MkT0 (T0 b) !Int + data SameKind :: k -> k -> * + data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl we allocate a unification variable kappa2 for k2, and then we -end up unifying kappa1 := kappa2 (because of the (T0 b). +end up unifying kappa1 := kappa2 (because of the (SameKind a b). Now we generalise over kappa2; but if kappa2's Name is k2, we'll end up giving T0 the kind forall k2. k2 -> *. Nothing -directly worng with that but when we typecheck the data constrautor +directly wrong with that but when we typecheck the data constrautor we end up giving it the type MkT0 :: forall k1 (a :: k1) k2 (b :: k2). - T0 @{k2} b -> Int -> T0 @{k2} a -which is boguus. The result type should be T0 @{k1} a. + SameKind @k2 a b -> Int -> T0 @{k2} a +which is bogus. The result type should be T0 @{k1} a. And there no reason /not/ to clone the Name when making a -unification variable. So taht's what we do. +unification variable. So that's what we do. -} newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar @@ -727,7 +727,7 @@ newSkolemTyVar name kind newTyVarTyVar :: Name -> Kind -> TcM TcTyVar -- See Note [TyVarTv] --- See Note [Unification variables should have fresh Names] +-- See Note [Unification variables get fresh Names] newTyVarTyVar name kind = do { details <- newMetaDetails TyVarTv ; name' <- cloneMetaTyVarName name @@ -1493,6 +1493,24 @@ quantifiableTv outer_tclvl tcv | otherwise = False +zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar +-- A tyvar binder is never a unification variable (TauTv), +-- rather it is always a skolem. It *might* be a TyVarTv. +-- (Because non-CUSK type declarations use TyVarTvs.) +-- Regardless, it may have a kind that has not yet been zonked, +-- and may include kind unification variables. +zonkAndSkolemise tyvar + | isTyVarTyVar 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_tyvar <- zonkTcTyVarToTyVar tyvar + ; skolemiseQuantifiedTyVar zonked_tyvar } + + | otherwise + = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar ) + zonkTyCoVarKind tyvar + skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables @@ -1994,28 +2012,6 @@ zonkTcType = mapType zonkTcTypeMapper () zonkCo :: Coercion -> TcM Coercion zonkCo = mapCoercion zonkTcTypeMapper () -zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar --- A tyvar binder is never a unification variable (TauTv), --- rather it is always a skolem. It *might* be a TyVarTv. --- (Because non-CUSK type declarations use TyVarTvs.) --- Regardless, it may have a kind that has not yet been zonked, --- and may include kind unification variables. -zonkTcTyCoVarBndr tyvar - | isTyVarTyVar 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_tyvar <- zonkTcTyVarToTyVar 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) } - ; skolemiseQuantifiedTyVar zonked_tyvar } - - | otherwise - = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar ) - zonkTyCoVarKind tyvar - zonkTcTyVar :: TcTyVar -> TcM TcType -- Simply look through all Flexis zonkTcTyVar tv diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index a2f2bc9442..ff8b3437a3 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -552,7 +552,7 @@ generaliseTcTyCon tc -- Step 0: zonk and skolemise the Specified and Required binders -- It's essential that they are skolems, not MetaTyVars, -- for Step 3 to work right - ; spec_req_tvs <- mapM zonkTcTyCoVarBndr spec_req_tvs + ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs -- Running example, where kk1 := kk2, so we get -- Step 1: find all the variables we want to quantify over, @@ -575,7 +575,7 @@ generaliseTcTyCon tc ; traceTc "generaliseTcTyCon: before zonkRec" (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs , text "inferred =" <+> pprTyVars inferred ]) - ; (ze, spec_req_tvs) <- zonkRecTyVarBndrsX spec_req_names spec_req_tvs + ; (ze, spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs -- So ze maps from the tyvars that have ended up -- @@ -583,7 +583,7 @@ generaliseTcTyCon tc -- (remember they all started as TyVarTvs). -- They have been skolemised by quantifyTyVars. ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind - + ; traceTc "generaliseTcTyCon: post zonk" $ vcat [ text "tycon =" <+> ppr tc , text "inferred =" <+> pprTyVars inferred @@ -594,6 +594,7 @@ generaliseTcTyCon tc -- Step 4: Find the Specified and Inferred variables -- NB: spec_req_tvs = spec_tvs ++ req_tvs -- And req_tvs is 1-1 with tyConTyVars + -- See Note [Scoped tyvars in a TcTyCon] in TyCon ; let n_spec = length spec_req_tvs - tyConArity tc (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs specified = scopedSort spec_tvs @@ -786,12 +787,30 @@ that do not have a CUSK. Consider We do kind inference as follows: * Step 1: getInitialKinds, and in particular kcLHsQTyVars_NonCusk. + Make a unification variable for each of the Required and Specified + type varialbes in the header. + + Record the connection between the Names the user wrote and the + fresh unification variables in the tcTyConScopedTyVars field + of the TcTyCon we are making + [ (a, aa) + , (k1, kk1) + , (k2, kk2) + , (x, xx) ] + (I'm using the convention that double letter like 'aa' or 'kk' + mean a unification variable.) + + These unification variables + - Are TyVarTvs: that is, unification variables that can + unify only with other type variables. + See Note [Signature skolems] in TcType + + - Have complete fresh Names; see TcMType + Note [Unification variables get fresh Names] + Assign initial monomorophic kinds to S, T S :: kk1 -> * -> kk2 -> * T :: kk3 -> * -> kk4 -> * - Here kk1 etc are TyVarTvs: that is, unification variables that - are allowed to unify only with other type variables. See - Note [Signature skolems] in TcType * Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and T, with these monomophic kinds. Now kind-check the declarations, @@ -809,18 +828,20 @@ We do kind inference as follows: Note [Required, Specified, and Inferred for types]), and perform some validity checks. - This makes the utterly-final TyConBinders for the TyCon + This makes the utterly-final TyConBinders for the TyCon. All this is very similar at the level of terms: see TcBinds Note [Quantified variables in partial type signatures] + But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon] + * Step 4. Extend the type environment with a TcTyCon for S and T, now with their utterly-final polymorphic kinds (needed for recursive occurrences of S, T). Now typecheck the declarations, and build the final AlgTyCOn for S and T resp. -The first three steps are in kcTyClGroup; -the fourth is in tcTyClDecls. +The first three steps are in kcTyClGroup; the fourth is in +tcTyClDecls. There are some wrinkles @@ -859,7 +880,51 @@ There are some wrinkles a) when collecting quantification candidates, in candidateQTyVarsOfKind, we must collect skolems b) quantifyTyVars should be a no-op on such a skolem --} + +Note [Tricky scoping in generaliseTcTyCon] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider Trac #16342 + class C (a::ka) x where + cop :: D a x => x -> Proxy a -> Proxy a + cop _ x = x :: Proxy (a::ka) + + class D (b::kb) y where + dop :: C b y => y -> Proxy b -> Proxy b + dop _ x = x :: Proxy (b::kb) + +C and D are mutually recursive, by the time we get to +generaliseTcTyCon we'll have unified kka := kkb. + +But when typechecking the default declarations for 'cop' and 'dop' in +tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope. +But at that point all we have is the utterly-final Class itself. + +Conclusion: the classTyVars of a class must have the same Mame as +that originally assigned by the user. In our example, C must have +classTyVars {a, ka, x} while D has classTyVars {a, kb, y}. Despite +the fact that kka and kkb got unified! + +We achieve this sleight of hand in generaliseTcTyCon, using +the specialised function zonkRecTyVarBndrs. We make the call + zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx] +where the [ka,a,x] are the Names originally assigned by the user, and +[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars. +zonkRecTyVarBndrs builds a recursive ZonkEnv that binds + kkb :-> (ka :: ) + aa :-> (a :: ) + etc +That is, it maps each skolemised TcTyVars to the utterly-final +TyVar to put in the class, with its correct user-specified name. +When generalising D we'll do the same thing, but the ZonkEnv will map + kkb :-> (kb :: ) + bb :-> (b :: ) + etc +Note that 'kkb' again appears in the domain of the mapping, but this +time mapped to 'kb'. That's how C and D end up with differently-named +final TyVars despite the fact that we unified kka:=kkb + +zonkRecTyVarBndrs we need to do knot-tying because of the need to +apply this same substitution to the kind of each. -} -------------- tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 571ceeb309..ce40d74278 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -871,29 +871,42 @@ data TyCon -- See Note [The binders/kind/arity fields of a TyCon] tyConBinders :: [TyConBinder], -- ^ Full binders - tyConTyVars :: [TyVar], -- ^ TyVar binders - tyConResKind :: Kind, -- ^ Result kind - tyConKind :: Kind, -- ^ Kind of this TyCon - tyConArity :: Arity, -- ^ Arity + tyConTyVars :: [TyVar], -- ^ TyVar binders + tyConResKind :: Kind, -- ^ Result kind + tyConKind :: Kind, -- ^ Kind of this TyCon + tyConArity :: Arity, -- ^ Arity + + -- NB: the TyConArity of a TcTyCon must match + -- the number of Required (positional, user-specified) + -- arguments to the type constructor; see the use + -- of tyConArity in generaliseTcTyCon tcTyConScopedTyVars :: [(Name,TyVar)], -- ^ Scoped tyvars over the tycon's body - -- See Note [How TcTyCons work] in TcTyClsDecls - -- - -- This list is specified_tvs ++ required_tvs - -- where required_tvs teh same as tyConTyVars - -- - -- 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. + -- See Note [Scoped tyvars in a TcTyCon] tcTyConIsPoly :: Bool, -- ^ Is this TcTyCon already generalized? tcTyConFlavour :: TyConFlavour -- ^ What sort of 'TyCon' this represents. } +{- Note [Scoped tyvars in a TcTyCon] + +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The tcTyConScopedTyVars field records the lexicial-binding connection +between the original, user-specified Name (i.e. thing in scope) and +the TcTyVar that the Name is bound to. + +Order *does* matter; the tcTyConScopedTyvars list consists of + specified_tvs ++ required_tvs + +where + * specified ones first + * required_tvs the same as tyConTyVars + * tyConArity = length required_tvs + +See also Note [How TcTyCons work] in TcTyClsDecls +-} -- | Represents right-hand-sides of 'TyCon's for algebraic types data AlgTyConRhs -- cgit v1.2.1