Commit 913287a0 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Fix scoping of TyCon binders in TcTyClsDecls

This patch fixes #17566 by refactoring the way we decide the final
identity of the tyvars in the TyCons of a possibly-recursive nest
of type and class decls, possibly with associated types.

It's all laid out in
  Note [Swizzling the tyvars before generaliseTcTyCon]

Main changes:

* We have to generalise each decl (with its associated types)
  all at once: TcTyClsDecls.generaliseTyClDecl

* The main new work is done in TcTyClsDecls.swizzleTcTyConBndrs

* The mysterious TcHsSyn.zonkRecTyVarBndrs dies altogether

Other smaller things:

* A little refactoring, moving bindTyClTyVars from tcTyClDecl1
  to tcDataDefn, tcSynRhs, etc.  Clearer, reduces the number of
  parameters

* Reduce the amount of swizzling required.
  Specifically, bindExplicitTKBndrs_Q_Tv doesn't need
    to clone a new Name for the TyVarTv, and not
    cloning means that in the vasly common case,
    swizzleTyConBndrs is a no-op

  In detail:
    Rename newTyVarTyVar --> cloneTyVarTyVar
    Add newTyVarTyTyVar that doesn't clone
    Use the non-cloning newTyVarTyVar in
       bindExplicitTKBndrs_Q_Tv
       Rename newFlexiKindedTyVarTyVar
           --> cloneFlexiKindedTyVarTyVar

* Define new utility function and use it
     HsDecls.familyDeclName ::
        FamilyDecl (GhcPass p) -> IdP (GhcPass p)

