diff options
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 66 | ||||
| -rw-r--r-- | libraries/base/GHC/Records.hs | 9 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T15592.hs | 5 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T15592.stderr | 11 | ||||
| -rw-r--r-- | 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 ae64f084b0..20c79bd46f 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 43c3931e86..3b1a4c2834 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@. 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 0000000000..7e81c42565 --- /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 0000000000..71dc3b20b3 --- /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 ae4ee51a21..010d0ac703 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, ['']) |