From bc5873d9a2195eac08a8d78e4562a608fc1eb6ce Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Thu, 5 Dec 2019 16:47:34 +0000 Subject: Warn on inferred polymorphic recursion 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} --- compiler/typecheck/TcClassDcl.hs | 10 +- compiler/typecheck/TcHsType.hs | 3 +- compiler/typecheck/TcTyClsDecls.hs | 125 ++++++++++++++++----- .../tests/dependent/should_fail/T16344.stderr | 4 + testsuite/tests/dependent/should_fail/T17131.hs | 12 ++ .../tests/dependent/should_fail/T17131.stderr | 10 ++ testsuite/tests/dependent/should_fail/T17541.hs | 20 ++++ .../tests/dependent/should_fail/T17541.stderr | 10 ++ testsuite/tests/dependent/should_fail/T17541b.hs | 9 ++ .../tests/dependent/should_fail/T17541b.stderr | 10 ++ testsuite/tests/dependent/should_fail/all.T | 3 + testsuite/tests/polykinds/T15789.stderr | 1 + testsuite/tests/polykinds/T15804.stderr | 1 + testsuite/tests/polykinds/T15881.stderr | 1 + testsuite/tests/polykinds/T15881a.stderr | 1 + testsuite/tests/polykinds/T16263.stderr | 4 +- testsuite/tests/saks/should_compile/Makefile | 3 + testsuite/tests/saks/should_fail/Makefile | 3 + 18 files changed, 191 insertions(+), 39 deletions(-) create mode 100644 testsuite/tests/dependent/should_fail/T17131.hs create mode 100644 testsuite/tests/dependent/should_fail/T17131.stderr create mode 100644 testsuite/tests/dependent/should_fail/T17541.hs create mode 100644 testsuite/tests/dependent/should_fail/T17541.stderr create mode 100644 testsuite/tests/dependent/should_fail/T17541b.hs create mode 100644 testsuite/tests/dependent/should_fail/T17541b.stderr create mode 100644 testsuite/tests/saks/should_compile/Makefile create mode 100644 testsuite/tests/saks/should_fail/Makefile 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 -- cgit v1.2.1