Updates haddock submodule.
parent cd110423
......@@ -83,7 +83,7 @@ module GHC.Hs.Decls (
RoleAnnotDecl(..), LRoleAnnotDecl, roleAnnotDeclName,
-- ** Injective type families
FamilyResultSig(..), LFamilyResultSig, InjectivityAnn(..), LInjectivityAnn,
resultVariableName,
resultVariableName, familyDeclLName, familyDeclName,
-- * Grouping
HsGroup(..), emptyRdrGroup, emptyRnGroup, appendGroups, hsGroupInstDecls,
......@@ -710,11 +710,14 @@ tyFamInstDeclLName (TyFamInstDecl (HsIB _ (XFamEqn nec)))
tyFamInstDeclLName (TyFamInstDecl (XHsImplicitBndrs nec))
= noExtCon nec
tyClDeclLName :: TyClDecl pass -> Located (IdP pass)
tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln
tyClDeclLName decl = tcdLName decl
tyClDeclLName :: TyClDecl (GhcPass p) -> Located (IdP (GhcPass p))
tyClDeclLName (FamDecl { tcdFam = fd }) = familyDeclLName fd
tyClDeclLName (SynDecl { tcdLName = ln }) = ln
tyClDeclLName (DataDecl { tcdLName = ln }) = ln
tyClDeclLName (ClassDecl { tcdLName = ln }) = ln
tyClDeclLName (XTyClDecl nec) = noExtCon nec
tcdName :: TyClDecl pass -> IdP pass
tcdName :: TyClDecl (GhcPass p) -> IdP (GhcPass p)
tcdName = unLoc . tyClDeclLName
tyClDeclTyVars :: TyClDecl pass -> LHsQTyVars pass
......@@ -1140,6 +1143,16 @@ data FamilyInfo pass
-- said "type family Foo x where .."
| ClosedTypeFamily (Maybe [LTyFamInstEqn pass])
------------- Functions over FamilyDecls -----------
familyDeclLName :: FamilyDecl (GhcPass p) -> Located (IdP (GhcPass p))
familyDeclLName (FamilyDecl { fdLName = n }) = n
familyDeclLName (XFamilyDecl nec) = noExtCon nec
familyDeclName :: FamilyDecl (GhcPass p) -> IdP (GhcPass p)
familyDeclName = unLoc . familyDeclLName
famResultKindSignature :: FamilyResultSig (GhcPass p) -> Maybe (LHsKind (GhcPass p))
famResultKindSignature (NoSig _) = Nothing
famResultKindSignature (KindSig _ ki) = Just ki
......@@ -1155,6 +1168,8 @@ resultVariableName :: FamilyResultSig (GhcPass a) -> Maybe (IdP (GhcPass a))
resultVariableName (TyVarSig _ sig) = Just $ hsLTyVarName sig
resultVariableName _ = Nothing
------------- Pretty printing FamilyDecls -----------
instance OutputableBndrId p
=> Outputable (FamilyDecl (GhcPass p)) where
ppr = pprFamilyDecl TopLevel
......
......@@ -14,7 +14,6 @@ import GHC.Hs.Binds
import GHC.Hs.Doc
import GHC.Hs.Decls
import GHC.Hs.Extension
import GHC.Hs.Pat
import GHC.Hs.Types
import GHC.Hs.Utils
import Name
......@@ -117,8 +116,7 @@ user-written. This lets us relate Names (from ClsInsts) to comments
(associated with InstDecls and DerivDecls).
-}
getMainDeclBinder :: XRec pass Pat ~ Located (Pat pass) =>
HsDecl pass -> [IdP pass]
getMainDeclBinder :: HsDecl (GhcPass p) -> [IdP (GhcPass p)]
getMainDeclBinder (TyClD _ d) = [tcdName d]
getMainDeclBinder (ValD _ d) =
case collectHsBindBinders d of
......
......@@ -36,7 +36,7 @@ module TcHsSyn (
zonkTopBndrs,
ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv,
zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX,
zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs,
zonkTyBndrs, zonkTyBndrsX,
zonkTcTypeToType, zonkTcTypeToTypeX,
zonkTcTypesToTypes, zonkTcTypesToTypesX,
zonkTyVarOcc,
......@@ -327,20 +327,14 @@ extendZonkEnv ze@(ZonkEnv { ze_tv_env = tyco_env, ze_id_env = id_env }) vars
where
(tycovars, ids) = partition isTyCoVar vars
extendIdZonkEnv1 :: ZonkEnv -> Var -> ZonkEnv
extendIdZonkEnv1 ze@(ZonkEnv { ze_id_env = id_env }) id
extendIdZonkEnv :: ZonkEnv -> Var -> ZonkEnv
extendIdZonkEnv ze@(ZonkEnv { ze_id_env = id_env }) id
= ze { ze_id_env = extendVarEnv id_env id id }
extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv
extendTyZonkEnv1 ze@(ZonkEnv { ze_tv_env = ty_env }) tv
extendTyZonkEnv :: ZonkEnv -> TyVar -> ZonkEnv
extendTyZonkEnv ze@(ZonkEnv { ze_tv_env = ty_env }) tv
= ze { ze_tv_env = extendVarEnv ty_env tv tv }
extendTyZonkEnvN :: ZonkEnv -> [(Name,TyVar)] -> ZonkEnv
extendTyZonkEnvN ze@(ZonkEnv { ze_tv_env = ty_env }) pairs
= ze { ze_tv_env = foldl add ty_env pairs }
where
add env (name, tv) = extendVarEnv_Directly env (getUnique name) tv
setZonkType :: ZonkEnv -> ZonkFlexi -> ZonkEnv
setZonkType ze flexi = ze { ze_flexi = flexi }
......@@ -429,7 +423,7 @@ zonkEvVarOcc env v
zonkCoreBndrX :: ZonkEnv -> Var -> TcM (ZonkEnv, Var)
zonkCoreBndrX env v
| isId v = do { v' <- zonkIdBndr env v
; return (extendIdZonkEnv1 env v', v') }
; return (extendIdZonkEnv env v', v') }
| otherwise = zonkTyBndrX env v
zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var])
......@@ -444,12 +438,16 @@ zonkTyBndrsX = mapAccumLM zonkTyBndrX
zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar)
-- This guarantees to return a TyVar (not a TcTyVar)
-- then we add it to the envt, so all occurrences are replaced
--
-- It does not clone: the new TyVar has the sane Name
-- as the old one. This important when zonking the
-- TyVarBndrs of a TyCon, whose Names may scope.
zonkTyBndrX env tv
= ASSERT2( isImmutableTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) )
do { ki <- zonkTcTypeToTypeX env (tyVarKind tv)
-- Internal names tidy up better, for iface files.
; let tv' = mkTyVar (tyVarName tv) ki
; return (extendTyZonkEnv1 env tv', tv') }
; return (extendTyZonkEnv env tv', tv') }
zonkTyVarBinders :: [VarBndr TcTyVar vis]
-> TcM (ZonkEnv, [VarBndr TyVar vis])
......@@ -466,22 +464,6 @@ zonkTyVarBinderX env (Bndr tv vis)
= do { (env', tv') <- zonkTyBndrX env tv
; return (env', Bndr tv' vis) }
zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar])
-- This rather specialised function is used in exactly one place.
-- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls.
zonkRecTyVarBndrs names tc_tvs
= initZonkEnv $ \ ze ->
fixM $ \ ~(_, rec_new_tvs) ->
do { let ze' = extendTyZonkEnvN ze $
zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv))
tc_tvs rec_new_tvs
; new_tvs <- zipWithM (zonk_one ze') names tc_tvs
; return (ze', new_tvs) }
where
zonk_one ze name tc_tv
= do { ki <- zonkTcTypeToTypeX ze (tyVarKind tc_tv)
; return (mkTyVar name ki) }
zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc)
zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e
......@@ -1357,7 +1339,7 @@ zonk_pat env (WildPat ty)
zonk_pat env (VarPat x (L l v))
= do { v' <- zonkIdBndr env v
; return (extendIdZonkEnv1 env v', VarPat x (L l v')) }
; return (extendIdZonkEnv env v', VarPat x (L l v')) }
zonk_pat env (LazyPat x pat)
= do { (env', pat') <- zonkPat env pat
......@@ -1369,7 +1351,7 @@ zonk_pat env (BangPat x pat)
zonk_pat env (AsPat x (L loc v) pat)
= do { v' <- zonkIdBndr env v
; (env', pat') <- zonkPat (extendIdZonkEnv1 env v') pat
; (env', pat') <- zonkPat (extendIdZonkEnv env v') pat
; return (env', AsPat x (L loc v') pat') }
zonk_pat env (ViewPat ty expr pat)
......@@ -1459,7 +1441,7 @@ zonk_pat env (NPlusKPat ty (L loc n) (L l lit1) lit2 e1 e2)
; lit1' <- zonkOverLit env2 lit1
; lit2' <- zonkOverLit env2 lit2
; ty' <- zonkTcTypeToTypeX env2 ty
; return (extendIdZonkEnv1 env2 n',
; return (extendIdZonkEnv env2 n',
NPlusKPat ty' (L loc n') (L l lit1') lit2' e1' e2') }
zonk_pat env (CoPat x co_fn pat ty)
......@@ -1607,7 +1589,7 @@ zonkCoreExpr env (Case scrut b ty alts)
= do scrut' <- zonkCoreExpr env scrut
ty' <- zonkTcTypeToTypeX env ty
b' <- zonkIdBndr env b
let env1 = extendIdZonkEnv1 env b'
let env1 = extendIdZonkEnv env b'
alts' <- mapM (zonkCoreAlt env1) alts
return $ Case scrut' b' ty' alts'
......@@ -1621,7 +1603,7 @@ zonkCoreBind :: ZonkEnv -> CoreBind -> TcM (ZonkEnv, CoreBind)
zonkCoreBind env (NonRec v e)
= do v' <- zonkIdBndr env v
e' <- zonkCoreExpr env e
let env1 = extendIdZonkEnv1 env v'
let env1 = extendIdZonkEnv env v'
return (env1, NonRec v' e')
zonkCoreBind env (Rec pairs)
= do (env1, pairs') <- fixM go
......
This diff is collapsed.
......@@ -57,7 +57,8 @@ module TcMType (
-- Instantiation
newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
newMetaTyVarTyVars, newMetaTyVarTyVarX,
newTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX,
newTyVarTyVar, cloneTyVarTyVar,
newPatSigTyVar, newSkolemTyVar, newWildCardX,
tcInstType,
tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
......@@ -707,30 +708,6 @@ cloneMetaTyVarName name
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment we give a unification variable a System Name, which
influences the way it is tidied; see TypeRep.tidyTyVarBndr.
Note [Unification variables need fresh Names]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whenever we allocate a unification variable (MetaTyVar) we give
it a fresh name. #16221 is a very tricky case that illustrates
why this is important:
data SameKind :: k -> k -> *
data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int
When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl
we allocate a unification variable kappa2 for k2, and then we
end up unifying kappa1 := kappa2 (because of the (SameKind a b).
Now we generalise over kappa2; but if kappa2's Name is k2,
we'll end up giving T0 the kind forall k2. k2 -> *. Nothing
directly wrong with that but when we typecheck the data constrautor
we end up giving it the type
MkT0 :: forall k1 (a :: k1) k2 (b :: k2).
SameKind @k2 a b -> Int -> T0 @{k2} a
which is bogus. The result type should be T0 @{k1} a.
And there no reason /not/ to clone the Name when making a
unification variable. So that's what we do.
-}
metaInfoToTyVarName :: MetaInfo -> FastString
......@@ -762,8 +739,17 @@ newSkolemTyVar name kind
newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
-- See Note [TyVarTv]
-- See Note [Unification variables need fresh Names]
-- Does not clone a fresh unique
newTyVarTyVar name kind
= do { details <- newMetaDetails TyVarTv
; let tyvar = mkTcTyVar name kind details
; traceTc "newTyVarTyVar" (ppr tyvar)
; return tyvar }
cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar
-- See Note [TyVarTv]
-- Clones a fresh unique
cloneTyVarTyVar name kind
= do { details <- newMetaDetails TyVarTv
; uniq <- newUnique
; let name' = name `setNameUnique` uniq
......@@ -772,7 +758,7 @@ newTyVarTyVar name kind
-- We want to keep the original more user-friendly Name
-- In practical terms that means that in error messages,
-- when the Name is tidied we get 'a' rather than 'a0'
; traceTc "newTyVarTyVar" (ppr tyvar)
; traceTc "cloneTyVarTyVar" (ppr tyvar)
; return tyvar }
newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
......@@ -1315,11 +1301,11 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty
go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty bound dv co
go dv (TyVarTy tv)
| is_bound tv = return dv
| otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
; case m_contents of
Just ind_ty -> go dv ind_ty
Nothing -> go_tv dv tv }
| is_bound tv = return dv
| otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv
; case m_contents of
Just ind_ty -> go dv ind_ty
Nothing -> go_tv dv tv }
go dv (ForAllTy (Bndr tv _) ty)
= do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv)
......
This diff is collapsed.
T11203.hs:7:24: error:
Couldn't match ‘k1’ with ‘k2’
• In the data type declaration for ‘Q’
Different names for the same type variable: ‘k1’ and ‘k2’
• In the data declaration for ‘Q’
T11821a.hs:4:31: error:
Couldn't match ‘k1’ with ‘k2’
• In the type synonym declaration for ‘SameKind’
Different names for the same type variable: ‘k1’ and ‘k2’
• In the type declaration for ‘SameKind’
......@@ -75,3 +75,8 @@ T14934:
$(RM) -f T14934a.o T14934a.hi T14934.o T14934.hi
'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934a.hs -O
'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934.hs -O
T17566:
$(RM) -f T17566a.o T17566a.hi T17566.o T17566.hi
'$(TEST_HC)' $(TEST_HC_OPTS) -c T17566a.hs
'$(TEST_HC)' $(TEST_HC_OPTS) -c T17566.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T17566 where
import Data.Kind
import Data.Proxy
import T17566a
type family F1 (x :: Proxy a) :: Proxy a
instance C1 Proxy z where
type T1 x = F1 x
data D1 x
type family F2 (x :: Proxy a) :: Proxy a
instance C2 Proxy z where
type T2 x = F2 x
data D2 x
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T17566a where
import Data.Kind
class C1 (f :: k -> Type) z where
type T1 (x :: f a) :: f a
data D1 (x :: f a)
class C2 f z where
type T2 (x :: f a) :: f a
data D2 (x :: f a)
......@@ -692,3 +692,4 @@ test('T17202', expect_broken(17202), compile, [''])
test('T15839a', normal, compile, [''])
test('T15839b', normal, compile, [''])
test('T17343', exit_code(1), compile_and_run, [''])
test('T17566', [extra_files(['T17566a.hs'])], makefile_test, [])
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T17566b where
class C f where
type T1 (f :: k1)
type T2 (f :: k2)
T17566b.hs:7:17: error:
• Different names for the same type variable: ‘k1’ and ‘k2’
• In the class declaration for ‘C’
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T17566c where
import Data.Kind
class C2 f z where
type T2 (f :: k -> Type)
data D2 (x :: (f :: k -> Type) a)
T17566c.hs:11:23: error:
• Different names for the same type variable:
‘k’ bound at T17566c.hs:10:17
‘k’ bound at T17566c.hs:11:23
• In the class declaration for ‘C2’
......@@ -550,3 +550,5 @@ test('T17355', normal, compile_fail, [''])
test('T17360', normal, compile_fail, [''])
test('T17563', normal, compile_fail, [''])
test('T16946', normal, compile_fail, [''])
test('T17566b', normal, compile_fail, [''])
test('T17566c', normal, compile_fail, [''])
Subproject commit 4808003d2238f76aee96d22cc022cee3e049f6a1
Subproject commit f3e3c4a766805a1bbea75bf23b84fdaaf053c226
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