diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2022-10-28 22:51:30 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-11-01 12:49:47 -0400 |
commit | 0560821f637fa2a4318fb068a969f4802acb5a89 (patch) | |
tree | 81f8e018b458c23f8c4003aaec3780665e617236 | |
parent | 30e625e6d4bdd15960edce8ecc40b85ce3d72b28 (diff) | |
download | haskell-0560821f637fa2a4318fb068a969f4802acb5a89.tar.gz |
Add accurate skolem info when quantifying
Ticket #22379 revealed that skolemiseQuantifiedTyVar was
dropping the passed-in skol_info on the floor when it encountered
a SkolemTv. Bad! Several TyCons thereby share a single SkolemInfo
on their binders, which lead to bogus error reports.
-rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/TyCl.hs | 110 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 22 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/deriving/should_fail/T21871.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_fail/T15870.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T22379a.hs | 31 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T22379b.hs | 30 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 2 |
9 files changed, 139 insertions, 64 deletions
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 77aa280af8..a664092221 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -3489,6 +3489,8 @@ bindTyClTyVars tycon_name thing_inside bindTyClTyVarsAndZonk :: Name -> ([TyConBinder] -> Kind -> TcM a) -> TcM a -- Like bindTyClTyVars, but in addition -- zonk the skolem TcTyVars of a PolyTcTyCon to TyVars +-- We always do this same zonking after a call to bindTyClTyVars, but +-- here we do it right away because there are no more unifications to come bindTyClTyVarsAndZonk tycon_name thing_inside = bindTyClTyVars tycon_name $ \ tc_bndrs tc_kind -> do { ze <- mkEmptyZonkEnv NoFlexi diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index ac5e336e65..225e53d83e 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -411,21 +411,27 @@ TcTyCons are used for two distinct purposes 2. When checking a type/class declaration (in module GHC.Tc.TyCl), we come upon knowledge of the eventual tycon in bits and pieces, and we use a TcTyCon to record what we know before we are ready to build the - final TyCon. + final TyCon. Here is the plan: - We first build a MonoTcTyCon, then generalise to a PolyTcTyCon - See Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType - Specifically: + Step 1 (inferInitialKinds, inference only, skipped for checking): + Make a MonoTcTyCon whose binders are TcTyVars, + which may contain free unification variables - S1) In kcTyClGroup, we use checkInitialKinds to get the - utterly-final Kind of all TyCons in the group that - (a) have a kind signature or - (b) have a CUSK. - This produces a PolyTcTyCon, that is, a TcTyCon in which the binders - and result kind are full of TyVars (not TcTyVars). No unification - variables here; everything is in its final form. + Step 2 (generaliseTcTyCon) + Generalise that MonoTcTyCon to make a PolyTcTyCon + Its binders are skolem TcTyVars, with accurate SkolemInfo + + Step 3 (tcTyClDecl) + Typecheck the type and class decls to produce a final TyCon + Its binders are final TyVars, not TcTyVars + + Note that a MonoTcTyCon can contain unification variables, + but a PolyTcTyCon does not: only skolem TcTyVars. See + Note [TcTyCon, MonoTcTyCon, and PolyTcTyCon] in GHC.Tc.Utils.TcType + + More details about /kind inference/: - S2) In kcTyClGroup, we use inferInitialKinds to look over the + S1) In kcTyClGroup, we use inferInitialKinds to look over the declaration of any TyCon that lacks a kind signature or CUSK, to determine its "shape"; for example, the number of parameters, and any kind signatures. @@ -434,27 +440,30 @@ TcTyCons are used for two distinct purposes "mono" because it has not been been generalised, and its binders and result kind may have free unification variables. - S3) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the + S2) Still in kcTyClGroup, we use kcLTyClDecl to kind-check the body (class methods, data constructors, etc.) of each of these MonoTcTyCons, which has the effect of filling in the metavariables in the tycon's initial kind. - S4) Still in kcTyClGroup, we use generaliseTyClDecl to generalize - each MonoTcTyCon to get a PolyTcTyCon, with final TyVars in it, + S3) Still in kcTyClGroup, we use generaliseTyClDecl to generalize + each MonoTcTyCon to get a PolyTcTyCon, with skolem TcTyVars in it, and a final, fixed kind. - S5) Finally, back in TcTyClDecls, we extend the environment with + S4) Finally, back in TcTyClDecls, we extend the environment with the PolyTcTyCons, and typecheck each declaration (regardless of kind signatures etc) to get final TyCon. - These TcTyCons are stored in the local environment in GHC.Tc.TyCl, - until the real full TyCons can be created during desugaring. A - desugared program should never have a TcTyCon. + More details about /kind checking/ -3. A MonoTcTyCon can contain unification variables, but a PolyTcTyCon - does not: only skolem TcTyVars. + S5) In kcTyClGroup, we use checkInitialKinds to get the + utterly-final Kind of all TyCons in the group that + (a) have a separate kind signature or + (b) have a CUSK. + This produces a PolyTcTyCon, that is, a TcTyCon in which the binders + and result kind are full of TyVars (not TcTyVars). No unification + variables here; everything is in its final form. -4. tyConScopedTyVars. A challenging piece in all of this is that we +3. tyConScopedTyVars. A challenging piece in all of this is that we end up taking three separate passes over every declaration: - one in inferInitialKind (this pass look only at the head, not the body) - one in kcTyClDecls (to kind-check the body) @@ -2425,15 +2434,15 @@ tcClassDecl1 :: RolesInfo -> Name -> Maybe (LHsContext GhcRn) -> TcM Class tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs = fixM $ \ clas -> -- We need the knot because 'clas' is passed into tcClassATs - bindTyClTyVars class_name $ \ binders res_kind -> + bindTyClTyVars class_name $ \ tc_bndrs res_kind -> do { checkClassKindSig res_kind - ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders) + ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tc_bndrs) ; let tycon_name = class_name -- We use the same name roles = roles_info tycon_name -- for TyCon and Class ; (ctxt, fds, sig_stuff, at_stuff) - <- pushLevelAndSolveEqualities skol_info binders $ - -- The (binderVars binders) is needed bring into scope the + <- pushLevelAndSolveEqualities skol_info tc_bndrs $ + -- The (binderVars tc_bndrs) is needed bring into scope the -- skolems bound by the class decl header (#17841) do { ctxt <- tcHsContext hs_ctxt ; fds <- mapM (addLocMA tc_fundep) fundeps @@ -2458,9 +2467,10 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs -- any unfilled coercion variables unless there is such an error -- The zonk also squeeze out the TcTyCons, and converts -- Skolems to tyvars. - ; ze <- mkEmptyZonkEnv NoFlexi - ; ctxt <- zonkTcTypesToTypesX ze ctxt - ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff + ; ze <- mkEmptyZonkEnv NoFlexi + ; (ze, bndrs) <- zonkTyVarBindersX ze tc_bndrs -- From TcTyVars to TyVars + ; ctxt <- zonkTcTypesToTypesX ze ctxt + ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff -- ToDo: do we need to zonk at_stuff? -- TODO: Allow us to distinguish between abstract class, @@ -2482,8 +2492,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs | otherwise = Just (ctxt, at_stuff, sig_stuff, mindef) - ; clas <- buildClass class_name binders roles fds body - ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$ + ; clas <- buildClass class_name bndrs roles fds body + ; traceTc "tcClassDecl" (ppr fundeps $$ ppr bndrs $$ ppr fds) ; return clas } where @@ -2712,7 +2722,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info , fdResultSig = L _ sig , fdInjectivityAnn = inj }) | DataFamily <- fam_info - = bindTyClTyVarsAndZonk tc_name $ \ binders res_kind -> do + = bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> do { traceTc "tcFamDecl1 data family:" (ppr tc_name) ; checkFamFlag tc_name @@ -2729,8 +2739,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- See also Note [Datatype return kinds] ; checkDataKindSig DataFamilySort res_kind ; tc_rep_name <- newTyConRepName tc_name - ; let inj = Injective $ replicate (length binders) True - tycon = mkFamilyTyCon tc_name binders + ; let inj = Injective $ replicate (length tc_bndrs) True + tycon = mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig) (DataFamilyTyCon tc_rep_name) @@ -2738,12 +2748,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info ; return tycon } | OpenTypeFamily <- fam_info - = bindTyClTyVarsAndZonk tc_name $ \ binders res_kind -> do + = bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> do { traceTc "tcFamDecl1 open type family:" (ppr tc_name) ; checkFamFlag tc_name - ; inj' <- tcInjectivity binders inj + ; inj' <- tcInjectivity tc_bndrs inj ; checkResultSigFlag tc_name sig -- check after injectivity for better errors - ; let tycon = mkFamilyTyCon tc_name binders res_kind + ; let tycon = mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig) OpenSynFamilyTyCon parent inj' ; return tycon } @@ -2754,10 +2764,10 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info do { traceTc "tcFamDecl1 Closed type family:" (ppr tc_name) -- the variables in the header scope only over the injectivity -- declaration but this is not involved here - ; (inj', binders, res_kind) - <- bindTyClTyVarsAndZonk tc_name $ \ binders res_kind -> - do { inj' <- tcInjectivity binders inj - ; return (inj', binders, res_kind) } + ; (inj', tc_bndrs, res_kind) + <- bindTyClTyVarsAndZonk tc_name $ \ tc_bndrs res_kind -> + do { inj' <- tcInjectivity tc_bndrs inj + ; return (inj', tc_bndrs, res_kind) } ; checkFamFlag tc_name -- make sure we have -XTypeFamilies ; checkResultSigFlag tc_name sig @@ -2766,14 +2776,14 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- but eqns might be empty in the Just case as well ; case mb_eqns of Nothing -> - return $ mkFamilyTyCon tc_name binders res_kind + return $ mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig) AbstractClosedSynFamilyTyCon parent inj' Just eqns -> do { -- Process the equations, creating CoAxBranches - ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind + ; let tc_fam_tc = mkTcTyCon tc_name tc_bndrs res_kind noTcTyConScopedTyVars False {- this doesn't matter here -} ClosedTypeFamilyFlavour @@ -2792,7 +2802,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) - fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig) + fam_tc = mkFamilyTyCon tc_name tc_bndrs res_kind (resultVariableName sig) (ClosedSynFamilyTyCon mb_co_ax) parent inj' -- We check for instance validity later, when doing validity @@ -2853,10 +2863,10 @@ tcInjectivity tcbs (Just (L loc (InjectivityAnn _ _ lInjNames))) tcTySynRhs :: RolesInfo -> Name -> LHsType GhcRn -> TcM TyCon tcTySynRhs roles_info tc_name hs_ty - = bindTyClTyVars tc_name $ \ binders res_kind -> + = bindTyClTyVars tc_name $ \ tc_bndrs res_kind -> do { env <- getLclEnv ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env)) - ; rhs_ty <- pushLevelAndSolveEqualities skol_info binders $ + ; rhs_ty <- pushLevelAndSolveEqualities skol_info tc_bndrs $ tcCheckLHsType hs_ty (TheKind res_kind) -- See Note [Error on unconstrained meta-variables] in GHC.Tc.Utils.TcMType @@ -2870,11 +2880,11 @@ tcTySynRhs roles_info tc_name hs_ty , ppr rhs_ty ] ) } ; doNotQuantifyTyVars dvs mk_doc - ; ze <- mkEmptyZonkEnv NoFlexi - ; (ze, binders) <- zonkTyVarBindersX ze binders - ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty + ; ze <- mkEmptyZonkEnv NoFlexi + ; (ze, bndrs) <- zonkTyVarBindersX ze tc_bndrs + ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty ; let roles = roles_info tc_name - ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) } + ; return (buildSynTyCon tc_name bndrs res_kind roles rhs_ty) } where skol_info = TyConSkol TypeSynonymFlavour tc_name diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 1cb4820745..68b8285af8 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -1735,12 +1735,6 @@ quantifyTyVars skol_info ns_strat dvs = return Nothing -- this can happen for a covar that's associated with -- a coercion hole. Test case: typecheck/should_compile/T2494 --- Omit: no TyVars now --- | not (isTcTyVar tkv) --- = return (Just tkv) -- For associated types in a class with a standalone --- -- kind signature, we have the class variables in --- -- scope, and they are TyVars not TcTyVars - | otherwise = Just <$> skolemiseQuantifiedTyVar skol_info tkv @@ -1785,13 +1779,19 @@ skolemiseQuantifiedTyVar :: SkolemInfo -> TcTyVar -> TcM TcTyVar skolemiseQuantifiedTyVar skol_info tv = case tcTyVarDetails tv of - SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv) - ; return (setTyVarKind tv kind) } - -- It might be a skolem type variable, - -- for example from a user type signature - MetaTv {} -> skolemiseUnboundMetaTyVar skol_info tv + SkolemTv _ lvl _ -- It might be a skolem type variable, + -- for example from a user type signature + -- But it might also be a shared meta-variable across several + -- type declarations, each with its own skol_info. The first + -- will skolemise it, but the other uses must update its + -- skolem info (#22379) + -> do { kind <- zonkTcType (tyVarKind tv) + ; let details = SkolemTv skol_info lvl False + name = tyVarName tv + ; return (mkTcTyVar name kind details) } + _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk -- | Default a type variable using the given defaulting strategy. diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 6592912d05..eae089c203 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -428,7 +428,7 @@ Invariants: - Flag tcTyConIsPoly = True; this is used only to short-cut zonking - tyConBinders are still TcTyConBinders, but they are /skolem/ TcTyVars, - with fixed kinds: no unification variables here + with fixed kinds, and accurate skolem info: no unification variables here tyConBinders includes the Inferred binders if any diff --git a/testsuite/tests/deriving/should_fail/T21871.stderr b/testsuite/tests/deriving/should_fail/T21871.stderr index 3ec33ef61b..4cb5bff9a1 100644 --- a/testsuite/tests/deriving/should_fail/T21871.stderr +++ b/testsuite/tests/deriving/should_fail/T21871.stderr @@ -3,7 +3,7 @@ T21871.hs:13:36: error: [GHC-25897] • Couldn't match kind ‘k’ with ‘*’ Expected kind ‘* -> *’, but ‘m’ has kind ‘k -> *’ ‘k’ is a rigid type variable bound by - the newtype declaration for ‘FooT’ + a `deriving' clause at T21871.hs:(10,1)-(13,36) • In the second argument of ‘ReaderT’, namely ‘m’ In the newtype declaration for ‘FooT’ diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr index ced646a276..35bc2a43b9 100644 --- a/testsuite/tests/indexed-types/should_fail/T15870.stderr +++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr @@ -3,7 +3,7 @@ T15870.hs:32:34: error: [GHC-25897] • Couldn't match kind ‘k’ with ‘*’ Expected kind ‘Optic @{k} a’, but ‘g2’ has kind ‘Optic @{*} b’ ‘k’ is a rigid type variable bound by - the instance declaration + a family instance declaration at T15870.hs:(27,1)-(32,35) • In the second argument of ‘Get’, namely ‘g2’ In the type ‘Get a g2’ diff --git a/testsuite/tests/polykinds/T22379a.hs b/testsuite/tests/polykinds/T22379a.hs new file mode 100644 index 0000000000..d4caa01048 --- /dev/null +++ b/testsuite/tests/polykinds/T22379a.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE Haskell2010 #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module Bug where + +import Data.Kind +import Data.Proxy (Proxy) + +data Delayed (env :: Type) (c :: Type) +data Handler (a :: Type) +data Router (a :: Type) + +-- class decl, then type decl + +class HasServer api where + type ServerT api (m :: Type -> Type) :: Type + + route :: + Proxy api + -> Delayed env (Server api) + -> Router env + + hoistServerWithContext + :: Proxy api + -> (forall x. m x -> n x) + -> ServerT api m + -> ServerT api n + +type Server aqi = ServerT aqi Handler + diff --git a/testsuite/tests/polykinds/T22379b.hs b/testsuite/tests/polykinds/T22379b.hs new file mode 100644 index 0000000000..78cd004090 --- /dev/null +++ b/testsuite/tests/polykinds/T22379b.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE Haskell2010 #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module Bug where + +import Data.Kind +import Data.Proxy (Proxy) + +data Delayed (env :: Type) (c :: Type) +data Handler (a :: Type) +data Router (a :: Type) + +-- type decl, then class decl + +type Server aqi = ServerT aqi Handler + +class HasServer api where + type ServerT api (m :: Type -> Type) :: Type + + route :: + Proxy api + -> Delayed env (Server api) + -> Router env + + hoistServerWithContext + :: Proxy api + -> (forall x. m x -> n x) + -> ServerT api m + -> ServerT api n diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index fbe65d4b1c..721e41cebd 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -239,3 +239,5 @@ test('T19739a', normal, compile, ['']) test('T19739b', normal, compile, ['']) test('T19739c', normal, compile, ['']) test('T19739d', normal, compile, ['']) +test('T22379a', normal, compile, ['']) +test('T22379b', normal, compile, ['']) |