Distinguish Inferred from Specified tyvars
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 3 Oct 2018 15:35:09 +0000 (16:35 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 4 Oct 2018 14:37:58 +0000 (15:37 +0100)
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

compiler/typecheck/TcTyClsDecls.hs
libraries/base/GHC/Records.hs
testsuite/tests/polykinds/T15592.hs [new file with mode: 0644]
testsuite/tests/polykinds/T15592.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index ae64f08..20c79bd 100644 (file)
@@ -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
index 43c3931..3b1a4c2 100644 (file)
@@ -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@.  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 (file)
index 0000000..7e81c42
--- /dev/null
@@ -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 (file)
index 0000000..71dc3b2
--- /dev/null
@@ -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]
index ae4ee51..010d0ac 100644 (file)
@@ -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, [''])