summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/hsSyn/HsTypes.hs17
-rw-r--r--compiler/rename/RnTypes.hs86
-rw-r--r--compiler/typecheck/TcHsType.hs2
-rw-r--r--compiler/types/Type.hs2
-rw-r--r--docs/users_guide/glasgow_exts.rst11
-rw-r--r--testsuite/tests/ghci/scripts/T15568.hs7
-rw-r--r--testsuite/tests/ghci/scripts/T15568.script4
-rw-r--r--testsuite/tests/ghci/scripts/T15568.stdout2
-rw-r--r--testsuite/tests/ghci/scripts/T6018ghcifail.stderr2
-rwxr-xr-xtestsuite/tests/ghci/scripts/all.T1
-rw-r--r--testsuite/tests/polykinds/T11821a.stderr2
-rw-r--r--testsuite/tests/polykinds/T14520.stderr2
-rw-r--r--testsuite/tests/typecheck/should_fail/T6018fail.stderr2
13 files changed, 123 insertions, 17 deletions
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index e578411360..04260bc0e1 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -245,10 +245,22 @@ 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.
+Implicitly bound variables are collected by the extract- family of functions
+(extractHsTysRdrTyVars, extractHsTyVarBndrsKVs, etc.) 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.
+Note that we also maintain this ordering in kind signatures. Even though
+there's no visible kind application (yet), having implicit variables be
+quantified in left-to-right order in kind signatures is nice since:
+
+* It's consistent with the treatment for type signatures.
+* It can affect how types are displayed with -fprint-explicit-kinds (see
+ #15568 for an example), which is a situation where knowing the order in
+ which implicit variables are quantified can be useful.
+* In the event that visible kind application is implemented, the order in
+ which we would expect implicit variables to be ordered in kinds will have
+ already been established.
-}
-- | Located Haskell Context
@@ -337,6 +349,7 @@ data HsImplicitBndrs pass thing -- See Note [HsType binders]
-- Implicitly-bound kind & type vars
-- Order is important; see
-- Note [Ordering of implicit variables]
+ -- in RnTypes
, hsib_body :: thing -- Main payload (type or list of types)
}
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index e5f51660da..a78caaf6ba 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -344,7 +344,7 @@ rnImplicitBndrs bind_free_tvs
; loc <- getSrcSpanM
-- NB: kinds before tvs, as mandated by
- -- Note [Ordering of implicit variables] in HsTypes
+ -- Note [Ordering of implicit variables]
; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
; traceRn "checkMixedVars2" $
@@ -837,7 +837,10 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
-- all these various things are doing
bndrs, kv_occs, implicit_kvs :: [Located RdrName]
bndrs = map hsLTyVarLocName hs_tv_bndrs
- kv_occs = nubL (body_kv_occs ++ bndr_kv_occs)
+ kv_occs = nubL (bndr_kv_occs ++ body_kv_occs)
+ -- Make sure to list the binder kvs before the
+ -- body kvs, as mandated by
+ -- Note [Ordering of implicit variables]
implicit_kvs = filter_occs rdr_env bndrs kv_occs
-- Deleting bndrs: See Note [Kind-variable ordering]
-- dep_bndrs is the subset of bndrs that are dependent
@@ -1519,7 +1522,10 @@ In general we want to walk over a type, and find
* The free kind variables of any kind signatures in the type
Hence we return a pair (kind-vars, type vars)
-See also Note [HsBSig binder lists] in HsTypes
+(See Note [HsBSig binder lists] in HsTypes.)
+Moreover, we preserve the left-to-right order of the first occurrence of each
+variable, while preserving dependency order.
+(See Note [Ordering of implicit variables].)
Most clients of this code just want to know the kind/type vars, without
duplicates. The function rmDupsInRdrTyVars removes duplicates. That function
@@ -1548,12 +1554,57 @@ var, then this would prevent it from being implicitly quantified (see
rnImplicitBndrs). In the `foo` example above, that would have the consequence
of the k in Proxy k being reported as out of scope.
+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 any function which returns a
+FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably
+includes the `extract-` family of functions (extractHsTysRdrTyVars,
+extractHsTyVarBndrsKVs, etc.).
+These functions thus promise to keep left-to-right ordering.
+Look for pointers to this note to see the places where the action happens.
+
+Note that we also maintain this ordering in kind signatures. Even though
+there's no visible kind application (yet), having implicit variables be
+quantified in left-to-right order in kind signatures is nice since:
+
+* It's consistent with the treatment for type signatures.
+* It can affect how types are displayed with -fprint-explicit-kinds (see
+ #15568 for an example), which is a situation where knowing the order in
+ which implicit variables are quantified can be useful.
+* In the event that visible kind application is implemented, the order in
+ which we would expect implicit variables to be ordered in kinds will have
+ already been established.
-}
-- 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.
+-- Note [Ordering of implicit variables].
data FreeKiTyVars = FKTV { fktv_kis :: [Located RdrName]
, fktv_tys :: [Located RdrName] }
@@ -1614,8 +1665,10 @@ extractHsTyRdrTyVarsDups ty
-- | Extracts the free kind variables (but not the type variables) of an
-- 'HsType'. Does not return any wildcards.
-- When the same name occurs multiple times in the type, only the first
--- occurrence is returned.
--- See Note [Kind and type-variable binders]
+-- occurrence is returned, and the left-to-right order of variables is
+-- preserved.
+-- See Note [Kind and type-variable binders] and
+-- Note [Ordering of implicit variables].
extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> RnM [Located RdrName]
extractHsTyRdrTyVarsKindVars ty
= freeKiTyVarsKindVars <$> extractHsTyRdrTyVars ty
@@ -1636,7 +1689,9 @@ extractHsTysRdrTyVarsDups tys
= extract_ltys TypeLevel tys emptyFKTV
extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> RnM [Located RdrName]
--- Returns the free kind variables of any explictly-kinded binders
+-- Returns the free kind variables of any explictly-kinded binders, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
-- NB: Does /not/ delete the binders themselves.
-- However duplicates are removed
-- E.g. given [k1, a:k1, b:k2]
@@ -1657,6 +1712,9 @@ rmDupsInRdrTyVars (FKTV kis tys)
tys' = nubL (filterOut (`elemRdr` kis') tys)
extractRdrKindSigVars :: LFamilyResultSig GhcPs -> RnM [Located RdrName]
+-- Returns the free kind variables in a type family result signature, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
extractRdrKindSigVars (L _ resultSig)
| KindSig _ k <- resultSig = kindRdrNameFromSig k
| TyVarSig _ (L _ (KindedTyVar _ _ k)) <- resultSig = kindRdrNameFromSig k
@@ -1677,6 +1735,8 @@ extractDataDefnKindVars :: HsDataDefn GhcPs -> RnM [Located RdrName]
-- data D = D
-- instance forall k (a::k). C @k @* a D where ...
--
+-- This returns variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
extractDataDefnKindVars (HsDataDefn { dd_ctxt = ctxt, dd_kindSig = ksig
, dd_cons = cons })
= (nubL . freeKiTyVarsKindVars) <$>
@@ -1800,7 +1860,9 @@ extract_hs_tv_bndrs tv_bndrs
(filterOut (`elemRdr` tv_bndr_rdrs) body_tvs ++ acc_tvs) }
extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> RnM [Located RdrName]
--- Returns the free kind variables of any explictly-kinded binders
+-- Returns the free kind variables of any explictly-kinded binders, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
-- NB: Does /not/ delete the binders themselves.
-- Duplicates are /not/ removed
-- E.g. given [k1, a:k1, b:k2]
@@ -1818,7 +1880,13 @@ extract_tv t_or_k ltv@(L _ tv) acc@(FKTV kvs tvs)
| isTypeLevel t_or_k = return (FKTV kvs (ltv : tvs))
| otherwise = return (FKTV (ltv : kvs) tvs)
--- just used in this module; seemed convenient here
+-- Deletes duplicates in a list of Located things.
+--
+-- Importantly, this function is stable with respect to the original ordering
+-- of things in the list. This is important, as it is a property that GHC
+-- relies on to maintain the left-to-right ordering of implicitly quantified
+-- type variables.
+-- See Note [Ordering of implicit variables].
nubL :: Eq a => [Located a] -> [Located a]
nubL = nubBy eqLocated
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index ed488320b0..a70db2ebda 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1744,7 +1744,7 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
-- use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
-- do a stable topological sort, following
- -- Note [Ordering of implicit variables] in HsTypes
+ -- Note [Ordering of implicit variables] in RnTypes
; let final_tvs = toposortTyVars skol_tvs
; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
; return (final_tvs, result) }
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 9b4aec670d..33cdae3e63 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1912,7 +1912,7 @@ predTypeEqRel ty
-- 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
+-- be so. See also Note [Ordering of implicit variables] in RnTypes
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 ca782a9399..abd679af3b 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10688,6 +10688,17 @@ Here are the details:
if you want the most accurate information with respect to visible type
application properties.
+- Although GHC supports visible *type* applications, it does not yet support
+ visible *kind* applications. However, GHC does follow similar rules for
+ quantifying variables in kind signatures as it does for quantifying type
+ signatures. For instance: ::
+
+ type family F (a :: j) (b :: k) :: l
+ -- F :: forall j k l. j -> k -> l
+
+ In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
+ is preserved.
+
.. _implicit-parameters:
Implicit parameters
diff --git a/testsuite/tests/ghci/scripts/T15568.hs b/testsuite/tests/ghci/scripts/T15568.hs
new file mode 100644
index 0000000000..2172fe2694
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15568 where
+
+import Data.Proxy
+
+type family F (a :: j) :: k
diff --git a/testsuite/tests/ghci/scripts/T15568.script b/testsuite/tests/ghci/scripts/T15568.script
new file mode 100644
index 0000000000..8218ccc7fd
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.script
@@ -0,0 +1,4 @@
+:load T15568
+:set -fprint-explicit-foralls
+putStrLn "-- This should print 'forall j k.', not 'forall k j.'"
+:kind F
diff --git a/testsuite/tests/ghci/scripts/T15568.stdout b/testsuite/tests/ghci/scripts/T15568.stdout
new file mode 100644
index 0000000000..e97cc6b040
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.stdout
@@ -0,0 +1,2 @@
+-- This should print 'forall j k.', not 'forall k j.'
+F :: forall j k. j -> k
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index d6ba833e35..9765244f1e 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -46,7 +46,7 @@
<interactive>:60:15: error:
Type family equation violates injectivity annotation.
- Kind variable ‘k2’ cannot be inferred from the right-hand side.
+ Kind variable ‘k1’ cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index b054be9c40..c02fb87e01 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -282,3 +282,4 @@ test('T14796', normal, ghci_script, ['T14796.script'])
test('T14969', normal, ghci_script, ['T14969.script'])
test('T15259', normal, ghci_script, ['T15259.script'])
test('T15341', normal, ghci_script, ['T15341.script'])
+test('T15568', normal, ghci_script, ['T15568.script'])
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
index 09077f83d3..2e443e637b 100644
--- a/testsuite/tests/polykinds/T11821a.stderr
+++ b/testsuite/tests/polykinds/T11821a.stderr
@@ -1,4 +1,4 @@
-T11821a.hs:4:77: error:
+T11821a.hs:4:31: error:
• Couldn't match ‘k1’ with ‘k2’
• In the type declaration for ‘SameKind’
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
index 07042fde92..9c290ff4a5 100644
--- a/testsuite/tests/polykinds/T14520.stderr
+++ b/testsuite/tests/polykinds/T14520.stderr
@@ -1,6 +1,6 @@
T14520.hs:15:24: error:
• Expected kind ‘bat w w’,
- but ‘Id’ has kind ‘XXX * a0 (XXX (a0 ~>> *) a0 kat0 b0) b0’
+ but ‘Id’ has kind ‘XXX a0 * (XXX a0 (a0 ~>> *) kat0 b0) b0’
• In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 829e14ad70..f2fdf82b25 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -66,7 +66,7 @@ T6018fail.hs:59:10: error:
T6018fail.hs:62:15: error:
Type family equation violates injectivity annotation.
- Kind variable ‘k2’ cannot be inferred from the right-hand side.
+ Kind variable ‘k1’ cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15
View Lorry Controller Status