Commit 2d1b9619 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

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}
parent f80c4a66
Pipeline #13677 failed with stages
in 599 minutes and 35 seconds
......@@ -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),
......
......@@ -1985,7 +1985,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 $
......
......@@ -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)
......
......@@ -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.
{-# 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 #)
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.
{-# 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#
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.
{-# LANGUAGE PolyKinds, GADTs #-}
module T17541b where
import Data.Kind
data T k :: k -> Type where
MkT1 :: T Type Int
MkT2 :: T (Type -> Type) Maybe
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.
......@@ -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, [''])
......@@ -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’
......@@ -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’
......@@ -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’
......@@ -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’
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’
TOP=../../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/test.mk
TOP=../../..
include $(TOP)/mk/boilerplate.mk
include $(TOP)/mk/test.mk
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment