diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2021-01-27 11:35:45 +0000 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2021-02-01 12:31:10 -0500 |
commit | f6e54c6216cfb13979ae925bece002492654c086 (patch) | |
tree | 315663b6df429cd9824d4eff2d44f80cd210eda1 | |
parent | c00901f87495a72c11fdced71b26ee8c4ab74f8a (diff) | |
download | haskell-f6e54c6216cfb13979ae925bece002492654c086.tar.gz |
Zonk the returned kind in tcFamTyPats
The motivation is given in Note [tcFamTyPats: zonking the result kind].
Fixes #19250 -- the fix is easy.
(cherry picked from commit 69cab37ae89db16cfd0b734d7fc657e56402a255)
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 30 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T19250.hs | 12 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 1 |
3 files changed, 43 insertions, 0 deletions
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 9617934c13..d0d6b2d561 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -2747,6 +2747,9 @@ tcFamTyPats fam_tc hs_pats -- GHC.Rename.Source tcInferApps typeLevelMode lhs_fun fun_ty hs_pats + -- Hack alert: see Note [tcFamTyPats: zonking the result kind] + ; res_kind <- zonkTcType res_kind + ; traceTc "End tcFamTyPats }" $ vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] @@ -2756,6 +2759,33 @@ tcFamTyPats fam_tc hs_pats fam_arity = tyConArity fam_tc lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) +{- Note [tcFamTyPats: zonking the result kind] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#19250) + F :: forall k. k -> k + type instance F (x :: Constraint) = () + +The tricky point is this: + is that () an empty type tuple (() :: Type), or + an empty constraint tuple (() :: Constraint)? +We work this out in a hacky way, by looking at the expected kind: +see Note [Inferring tuple kinds]. + +In this case, we kind-check the RHS using the kind gotten from the LHS: +see the call to tcCheckLHsType in tcTyFamInstEqnGuts in GHC.Tc.Tycl. + +But we want the kind from the LHS to be /zonked/, so that when +kind-checking the RHS (tcCheckLHsType) we can "see" what we learned +from kind-checking the LHS (tcFamTyPats). In our example above, the +type of the LHS is just `kappa` (by instantiating the forall k), but +then we learn (from x::Constraint) that kappa ~ Constraint. We want +that info when kind-checking the RHS. + +Easy solution: just zonk that return kind. Of course this won't help +if there is lots of type-family reduction to do, but it works fine in +common cases. +-} + unravelFamInstPats :: TcType -> [TcType] -- Decompose fam_app to get the argument patterns -- diff --git a/testsuite/tests/polykinds/T19250.hs b/testsuite/tests/polykinds/T19250.hs new file mode 100644 index 0000000000..6781e4bd39 --- /dev/null +++ b/testsuite/tests/polykinds/T19250.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeOperators, TypeFamilies, ConstraintKinds, PolyKinds, DataKinds, EmptyDataDecls #-} + +module T19250 where + +import Data.Kind + +type Exp a = a -> Type + +type family Eval (e :: Exp a) :: a + +data Collapse :: [Constraint] -> Exp Constraint +type instance Eval (Collapse '[]) = () diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 6b998f2872..c8d89e0b60 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -216,3 +216,4 @@ test('T16263', normal, compile_fail, ['']) test('T16902', normal, compile_fail, ['']) test('CuskFam', normal, compile, ['']) test('T17841', normal, compile_fail, ['']) +test('T19250', normal, compile, ['']) |