Commit 6e0e0b0e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only

Better comment on con_qvars in ConDecl
parent 29da01e0
...@@ -1155,9 +1155,9 @@ data ConDecl pass ...@@ -1155,9 +1155,9 @@ data ConDecl pass
, con_qvars :: Maybe (LHsQTyVars pass) , con_qvars :: Maybe (LHsQTyVars pass)
-- User-written forall (if any), and its implicit -- User-written forall (if any), and its implicit
-- kind variables -- kind variables
-- Non-Nothing needs -XExistentialQuantification -- Non-Nothing means an explicit user-written forall
-- e.g. data T a = forall b. MkT b (b->a) -- e.g. data T a = forall b. MkT b (b->a)
-- con_qvars = {b} -- con_qvars = {b}
, con_cxt :: Maybe (LHsContext pass) , con_cxt :: Maybe (LHsContext pass)
-- ^ User-written context (if any) -- ^ User-written context (if any)
......
...@@ -254,11 +254,16 @@ type LHsTyVarBndr pass = Located (HsTyVarBndr pass) ...@@ -254,11 +254,16 @@ type LHsTyVarBndr pass = Located (HsTyVarBndr pass)
-- | Located Haskell Quantified Type Variables -- | Located Haskell Quantified Type Variables
data LHsQTyVars pass -- See Note [HsType binders] data LHsQTyVars pass -- See Note [HsType binders]
= HsQTvs { hsq_implicit :: PostRn pass [Name] = HsQTvs { hsq_implicit :: PostRn pass [Name]
-- implicit (dependent) variables -- Implicit (dependent) variables
, hsq_explicit :: [LHsTyVarBndr pass] -- explicit variables
-- See Note [HsForAllTy tyvar binders] , hsq_explicit :: [LHsTyVarBndr pass]
-- Explicit variables, written by the user
-- See Note [HsForAllTy tyvar binders]
, hsq_dependent :: PostRn pass NameSet , hsq_dependent :: PostRn pass NameSet
-- which explicit vars are dependent -- Which members of hsq_explicit are dependent; that is,
-- mentioned in the kind of a later hsq_explicit,
-- or mentioned in a kind in the scope of this HsQTvs
-- See Note [Dependent LHsQTyVars] in TcHsType -- See Note [Dependent LHsQTyVars] in TcHsType
} }
......
...@@ -1290,14 +1290,38 @@ Note [Dependent LHsQTyVars] ...@@ -1290,14 +1290,38 @@ Note [Dependent LHsQTyVars]
We track (in the renamer) which explicitly bound variables in a We track (in the renamer) which explicitly bound variables in a
LHsQTyVars are manifestly dependent; only precisely these variables LHsQTyVars are manifestly dependent; only precisely these variables
may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs may be used within the LHsQTyVars. We must do this so that kcHsTyVarBndrs
can produce the right TyConBinders, and tell Anon vs. Named. Earlier, can produce the right TyConBinders, and tell Anon vs. Required.
I thought it would work simply to do a free-variable check during
kcHsTyVarBndrs, but this is bogus, because there may be unsolved Example data T k1 (a:k1) (b:k2) c
equalities about. And we don't want to eagerly solve the equalities, = MkT (Proxy a) (Proxy b) (Proxy c)
because we may get further information after kcHsTyVarBndrs is called.
(Recall that kcHsTyVarBndrs is usually called from getInitialKind. Here
The only other case is in kcConDecl.) This is what implements the rule (a:k1),(b:k2),(c:k3)
that all variables intended to be dependent must be manifestly so. 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 [TyVarBndrs, TyVarBinders, TyConBinders, and visiblity]
in TyCoRep.
kcHsTyVarBndrs 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 kcHsTyVarBndrs, 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
kcHsTyVarBndrs is called. (Recall that kcHsTyVarBndrs is usually
called from getInitialKind. The only other case is in kcConDecl.)
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) 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 as a degenerate case of some (pi (x :: t) -> s) and then this will
...@@ -1682,16 +1706,16 @@ Consider ...@@ -1682,16 +1706,16 @@ Consider
data T = MkT (forall (a :: k). Proxy a) data T = MkT (forall (a :: k). Proxy a)
-- from test ghci/scripts/T7873 -- from test ghci/scripts/T7873
This is not an existential datatype, but a higher-rank one. Note that This is not an existential datatype, but a higher-rank one (the forall
the forall to the right of MkT. Also consider to the right of MkT). Also consider
data S a = MkS (Proxy (a :: k)) data S a = MkS (Proxy (a :: k))
According to the rules around implicitly-bound kind variables, those According to the rules around implicitly-bound kind variables, in both
k's scope over the whole declarations. The renamer grabs it and adds it cases those k's scope over the whole declaration. The renamer grabs
to the hsq_implicits field of the HsQTyVars of the tycon. So it must it and adds it to the hsq_implicits field of the HsQTyVars of the
be in scope during type-checking, but we want to reject T while accepting tycon. So it must be in scope during type-checking, but we want to
S. reject T while accepting S.
Why reject T? Because the kind variable isn't fixed by anything. For Why reject T? Because the kind variable isn't fixed by anything. For
a variable like k to be implicit, it needs to be mentioned in the kind a variable like k to be implicit, it needs to be mentioned in the kind
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment