Fix SigTvs at the kind level
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 11 Dec 2017 15:53:32 +0000 (15:53 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 11 Dec 2017 17:35:14 +0000 (17:35 +0000)
This patch fixes two bugs in the treatment of SigTvs at the
kind level:

- We should always generalise them, never default them
  (Trac #14555, #14563)

- We should check if they get unified with each other
  (Trac #11203)

Both are described in TcHsType
   Note [Kind generalisation and SigTvs]

15 files changed:
compiler/typecheck/TcBinds.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/types/TyCon.hs
testsuite/tests/polykinds/T11203.hs [new file with mode: 0644]
testsuite/tests/polykinds/T11203.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T11821a.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T14555.hs [new file with mode: 0644]
testsuite/tests/polykinds/T14555.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T14563.hs [new file with mode: 0644]
testsuite/tests/polykinds/T14563.stderr [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index 6b35183..8e7f6dc 100644 (file)
@@ -955,26 +955,24 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
 
     mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
     mk_psig_qtvs annotated_tvs
-       = do { let (sig_tv_names, sig_tvs) = unzip annotated_tvs
-            ; psig_qtvs <- mapM zonkTcTyVarToTyVar sig_tvs
+       = do { annotated_tvs <- zonkSigTyVarPairs annotated_tvs
 
             -- Report an error if the quantified variables of the
             -- partial signature have been unified together
             -- See Note [Quantified variables in partial type signatures]
-            ; let bad_sig_tvs = findDupsEq eq (sig_tv_names `zip` psig_qtvs)
-                  eq (_,tv1) (_,tv2) = tv1 == tv2
-            ; mapM_ (report_sig_tv_err sig) bad_sig_tvs
+            ; mapM_ report_sig_tv_err (findDupSigTvs annotated_tvs)
 
-            ; return (mkVarSet psig_qtvs) }
+            ; return (mkVarSet (map snd annotated_tvs)) }
 
-    report_sig_tv_err (PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty })
-                      ((n1,_) :| (n2,_) : _)
+    report_sig_tv_err (n1,n2)
+      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
       = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
                         <+> text "with" <+> quotes (ppr n2))
                      2 (hang (text "both bound by the partial type signature:")
                            2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
-    report_sig_tv_err sig _ = pprPanic "report_sig_tv_err" (ppr sig)
-                              -- Can't happen; by now we know it's a partial sig
+
+      | otherwise -- Can't happen; by now we know it's a partial sig
+      = pprPanic "report_sig_tv_err" (ppr sig)
 
     choose_psig_context :: VarSet -> TcThetaType -> Maybe TcTyVar
                         -> TcM (VarSet, TcThetaType)
@@ -1118,7 +1116,7 @@ Consider
   g :: forall b. b -> b -> _
   g x y = [x, y]
 
-Here, 'f' and 'g' are mutually recursive, and we end up unifyin 'a' and 'b'
+Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
 together, which is fine.  So we bind 'a' and 'b' to SigTvs, which can then
 unify with each other.
 
index 72bc843..3de808c 100644 (file)
@@ -1378,6 +1378,40 @@ Sidenote: It's quite possible that later, we'll consider (t -> s)
 as a degenerate case of some (pi (x :: t) -> s) and then this will
 all get more permissive.
 
+Note [Kind generalisation and SigTvs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  data T (a :: k1) x = MkT (S a ())
+  data S (b :: k2) y = MkS (T b ())
+
+While we are doing kind inference for the mutually-recursive S,T,
+we will end up unifying k1 and k2 together. So they can't be skolems.
+We therefore make them SigTvs, which can unify with type variables,
+but not with general types.  All this is very similar at the level
+of terms: see Note [Quantified variables in partial type signatures]
+in TcBinds.
+
+There are some wrinkles
+
+* We always want to kind-generalise over SigTvs, and /not/ default
+  them to Type.  Another way to say this is: a SigTV should /never/
+  stand for a type, even via defaulting. Hence the check in
+  TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar.  Here's
+  another example (Trac #14555):
+     data Exp :: [TYPE rep] -> TYPE rep -> Type where
+        Lam :: Exp (a:xs) b -> Exp xs (a -> b)
+  We want to kind-generalise over the 'rep' variable.
+  Trac #14563 is another example.
+
+* Consider Trac #11203
+    data SameKind :: k -> k -> *
+    data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
+  Here we will unify k1 with k2, but this time doing so is an error,
+  because k1 and k2 are bound in the same delcaration.
+
+  We sort this out using findDupSigTvs, in TcTyClTyVars; very much
+  as we do with partial type signatures in mk_psig_qtvs in
+  TcBinds.chooseInferredQuantifiers
 -}
 
 tcWildCardBinders :: [Name]
@@ -1420,8 +1454,8 @@ kcLHsQTyVars name flav cusk all_kind_vars
   | cusk
   = do { kv_kinds <- mk_kv_kinds
        ; lvl <- getTcLevel
-       ; let scoped_kvs = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
-       ; tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
+       ; let scoped_kvs    = zipWith (mk_skolem_tv lvl) kv_ns kv_kinds
+       ; tcExtendTyVarEnv scoped_kvs $
     do { (tc_tvs, (res_kind, stuff))
               <- solveEqualities $
                  kcLHsTyVarBndrs open_fam hs_tvs thing_inside
@@ -1455,7 +1489,8 @@ kcLHsQTyVars name flav cusk all_kind_vars
        ; let final_binders = map (mkNamedTyConBinder Specified) good_tvs
                             ++ tc_binders
              tycon = mkTcTyCon name final_binders res_kind
-                               (scoped_kvs ++ tc_tvs) flav
+                               (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
+                               flav
                            -- the tvs contain the binders already
                            -- in scope from an enclosing class, but
                            -- re-adding tvs to the env't doesn't cause
@@ -1471,7 +1506,7 @@ kcLHsQTyVars name flav cusk all_kind_vars
   | otherwise
   = do { kv_kinds <- mk_kv_kinds
        ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds
-                     -- the names must line up in splitTelescopeTvs
+           -- Why newSigTyVar?  See Note [Kind generalisation and sigTvs]
        ; (tc_tvs, (res_kind, stuff))
            <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $
               kcLHsTyVarBndrs open_fam hs_tvs thing_inside
@@ -1479,7 +1514,8 @@ kcLHsQTyVars name flav cusk all_kind_vars
                -- must remain lined up with the binders
              tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
              tycon = mkTcTyCon name tc_binders res_kind
-                               (scoped_kvs ++ binderVars tc_binders) flav
+                               (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
+                               flav
 
        ; traceTc "kcLHsQTyVars: not-cusk" $
          vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
@@ -1870,7 +1906,7 @@ kcLookupTcTyCon nm
 kcTyClTyVars :: Name -> TcM a -> TcM a
 kcTyClTyVars tycon_name thing_inside
   = do { tycon <- kcLookupTcTyCon tycon_name
-       ; tcExtendTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
+       ; tcExtendTyVarEnv2 (tcTyConScopedTyVars tycon) $ thing_inside }
 
 tcTyClTyVars :: Name
              -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
@@ -1893,26 +1929,29 @@ tcTyClTyVars :: Name
 tcTyClTyVars tycon_name thing_inside
   = do { tycon <- kcLookupTcTyCon tycon_name
 
-       ; let scoped_tvs = tcTyConScopedTyVars tycon
-               -- these are all zonked:
-             res_kind   = tyConResKind tycon
-             binders    = correct_binders (tyConBinders tycon) res_kind
+       -- Do checks on scoped tyvars
+       -- See Note [Free-floating kind vars]
+       ; let scoped_prs = tcTyConScopedTyVars tycon
+             scoped_tvs = map snd scoped_prs
+             still_sig_tvs = filter isSigTyVar scoped_tvs
+
+       ; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
 
-       ; traceTc "tcTyClTyVars" (vcat [ ppr tycon
-                                      , ppr (tyConBinders tycon)
-                                      , ppr (tcTyConScopedTyVars tycon) ])
-          -- See Note [Free-floating kind vars]
-       ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs
-       ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs
        ; checkNoErrs $ reportFloatingKvs tycon_name (tyConFlavour tycon)
-                                         zonked_scoped_tvs still_sig_tvs
+                                         scoped_tvs still_sig_tvs
 
-          -- Add the *unzonked* tyvars to the env't, because those
-          -- are the ones mentioned in the source.
+       ; let res_kind   = tyConResKind tycon
+             binders    = correct_binders (tyConBinders tycon) res_kind
        ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
-       ; tcExtendTyVarEnv scoped_tvs $
+
+       ; tcExtendTyVarEnv2 scoped_prs $
          thing_inside binders res_kind }
   where
+    report_sig_tv_err (n1, n2)
+      = setSrcSpan (getSrcSpan n2) $
+        addErrTc (text "Couldn't match" <+> quotes (ppr n1)
+                        <+> text "with" <+> quotes (ppr n2))
+
     -- Given some TyConBinders and a TyCon's result kind, make sure that the
     -- correct any wrong Named/Anon choices. For example, consider
     --   type Syn k = forall (a :: k). Proxy a
index 7473967..7f2f92a 100644 (file)
@@ -68,7 +68,8 @@ module TcMType (
   zonkTidyTcType, zonkTidyOrigin,
   tidyEvVar, tidyCt, tidySkolemInfo,
   skolemiseRuntimeUnk,
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
+  zonkTcTyVar, zonkTcTyVars,
+  zonkTcTyVarToTyVar, zonkSigTyVarPairs,
   zonkTyCoVarsAndFV, zonkTcTypeAndFV,
   zonkTyCoVarsAndFVList,
   zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
@@ -1024,24 +1025,28 @@ defaultTyVar default_kind tv
   | not (isMetaTyVar tv)
   = return False
 
-  | isRuntimeRepVar tv && not_sig_tv  -- We never quantify over a RuntimeRep var
+  | isSigTyVar tv
+    -- Do not default SigTvs. Doing so would violate the invariants
+    -- on SigTvs; see Note [Signature skolems] in TcType.
+    -- Trac #13343 is an example; #14555 is another
+    -- See Note [Kind generalisation and SigTvs]
+  = return False
+
+
+  | isRuntimeRepVar tv  -- Do not quantify over a RuntimeRep var
+                        -- unless it is a SigTv, handled earlier
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
 
-  | default_kind && not_sig_tv        -- -XNoPolyKinds and this is a kind var
-  = do { default_kind_var tv          -- so default it to * if possible
+  | default_kind                 -- -XNoPolyKinds and this is a kind var
+  = do { default_kind_var tv     -- so default it to * if possible
        ; return True }
 
   | otherwise
   = return False
 
   where
-    -- Do not default SigTvs. Doing so would violate the invariants
-    -- on SigTvs; see Note [Signature skolems] in TcType.
-    -- Trac #13343 is an example
-    not_sig_tv = not (isSigTyVar tv)
-
     default_kind_var :: TyVar -> TcM ()
        -- defaultKindVar is used exclusively with -XNoPolyKinds
        -- See Note [Defaulting with -XNoPolyKinds]
@@ -1541,6 +1546,13 @@ zonkTcTyVarToTyVar tv
                                           (ppr tv $$ ppr ty)
        ; return tv' }
 
+zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
+zonkSigTyVarPairs prs
+  = mapM do_one prs
+  where
+    do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
+                         ; return (nm, tv') }
+
 {-
 %************************************************************************
 %*                                                                      *
index 627a378..16bf345 100644 (file)
@@ -1782,6 +1782,9 @@ promoteTyVarTcS tclvl tv
 defaultTyVarTcS :: TcTyVar -> TcS Bool
 defaultTyVarTcS the_tv
   | isRuntimeRepVar the_tv
+  , not (isSigTyVar the_tv)  -- SigTvs should only be unified with a tyvar
+                             -- never with a type; c.f. TcMType.defaultTyVar
+                             -- See Note [Kind generalisation and SigTvs]
   = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
        ; unifyTyVar the_tv liftedRepTy
        ; return True }
index 5c5cf2f..e1ea4aa 100644 (file)
@@ -302,6 +302,52 @@ environment. (This is handled by `allDecls').
 
 See also Note [Kind checking recursive type and class declarations]
 
+Note [How TcTyCons work]
+o~~~~~~~~~~~~~~~~~~~~~~~~
+TcTyCons are used for two distinct purposes
+
+1.  When recovering from a type error in a type declaration,
+    we want to put the erroneous TyCon in the environment in a
+    way that won't lead to more errors.  We use a TcTyCon for this;
+    see makeRecoveryTyCon.
+
+2.  When checking a type/class declaration (in module TcTyClsDecls), we come
+    upon knowledge of the eventual tycon in bits and pieces.
+
+      S1) First, we use getInitialKinds to look over the user-provided
+          kind signature of a tycon (including, for example, the number
+          of parameters written to the tycon) to get an initial shape of
+          the tycon's kind.  We record that shape in a TcTyCon.
+
+      S2) Then, using these initial kinds, we kind-check the body of the
+          tycon (class methods, data constructors, etc.), filling in the
+          metavariables in the tycon's initial kind.
+
+      S3) We then generalize to get the tycon's final, fixed
+          kind. Finally, once this has happened for all tycons in a
+          mutually recursive group, we can desugar the lot.
+
+    For convenience, we store partially-known tycons in TcTyCons, which
+    might store meta-variables. These TcTyCons are stored in the local
+    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:
+      - 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.
+
+    In a TcTyCon, everything is zonked after the kind-checking pass (S2).
 -}
 
 
@@ -367,24 +413,28 @@ kcTyClGroup decls
       = do { let tc = case lookupNameEnv kind_env name of
                         Just (ATcTyCon tc) -> tc
                         _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
-                 kc_binders  = tyConBinders tc
-                 kc_res_kind = tyConResKind tc
-                 kc_tyvars   = tyConTyVars tc
-           ; kvs <- kindGeneralize (mkTyConKind kc_binders kc_res_kind)
-           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ kc_binders
+                 tc_binders  = tyConBinders tc
+                 tc_res_kind = tyConResKind tc
+                 tc_tyvars   = tyConTyVars tc
+                 scoped_tvs  = tcTyConScopedTyVars tc
+
+           ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
+
+           ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
 
            ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
-           ; kc_res_kind'        <- zonkTcTypeToType env kc_res_kind
+           ; tc_res_kind'        <- zonkTcTypeToType env tc_res_kind
+           ; scoped_tvs'         <- zonkSigTyVarPairs scoped_tvs
 
-                      -- Make sure kc_kind' has the final, zonked kind variables
+                      -- Make sure tc_kind' has the final, zonked kind variables
            ; traceTc "Generalise kind" $
-             vcat [ ppr name, ppr kc_binders, ppr (mkTyConKind kc_binders kc_res_kind)
-                  , ppr kvs, ppr all_binders, ppr kc_res_kind
-                  , ppr all_binders', ppr kc_res_kind'
-                  , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)]
+             vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
+                  , ppr kvs, ppr all_binders, ppr tc_res_kind
+                  , ppr all_binders', ppr tc_res_kind'
+                  , ppr tc_tyvars, ppr (tcTyConScopedTyVars tc)]
 
-           ; return (mkTcTyCon name all_binders' kc_res_kind'
-                               (tcTyConScopedTyVars tc)
+           ; return (mkTcTyCon name all_binders' tc_res_kind'
+                               scoped_tvs'
                                (tyConFlavour tc)) }
 
     generaliseTCD :: TcTypeEnv
index f1ea864..ef0e17f 100644 (file)
@@ -46,6 +46,7 @@ module TcType (
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar, isTouchableOrFmv,
   isFloatedTouchableMetaTyVar,
+  findDupSigTvs, mkTyVarNamePairs,
 
   --------------------------------
   -- Builders
@@ -226,7 +227,7 @@ import BasicTypes
 import Util
 import Bag
 import Maybes
-import ListSetOps ( getNth )
+import ListSetOps ( getNth, findDupsEq )
 import Outputable
 import FastString
 import ErrUtils( Validity(..), MsgDoc, isValid )
@@ -234,6 +235,7 @@ import FV
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.IORef
+import Data.List.NonEmpty( NonEmpty(..) )
 import Data.Functor.Identity
 import qualified Data.Semigroup as Semi
 
@@ -1306,6 +1308,20 @@ isRuntimeUnkSkol x
   | RuntimeUnk <- tcTyVarDetails x = True
   | otherwise                      = False
 
+mkTyVarNamePairs :: [TyVar] -> [(Name,TyVar)]
+-- Just pair each TyVar with its own name
+mkTyVarNamePairs tvs = [(tyVarName tv, tv) | tv <- tvs]
+
+findDupSigTvs :: [(Name,TcTyVar)] -> [(Name,Name)]
+-- If we have [...(x1,tv)...(x2,tv)...]
+-- return (x1,x2) in the result list
+findDupSigTvs prs
+  = concatMap mk_result_prs $
+    findDupsEq eq_snd prs
+  where
+    eq_snd (_,tv1) (_,tv2) = tv1 == tv2
+    mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs
+
 {-
 ************************************************************************
 *                                                                      *
index 596c5f3..cf96a49 100644 (file)
@@ -814,8 +814,10 @@ data TyCon
         tyConKind    :: Kind,             -- ^ Kind of this TyCon
         tyConArity   :: Arity,            -- ^ Arity
 
-        tcTyConScopedTyVars :: [TyVar], -- ^ Scoped tyvars over the
-                                        -- tycon's body. See Note [TcTyCon]
+        tcTyConScopedTyVars :: [(Name,TyVar)],
+                           -- ^ Scoped tyvars over the tycon's body
+                           -- See Note [How TcTyCons work] in TcTyClsDecls
+
         tcTyConFlavour :: TyConFlavour
                            -- ^ What sort of 'TyCon' this represents.
       }
@@ -1136,51 +1138,6 @@ so the coercion tycon CoT must have
         kind:    T ~ []
  and    arity:   0
 
-Note [TcTyCon]
-~~~~~~~~~~~~~~
-TcTyCons are used for two distinct purposes
-
-1.  When recovering from a type error in a type declaration,
-    we want to put the erroneous TyCon in the environment in a
-    way that won't lead to more errors.  We use a TcTyCon for this;
-    see makeRecoveryTyCon.
-
-2.  When checking a type/class declaration (in module TcTyClsDecls), we come
-    upon knowledge of the eventual tycon in bits and pieces. First, we use
-    getInitialKinds to look over the user-provided kind signature of a tycon
-    (including, for example, the number of parameters written to the tycon)
-    to get an initial shape of the tycon's kind. Then, using these initial
-    kinds, we kind-check the body of the tycon (class methods, data constructors,
-    etc.), filling in the metavariables in the tycon's initial kind.
-    We then generalize to get the tycon's final, fixed kind. Finally, once
-    this has happened for all tycons in a mutually recursive group, we
-    can desugar the lot.
-
-    For convenience, we store partially-known tycons in TcTyCons, which
-    might store meta-variables. These TcTyCons are stored in the local
-    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: one in getInitialKind (this pass look only
-    at the head, not the body), one in kcTyClDecls (to kind-check the body),
-    and 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 later passes when we create
-    a TcTyCon in getInitialKinds. Much easier this way! These tyvars are
-    brought into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
-
-    It is important that the scoped type variables not be zonked, as some
-    scoped type variables come into existence as SigTvs. If we zonk, the
-    Unique will change and the user-written occurrences won't match up with
-    what we expect.
-
-    In a TcTyCon, everything is zonked (except the scoped vars) after
-    the kind-checking pass.
 
 ************************************************************************
 *                                                                      *
@@ -1548,7 +1505,8 @@ mkSumTyCon name binders res_kind arity tyvars cons parent
 mkTcTyCon :: Name
           -> [TyConBinder]
           -> Kind                -- ^ /result/ kind only
-          -> [TyVar]             -- ^ Scoped type variables, see Note [TcTyCon]
+          -> [(Name,TyVar)]      -- ^ Scoped type variables;
+                                 -- see Note [How TcTyCons work] in TcTyClsDecls
           -> TyConFlavour        -- ^ What sort of 'TyCon' this represents
           -> TyCon
 mkTcTyCon name binders res_kind scoped_tvs flav
@@ -1754,7 +1712,7 @@ isInjectiveTyCon (PrimTyCon {})                _                = True
 isInjectiveTyCon (PromotedDataCon {})          _                = True
 isInjectiveTyCon (TcTyCon {})                  _                = True
   -- Reply True for TcTyCon to minimise knock on type errors
-  -- See Note [TcTyCon] item (1)
+  -- See Note [How TcTyCons work] item (1) in TcTyClsDecls
 
 -- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
 -- (where X is the role passed in):
diff --git a/testsuite/tests/polykinds/T11203.hs b/testsuite/tests/polykinds/T11203.hs
new file mode 100644 (file)
index 0000000..cff89df
--- /dev/null
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds, KindSignatures #-}
+
+module T11203 where
+
+data SameKind :: k -> k -> *
+
+data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr
new file mode 100644 (file)
index 0000000..5d62e00
--- /dev/null
@@ -0,0 +1,4 @@
+
+T11203.hs:7:24: error:
+    • Couldn't match ‘k1’ with ‘k2’
+    • In the data declaration for ‘Q’
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
new file mode 100644 (file)
index 0000000..09077f8
--- /dev/null
@@ -0,0 +1,4 @@
+
+T11821a.hs:4:77: error:
+    • Couldn't match ‘k1’ with ‘k2’
+    • In the type declaration for ‘SameKind’
diff --git a/testsuite/tests/polykinds/T14555.hs b/testsuite/tests/polykinds/T14555.hs
new file mode 100644 (file)
index 0000000..0ab71b1
--- /dev/null
@@ -0,0 +1,12 @@
+{-# Language TypeInType #-}
+{-# Language TypeOperators, DataKinds, PolyKinds, GADTs #-}
+
+module T14555 where
+
+import Data.Kind
+import GHC.Types (TYPE)
+
+data Exp :: [TYPE rep] -> TYPE rep -> Type where
+--data Exp (x :: [TYPE rep]) (y :: TYPE rep) where
+--data Exp (x :: [TYPE rep]) y where
+  Lam :: Exp (a:xs) b -> Exp xs (a -> b)
diff --git a/testsuite/tests/polykinds/T14555.stderr b/testsuite/tests/polykinds/T14555.stderr
new file mode 100644 (file)
index 0000000..66fb55a
--- /dev/null
@@ -0,0 +1,6 @@
+
+T14555.hs:12:34: error:
+    • Expected kind ‘TYPE rep’, but ‘a -> b’ has kind ‘*’
+    • In the second argument of ‘Exp’, namely ‘(a -> b)’
+      In the type ‘Exp xs (a -> b)’
+      In the definition of data constructor ‘Lam’
diff --git a/testsuite/tests/polykinds/T14563.hs b/testsuite/tests/polykinds/T14563.hs
new file mode 100644 (file)
index 0000000..7959d92
--- /dev/null
@@ -0,0 +1,9 @@
+{-# Language TypeInType #-}
+{-# Language RankNTypes, KindSignatures, PolyKinds #-}
+
+import GHC.Types (TYPE)
+import Data.Kind
+
+data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where
+  Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a.
+         (g xx -> a) -> h xx -> Lan g h a
diff --git a/testsuite/tests/polykinds/T14563.stderr b/testsuite/tests/polykinds/T14563.stderr
new file mode 100644 (file)
index 0000000..1265ec0
--- /dev/null
@@ -0,0 +1,7 @@
+
+T14563.hs:9:39: error:
+    • Expected kind ‘TYPE rep -> TYPE rep''’,
+        but ‘h’ has kind ‘TYPE rep -> *’
+    • In the second argument of ‘Lan’, namely ‘h’
+      In the type ‘Lan g h a’
+      In the definition of data constructor ‘Lan’
index 9f34f30..8a03e89 100644 (file)
@@ -146,7 +146,7 @@ test('T11648', normal, compile, [''])
 test('T11648b', normal, compile_fail, [''])
 test('KindVType', normal, compile_fail, [''])
 test('T11821', normal, compile, [''])
-test('T11821a', normal, compile, [''])
+test('T11821a', normal, compile_fail, [''])
 test('T11640', normal, compile, [''])
 test('T11554', normal, compile_fail, [''])
 test('T12055', normal, compile, [''])
@@ -177,3 +177,7 @@ test('T14450', normal, compile_fail, [''])
 test('T14174', normal, compile_fail, [''])
 test('T14174a', expect_broken(14174), compile_fail, [''])
 test('T14520', normal, compile_fail, [''])
+test('T11203', normal, compile_fail, [''])
+test('T14555', normal, compile_fail, [''])
+test('T14563', normal, compile_fail, [''])
+