Warn on inferred polymorphic recursionwip/t17541

Silly users sometimes try to use visible dependent quantification
and polymorphic recursion without a CUSK or SAK. This causes
unexpected errors. So we now adjust expectations with a bit
of helpful messaging.

Closes #17541 and closes #17131.

test cases: dependent/should_fail/T{17541{,b},17131}

18 files changed, 191 insertions, 39 deletions

diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index 09a9bb2f6e..f6abd5a0c7 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -13,7 +13,7 @@ module TcClassDcl ( tcClassSigs, tcClassDecl2,
                     findMethodBind, instantiateMethod,
                     tcClassMinimalDef,
                     HsSigFun, mkHsSigFun,
-                    tcMkDeclCtxt, tcAddDeclCtxt, badMethodErr,
+                    badMethodErr,
                     instDeclCtxt1, instDeclCtxt2, instDeclCtxt3,
                     tcATDefault
                   ) where
@@ -423,14 +423,6 @@ This makes the error messages right.
 ************************************************************************
 -}
 
-tcMkDeclCtxt :: TyClDecl GhcRn -> SDoc
-tcMkDeclCtxt decl = hsep [text "In the", pprTyClDeclFlavour decl,
-                      text "declaration for", quotes (ppr (tcdName decl))]
-
-tcAddDeclCtxt :: TyClDecl GhcRn -> TcM a -> TcM a
-tcAddDeclCtxt decl thing_inside
-  = addErrCtxt (tcMkDeclCtxt decl) thing_inside
-
 badMethodErr :: Outputable a => a -> Name -> SDoc
 badMethodErr clas op
   = hsep [text "Class", quotes (ppr clas),
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 9a5d745dea..b0a4ef420f 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1941,7 +1941,8 @@ kcInferDeclHeader name flav
                       , hsq_explicit = hs_tvs }) kc_res_ki
   -- No standalane kind signature and no CUSK.
   -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
-  = do { (scoped_kvs, (tc_tvs, res_kind))
+  = addTyConFlavCtxt name flav $
+    do { (scoped_kvs, (tc_tvs, res_kind))
            -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
            -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
            <- bindImplicitTKBndrs_Q_Tv kv_ns            $
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 545f001f00..bfd5567949 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -316,8 +316,8 @@ support making synonyms of types with higher-rank kinds.  But
 you can always specify a CUSK directly to make this work out.
 See tc269 for an example.
 
-Note [Skip decls with CUSKs in kcLTyClDecl]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [CUSKs and PolyKinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
     data T (a :: *) = MkT (S a)   -- Has CUSK
@@ -530,7 +530,8 @@ kcTyClGroup kisig_env decls
           --    3. Generalise the inferred kinds
           -- See Note [Kind checking for type and class decls]
 
-        ; cusks_enabled <- xoptM LangExt.CUSKs
+        ; cusks_enabled <- xoptM LangExt.CUSKs <&&> xoptM LangExt.PolyKinds
+                    -- See Note [CUSKs and PolyKinds]
         ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls
 
               get_kind d
@@ -559,10 +560,8 @@ kcTyClGroup kisig_env decls
                     -- NB: the environment extension overrides the tycon
                     --     promotion-errors bindings
                     --     See Note [Type environment evolution]
-                  ; poly_kinds  <- xoptM LangExt.PolyKinds
                   ; tcExtendKindEnvWithTyCons mono_tcs $
-                    mapM_ kcLTyClDecl (if poly_kinds then kindless_decls else decls)
-                    -- See Note [Skip decls with CUSKs in kcLTyClDecl]
+                    mapM_ kcLTyClDecl kindless_decls
 
                   ; return mono_tcs }
 
@@ -974,7 +973,39 @@ time mapped to 'kb'.  That's how C and D end up with differently-named
 final TyVars despite the fact that we unified kka:=kkb
 
 zonkRecTyVarBndrs we need to do knot-tying because of the need to
-apply this same substitution to the kind of each.  -}
+apply this same substitution to the kind of each.
+
+Note [Inferring visible dependent quantification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  data T k :: k -> Type where
+    MkT1 :: T Type Int
+    MkT2 :: T (Type -> Type) Maybe
+
+This looks like it should work. However, it is polymorphically recursive,
+as the uses of T in the constructor types specialize the k in the kind
+of T. This trips up our dear users (#17131, #17541), and so we add
+a "landmark" context (which cannot be suppressed) whenever we
+spot inferred visible dependent quantification (VDQ).
+
+It's hard to know when we've actually been tripped up by polymorphic recursion
+specifically, so we just include a note to users whenever we infer VDQ. The
+testsuite did not show up a single spurious inclusion of this message.
+
+The context is added in addVDQNote, which looks for a visible TyConBinder
+that also appears in the TyCon's kind. (I first looked at the kind for
+a visible, dependent quantifier, but Note [No polymorphic recursion] in
+TcHsType defeats that approach.) addVDQNote is used in kcTyClDecl,
+which is used only when inferring the kind of a tycon (never with a CUSK or
+SAK).
+
+Once upon a time, I (Richard E) thought that the tycon-kind could
+not be a forall-type. But this is wrong: data T :: forall k. k -> Type
+(with -XNoCUSKs) could end up here. And this is all OK.
+
+
+-}
 
 --------------
 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
@@ -1258,30 +1289,32 @@ Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing.
 ------------------------------------------------------------------------
 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
   -- See Note [Kind checking for type and class decls]
+  -- Called only for declarations without a signature (no CUSKs or SAKs here)
 kcLTyClDecl (L loc decl)
   = setSrcSpan loc $
-    tcAddDeclCtxt decl $
-    do { traceTc "kcTyClDecl {" (ppr tc_name)
-       ; kcTyClDecl decl
+    do { tycon <- kcLookupTcTyCon tc_name
+       ; traceTc "kcTyClDecl {" (ppr tc_name)
+       ; addVDQNote tycon $   -- See Note [Inferring visible dependent quantification]
+         addErrCtxt (tcMkDeclCtxt decl) $
+         kcTyClDecl decl tycon
        ; traceTc "kcTyClDecl done }" (ppr tc_name) }
   where
-    tc_name = tyClDeclLName decl
+    tc_name = tcdName decl
 
-kcTyClDecl :: TyClDecl GhcRn -> TcM ()
+kcTyClDecl :: TyClDecl GhcRn -> TcTyCon -> TcM ()
 -- This function is used solely for its side effect on kind variables
 -- NB kind signatures on the type variables and
 --    result kind signature have already been dealt with
 --    by inferInitialKind, so we can ignore them here.
 
 kcTyClDecl (DataDecl { tcdLName    = (L _ name)
-                     , tcdDataDefn = defn })
+                     , tcdDataDefn = defn }) tyCon
   | HsDataDefn { dd_cons = cons@((L _ (ConDeclGADT {})) : _)
                , dd_ctxt = (L _ [])
                , dd_ND = new_or_data } <- defn
-  = do { tyCon <- kcLookupTcTyCon name
-         -- See Note [Implementation of UnliftedNewtypes] STEP 2
-       ; kcConDecls new_or_data (tyConResKind tyCon) cons
-       }
+  = -- See Note [Implementation of UnliftedNewtypes] STEP 2
+    kcConDecls new_or_data (tyConResKind tyCon) cons
+
     -- hs_tvs and dd_kindSig already dealt with in inferInitialKind
     -- This must be a GADT-style decl,
     --        (see invariants of DataDefn declaration)
