Skip to content
Snippets Groups Projects
Commit 4d6394dd authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot
Browse files

Fix missing escaping-kind check in tcPatSynSig

Note [Escaping kind in type signatures] explains how we deal
with escaping kinds in type signatures, e.g.
    f :: forall r (a :: TYPE r). a
where the kind of the body is (TYPE r), but `r` is not in
scope outside the forall-type.

I had missed this subtlety in tcPatSynSig, leading to #24686.
This MR fixes it; and a similar bug in tc_top_lhs_type. (The
latter is tested by T24686a.)
parent bac57298
No related branches found
No related tags found
No related merge requests found
...@@ -56,7 +56,7 @@ module GHC.Tc.Gen.HsType ( ...@@ -56,7 +56,7 @@ module GHC.Tc.Gen.HsType (
tcHsLiftedType, tcHsOpenType, tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC, tcHsLiftedTypeNC, tcHsOpenTypeNC,
tcInferLHsType, tcInferLHsTypeKind, tcInferLHsTypeUnsaturated, tcInferLHsType, tcInferLHsTypeKind, tcInferLHsTypeUnsaturated,
tcCheckLHsTypeInContext, tcCheckLHsTypeInContext, tcCheckLHsType,
tcHsContext, tcLHsPredType, tcHsContext, tcLHsPredType,
kindGeneralizeAll, kindGeneralizeAll,
...@@ -496,7 +496,7 @@ tc_lhs_sig_type skol_info full_hs_ty@(L loc (HsSig { sig_bndrs = hs_outer_bndrs ...@@ -496,7 +496,7 @@ tc_lhs_sig_type skol_info full_hs_ty@(L loc (HsSig { sig_bndrs = hs_outer_bndrs
{- Note [Escaping kind in type signatures] {- Note [Escaping kind in type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider kind-checking the signature for `foo` (#19495): Consider kind-checking the signature for `foo` (#19495, #24686):
type family T (r :: RuntimeRep) :: TYPE r type family T (r :: RuntimeRep) :: TYPE r
foo :: forall (r :: RuntimeRep). T r foo :: forall (r :: RuntimeRep). T r
...@@ -508,7 +508,8 @@ because we allow signatures like `foo :: Int#`.) ...@@ -508,7 +508,8 @@ because we allow signatures like `foo :: Int#`.)
Suppose we are at level L currently. We do this Suppose we are at level L currently. We do this
* pushLevelAndSolveEqualitiesX: moves to level L+1 * pushLevelAndSolveEqualitiesX: moves to level L+1
* newExpectedKind: allocates delta{L+1} * newExpectedKind: allocates delta{L+1}. Note carefully that
this call is /outside/ the tcOuterTKBndrs call.
* tcOuterTKBndrs: pushes the level again to L+2, binds skolem r{L+2} * tcOuterTKBndrs: pushes the level again to L+2, binds skolem r{L+2}
* kind-check the body (T r) :: TYPE delta{L+1} * kind-check the body (T r) :: TYPE delta{L+1}
...@@ -607,9 +608,9 @@ tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs ...@@ -607,9 +608,9 @@ tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
; skol_info <- mkSkolemInfo skol_info_anon ; skol_info <- mkSkolemInfo skol_info_anon
; (tclvl, wanted, (outer_bndrs, ty)) ; (tclvl, wanted, (outer_bndrs, ty))
<- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $ <- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
tcOuterTKBndrs skol_info hs_outer_bndrs $
do { kind <- newExpectedKind (expectedKindInCtxt ctxt) do { kind <- newExpectedKind (expectedKindInCtxt ctxt)
; tc_check_lhs_type (mkMode tyki) body kind } ; tcOuterTKBndrs skol_info hs_outer_bndrs $
tc_check_lhs_type (mkMode tyki) body kind }
; outer_bndrs <- scopedSortOuter outer_bndrs ; outer_bndrs <- scopedSortOuter outer_bndrs
; let outer_tv_bndrs = outerTyVarBndrs outer_bndrs ; let outer_tv_bndrs = outerTyVarBndrs outer_bndrs
......
...@@ -36,7 +36,7 @@ import GHC.Tc.Gen.HsType ...@@ -36,7 +36,7 @@ import GHC.Tc.Gen.HsType
import GHC.Tc.Types import GHC.Tc.Types
import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities ) import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep ) import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep, newOpenTypeKind )
import GHC.Tc.Zonk.Type import GHC.Tc.Zonk.Type
import GHC.Tc.Types.Origin import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcType
...@@ -386,14 +386,16 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty ...@@ -386,14 +386,16 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty
; (tclvl, wanted, (outer_bndrs, (ex_bndrs, (req, prov, body_ty)))) ; (tclvl, wanted, (outer_bndrs, (ex_bndrs, (req, prov, body_ty))))
<- pushLevelAndSolveEqualitiesX "tcPatSynSig" $ <- pushLevelAndSolveEqualitiesX "tcPatSynSig" $
-- See Note [Report unsolved equalities in tcPatSynSig] -- See Note [Report unsolved equalities in tcPatSynSig]
tcOuterTKBndrs skol_info hs_outer_bndrs $ do { res_kind <- newOpenTypeKind
tcExplicitTKBndrs skol_info ex_hs_tvbndrs $ -- "open" because a (literal) pattern can be unlifted;
do { req <- tcHsContext hs_req -- e.g. pattern Zero <- 0# (#12094)
; prov <- tcHsContext hs_prov -- See Note [Escaping kind in type signatures] in GHC.Tc.Gen.HsType
; body_ty <- tcHsOpenType hs_body_ty ; tcOuterTKBndrs skol_info hs_outer_bndrs $
-- A (literal) pattern can be unlifted; tcExplicitTKBndrs skol_info ex_hs_tvbndrs $
-- e.g. pattern Zero <- 0# (#12094) do { req <- tcHsContext hs_req
; return (req, prov, body_ty) } ; prov <- tcHsContext hs_prov
; body_ty <- tcCheckLHsType hs_body_ty res_kind
; return (req, prov, body_ty) } }
; let implicit_tvs :: [TcTyVar] ; let implicit_tvs :: [TcTyVar]
univ_bndrs :: [TcInvisTVBinder] univ_bndrs :: [TcInvisTVBinder]
......
{-# LANGUAGE ViewPatterns, PatternSynonyms #-}
module T24686 where
import GHC.Exts
import GHC.Stack
{-
on GHC 9.4 / 9.6 / 9.8 this panics with
<no location info>: error:
panic! (the 'impossible' happened)
GHC version 9.4.8:
typeKind
forall {r :: RuntimeRep} (a :: TYPE r). a
[r_aNu, a_aNy]
a_aNy :: TYPE r_aNu
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:182:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:3059:18 in ghc:GHC.Core.Type
This regression test exists to make sure the fix introduced between 9.8 and 9.11 does not get removed
again.
-}
pattern Bug :: forall. HasCallStack => forall {r :: RuntimeRep} (a :: TYPE r). a
pattern Bug <- (undefined -> _unused)
where
Bug = undefined
T24686.hs:25:80: error: [GHC-25897]
Couldn't match kind ‘r’ with ‘LiftedRep’
Expected kind ‘*’, but ‘a’ has kind ‘TYPE r’
‘r’ is a rigid type variable bound by
the type signature for ‘Bug’
at T24686.hs:25:48
{-# LANGUAGE StandaloneKindSignatures #-}
module T24686a where
import GHC.Exts
-- This one crashed GHC too: see #24686
type T :: forall a (b:: TYPE a). b
data T
T24686a.hs:8:34: error: [GHC-25897]
• Couldn't match kind ‘a’ with ‘LiftedRep’
Expected kind ‘*’, but ‘b’ has kind ‘TYPE a’
‘a’ is a rigid type variable bound by
a standalone kind signature for ‘T’
at T24686a.hs:8:18
• In a standalone kind signature for ‘T’: forall a (b :: TYPE a). b
...@@ -245,3 +245,5 @@ test('T22742', normal, compile_fail, ['']) ...@@ -245,3 +245,5 @@ test('T22742', normal, compile_fail, [''])
test('T22793', normal, compile_fail, ['']) test('T22793', normal, compile_fail, [''])
test('T24083', normal, compile_fail, ['']) test('T24083', normal, compile_fail, [''])
test('T24083a', normal, compile, ['']) test('T24083a', normal, compile, [''])
test('T24686', normal, compile_fail, [''])
test('T24686a', normal, compile_fail, [''])
RepPolyPatSynRes.hs:13:1: error: [GHC-18478] RepPolyPatSynRes.hs:13:59: error: [GHC-25897]
The pattern synonym scrutinee does not have a fixed runtime representation: Couldn't match kind ‘rep’ with ‘LiftedRep’
• a :: TYPE rep Expected kind ‘*’, but ‘a’ has kind ‘TYPE rep’
‘rep’ is a rigid type variable bound by
the type signature for ‘Pat’
at RepPolyPatSynRes.hs:13:23-25
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment