summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/typecheck/TcClassDcl.hs10
-rw-r--r--compiler/typecheck/TcHsType.hs3
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs125
-rw-r--r--testsuite/tests/dependent/should_fail/T16344.stderr4
-rw-r--r--testsuite/tests/dependent/should_fail/T17131.hs12
-rw-r--r--testsuite/tests/dependent/should_fail/T17131.stderr10
-rw-r--r--testsuite/tests/dependent/should_fail/T17541.hs20
-rw-r--r--testsuite/tests/dependent/should_fail/T17541.stderr10
-rw-r--r--testsuite/tests/dependent/should_fail/T17541b.hs9
-rw-r--r--testsuite/tests/dependent/should_fail/T17541b.stderr10
-rw-r--r--testsuite/tests/dependent/should_fail/all.T3
-rw-r--r--testsuite/tests/polykinds/T15789.stderr1
-rw-r--r--testsuite/tests/polykinds/T15804.stderr1
-rw-r--r--testsuite/tests/polykinds/T15881.stderr1
-rw-r--r--testsuite/tests/polykinds/T15881a.stderr1
-rw-r--r--testsuite/tests/polykinds/T16263.stderr4
-rw-r--r--testsuite/tests/saks/should_compile/Makefile3
-rw-r--r--testsuite/tests/saks/should_fail/Makefile3
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 9f688f918a..c4f67bbb64 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -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 $
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
View Lorry Controller Status