@@ -1294,18 +1327,17 @@ kcTyClDecl (DataDecl { tcdLName    = (L _ name)
                , dd_ND = new_or_data } <- defn
   = bindTyClTyVars name $ \ _ _ ->
     do { _ <- tcHsContext ctxt
-       ; tyCon <- kcLookupTcTyCon name
        ; kcConDecls new_or_data (tyConResKind tyCon) cons
        }
 
-kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs })
+kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon
   = bindTyClTyVars name $ \ _ res_kind ->
     discardResult $ tcCheckLHsType rhs res_kind
         -- NB: check against the result kind that we allocated
         -- in inferInitialKinds.
 
 kcTyClDecl (ClassDecl { tcdLName = L _ name
-                      , tcdCtxt = ctxt, tcdSigs = sigs })
+                      , tcdCtxt = ctxt, tcdSigs = sigs }) _tycon
   = bindTyClTyVars name $ \ _ _ ->
     do  { _ <- tcHsContext ctxt
         ; mapM_ (wrapLocM_ kc_sig) sigs }
@@ -1315,18 +1347,15 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name
 
     skol_info = TyConSkol ClassFlavour name
 
-kcTyClDecl (FamDecl _ (FamilyDecl { fdLName  = L _ fam_tc_name
-                                  , fdInfo   = fd_info }))
+kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo   = fd_info })) fam_tc
 -- closed type families look at their equations, but other families don't
 -- do anything here
   = case fd_info of
-      ClosedTypeFamily (Just eqns) ->
-        do { fam_tc <- kcLookupTcTyCon fam_tc_name
-           ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
+      ClosedTypeFamily (Just eqns) -> mapM_ (kcTyFamInstEqn fam_tc) eqns
       _ -> return ()
-kcTyClDecl (FamDecl _ (XFamilyDecl nec))        = noExtCon nec
-kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec
-kcTyClDecl (XTyClDecl nec)                      = noExtCon nec
+kcTyClDecl (FamDecl _ (XFamilyDecl nec))        _ = noExtCon nec
+kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) _ = noExtCon nec
+kcTyClDecl (XTyClDecl nec)                      _ = noExtCon nec
 
 -------------------
 
@@ -4157,6 +4186,46 @@ checkValidRoles tc
 ************************************************************************
 -}
 
+tcMkDeclCtxt :: TyClDecl GhcRn -> SDoc
+tcMkDeclCtxt decl = hsep [text "In the", pprTyClDeclFlavour decl,
+                      text "declaration for", quotes (ppr (tcdName decl))]
+
+addVDQNote :: TcTyCon -> TcM a -> TcM a
+-- See Note [Inferring visible dependent quantification]
+-- Only types without a signature (CUSK or SAK) here
+addVDQNote tycon thing_inside
+  | ASSERT2( isTcTyCon tycon, ppr tycon )
+    ASSERT2( not (tcTyConIsPoly tycon), ppr tycon $$ ppr tc_kind )
+    has_vdq
+  = addLandmarkErrCtxt vdq_warning thing_inside
+  | otherwise
+  = thing_inside
+  where
+      -- Check whether a tycon has visible dependent quantification.
+      -- This will *always* be a TcTyCon. Furthermore, it will *always*
+      -- be an ungeneralised TcTyCon, straight out of kcInferDeclHeader.
+      -- Thus, all the TyConBinders will be anonymous. Thus, the
+      -- free variables of the tycon's kind will be the same as the free
+      -- variables from all the binders.
+    has_vdq  = any is_vdq_tcb (tyConBinders tycon)
+    tc_kind  = tyConKind tycon
+    kind_fvs = tyCoVarsOfType tc_kind
+
+    is_vdq_tcb tcb = (binderVar tcb `elemVarSet` kind_fvs) &&
+                     isVisibleTyConBinder tcb
+
+    vdq_warning = vcat
+      [ text "NB: Type" <+> quotes (ppr tycon) <+>
+        text "was inferred to use visible dependent quantification."
+      , text "Most types with visible dependent quantification are"
+      , text "polymorphically recursive and need a standalone kind"
+      , text "signature. Perhaps supply one, with StandaloneKindSignatures."
+      ]
+
+tcAddDeclCtxt :: TyClDecl GhcRn -> TcM a -> TcM a
+tcAddDeclCtxt decl thing_inside
+  = addErrCtxt (tcMkDeclCtxt decl) thing_inside
+
 tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a
 tcAddTyFamInstCtxt decl
   = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
