From dc7e5aea3b30bf23349b532bedf54a6d09d0646a Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Mon, 21 Dec 2020 17:47:26 +0000 Subject: Clone the binders of a SAKS where necessary Given a kind signature type T :: forall k. k -> forall k. k -> blah data T a b = ... where those k's have the same unique (which is possible; see #19093) we were giving the tyConBinders in tycon T the same unique, which caused chaos. Fix is simple: ensure uniqueness when decomposing the kind signature. See GHC.Tc.Gen.HsType.zipBinders --- compiler/GHC/Core/TyCo/Subst.hs | 8 ++++++ compiler/GHC/Core/Type.hs | 1 + compiler/GHC/Tc/Gen/HsType.hs | 56 ++++++++++++++++++------------------- testsuite/tests/polykinds/T19092.hs | 29 +++++++++++++++++++ testsuite/tests/polykinds/T19093.hs | 19 +++++++++++++ testsuite/tests/polykinds/T19094.hs | 29 +++++++++++++++++++ testsuite/tests/polykinds/all.T | 3 ++ 7 files changed, 117 insertions(+), 28 deletions(-) create mode 100644 testsuite/tests/polykinds/T19092.hs create mode 100644 testsuite/tests/polykinds/T19093.hs create mode 100644 testsuite/tests/polykinds/T19094.hs diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs index bc6632f1bf..7ea61bdae2 100644 --- a/compiler/GHC/Core/TyCo/Subst.hs +++ b/compiler/GHC/Core/TyCo/Subst.hs @@ -46,6 +46,7 @@ module GHC.Core.TyCo.Subst substTyVarBndr, substTyVarBndrs, substCoVarBndr, substTyVar, substTyVars, substTyCoVars, + substTyCoBndr, substForAllCoBndr, substVarBndrUsing, substForAllCoBndrUsing, checkValidSubst, isValidTCvSubst, @@ -1054,3 +1055,10 @@ cloneTyVarBndrs subst (t:ts) usupply = (subst'', tv:tvs) (uniq, usupply') = takeUniqFromSupply usupply (subst' , tv ) = cloneTyVarBndr subst t uniq (subst'', tvs) = cloneTyVarBndrs subst' ts usupply' + +substTyCoBndr :: TCvSubst -> TyCoBinder -> (TCvSubst, TyCoBinder) +substTyCoBndr subst (Anon af ty) = (subst, Anon af (substScaledTy subst ty)) +substTyCoBndr subst (Named (Bndr tv vis)) = (subst', Named (Bndr tv' vis)) + where + (subst', tv') = substVarBndr subst tv + diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index e5d0da93fd..af92b92e52 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -212,6 +212,7 @@ module GHC.Core.Type ( substCoUnchecked, substCoWithUnchecked, substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars, substVarBndr, substVarBndrs, + substTyCoBndr, cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, -- * Tidying type related things up for printing diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index ecd4e82304..ac6c95d954 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -2438,7 +2438,7 @@ kcCheckDeclHeader_sig kisig name flav -- ^^^^^^^^^ -- We do it here because at this point the environment has been -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'. - ; ctx_k <- kc_res_ki + ; ctx_k <- kc_res_ki ; m_res_ki <- case ctx_k of AnyKind -> return Nothing _ -> Just <$> newExpectedKind ctx_k @@ -2466,12 +2466,12 @@ kcCheckDeclHeader_sig kisig name flav ; return (invis_binders, r_ki) } - -- Zonk the implicitly quantified variables. - ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs - -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders. ; invis_tcbs <- mapM invis_to_tcb invis_binders + -- Zonk the implicitly quantified variables. + ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs + -- Build the final, generalized TcTyCon ; let tcbs = vis_tcbs ++ invis_tcbs implicit_tv_prs = implicit_nms `zip` implicit_tvs @@ -2589,34 +2589,34 @@ kcCheckDeclHeader_sig kisig name flav in splitInvisPiTysN n_inst sig_ki -- A quantifier from a kind signature zipped with a user-written binder for it. -data ZippedBinder = - ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn)) +data ZippedBinder = ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn)) -- See Note [Arity inference in kcCheckDeclHeader_sig] zipBinders - :: Kind -- kind signature - -> [LHsTyVarBndr () GhcRn] -- user-written binders - -> ([ZippedBinder], -- zipped binders - [LHsTyVarBndr () GhcRn], -- remaining user-written binders - Kind) -- remainder of the kind signature -zipBinders = zip_binders [] + :: Kind -- Kind signature + -> [LHsTyVarBndr () GhcRn] -- User-written binders + -> ( [ZippedBinder] -- Zipped binders + , [LHsTyVarBndr () GhcRn] -- Leftover user-written binders + , Kind ) -- Remainder of the kind signature +zipBinders = zip_binders [] emptyTCvSubst where - zip_binders acc ki [] = (reverse acc, [], ki) - zip_binders acc ki (b:bs) = - case tcSplitPiTy_maybe ki of - Nothing -> (reverse acc, b:bs, ki) - Just (tb, ki') -> - let - (zb, bs') | zippable = (ZippedBinder tb (Just b), bs) - | otherwise = (ZippedBinder tb Nothing, b:bs) - zippable = - case tb of - Named (Bndr _ (Invisible _)) -> False - Named (Bndr _ Required) -> True - Anon InvisArg _ -> False - Anon VisArg _ -> True - in - zip_binders (zb:acc) ki' bs' + -- subst: we substitute as we go, to ensure that the resulting + -- binders in the [ZippedBndr] all have distinct uniques. + -- If not, the TyCon may get multiple binders with the same unique, + -- which results in chaos (see #19092,3,4) + -- (The incoming kind might be forall k. k -> forall k. k -> Type + -- where those two k's have the same unique. Without the substitution + -- we'd get a repeated 'k'.) + zip_binders acc subst ki bs + | (b:bs') <- bs -- Stop as soon as 'bs' becomes empty + , Just (tb,ki') <- tcSplitPiTy_maybe ki + , let (subst', tb') = substTyCoBndr subst tb + = if isInvisibleBinder tb + then zip_binders (ZippedBinder tb' Nothing : acc) subst' ki' bs + else zip_binders (ZippedBinder tb' (Just b) : acc) subst' ki' bs' + + | otherwise + = (reverse acc, bs, substTy subst ki) tooManyBindersErr :: Kind -> [LHsTyVarBndr () GhcRn] -> SDoc tooManyBindersErr ki bndrs = diff --git a/testsuite/tests/polykinds/T19092.hs b/testsuite/tests/polykinds/T19092.hs new file mode 100644 index 0000000000..d63db880ea --- /dev/null +++ b/testsuite/tests/polykinds/T19092.hs @@ -0,0 +1,29 @@ +{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-} + +module T19092 where + +import Data.Type.Equality +import Data.Kind + +type PolyKinded :: Type -> Type +type PolyKinded res = (forall (k :: Type). k -> res) + +infix 4 + === +type + (===) :: PolyKinded (PolyKinded Bool) +type family + a === b where + a === a = True + _ === _ = False + +type TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint +class (a === b) ~ cond + => TryUnify cond a b +instance (a === b) ~ False + => TryUnify False @k a @j b +instance {-# Incoherent #-} + ( (a === b) ~ True + , a ~~ b + ) + => TryUnify True @k a @j b diff --git a/testsuite/tests/polykinds/T19093.hs b/testsuite/tests/polykinds/T19093.hs new file mode 100644 index 0000000000..4e322e1108 --- /dev/null +++ b/testsuite/tests/polykinds/T19093.hs @@ -0,0 +1,19 @@ +{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, + TypeOperators, StandaloneKindSignatures, TypeFamilies, + FlexibleInstances, MultiParamTypeClasses #-} + +module T19093 where + +import Data.Proxy +import Data.Type.Equality +import Data.Kind + +type PolyKinded :: Type -> Type +type PolyKinded res = (forall (k :: Type). k -> res) + + +type TryUnify :: PolyKinded (PolyKinded Constraint) +-- type TryUnify :: Bool -> forall k. k -> forall k. k -> Constraint +-- type TryUnify :: Bool -> PolyKinded (forall k. k -> Constraint) + +class TryUnify a b where diff --git a/testsuite/tests/polykinds/T19094.hs b/testsuite/tests/polykinds/T19094.hs new file mode 100644 index 0000000000..7b2b03e713 --- /dev/null +++ b/testsuite/tests/polykinds/T19094.hs @@ -0,0 +1,29 @@ +{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-} + +module T19094 where + +import Data.Type.Equality +import Data.Kind + +type PolyKinded :: Type -> Type +type PolyKinded res = (forall (k :: Type). k -> res) + +infix 4 + === +type + (===) :: PolyKinded (PolyKinded Bool) +type family + a === b where + a === a = True + _ === _ = False + +type TryUnify :: Bool -> PolyKinded (PolyKinded Constraint) +class (a === b) ~ cond + => TryUnify cond a b +instance (a === b) ~ False + => TryUnify False @k a @j b +instance {-# Incoherent #-} + ( (a === b) ~ True + , a ~~ b + ) + => TryUnify True @k a @j b diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 35d4df559d..52529f882a 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -230,3 +230,6 @@ test('T18451a', normal, compile_fail, ['']) test('T18451b', normal, compile_fail, ['']) test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script']) test('T18855', normal, compile, ['']) +test('T19092', normal, compile, ['']) +test('T19093', normal, compile, ['']) +test('T19094', normal, compile, ['']) -- cgit v1.2.1