Commit 030211d2 authored by Richard Eisenberg's avatar Richard Eisenberg

Kind-check CUSK associated types separately

Previously, we kind-checked associated types while while still
figuring out the kind of a CUSK class. This caused trouble, as
documented in Note [Don't process associated types in kcLHsQTyVars]
in TcTyClsDecls. This commit moves this process after the initial
kind of the class is determined.

Fixes #15142.

Test case: indexed-types/should_compile/T15142.hs
parent 042df603
...@@ -1591,14 +1591,14 @@ kcLHsQTyVars :: Name -- ^ of the thing being checked ...@@ -1591,14 +1591,14 @@ kcLHsQTyVars :: Name -- ^ of the thing being checked
-> TyConFlavour -- ^ What sort of 'TyCon' is being checked -> TyConFlavour -- ^ What sort of 'TyCon' is being checked
-> Bool -- ^ True <=> the decl being checked has a CUSK -> Bool -- ^ True <=> the decl being checked has a CUSK
-> LHsQTyVars GhcRn -> LHsQTyVars GhcRn
-> TcM (Kind, r) -- ^ The result kind, possibly with other info -> TcM Kind -- ^ The result kind
-> TcM (TcTyCon, r) -- ^ A suitably-kinded TcTyCon -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon
kcLHsQTyVars name flav cusk kcLHsQTyVars name flav cusk
user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
, hsq_dependent = dep_names } , hsq_dependent = dep_names }
, hsq_explicit = hs_tvs }) thing_inside , hsq_explicit = hs_tvs }) thing_inside
| cusk | cusk
= do { (scoped_kvs, (tc_tvs, (res_kind, stuff))) = do { (scoped_kvs, (tc_tvs, res_kind))
<- solveEqualities $ <- solveEqualities $
tcImplicitQTKBndrs skol_info kv_ns $ tcImplicitQTKBndrs skol_info kv_ns $
kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
...@@ -1645,10 +1645,10 @@ kcLHsQTyVars name flav cusk ...@@ -1645,10 +1645,10 @@ kcLHsQTyVars name flav cusk
, ppr tc_tvs, ppr (mkTyConKind final_binders res_kind) , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
, ppr qkvs, ppr final_binders ] , ppr qkvs, ppr final_binders ]
; return (tycon, stuff) } ; return tycon }
| otherwise | otherwise
= do { (scoped_kvs, (tc_tvs, (res_kind, stuff))) = do { (scoped_kvs, (tc_tvs, res_kind))
-- Why kcImplicitTKBndrs which uses newSigTyVar? -- Why kcImplicitTKBndrs which uses newSigTyVar?
-- See Note [Kind generalisation and sigTvs] -- See Note [Kind generalisation and sigTvs]
<- kcImplicitTKBndrs kv_ns $ <- kcImplicitTKBndrs kv_ns $
...@@ -1664,7 +1664,7 @@ kcLHsQTyVars name flav cusk ...@@ -1664,7 +1664,7 @@ kcLHsQTyVars name flav cusk
; 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 dep_names
, ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ] , ppr tc_tvs, ppr (mkTyConKind tc_binders res_kind) ]
; return (tycon, stuff) } ; return tycon }
where where
open_fam = tcFlavourIsOpen flav open_fam = tcFlavourIsOpen flav
skol_info = TyConSkol flav name skol_info = TyConSkol flav name
......
...@@ -460,6 +460,29 @@ to Note [Single function non-recursive binding special-case]: ...@@ -460,6 +460,29 @@ to Note [Single function non-recursive binding special-case]:
Unfortunately this requires reworking a bit of the code in Unfortunately this requires reworking a bit of the code in
'kcLTyClDecl' so I've decided to punt unless someone shouts about it. 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
Note [Don't process associated types in kcLHsQTyVars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Previously, we processed associated types in the thing_inside in kcLHsQTyVars,
but this was wrong -- we want to do ATs sepearately.
The consequence for not doing it this way is #15142:
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
We assign k a kind kappa[1]. When checking the tuple (k, Type), we try to unify
kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring
`tuple` into scope. Thus, when we check ListToTuple, kappa[1] still hasn't
unified with Type. And then, when we generalize the kind of ListToTuple (which
indeed has a CUSK, according to the rules), we skolemize the free metavariable
kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple,
because the solveEqualities in kcLHsQTyVars is at TcLevel 1 and so kappa[1]
will unify with Type.
Bottom line: as associated types should have no effect on a CUSK enclosing class,
we move processing them to a separate action, run after the outer kind has
been generalized.
-} -}
kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon] kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
...@@ -603,22 +626,22 @@ getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon] ...@@ -603,22 +626,22 @@ getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon]
getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
= do { let cusk = hsDeclHasCusk decl = do { let cusk = hsDeclHasCusk decl
; (tycon, inner_tcs) <- ; tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
kcLHsQTyVars name ClassFlavour cusk ktvs $ return constraintKind
do { inner_tcs <- getFamDeclInitialKinds (Just cusk) ats -- See Note [Don't process associated types in kcLHsQTyVars]
; return (constraintKind, inner_tcs) } ; inner_tcs <- tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $
getFamDeclInitialKinds (Just cusk) ats
; return (tycon : inner_tcs) } ; return (tycon : inner_tcs) }
getInitialKind decl@(DataDecl { tcdLName = L _ name getInitialKind decl@(DataDecl { tcdLName = L _ name
, tcdTyVars = ktvs , tcdTyVars = ktvs
, tcdDataDefn = HsDataDefn { dd_kindSig = m_sig , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
, dd_ND = new_or_data } }) , dd_ND = new_or_data } })
= do { (tycon, _) <- = do { tycon <-
kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $ kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
do { res_k <- case m_sig of case m_sig of
Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
Nothing -> return liftedTypeKind Nothing -> return liftedTypeKind
; return (res_k, ()) }
; return [tycon] } ; return [tycon] }
getInitialKind (FamDecl { tcdFam = decl }) getInitialKind (FamDecl { tcdFam = decl })
...@@ -628,12 +651,10 @@ getInitialKind (FamDecl { tcdFam = decl }) ...@@ -628,12 +651,10 @@ getInitialKind (FamDecl { tcdFam = decl })
getInitialKind decl@(SynDecl { tcdLName = L _ name getInitialKind decl@(SynDecl { tcdLName = L _ name
, tcdTyVars = ktvs , tcdTyVars = ktvs
, tcdRhs = rhs }) , tcdRhs = rhs })
= do { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour = do { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) ktvs $
(hsDeclHasCusk decl) ktvs $ case kind_annotation rhs of
do { res_k <- case kind_annotation rhs of Nothing -> newMetaKindVar
Nothing -> newMetaKindVar Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
; return (res_k, ()) }
; return [tycon] } ; return [tycon] }
where where
-- Keep this synchronized with 'hsDeclHasCusk'. -- Keep this synchronized with 'hsDeclHasCusk'.
...@@ -659,17 +680,15 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name ...@@ -659,17 +680,15 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name
, fdTyVars = ktvs , fdTyVars = ktvs
, fdResultSig = L _ resultSig , fdResultSig = L _ resultSig
, fdInfo = info }) , fdInfo = info })
= do { (tycon, _) <- = do { tycon <- kcLHsQTyVars name flav cusk ktvs $
kcLHsQTyVars name flav cusk ktvs $ case resultSig of
do { res_k <- case resultSig of KindSig _ ki -> tcLHsKindSig ctxt ki
KindSig _ ki -> tcLHsKindSig ctxt ki TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki _ -- open type families have * return kind by default
_ -- open type families have * return kind by default | tcFlavourIsOpen flav -> return liftedTypeKind
| tcFlavourIsOpen flav -> return liftedTypeKind -- closed type families have their return kind inferred
-- closed type families have their return kind inferred -- by default
-- by default | otherwise -> newMetaKindVar
| otherwise -> newMetaKindVar
; return (res_k, ()) }
; return tycon } ; return tycon }
where where
cusk = famDeclHasCusk mb_cusk decl cusk = famDeclHasCusk mb_cusk decl
......
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module T15142 where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
class C (a :: Type) (b :: k) where
type T b
...@@ -287,3 +287,4 @@ test('T14164', normal, compile, ['']) ...@@ -287,3 +287,4 @@ test('T14164', normal, compile, [''])
test('T15318', normal, compile, ['']) test('T15318', normal, compile, [''])
test('T15322', normal, compile, ['']) test('T15322', normal, compile, [''])
test('T15322a', normal, compile_fail, ['']) test('T15322a', normal, compile_fail, [''])
test('T15142', normal, compile, [''])
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