[commit: ghc] master: Note [Ordering of implicit variables] (7f4dd88)
git at git.haskell.org
git at git.haskell.org
Tue Jul 10 23:55:42 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab/ghc
>---------------------------------------------------------------
commit 7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date: Tue Jul 10 18:03:09 2018 -0400
Note [Ordering of implicit variables]
This addresses #14808
[ci skip]
>---------------------------------------------------------------
7f4dd888f12ec9a24cc2d7f60f214706bd33a1ab
compiler/hsSyn/HsTypes.hs | 33 +++++++++++++++++++++++++++++++++
compiler/rename/RnTypes.hs | 5 +++++
compiler/typecheck/TcHsType.hs | 2 ++
compiler/types/TyCon.hs | 2 +-
compiler/types/Type.hs | 5 +++++
docs/users_guide/glasgow_exts.rst | 29 +++++++++++++++++++++++++----
6 files changed, 71 insertions(+), 5 deletions(-)
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index cbaa9fb..8a1f33f 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -217,6 +217,37 @@ Note carefully:
* After type checking is done, we report what types the wildcards
got unified with.
+Note [Ordering of implicit variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Since the advent of -XTypeApplications, GHC makes promises about the ordering
+of implicit variable quantification. Specifically, we offer that implicitly
+quantified variables (such as those in const :: a -> b -> a, without a `forall`)
+will occur in left-to-right order of first occurrence. Here are a few examples:
+
+ const :: a -> b -> a -- forall a b. ...
+ f :: Eq a => b -> a -> a -- forall a b. ... contexts are included
+
+ type a <-< b = b -> a
+ g :: a <-< b -- forall a b. ... type synonyms matter
+
+ class Functor f where
+ fmap :: (a -> b) -> f a -> f b -- forall f a b. ...
+ -- The f is quantified by the class, so only a and b are considered in fmap
+
+This simple story is complicated by the possibility of dependency: all variables
+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.
+
+Implicitly bound variables are collected by extractHsTysRdrTyVars and friends
+in RnTypes. These functions thus promise to keep left-to-right ordering.
+Look for pointers to this note to see the places where the action happens.
+
-}
-- | Located Haskell Context
@@ -308,6 +339,8 @@ data HsImplicitBndrs pass thing -- See Note [HsType binders]
data HsIBRn
= HsIBRn { hsib_vars :: [Name] -- Implicitly-bound kind & type vars
+ -- Order is important; see
+ -- Note [Ordering of implicit variables]
, hsib_closed :: Bool -- Taking the hsib_vars into account,
-- is the payload closed? Used in
-- TcHsType.decideKindGeneralisationPlan
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index c8ddd0a..a9e02dc 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -340,6 +340,8 @@ rnImplicitBndrs bind_free_tvs
implicit_kind_vars_msg kvs
; loc <- getSrcSpanM
+ -- NB: kinds before tvs, as mandated by
+ -- Note [Ordering of implicit variables] in HsTypes
; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
; traceRn "checkMixedVars2" $
@@ -1558,6 +1560,9 @@ of the k in Proxy k being reported as out of scope.
-}
-- See Note [Kind and type-variable binders]
+-- These lists are guaranteed to preserve left-to-right ordering of
+-- the types the variables were extracted from. See also
+-- Note [Ordering of implicit variables] in HsTypes.
data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName]
, fktv_tys :: [Located RdrName] }
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 8373472..6039eea 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1839,6 +1839,8 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
-- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
+ -- do a stable topological sort, following
+ -- Note [Ordering of implicit variables] in HsTypes
; let final_tvs = toposortTyVars skol_tvs
; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
; return (final_tvs, result) }
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 3801137..7836a02 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -391,7 +391,7 @@ See also:
-}
type TyConBinder = TyVarBndr TyVar TyConBndrVis
- -- See also Note [TyBinder] in TyCoRep
+ -- See also Note [TyBinders] in TyCoRep
data TyConBndrVis
= NamedTCB ArgFlag
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 0833665..e96188f 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1815,6 +1815,11 @@ predTypeEqRel ty
--
-- This is a deterministic sorting operation
-- (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 HsTypes
toposortTyVars :: [TyCoVar] -> [TyCoVar]
toposortTyVars tvs = reverse $
[ node_payload node | node <- topologicalSortG $
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 041cfb4..678f75c 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10606,14 +10606,35 @@ Here are the details:
will have its type variables
ordered as ``m, a, b, c``.
+- If the type signature includes any kind annotations (either on variable
+ binders or as annotations on types), any variables used in kind
+ annotations come before any variables never used in kind annotations.
+ This rule is not recursive: if there is an annotation within an annotation,
+ then the variables used therein are on equal footing. Examples::
+
+ f :: Proxy (a :: k) -> Proxy (b :: j) -> ()
+ -- as if f :: forall k j a b. ...
+
+ g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> ()
+ -- as if g :: forall j k b a. ...
+ -- NB: k is in a kind annotation within a kind annotation
+
- If any of the variables depend on other variables (that is, if some
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.
-
- For example: if we have ``bar :: Proxy (a :: (j, k)) -> b``, then
- the variables are ordered ``j``, ``k``, ``a``, ``b``.
+ stable topological sort on the variables. Examples::
+
+ h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
+ -- as if h :: forall j k a b. ...
+
+ In this example, all of ``a``, ``j``, and ``k`` are considered kind
+ variables and will always be placed before ``b``, a lowly type variable.
+ (Note that ``a`` is used in ``b``\'s kind.) Yet, even though ``a`` appears
+ lexically before ``j`` and ``k``, ``j`` and ``k`` are quantified first,
+ because ``a`` depends on ``j`` and ``k``. Note further that ``j`` and ``k``
+ are not reordered with respect to eacho 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
More information about the ghc-commits
mailing list