diff options
Diffstat (limited to 'compiler/typecheck/TcHsType.hs')
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 116 |
1 files changed, 57 insertions, 59 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index b3c40274c4..0357c1046d 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -91,7 +91,7 @@ import ConLike import DataCon import Class import Name -import NameSet +-- import NameSet import VarEnv import TysWiredIn import BasicTypes @@ -1611,48 +1611,6 @@ addTypeCtxt (L _ ty) thing %* * %************************************************************************ -Note [Dependent LHsQTyVars] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We track (in the renamer) which explicitly bound variables in a -LHsQTyVars are manifestly dependent; only precisely these variables -may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars -can produce the right TyConBinders, and tell Anon vs. Required. - -Example data T k1 (a:k1) (b:k2) c - = MkT (Proxy a) (Proxy b) (Proxy c) - -Here - (a:k1),(b:k2),(c:k3) - are Anon (explicitly specified as a binder, not used - in the kind of any other binder - k1 is Required (explicitly specifed as a binder, but used - in the kind of another binder i.e. dependently) - k2 is Specified (not explicitly bound, but used in the kind - of another binder) - k3 in Inferred (not lexically in scope at all, but inferred - by kind inference) -and - T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> * - -See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] -in TyCoRep. - -kcLHsQTyVars uses the hsq_dependent field to decide whether -k1, a, b, c should be Required or Anon. - -Earlier, thought it would work simply to do a free-variable check -during kcLHsQTyVars, but this is bogus, because there may be -unsolved equalities about. And we don't want to eagerly solve the -equalities, because we may get further information after -kcLHsQTyVars is called. (Recall that kcLHsQTyVars is called -only from getInitialKind.) -This is what implements the rule that all variables intended to be -dependent must be manifestly so. - -Sidenote: It's quite possible that later, we'll consider (t -> s) -as a degenerate case of some (pi (x :: t) -> s) and then this will -all get more permissive. - Note [Keeping scoped variables in order: Explicit] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When the user writes `forall a b c. blah`, we bring a, b, and c into @@ -1822,8 +1780,7 @@ kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk ------------------------------ kcLHsQTyVars_Cusk name flav - (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns - , hsq_dependent = dep_names } + (HsQTvs { hsq_ext = kv_ns , hsq_explicit = hs_tvs }) thing_inside -- CUSK case -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls @@ -1874,7 +1831,6 @@ kcLHsQTyVars_Cusk name flav vcat [ text "name" <+> ppr name , text "kv_ns" <+> ppr kv_ns , text "hs_tvs" <+> ppr hs_tvs - , text "dep_names" <+> ppr dep_names , text "scoped_kvs" <+> ppr scoped_kvs , text "tc_tvs" <+> ppr tc_tvs , text "res_kind" <+> ppr res_kind @@ -1895,8 +1851,7 @@ kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" ------------------------------ kcLHsQTyVars_NonCusk name flav - (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns - , hsq_dependent = dep_names } + (HsQTvs { hsq_ext = kv_ns , hsq_explicit = hs_tvs }) thing_inside -- Non_CUSK case -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls @@ -1913,22 +1868,26 @@ kcLHsQTyVars_NonCusk name flav -- might unify with kind vars in other types in a mutually -- recursive group. -- See Note [Inferring kinds for type declarations] in TcTyClsDecls - tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs + + tc_binders = mkAnonTyConBinders VisArg 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 + -- + -- mkAnonTyConBinder: see Note [No polymorphic recursion] 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 need fresh Names] + tycon = mkTcTyCon name tc_binders res_kind all_tv_prs False -- not yet generalised flav ; traceTc "kcLHsQTyVars: not-cusk" $ - vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names + vcat [ ppr name, ppr kv_ns, ppr hs_tvs , ppr scoped_kvs , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] ; return tycon } @@ -1936,18 +1895,57 @@ kcLHsQTyVars_NonCusk name flav ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind | otherwise = AnyKind - mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder - -- See Note [Dependent LHsQTyVars] - mk_tc_binder hs_tv tv - | hsLTyVarName hs_tv `elemNameSet` dep_names - = mkNamedTyConBinder Required tv - | otherwise - = mkAnonTyConBinder VisArg tv - kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" -{- Note [Kind-checking tyvar binders for associated types] +{- Note [No polymorphic recursion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Should this kind-check? + data T ka (a::ka) b = MkT (T Type Int Bool) + (T (Type -> Type) Maybe Bool) + +Notice that T is used at two different kinds in its RHS. No! +This should not kind-check. Polymorphic recursion is known to +be a tough nut. + +Previously, we laboriously (with help from the renamer) +tried to give T the polymoprhic kind + T :: forall ka -> ka -> kappa -> Type +where kappa is a unification variable, even in the getInitialKinds +phase (which is what kcLHsQTyVars_NonCusk is all about). But +that is dangerously fragile (see the ticket). + +Solution: make kcLHsQTyVars_NonCusk give T a straightforward +monomorphic kind, with no quantification whatsoever. That's why +we use mkAnonTyConBinder for all arguments when figuring out +tc_binders. + +But notice that (Trac #16322 comment:3) + +* The algorithm successfully kind-checks this declaration: + data T2 ka (a::ka) = MkT2 (T2 Type a) + + Starting with (getInitialKinds) + T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> * + we get + kappa4 := kappa1 -- from the (a:ka) kind signature + kappa1 := Type -- From application T2 Type + + These constraints are soluble so generaliseTcTyCon gives + T2 :: forall (k::Type) -> k -> * + + But now the /typechecking/ (aka desugaring, tcTyClDecl) phase + fails, because the call (T2 Type a) in the RHS is ill-kinded. + + We'd really prefer all errors to show up in the kind checking + phase. + +* This algorithm still accepts (in all phases) + data T3 ka (a::ka) = forall b. MkT3 (T3 Type b) + although T3 is really polymorphic-recursive too. + Perhaps we should somehow reject that. + +Note [Kind-checking tyvar binders for associated types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When kind-checking the type-variable binders for associated data/newtype decls |