Commit 1f5cc9dc authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Stop inferring over-polymorphic kinds

Before this patch GHC was trying to be too clever
(Trac #16344); it succeeded in kind-checking this
polymorphic-recursive declaration

    data T ka (a::ka) b
      = MkT (T Type           Int   Bool)
            (T (Type -> Type) Maybe Bool)

As Note [No polymorphic recursion] discusses, the "solution" was
horribly fragile.  So this patch deletes the key lines in
TcHsType, and a wodge of supporting stuff in the renamer.

There were two regressions, both the same: a closed type family
decl like this (T12785b) does not have a CUSK:
  type family Payload (n :: Peano) (s :: HTree n x) where
    Payload Z (Point a) = a
    Payload (S n) (a `Branch` stru) = a

To kind-check the equations we need a dependent kind for
Payload, and we don't get that any more.  Solution: make it
a CUSK by giving the result kind -- probably a good thing anyway.

The other case (T12442) was very similar: a close type family
declaration without a CUSK.
parent 2762f94d
...@@ -43,7 +43,6 @@ import Id ...@@ -43,7 +43,6 @@ import Id
import Name hiding( isVarOcc, isTcOcc, varName, tcName ) import Name hiding( isVarOcc, isTcOcc, varName, tcName )
import THNames import THNames
import NameEnv import NameEnv
import NameSet
import TcType import TcType
import TyCon import TyCon
import TysWiredIn import TysWiredIn
...@@ -392,9 +391,7 @@ repFamilyDecl decl@(dL->L loc (FamilyDecl { fdInfo = info ...@@ -392,9 +391,7 @@ repFamilyDecl decl@(dL->L loc (FamilyDecl { fdInfo = info
, fdInjectivityAnn = injectivity })) , fdInjectivityAnn = injectivity }))
= do { tc1 <- lookupLOcc tc -- See note [Binders and occurrences] = do { tc1 <- lookupLOcc tc -- See note [Binders and occurrences]
; let mkHsQTvs :: [LHsTyVarBndr GhcRn] -> LHsQTyVars GhcRn ; let mkHsQTvs :: [LHsTyVarBndr GhcRn] -> LHsQTyVars GhcRn
mkHsQTvs tvs = HsQTvs { hsq_ext = HsQTvsRn mkHsQTvs tvs = HsQTvs { hsq_ext = []
{ hsq_implicit = []
, hsq_dependent = emptyNameSet }
, hsq_explicit = tvs } , hsq_explicit = tvs }
resTyVar = case resultSig of resTyVar = case resultSig of
TyVarSig _ bndr -> mkHsQTvs [bndr] TyVarSig _ bndr -> mkHsQTvs [bndr]
...@@ -569,9 +566,7 @@ repTyFamEqn (HsIB { hsib_ext = var_names ...@@ -569,9 +566,7 @@ repTyFamEqn (HsIB { hsib_ext = var_names
, feqn_fixity = fixity , feqn_fixity = fixity
, feqn_rhs = rhs }}) , feqn_rhs = rhs }})
= do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences] = do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences]
; let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn ; let hs_tvs = HsQTvs { hsq_ext = var_names
{ hsq_implicit = var_names
, hsq_dependent = emptyNameSet } -- Yuk
, hsq_explicit = fromMaybe [] mb_bndrs } , hsq_explicit = fromMaybe [] mb_bndrs }
; addTyClTyVarBinds hs_tvs $ \ _ -> ; addTyClTyVarBinds hs_tvs $ \ _ ->
do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName
...@@ -610,9 +605,7 @@ repDataFamInstD (DataFamInstDecl { dfid_eqn = ...@@ -610,9 +605,7 @@ repDataFamInstD (DataFamInstDecl { dfid_eqn =
, feqn_fixity = fixity , feqn_fixity = fixity
, feqn_rhs = defn }})}) , feqn_rhs = defn }})})
= do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences] = do { tc <- lookupLOcc tc_name -- See note [Binders and occurrences]
; let hs_tvs = HsQTvs { hsq_ext = HsQTvsRn ; let hs_tvs = HsQTvs { hsq_ext = var_names
{ hsq_implicit = var_names
, hsq_dependent = emptyNameSet } -- Yuk
, hsq_explicit = fromMaybe [] mb_bndrs } , hsq_explicit = fromMaybe [] mb_bndrs }
; addTyClTyVarBinds hs_tvs $ \ _ -> ; addTyClTyVarBinds hs_tvs $ \ _ ->
do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName do { mb_bndrs1 <- repMaybeList tyVarBndrQTyConName
...@@ -1052,7 +1045,7 @@ addTyVarBinds :: LHsQTyVars GhcRn -- the binders to be added ...@@ -1052,7 +1045,7 @@ addTyVarBinds :: LHsQTyVars GhcRn -- the binders to be added
-- gensym a list of type variables and enter them into the meta environment; -- gensym a list of type variables and enter them into the meta environment;
-- the computations passed as the second argument is executed in that extended -- the computations passed as the second argument is executed in that extended
-- meta environment and gets the *new* names on Core-level as an argument -- meta environment and gets the *new* names on Core-level as an argument
addTyVarBinds (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_tvs} addTyVarBinds (HsQTvs { hsq_ext = imp_tvs
, hsq_explicit = exp_tvs }) , hsq_explicit = exp_tvs })
thing_inside thing_inside
= addSimpleTyVarBinds imp_tvs $ = addSimpleTyVarBinds imp_tvs $
......
...@@ -1474,7 +1474,7 @@ instance ToHie (TVScoped (LHsTyVarBndr GhcRn)) where ...@@ -1474,7 +1474,7 @@ instance ToHie (TVScoped (LHsTyVarBndr GhcRn)) where
XTyVarBndr _ -> [] XTyVarBndr _ -> []
instance ToHie (TScoped (LHsQTyVars GhcRn)) where instance ToHie (TScoped (LHsQTyVars GhcRn)) where
toHie (TS sc (HsQTvs (HsQTvsRn implicits _) vars)) = concatM $ toHie (TS sc (HsQTvs implicits vars)) = concatM $
[ pure $ bindingsOnly bindings [ pure $ bindingsOnly bindings
, toHie $ tvScopes sc NoScope vars , toHie $ tvScopes sc NoScope vars
] ]
......
...@@ -20,7 +20,7 @@ HsTypes: Abstract syntax: user-defined types ...@@ -20,7 +20,7 @@ HsTypes: Abstract syntax: user-defined types
module HsTypes ( module HsTypes (
HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind, HsType(..), NewHsTypeX(..), LHsType, HsKind, LHsKind,
HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..), HsTyVarBndr(..), LHsTyVarBndr, ForallVisFlag(..),
LHsQTyVars(..), HsQTvsRn(..), LHsQTyVars(..),
HsImplicitBndrs(..), HsImplicitBndrs(..),
HsWildCardBndrs(..), HsWildCardBndrs(..),
LHsSigType, LHsSigWcType, LHsWcType, LHsSigType, LHsSigWcType, LHsWcType,
...@@ -79,7 +79,6 @@ import HsLit () -- for instances ...@@ -79,7 +79,6 @@ import HsLit () -- for instances
import Id ( Id ) import Id ( Id )
import Name( Name ) import Name( Name )
import RdrName ( RdrName ) import RdrName ( RdrName )
import NameSet ( NameSet, emptyNameSet )
import DataCon( HsSrcBang(..), HsImplBang(..), import DataCon( HsSrcBang(..), HsImplBang(..),
SrcStrictness(..), SrcUnpackedness(..) ) SrcStrictness(..), SrcUnpackedness(..) )
import TysPrim( funTyConName ) import TysPrim( funTyConName )
...@@ -322,21 +321,13 @@ data LHsQTyVars pass -- See Note [HsType binders] ...@@ -322,21 +321,13 @@ data LHsQTyVars pass -- See Note [HsType binders]
} }
| XLHsQTyVars (XXLHsQTyVars pass) | XLHsQTyVars (XXLHsQTyVars pass)
data HsQTvsRn type HsQTvsRn = [Name] -- Implicit variables
= HsQTvsRn -- For example, in data T (a :: k1 -> k2) = ...
{ hsq_implicit :: [Name] -- the 'a' is explicit while 'k1', 'k2' are implicit
-- Implicit (dependent) variables
, hsq_dependent :: NameSet type instance XHsQTvs GhcPs = NoExt
-- Which members of hsq_explicit are dependent; that is, type instance XHsQTvs GhcRn = HsQTvsRn
-- mentioned in the kind of a later hsq_explicit, type instance XHsQTvs GhcTc = HsQTvsRn
-- or mentioned in a kind in the scope of this HsQTvs
-- See Note [Dependent LHsQTyVars] in TcHsType
} deriving Data
type instance XHsQTvs GhcPs = NoExt
type instance XHsQTvs GhcRn = HsQTvsRn
type instance XHsQTvs GhcTc = HsQTvsRn
type instance XXLHsQTyVars (GhcPass _) = NoExt type instance XXLHsQTyVars (GhcPass _) = NoExt
...@@ -347,11 +338,12 @@ hsQTvExplicit :: LHsQTyVars pass -> [LHsTyVarBndr pass] ...@@ -347,11 +338,12 @@ hsQTvExplicit :: LHsQTyVars pass -> [LHsTyVarBndr pass]
hsQTvExplicit = hsq_explicit hsQTvExplicit = hsq_explicit
emptyLHsQTvs :: LHsQTyVars GhcRn emptyLHsQTvs :: LHsQTyVars GhcRn
emptyLHsQTvs = HsQTvs (HsQTvsRn [] emptyNameSet) [] emptyLHsQTvs = HsQTvs { hsq_ext = [], hsq_explicit = [] }
isEmptyLHsQTvs :: LHsQTyVars GhcRn -> Bool isEmptyLHsQTvs :: LHsQTyVars GhcRn -> Bool
isEmptyLHsQTvs (HsQTvs (HsQTvsRn [] _) []) = True isEmptyLHsQTvs (HsQTvs { hsq_ext = imp, hsq_explicit = exp })
isEmptyLHsQTvs _ = False = null imp && null exp
isEmptyLHsQTvs _ = False
------------------------------------------------ ------------------------------------------------
-- HsImplicitBndrs -- HsImplicitBndrs
...@@ -997,7 +989,7 @@ hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs) ...@@ -997,7 +989,7 @@ hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs)
hsAllLTyVarNames :: LHsQTyVars GhcRn -> [Name] hsAllLTyVarNames :: LHsQTyVars GhcRn -> [Name]
-- All variables -- All variables
hsAllLTyVarNames (HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kvs } hsAllLTyVarNames (HsQTvs { hsq_ext = kvs
, hsq_explicit = tvs }) , hsq_explicit = tvs })
= kvs ++ hsLTyVarNames tvs = kvs ++ hsLTyVarNames tvs
hsAllLTyVarNames (XLHsQTyVars _) = panic "hsAllLTyVarNames" hsAllLTyVarNames (XLHsQTyVars _) = panic "hsAllLTyVarNames"
......
...@@ -2166,9 +2166,7 @@ rnConDecl decl@(ConDeclGADT { con_names = names ...@@ -2166,9 +2166,7 @@ rnConDecl decl@(ConDeclGADT { con_names = names
-- See Note [GADT abstract syntax] in HsDecls -- See Note [GADT abstract syntax] in HsDecls
(PrefixCon arg_tys, final_res_ty) (PrefixCon arg_tys, final_res_ty)
new_qtvs = HsQTvs { hsq_ext = HsQTvsRn new_qtvs = HsQTvs { hsq_ext = implicit_tkvs
{ hsq_implicit = implicit_tkvs
, hsq_dependent = emptyNameSet }
, hsq_explicit = explicit_tkvs } , hsq_explicit = explicit_tkvs }
; traceRn "rnConDecl2" (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs) ; traceRn "rnConDecl2" (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
......
...@@ -822,11 +822,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside ...@@ -822,11 +822,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
-- body kvs, as mandated by -- body kvs, as mandated by
-- Note [Ordering of implicit variables] -- Note [Ordering of implicit variables]
implicit_kvs = filter_occs bndrs kv_occs implicit_kvs = filter_occs bndrs kv_occs
-- dep_bndrs is the subset of bndrs that are dependent del = deleteBys eqLocated
-- i.e. appear in bndr/body_kv_occs
-- Can't use implicit_kvs because we've deleted bndrs from that!
dep_bndrs = filter (`elemRdr` kv_occs) bndrs
del = deleteBys eqLocated
all_bound_on_lhs = null ((body_kv_occs `del` bndrs) `del` bndr_kv_occs) all_bound_on_lhs = null ((body_kv_occs `del` bndrs) `del` bndr_kv_occs)
; traceRn "checkMixedVars3" $ ; traceRn "checkMixedVars3" $
...@@ -841,10 +837,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside ...@@ -841,10 +837,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
; bindLocalNamesFV implicit_kv_nms $ ; bindLocalNamesFV implicit_kv_nms $
bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \ rn_bndrs -> bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \ rn_bndrs ->
do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs) do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$ ppr rn_bndrs)
; dep_bndr_nms <- mapM (lookupLocalOccRn . unLoc) dep_bndrs ; thing_inside (HsQTvs { hsq_ext = implicit_kv_nms
; thing_inside (HsQTvs { hsq_ext = HsQTvsRn
{ hsq_implicit = implicit_kv_nms
, hsq_dependent = mkNameSet dep_bndr_nms }
, hsq_explicit = rn_bndrs }) , hsq_explicit = rn_bndrs })
all_bound_on_lhs } } all_bound_on_lhs } }
...@@ -879,9 +872,6 @@ Then: ...@@ -879,9 +872,6 @@ Then:
* We want to quantify add implicit bindings for implicit_kvs * We want to quantify add implicit bindings for implicit_kvs
* The "dependent" bndrs (hsq_dependent) are the subset of
bndrs that are free in bndr_kv_occs or body_kv_occs
* If implicit_body_kvs is non-empty, then there is a kind variable * If implicit_body_kvs is non-empty, then there is a kind variable
mentioned in the kind signature that is not bound "on the left". mentioned in the kind signature that is not bound "on the left".
That's one of the rules for a CUSK, so we pass that info on That's one of the rules for a CUSK, so we pass that info on
......
...@@ -91,7 +91,7 @@ import ConLike ...@@ -91,7 +91,7 @@ import ConLike
import DataCon import DataCon
import Class import Class
import Name import Name
import NameSet -- import NameSet
import VarEnv import VarEnv
import TysWiredIn import TysWiredIn
import BasicTypes import BasicTypes
...@@ -1611,48 +1611,6 @@ addTypeCtxt (L _ ty) thing ...@@ -1611,48 +1611,6 @@ addTypeCtxt (L _ ty) thing
%* * %* *
%************************************************************************ %************************************************************************
Note [Dependent LHsQTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We track (in the renamer) which explicitly bound variables in a
LHsQTyVars are manifestly dependent; only precisely these variables
may be used within the LHsQTyVars. We must do this so that kcLHsQTyVars
can produce the right TyConBinders, and tell Anon vs. Required.
Example data T k1 (a:k1) (b:k2) c
= MkT (Proxy a) (Proxy b) (Proxy c)
Here
(a:k1),(b:k2),(c:k3)
are Anon (explicitly specified as a binder, not used
in the kind of any other binder
k1 is Required (explicitly specifed as a binder, but used
in the kind of another binder i.e. dependently)
k2 is Specified (not explicitly bound, but used in the kind
of another binder)
k3 in Inferred (not lexically in scope at all, but inferred
by kind inference)
and
T :: forall {k3} k1. forall k3 -> k1 -> k2 -> k3 -> *
See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
in TyCoRep.
kcLHsQTyVars uses the hsq_dependent field to decide whether
k1, a, b, c should be Required or Anon.
Earlier, thought it would work simply to do a free-variable check
during kcLHsQTyVars, but this is bogus, because there may be
unsolved equalities about. And we don't want to eagerly solve the
equalities, because we may get further information after
kcLHsQTyVars is called. (Recall that kcLHsQTyVars is called
only from getInitialKind.)
This is what implements the rule that all variables intended to be
dependent must be manifestly so.
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 [Keeping scoped variables in order: Explicit] Note [Keeping scoped variables in order: Explicit]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the user writes `forall a b c. blah`, we bring a, b, and c into When the user writes `forall a b c. blah`, we bring a, b, and c into
...@@ -1822,8 +1780,7 @@ kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk ...@@ -1822,8 +1780,7 @@ kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
------------------------------ ------------------------------
kcLHsQTyVars_Cusk name flav kcLHsQTyVars_Cusk name flav
(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns (HsQTvs { hsq_ext = kv_ns
, hsq_dependent = dep_names }
, hsq_explicit = hs_tvs }) thing_inside , hsq_explicit = hs_tvs }) thing_inside
-- CUSK case -- CUSK case
-- See note [Required, Specified, and Inferred for types] in TcTyClsDecls -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
...@@ -1874,7 +1831,6 @@ kcLHsQTyVars_Cusk name flav ...@@ -1874,7 +1831,6 @@ kcLHsQTyVars_Cusk name flav
vcat [ text "name" <+> ppr name vcat [ text "name" <+> ppr name
, text "kv_ns" <+> ppr kv_ns , text "kv_ns" <+> ppr kv_ns
, text "hs_tvs" <+> ppr hs_tvs , text "hs_tvs" <+> ppr hs_tvs
, text "dep_names" <+> ppr dep_names
, text "scoped_kvs" <+> ppr scoped_kvs , text "scoped_kvs" <+> ppr scoped_kvs
, text "tc_tvs" <+> ppr tc_tvs , text "tc_tvs" <+> ppr tc_tvs
, text "res_kind" <+> ppr res_kind , text "res_kind" <+> ppr res_kind
...@@ -1895,8 +1851,7 @@ kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" ...@@ -1895,8 +1851,7 @@ kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
------------------------------ ------------------------------
kcLHsQTyVars_NonCusk name flav kcLHsQTyVars_NonCusk name flav
(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns (HsQTvs { hsq_ext = kv_ns
, hsq_dependent = dep_names }
, hsq_explicit = hs_tvs }) thing_inside , hsq_explicit = hs_tvs }) thing_inside
-- Non_CUSK case -- Non_CUSK case
-- See note [Required, Specified, and Inferred for types] in TcTyClsDecls -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
...@@ -1913,22 +1868,26 @@ kcLHsQTyVars_NonCusk name flav ...@@ -1913,22 +1868,26 @@ kcLHsQTyVars_NonCusk name flav
-- might unify with kind vars in other types in a mutually -- might unify with kind vars in other types in a mutually
-- recursive group. -- recursive group.
-- See Note [Inferring kinds for type declarations] in TcTyClsDecls -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs
tc_binders = mkAnonTyConBinders VisArg tc_tvs
-- Also, note that tc_binders has the tyvars from only the -- Also, note that tc_binders has the tyvars from only the
-- user-written tyvarbinders. See S1 in Note [How TcTyCons work] -- user-written tyvarbinders. See S1 in Note [How TcTyCons work]
-- in TcTyClsDecls -- in TcTyClsDecls
--
-- mkAnonTyConBinder: see Note [No polymorphic recursion]
all_tv_prs = (kv_ns `zip` scoped_kvs) ++ all_tv_prs = (kv_ns `zip` scoped_kvs) ++
(hsLTyVarNames hs_tvs `zip` tc_tvs) (hsLTyVarNames hs_tvs `zip` tc_tvs)
-- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification
-- variables, hence the need to zip here. Ditto bindExplicit.. -- variables, hence the need to zip here. Ditto bindExplicit..
-- See TcMType Note [Unification variables need fresh Names] -- See TcMType Note [Unification variables need fresh Names]
tycon = mkTcTyCon name tc_binders res_kind all_tv_prs tycon = mkTcTyCon name tc_binders res_kind all_tv_prs
False -- not yet generalised False -- not yet generalised
flav flav
; traceTc "kcLHsQTyVars: not-cusk" $ ; traceTc "kcLHsQTyVars: not-cusk" $
vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names vcat [ ppr name, ppr kv_ns, ppr hs_tvs
, ppr scoped_kvs , ppr scoped_kvs
, ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
; return tycon } ; return tycon }
...@@ -1936,18 +1895,57 @@ kcLHsQTyVars_NonCusk name flav ...@@ -1936,18 +1895,57 @@ kcLHsQTyVars_NonCusk name flav
ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
| otherwise = AnyKind | otherwise = AnyKind
mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
-- See Note [Dependent LHsQTyVars]
mk_tc_binder hs_tv tv
| hsLTyVarName hs_tv `elemNameSet` dep_names
= mkNamedTyConBinder Required tv
| otherwise
= mkAnonTyConBinder VisArg tv
kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
{- Note [Kind-checking tyvar binders for associated types] {- Note [No polymorphic recursion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Should this kind-check?
data T ka (a::ka) b = MkT (T Type Int Bool)
(T (Type -> Type) Maybe Bool)
Notice that T is used at two different kinds in its RHS. No!
This should not kind-check. Polymorphic recursion is known to
be a tough nut.
Previously, we laboriously (with help from the renamer)
tried to give T the polymoprhic kind
T :: forall ka -> ka -> kappa -> Type
where kappa is a unification variable, even in the getInitialKinds
phase (which is what kcLHsQTyVars_NonCusk is all about). But
that is dangerously fragile (see the ticket).
Solution: make kcLHsQTyVars_NonCusk give T a straightforward
monomorphic kind, with no quantification whatsoever. That's why
we use mkAnonTyConBinder for all arguments when figuring out
tc_binders.
But notice that (Trac #16322 comment:3)
* The algorithm successfully kind-checks this declaration:
data T2 ka (a::ka) = MkT2 (T2 Type a)
Starting with (getInitialKinds)
T2 :: (kappa1 :: kappa2 :: *) -> (kappa3 :: kappa4 :: *) -> *
we get
kappa4 := kappa1 -- from the (a:ka) kind signature
kappa1 := Type -- From application T2 Type
These constraints are soluble so generaliseTcTyCon gives
T2 :: forall (k::Type) -> k -> *
But now the /typechecking/ (aka desugaring, tcTyClDecl) phase
fails, because the call (T2 Type a) in the RHS is ill-kinded.
We'd really prefer all errors to show up in the kind checking
phase.
* This algorithm still accepts (in all phases)
data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
although T3 is really polymorphic-recursive too.
Perhaps we should somehow reject that.
Note [Kind-checking tyvar binders for associated types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When kind-checking the type-variable binders for associated When kind-checking the type-variable binders for associated
data/newtype decls data/newtype decls
......
...@@ -1154,7 +1154,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs ...@@ -1154,7 +1154,7 @@ kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
kcConDecl (ConDeclGADT { con_names = names kcConDecl (ConDeclGADT { con_names = names
, con_qvars = qtvs, con_mb_cxt = cxt , con_qvars = qtvs, con_mb_cxt = cxt
, con_args = args, con_res_ty = res_ty }) , con_args = args, con_res_ty = res_ty })
| HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms } | HsQTvs { hsq_ext = implicit_tkv_nms
, hsq_explicit = explicit_tkv_nms } <- qtvs , hsq_explicit = explicit_tkv_nms } <- qtvs
= -- Even though the data constructor's type is closed, we = -- Even though the data constructor's type is closed, we
-- must still kind-check the type, because that may influence -- must still kind-check the type, because that may influence
...@@ -1492,7 +1492,7 @@ tcDefaultAssocDecl _ (d1:_:_) ...@@ -1492,7 +1492,7 @@ tcDefaultAssocDecl _ (d1:_:_)
tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
, feqn_pats = hs_tvs , feqn_pats = hs_tvs
, feqn_rhs = hs_rhs_ty })] , feqn_rhs = hs_rhs_ty })]
| HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars} | HsQTvs { hsq_ext = imp_vars
, hsq_explicit = exp_vars } <- hs_tvs , hsq_explicit = exp_vars } <- hs_tvs
= -- See Note [Type-checking default assoc decls] = -- See Note [Type-checking default assoc decls]
setSrcSpan loc $ setSrcSpan loc $
...@@ -2281,7 +2281,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl ...@@ -2281,7 +2281,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
, con_qvars = qtvs , con_qvars = qtvs
, con_mb_cxt = cxt, con_args = hs_args , con_mb_cxt = cxt, con_args = hs_args
, con_res_ty = hs_res_ty }) , con_res_ty = hs_res_ty })
| HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms } | HsQTvs { hsq_ext = implicit_tkv_nms
, hsq_explicit = explicit_tkv_nms } <- qtvs , hsq_explicit = explicit_tkv_nms } <- qtvs
= addErrCtxt (dataConCtxtName names) $ = addErrCtxt (dataConCtxtName names) $
do { traceTc "tcConDecl 1 gadt" (ppr names) do { traceTc "tcConDecl 1 gadt" (ppr names)
......
...@@ -33,7 +33,8 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where ...@@ -33,7 +33,8 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
data instance Sing (elem :: EffElem x a xs) where data instance Sing (elem :: EffElem x a xs) where
SHere :: Sing Here SHere :: Sing Here
type family UpdateResTy b t (xs :: [EFFECT]) (elem :: EffElem e a xs) type family UpdateResTy (b :: Type) (t :: Type)
(xs :: [EFFECT]) (elem :: EffElem e a xs)
(thing :: e @@ a @@ b @@ t) :: [EFFECT] where (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
......
...@@ -20,7 +20,9 @@ type DComp a ...@@ -20,7 +20,9 @@ type DComp a
(x :: a) = (x :: a) =
f (g x) f (g x)
type family ElimList a -- Ensure that ElimList has a CUSK, beuas it is
-- is used polymorphically its RHS (c.f. Trac #16344)
type family ElimList (a :: Type)
(p :: [a] -> Type) (p :: [a] -> Type)
(s :: [a]) (s :: [a])
(pNil :: p '[]) (pNil :: p '[])
......
{-# LANGUAGE TypeInType, GADTs, KindSignatures #-}
module T16344 where
import Data.Kind
-- This one is accepted, even though it is polymorphic-recursive.
-- See Note [No polymorphic recursion] in TcHsType
data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)
...@@ -68,3 +68,5 @@ test('T14729kind', normal, ghci_script, ['T14729kind.script']) ...@@ -68,3 +68,5 @@ test('T14729kind', normal, ghci_script, ['T14729kind.script'])
test('T16326_Compile1', normal, compile, ['']) test('T16326_Compile1', normal, compile, [''])
test('T16326_Compile2', normal, compile, ['']) test('T16326_Compile2', normal, compile, [''])
test('T16391a', normal, compile, ['']) test('T16391a', normal, compile, [''])
test('T16344b', normal, compile, [''])
{-# LANGUAGE TypeInType, KindSignatures #-}
module T16344 where
import Data.Kind
data T ka (a::ka) b = MkT (T Type Int Bool)
(T (Type -> Type) Maybe Bool)
T16344.hs:7:46: error:
• Expected kind ‘ka’, but ‘Int’ has kind ‘*’
• In the second argument of ‘T’, namely ‘Int’
In the type ‘(T Type Int Bool)’
In the definition of data constructor ‘MkT’
{-# LANGUAGE TypeInType, KindSignatures #-}
module T16344 where
import Data.Kind
-- This one is rejected, but in the typechecking phase
-- which is a bit nasty.
-- See Note [No polymorphic recursion] in TcHsType
data T2 ka (a::ka) = MkT2 (T2 Type a)
T16344a.hs:11:36: error:
• Expected a type, but ‘a’ has kind ‘ka’
• In the second argument of ‘T2’, namely ‘a’
In the type ‘(T2 Type a)’
In the definition of data constructor ‘MkT2’
...@@ -53,3 +53,5 @@ test('T16326_Fail10', normal, compile_fail, ['']) ...@@ -53,3 +53,5 @@ test('T16326_Fail10', normal, compile_fail, [''])
test('T16326_Fail11', normal, compile_fail, ['']) test('T16326_Fail11', normal, compile_fail, [''])
test('T16326_Fail12', normal, compile_fail, ['']) test('T16326_Fail12', normal, compile_fail, [''])
test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps']) test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
test('T16344', normal, compile_fail, [''])
test('T16344a', normal, compile_fail, [''])
...@@ -68,10 +68,7 @@ ...@@ -68,10 +68,7 @@
({ DumpRenamedAst.hs:9:6-10 } ({ DumpRenamedAst.hs:9:6-10 }
{Name: DumpRenamedAst.Peano}) {Name: DumpRenamedAst.Peano})
(HsQTvs (HsQTvs
(HsQTvsRn []
[]
{NameSet:
[]})
[]) [])