[commit: ghc] master: Distinguish Inferred from Specified tyvars (2f09753)
git at git.haskell.org
git at git.haskell.org
Thu Oct 4 15:03:56 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/2f09753f96207c12efd43090f5de55b05aef35d3/ghc
>---------------------------------------------------------------
commit 2f09753f96207c12efd43090f5de55b05aef35d3
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Wed Oct 3 16:35:09 2018 +0100
Distinguish Inferred from Specified tyvars
In a declared type we need to distinguish between Inferred
and Specified type variables. This was exposed by Trac #15592.
See Note [Work out final tyConBinders] in TcTyClsDecls.
I had to change the definition of HasField in GHC.Records to
class HasField x r a | x r -> a where
so as to have an /inferred/ kind argument rather than a
specfied one. So
HasField :: forall {k}. k -> * -> * -> Constraint
>---------------------------------------------------------------
2f09753f96207c12efd43090f5de55b05aef35d3
compiler/typecheck/TcTyClsDecls.hs | 66 ++++++++++++++++++++++++++++-----
libraries/base/GHC/Records.hs | 9 ++++-
testsuite/tests/polykinds/T15592.hs | 5 +++
testsuite/tests/polykinds/T15592.stderr | 11 ++++++
testsuite/tests/polykinds/all.T | 1 +
5 files changed, 81 insertions(+), 11 deletions(-)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index ae64f08..20c79bd 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -359,24 +359,36 @@ TcTyCons are used for two distinct purposes
environment in TcTyClsDecls, until the real full TyCons can be created
during desugaring. A desugared program should never have a TcTyCon.
- A challenging piece in all of this is that we end up taking three separate
- passes over every declaration:
+3. In a TcTyCon, everything is zonked after the kind-checking pass (S2).
+
+4. tyConScopedTyVars. A challenging piece in all of this is that we
+ end up taking three separate passes over every declaration:
- one in getInitialKind (this pass look only at the head, not the body)
- one in kcTyClDecls (to kind-check the body)
- a final one in tcTyClDecls (to desugar)
+
In the latter two passes, we need to connect the user-written type
variables in an LHsQTyVars with the variables in the tycon's
inferred kind. Because the tycon might not have a CUSK, this
matching up is, in general, quite hard to do. (Look through the
git history between Dec 2015 and Apr 2016 for
- TcHsType.splitTelescopeTvs!) Instead of trying, we just store the
- list of type variables to bring into scope, in the
- tyConScopedTyVars field of the TcTyCon. These tyvars are brought
- into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
+ TcHsType.splitTelescopeTvs!)
+
+ Instead of trying, we just store the list of type variables to
+ bring into scope, in the tyConScopedTyVars field of the TcTyCon.
+ These tyvars are brought into scope in kcTyClTyVars and
+ tcTyClTyVars, both in TcHsType.
- In a TcTyCon, everything is zonked after the kind-checking pass (S2).
+ In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
+ than just [TcTyVar]? Consider these mutually-recursive decls
+ data T (a :: k1) b = MkT (S a b)
+ data S (c :: k2) d = MkS (T c d)
+ We start with k1 bound to kappa1, and k2 to kappa2; so initially
+ in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But
+ then kappa1 and kappa2 get unified; so after the zonking in
+ 'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ.
- See also Note [Type checking recursive type and class declarations].
+See also Note [Type checking recursive type and class declarations].
Note [Check telescope again during generalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -551,11 +563,17 @@ kcTyClGroup decls
; checkValidTelescope tc_binders user_tyvars empty
; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
- ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
+ -- See Note [Work out final tyConBinders]
+ ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
+ ; let (specified_kvs, inferred_kvs) = partition is_specified kvs
+ user_specified_tkvs = mkVarSet (map snd scoped_tvs')
+ is_specified kv = kv `elemVarSet` user_specified_tkvs
+ all_binders = mkNamedTyConBinders Inferred inferred_kvs ++
+ mkNamedTyConBinders Specified specified_kvs ++
+ tc_binders
; (env, all_binders') <- zonkTyVarBinders all_binders
; tc_res_kind' <- zonkTcTypeToTypeX env tc_res_kind
- ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs
-- See Note [Check telescope again during generalisation]
; let extra = text "NB: Implicitly declared variables come before others."
@@ -573,6 +591,34 @@ kcTyClGroup decls
(tyConFlavour tc)) }
+{- Note [Work out final tyConBinders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ data T f (a::k1) b = MkT (f a b) (T f a b)
+
+We should get
+ T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> *
+
+Note that:
+ * k1 is Specified, because it appears in a user-written kind
+ * k2 is Inferred, because it doesn't appear at all in the
+ original declaration
+
+However, at this point in kcTyClGroup, the tc_binders are
+simply [f, a, b], the user-written argumennts to the TyCon.
+(Why? Because that's what we need for the recursive uses in
+T's RHS.)
+
+So kindGeneralize will generalise over /both/ k1 /and/ k2.
+Yet we must distinguish them, and we must put the Inferred
+ones first. How can we tell the difference? Well, the
+Specified variables will be among the tyConScopedTyVars of
+the TcTyCon.
+
+Hence partitioning by is_specified. See Trac #15592 for
+some discussion.
+-}
+
--------------
tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
tcExtendKindEnvWithTyCons tcs
diff --git a/libraries/base/GHC/Records.hs b/libraries/base/GHC/Records.hs
index 43c3931..3b1a4c2 100644
--- a/libraries/base/GHC/Records.hs
+++ b/libraries/base/GHC/Records.hs
@@ -29,6 +29,13 @@ module GHC.Records
-- | Constraint representing the fact that the field @x@ belongs to
-- the record type @r@ and has field type @a at . This will be solved
-- automatically, but manual instances may be provided as well.
-class HasField (x :: k) r a | x r -> a where
+--
+-- HasField :: forall {k}. k -> * -> * -> Constraint
+-- getField :: forall {k} (x::k) r a. HasField x r a => r -> a
+-- NB: The {k} means that k is an 'inferred' type variable, and
+-- hence not provided in visible type applications. Thus you
+-- say getField @"foo"
+-- not getField @Symbol @"foo"
+class HasField x r a | x r -> a where
-- | Selector function to extract the field from the record.
getField :: r -> a
diff --git a/testsuite/tests/polykinds/T15592.hs b/testsuite/tests/polykinds/T15592.hs
new file mode 100644
index 0000000..7e81c42
--- /dev/null
+++ b/testsuite/tests/polykinds/T15592.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeInType #-}
+{-# OPTIONS_GHC -ddump-types -fprint-explicit-foralls #-}
+module T15592 where
+
+data T f (a::k1) b = MkT (f a b) (T f a b)
diff --git a/testsuite/tests/polykinds/T15592.stderr b/testsuite/tests/polykinds/T15592.stderr
new file mode 100644
index 0000000..71dc3b2
--- /dev/null
+++ b/testsuite/tests/polykinds/T15592.stderr
@@ -0,0 +1,11 @@
+TYPE SIGNATURES
+ T15592.MkT ::
+ forall {k} k1 (f :: k1 -> k -> *) (a :: k1) (b :: k).
+ f a b -> T f a b -> T f a b
+TYPE CONSTRUCTORS
+ type role T nominal nominal representational nominal nominal
+ T :: forall {k} k1. (k1 -> k -> *) -> k1 -> k -> *
+COERCION AXIOMS
+Dependent modules: []
+Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
+ integer-gmp-1.0.2.0]
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index ae4ee51..010d0ac 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -193,3 +193,4 @@ test('T15116a', normal, compile_fail, [''])
test('T15170', normal, compile, [''])
test('T14939', normal, compile, ['-O'])
test('T15577', normal, compile_fail, ['-O'])
+test('T15592', normal, compile, [''])
More information about the ghc-commits
mailing list