diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-12-21 11:11:31 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-12-21 11:14:13 +0000 |
commit | 71e26a74da5e5e9a61163b87ab4d22de88a2d04a (patch) | |
tree | f43c989640daa727011c099ba790bb2c795399cb | |
parent | 28f41f1a7a0ebae7b50ca41dbf78c04ee5b8b5b7 (diff) | |
download | haskell-71e26a74da5e5e9a61163b87ab4d22de88a2d04a.tar.gz |
Make candidateQTvs contain tyvar with zonked kinds
candidateQTyVars was failing to return fully-zonked
tyvars, and that made things fall over chaotically
when we try to sort them into a well-scoped telescope.
Result: Trac #15795
So I made candidateQTvs guarantee to have fully-zonked
tyvars (i.e. with zonked kinds). That's a bit annoying
but not really difficult.
-rw-r--r-- | compiler/typecheck/TcMType.hs | 150 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T15795.hs | 15 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T15795a.hs | 9 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 3 |
4 files changed, 109 insertions, 68 deletions
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 1516480789..ffeb602382 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -993,42 +993,6 @@ newMetaTyVarTyAtLevel tc_lvl kind * * ********************************************************************* -} -data CandidatesQTvs -- See Note [Dependent type variables] - -- See Note [CandidatesQTvs determinism and order] - -- NB: All variables stored here are MetaTvs. No exceptions. - = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) - , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) - -- A variable may appear in both sets - -- E.g. T k (x::k) The first occurrence of k makes it - -- show up in dv_tvs, the second in dv_kvs - -- See Note [Dependent type variables] - , dv_cvs :: CoVarSet - -- These are covars. We will *not* quantify over these, but - -- we must make sure also not to quantify over any cv's kinds, - -- so we include them here as further direction for quantifyTyVars - } - -instance Semi.Semigroup CandidatesQTvs where - (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 }) - <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 }) - = DV { dv_kvs = kv1 `unionDVarSet` kv2 - , dv_tvs = tv1 `unionDVarSet` tv2 - , dv_cvs = cv1 `unionVarSet` cv2 } - -instance Monoid CandidatesQTvs where - mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet } - mappend = (Semi.<>) - -instance Outputable CandidatesQTvs where - ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) - = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs - , text "dv_tvs =" <+> ppr tvs - , text "dv_cvs =" <+> ppr cvs ]) - - -candidateKindVars :: CandidatesQTvs -> TyVarSet -candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) - {- Note [Dependent type variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ In Haskell type inference we quantify over type variables; but we only @@ -1136,6 +1100,48 @@ what skolems are in scope. -} +data CandidatesQTvs + -- See Note [Dependent type variables] + -- See Note [CandidatesQTvs determinism and order] + -- + -- Invariants: + -- * All variables stored here are MetaTvs. No exceptions. + -- * All variables are fully zonked, including their kinds + -- + = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) + , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) + -- A variable may appear in both sets + -- E.g. T k (x::k) The first occurrence of k makes it + -- show up in dv_tvs, the second in dv_kvs + -- See Note [Dependent type variables] + + , dv_cvs :: CoVarSet + -- These are covars. We will *not* quantify over these, but + -- we must make sure also not to quantify over any cv's kinds, + -- so we include them here as further direction for quantifyTyVars + } + +instance Semi.Semigroup CandidatesQTvs where + (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 }) + <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 }) + = DV { dv_kvs = kv1 `unionDVarSet` kv2 + , dv_tvs = tv1 `unionDVarSet` tv2 + , dv_cvs = cv1 `unionVarSet` cv2 } + +instance Monoid CandidatesQTvs where + mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet } + mappend = (Semi.<>) + +instance Outputable CandidatesQTvs where + ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) + = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs + , text "dv_tvs =" <+> ppr tvs + , text "dv_cvs =" <+> ppr cvs ]) + + +candidateKindVars :: CandidatesQTvs -> TyVarSet +candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) + -- | Gathers free variables to use as quantification candidates (in -- 'quantifyTyVars'). This might output the same var -- in both sets, if it's used in both a type and a kind. @@ -1153,11 +1159,11 @@ candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempt -- to be dependent. This is appropriate when generalizing a *kind*, -- instead of a type. (That way, -XNoPolyKinds will default the variables -- to Type.) -candidateQTyVarsOfKind :: TcKind -- not necessarily zonked +candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked -> TcM CandidatesQTvs candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty -candidateQTyVarsOfKinds :: [TcKind] -- not necessarily zonked +candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked -> TcM CandidatesQTvs candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys @@ -1167,9 +1173,24 @@ delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars , dv_tvs = tvs `delDVarSetList` vars , dv_cvs = cvs `delVarSetList` vars } -collect_cand_qtvs :: Bool -- True <=> consider every fv in Type to be dependent - -> VarSet -- bound variables (both locally bound and globally bound) - -> CandidatesQTvs -> Type -> TcM CandidatesQTvs +collect_cand_qtvs + :: Bool -- True <=> consider every fv in Type to be dependent + -> VarSet -- Bound variables (both locally bound and globally bound) + -> CandidatesQTvs -- Accumulating parameter + -> Type -- Not necessarily zonked + -> TcM CandidatesQTvs + +-- Key points: +-- * Looks through meta-tyvars as it goes; +-- no need to zonk in advance +-- +-- * Needs to be monadic anyway, because it does the zap-naughty +-- stuff; see Note [Naughty quantification candidates] +-- +-- * Returns fully-zonked CandidateQTvs, including their kinds +-- so that subsequent dependency analysis (to build a well +-- scoped telescope) works correctly + collect_cand_qtvs is_dep bound dvs ty = go dvs ty where @@ -1199,34 +1220,27 @@ collect_cand_qtvs is_dep bound dvs ty ----------------- go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv - | is_dep - = case tv `elemDVarSet` kvs of - True -> return dv -- We have met this tyvar aleady - False | intersectsVarSet bound (tyCoVarsOfType tv_kind) - -> -- See Note [Naughty quantification candidates] - zap_naughty - | otherwise - -> collect_cand_qtvs True emptyVarSet dv' tv_kind - where - dv' = dv { dv_kvs = kvs `extendDVarSet` tv } - -- See Note [Order of accumulation] - + | tv `elemDVarSet` kvs = return dv -- We have met this tyvar aleady + | not is_dep + , tv `elemDVarSet` tvs = return dv -- We have met this tyvar aleady | otherwise - = case tv `elemDVarSet` kvs || tv `elemDVarSet` tvs of - True -> return dv -- We have met this tyvar aleady - False | intersectsVarSet bound (tyCoVarsOfType tv_kind) - -> -- See Note [Naughty quantification candidates] - zap_naughty - | otherwise - -> collect_cand_qtvs True emptyVarSet dv' tv_kind - where - dv' = dv { dv_tvs = tvs `extendDVarSet` tv } - -- See Note [Order of accumulation] - where - tv_kind = tyVarKind tv - zap_naughty = do { traceTc "Zapping naughty quantifier" (pprTyVar tv) - ; writeMetaTyVar tv (anyTypeOfKind tv_kind) - ; collect_cand_qtvs True bound dv tv_kind } + = do { tv_kind <- zonkTcType (tyVarKind tv) + -- This zonk is annoying, but it is necessary, both to + -- ensure that the collected candidates have zonked kinds + -- (Trac #15795) and to make the naughty check + -- (which comes next) works correctly + ; if intersectsVarSet bound (tyCoVarsOfType tv_kind) + + then -- See Note [Naughty quantification candidates] + do { traceTc "Zapping naughty quantifier" (pprTyVar tv) + ; writeMetaTyVar tv (anyTypeOfKind tv_kind) + ; collect_cand_qtvs True bound dv tv_kind } + + else do { let tv' = tv `setTyVarKind` tv_kind + dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' } + | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' } + -- See Note [Order of accumulation] + ; collect_cand_qtvs True emptyVarSet dv' tv_kind } } collect_cand_qtvs_co :: VarSet -- bound variables -> CandidatesQTvs -> Coercion diff --git a/testsuite/tests/polykinds/T15795.hs b/testsuite/tests/polykinds/T15795.hs new file mode 100644 index 0000000000..e8a6bc7362 --- /dev/null +++ b/testsuite/tests/polykinds/T15795.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +module T15795 where + +import Data.Kind + +type KindOf (a :: k) = k + +data T :: forall j (a :: j). KindOf a -> Type where + MkT :: forall k (b :: k). T b + +f :: forall k (b :: k). T b +f = error "urk" diff --git a/testsuite/tests/polykinds/T15795a.hs b/testsuite/tests/polykinds/T15795a.hs new file mode 100644 index 0000000000..9ad7406adf --- /dev/null +++ b/testsuite/tests/polykinds/T15795a.hs @@ -0,0 +1,9 @@ +{-# Language RankNTypes #-} +{-# Language PolyKinds #-} +{-# Language GADTs #-} + +module T15795a where +import Data.Kind + +data F :: forall (cat1 :: ob1). ob1 -> Type where + Prod :: F (a :: u) diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 18eb8a5d7d..21de7f87cc 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -204,3 +204,6 @@ test('T15817', normal, compile, ['']) test('T15874', normal, compile, ['']) test('T14887a', normal, compile, ['']) test('T14847', normal, compile, ['']) +test('T15795', normal, compile, ['']) +test('T15795a', normal, compile, ['']) + |