diff --git a/testsuite/tests/dependent/should_fail/T16344.stderr b/testsuite/tests/dependent/should_fail/T16344.stderr
index b47561771f..d567defeee 100644
--- a/testsuite/tests/dependent/should_fail/T16344.stderr
+++ b/testsuite/tests/dependent/should_fail/T16344.stderr
@@ -4,3 +4,7 @@ T16344.hs:7:46: error:
     • In the second argument of ‘T’, namely ‘Int’
       In the type ‘(T Type Int Bool)’
       In the definition of data constructor ‘MkT’
+      NB: Type ‘T’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17131.hs b/testsuite/tests/dependent/should_fail/T17131.hs
new file mode 100644
index 0000000000..d4294c0216
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17131.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MagicHash, UnboxedTuples, TypeInType, TypeFamilies, TypeOperators #-}
+
+module T17131 where
+
+import GHC.Exts
+
+type family TypeReps xs where
+   TypeReps '[]                 = '[]
+   TypeReps ((a::TYPE k) ': as) = k ': TypeReps as
+
+type family Tuple# xs = (t :: TYPE ('TupleRep (TypeReps xs))) where
+   Tuple# '[a]                 = (# a #)
diff --git a/testsuite/tests/dependent/should_fail/T17131.stderr b/testsuite/tests/dependent/should_fail/T17131.stderr
new file mode 100644
index 0000000000..dd250ed414
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17131.stderr
@@ -0,0 +1,10 @@
+
+T17131.hs:12:34: error:
+    • Expected kind ‘TYPE ('TupleRep (TypeReps xs))’,
+        but ‘(# a #)’ has kind ‘TYPE ('TupleRep '[ 'LiftedRep])’
+    • In the type ‘(# a #)’
+      In the type family declaration for ‘Tuple#’
+      NB: Type ‘Tuple#’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17541.hs b/testsuite/tests/dependent/should_fail/T17541.hs
new file mode 100644
index 0000000000..dcf6e91381
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE
+             MagicHash,
+             FlexibleInstances,
+             MultiParamTypeClasses,
+             TypeFamilies,
+             PolyKinds,
+             DataKinds,
+             FunctionalDependencies,
+             TypeFamilyDependencies #-}
+module T17541 where
+
+import GHC.Prim
+import GHC.Exts
+
+
+type family Rep rep where
+  Rep Int = IntRep
+
+type family Unboxed rep = (urep :: TYPE (Rep rep)) | urep -> rep where
+  Unboxed Int = Int#
diff --git a/testsuite/tests/dependent/should_fail/T17541.stderr b/testsuite/tests/dependent/should_fail/T17541.stderr
new file mode 100644
index 0000000000..e17206c734
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541.stderr
@@ -0,0 +1,10 @@
+
+T17541.hs:20:17: error:
+    • Expected kind ‘TYPE (Rep rep)’,
+        but ‘Int#’ has kind ‘TYPE 'IntRep’
+    • In the type ‘Int#’
+      In the type family declaration for ‘Unboxed’
+      NB: Type ‘Unboxed’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/T17541b.hs b/testsuite/tests/dependent/should_fail/T17541b.hs
new file mode 100644
index 0000000000..6defdf705a
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds, GADTs #-}
+
+module T17541b where
+
+import Data.Kind
+
+data T k :: k -> Type where
+    MkT1 :: T Type Int
+    MkT2 :: T (Type -> Type) Maybe
diff --git a/testsuite/tests/dependent/should_fail/T17541b.stderr b/testsuite/tests/dependent/should_fail/T17541b.stderr
new file mode 100644
index 0000000000..7502f21373
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17541b.stderr
@@ -0,0 +1,10 @@
+
+T17541b.hs:8:20: error:
+    • Expected kind ‘k’, but ‘Int’ has kind ‘*’
+    • In the second argument of ‘T’, namely ‘Int’
+      In the type ‘T Type Int’
+      In the definition of data constructor ‘MkT1’
+      NB: Type ‘T’ was inferred to use visible dependent quantification.
+      Most types with visible dependent quantification are
+      polymorphically recursive and need a standalone kind
+      signature. Perhaps supply one, with StandaloneKindSignatures.
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 97580ce1cd..8ff5a88961 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -57,3 +57,6 @@ test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T16344', normal, compile_fail, [''])
 test('T16344a', normal, compile_fail, [''])
 test('T16418', normal, compile_fail, [''])
+test('T17541', normal, compile_fail, [''])
+test('T17541b', normal, compile_fail, [''])
+test('T17131', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T15789.stderr b/testsuite/tests/polykinds/T15789.stderr
index c0fd4eab34..dc052ceaa7 100644
--- a/testsuite/tests/polykinds/T15789.stderr
+++ b/testsuite/tests/polykinds/T15789.stderr
@@ -4,3 +4,4 @@ T15789.hs:10:80: error:
     • In the first argument of ‘Cat’, namely ‘(forall b. cat b u)’
       In the kind ‘forall (cat :: forall xx. xx -> Type) a.
                    forall b. Cat (forall b. cat b u)’
+      In the data type declaration for ‘Zero’
diff --git a/testsuite/tests/polykinds/T15804.stderr b/testsuite/tests/polykinds/T15804.stderr
index 52262b675f..e89bbf8c80 100644
--- a/testsuite/tests/polykinds/T15804.stderr
+++ b/testsuite/tests/polykinds/T15804.stderr
@@ -2,3 +2,4 @@
 T15804.hs:5:12: error:
     • Expected a type, but ‘a :: k’ has kind ‘k’
     • In the kind ‘(a :: k) -> *’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/polykinds/T15881.stderr b/testsuite/tests/polykinds/T15881.stderr
index 4fde71dab7..8f395735db 100644
--- a/testsuite/tests/polykinds/T15881.stderr
+++ b/testsuite/tests/polykinds/T15881.stderr
@@ -3,3 +3,4 @@ T15881.hs:8:18: error:
     • Occurs check: cannot construct the infinite kind: k0 ~ k0 -> *
     • In the first argument of ‘n’, namely ‘n’
       In the kind ‘n n’
+      In the data type declaration for ‘A’
diff --git a/testsuite/tests/polykinds/T15881a.stderr b/testsuite/tests/polykinds/T15881a.stderr
index 84014c7abc..23f207dff3 100644
--- a/testsuite/tests/polykinds/T15881a.stderr
+++ b/testsuite/tests/polykinds/T15881a.stderr
@@ -2,3 +2,4 @@
 T15881a.hs:8:22: error:
     • Expected a type, but ‘a’ has kind ‘n’
     • In the kind ‘a -> Type’
+      In the data type declaration for ‘A’
diff --git a/testsuite/tests/polykinds/T16263.stderr b/testsuite/tests/polykinds/T16263.stderr
index 821a5fe307..9696f2238d 100644
--- a/testsuite/tests/polykinds/T16263.stderr
+++ b/testsuite/tests/polykinds/T16263.stderr
@@ -1,2 +1,4 @@
 
-T16263.hs:7:1: error: Illegal constraint in a kind: Eq a => *
+T16263.hs:7:1: error:
+    • Illegal constraint in a kind: Eq a => *
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/saks/should_compile/Makefile b/testsuite/tests/saks/should_compile/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/saks/should_compile/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/saks/should_fail/Makefile b/testsuite/tests/saks/should_fail/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk