Note [Ordering of implicit variables]
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 10 Jul 2018 22:03:09 +0000 (18:03 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 10 Jul 2018 23:54:53 +0000 (19:54 -0400)
This addresses #14808

[ci skip]

compiler/hsSyn/HsTypes.hs
compiler/rename/RnTypes.hs
compiler/typecheck/TcHsType.hs
compiler/types/TyCon.hs
compiler/types/Type.hs
docs/users_guide/glasgow_exts.rst

index cbaa9fb..8a1f33f 100644 (file)
@@ -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
index c8ddd0a..a9e02dc 100644 (file)
@@ -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] }
 
index 8373472..6039eea 100644 (file)
@@ -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) }
index 3801137..7836a02 100644 (file)
@@ -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
index 0833665..e96188f 100644 (file)
@@ -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 $
index 041cfb4..678f75c 100644 (file)
@@ -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