summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/GHC/Core/TyCo/Subst.hs8
-rw-r--r--compiler/GHC/Core/Type.hs1
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs56
-rw-r--r--testsuite/tests/polykinds/T19092.hs29
-rw-r--r--testsuite/tests/polykinds/T19093.hs19
-rw-r--r--testsuite/tests/polykinds/T19094.hs29
-rw-r--r--testsuite/tests/polykinds/all.T3
7 files changed, 117 insertions, 28 deletions
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, [''])
View Lorry Controller Status