Commit 068b7e98 authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Fix #16391 by using occCheckExpand in TcValidity

The type-variables-escaping-their-scope-via-kinds check in
`TcValidity` was failing to properly expand type synonyms, which led
to #16391. This is easily fixed by using `occCheckExpand` before
performing the validity check.

Along the way, I refactored this check out into its own function,
and sprinkled references to Notes to better explain all of the moving
parts. Many thanks to @simonpj for the suggestions.

Bumps the haddock submodule.
parent 7a68254a
Pipeline #3223 passed with stages
in 367 minutes and 46 seconds
......@@ -806,7 +806,7 @@ starting the search; and we make sure to update the starting point for "a"
after we allocate a new one.
Node [Tidying multiple names at once]
Note [Tidying multiple names at once]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
......
......@@ -689,20 +689,11 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
; check_type (ve{ve_tidy_env = env'}) tau
-- Allow foralls to right of arrow
; checkTcM (not (any (`elemVarSet` tyCoVarsOfType phi_kind) tvs))
(forAllEscapeErr env' ty tau_kind)
}
; checkEscapingKind env' tvbs' theta tau }
where
(tvbs, phi) = tcSplitForAllVarBndrs ty
(theta, tau) = tcSplitPhiTy phi
tvs = binderVars tvbs
(env', _) = tidyVarBndrs env tvs
tau_kind = tcTypeKind tau
phi_kind | null theta = tau_kind
| otherwise = liftedTypeKind
-- If there are any constraints, the kind is *. (#11405)
(tvbs, phi) = tcSplitForAllVarBndrs ty
(theta, tau) = tcSplitPhiTy phi
(env', tvbs') = tidyTyCoVarBinders env tvbs
check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ arg_ty res_ty)
= do { check_type (ve{ve_rank = arg_rank}) arg_ty
......@@ -877,13 +868,52 @@ forAllTyErr env rank ty
MonoType d -> d
_ -> Outputable.empty -- Polytype is always illegal
forAllEscapeErr :: TidyEnv -> Type -> Kind -> (TidyEnv, SDoc)
forAllEscapeErr env ty tau_kind
-- | Reject type variables that would escape their escape through a kind.
-- See @Note [Type variables escaping through kinds]@.
checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM ()
checkEscapingKind env tvbs theta tau =
case occCheckExpand (binderVars tvbs) phi_kind of
-- Ensure that none of the tvs occur in the kind of the forall
-- /after/ expanding type synonyms.
-- See Note [Phantom type variables in kinds] in Type
Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind
Just _ -> pure ()
where
tau_kind = tcTypeKind tau
phi_kind | null theta = tau_kind
| otherwise = liftedTypeKind
-- If there are any constraints, the kind is *. (#11405)
forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind
-> (TidyEnv, SDoc)
forAllEscapeErr env tvbs theta tau tau_kind
= ( env
, hang (vcat [ text "Quantified type's kind mentions quantified type variable"
, text "(skolem escape)" ])
2 (vcat [ text " type:" <+> ppr_tidy env ty
, text "of kind:" <+> ppr_tidy env tau_kind ]) )
, vcat [ hang (text "Quantified type's kind mentions quantified type variable")
2 (text "type:" <+> quotes (ppr (mkSigmaTy tvbs theta tau)))
-- NB: Don't tidy this type since the tvbs were already tidied
-- previously, and re-tidying them will make the names of type
-- variables different from tau_kind.
, hang (text "where the body of the forall has this kind:")
2 (quotes (ppr_tidy env tau_kind)) ] )
{-
Note [Type variables escaping through kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider:
type family T (r :: RuntimeRep) :: TYPE r
foo :: forall r. T r
Something smells funny about the type of `foo`. If you spell out the kind
explicitly, it becomes clearer from where the smell originates:
foo :: ((forall r. T r) :: TYPE r)
The type variable `r` appears in the result kind, which escapes the scope of
its binding site! This is not desirable, so we establish a validity check
(`checkEscapingKind`) to catch any type variables that might escape through
kinds in this way.
-}
ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
ubxArgTyErr env ty
......
......@@ -3909,7 +3909,7 @@ tidyVarBndr tidy_env@(occ_env, subst) var
avoidNameClashes :: [TyCoVar] -> TidyEnv -> TidyEnv
-- Seed the occ_env with clashes among the names, see
-- Node [Tidying multiple names at once] in OccName
-- Note [Tidying multiple names at once] in OccName
avoidNameClashes tvs (occ_env, subst)
= (avoidClashesOccEnv occ_env occs, subst)
where
......@@ -3939,7 +3939,9 @@ tidyTyCoVarBinder tidy_env (Bndr tv vis)
tidyTyCoVarBinders :: TidyEnv -> [VarBndr TyCoVar vis]
-> (TidyEnv, [VarBndr TyCoVar vis])
tidyTyCoVarBinders = mapAccumL tidyTyCoVarBinder
tidyTyCoVarBinders tidy_env tvbs
= mapAccumL tidyTyCoVarBinder
(avoidNameClashes (binderVars tvbs) tidy_env) tvbs
---------------
tidyFreeTyCoVars :: TidyEnv -> [TyCoVar] -> TidyEnv
......
......@@ -2712,6 +2712,30 @@ In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct:
Note that:
* The only way we distinguish '->' from '=>' is by the fact
that the argument is a PredTy. Both are FunTys
Note [Phantom type variables in kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type K (r :: RuntimeRep) = Type -- Note 'r' is unused
data T r :: K r -- T :: forall r -> K r
foo :: forall r. T r
The body of the forall in foo's type has kind (K r), and
normally it would make no sense to have
forall r. (ty :: K r)
because the kind of the forall would escape the binding
of 'r'. But in this case it's fine because (K r) exapands
to Type, so we expliclity /permit/ the type
forall r. T r
To accommodate such a type, in typeKind (forall a.ty) we use
occCheckExpand to expand any type synonyms in the kind of 'ty'
to eliminate 'a'. See kinding rule (FORALL) in
Note [Kinding rules for types]
And in TcValidity.checkEscapingKind, we use also use
occCheckExpand, for the same reason.
-}
-----------------------------
......@@ -2734,8 +2758,11 @@ typeKind (AppTy fun arg)
go fun args = piResultTys (typeKind fun) args
typeKind ty@(ForAllTy {})
= case occCheckExpand tvs body_kind of -- We must make sure tv does not occur in kind
Just k' -> k' -- As it is already out of scope!
= case occCheckExpand tvs body_kind of
-- We must make sure tv does not occur in kind
-- As it is already out of scope!
-- See Note [Phantom type variables in kinds]
Just k' -> k'
Nothing -> pprPanic "typeKind"
(ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
where
......@@ -2772,8 +2799,11 @@ tcTypeKind ty@(ForAllTy {})
= constraintKind
| otherwise
= case occCheckExpand tvs body_kind of -- We must make sure tv does not occur in kind
Just k' -> k' -- As it is already out of scope!
= case occCheckExpand tvs body_kind of
-- We must make sure tv does not occur in kind
-- As it is already out of scope!
-- See Note [Phantom type variables in kinds]
Just k' -> k'
Nothing -> pprPanic "tcTypeKind"
(ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
where
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T16391a where
import Data.Kind
type Const (a :: Type) (b :: Type) = a
type family F :: Const Type a where
F = Int
type TS = (Int :: Const Type a)
data T1 :: Const Type a where
MkT1 :: T1
data T2 :: Const Type a -> Type where
MkT2 :: T2 b
......@@ -67,3 +67,4 @@ test('T14729', normal, compile, ['-ddump-types -fprint-typechecker-elaboration -
test('T14729kind', normal, ghci_script, ['T14729kind.script'])
test('T16326_Compile1', normal, compile, [''])
test('T16326_Compile2', normal, compile, [''])
test('T16391a', normal, compile, [''])
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T16391b where
import GHC.Exts
type family T (r :: RuntimeRep) :: TYPE r
foo :: T r
foo = foo
T16391b.hs:10:8: error:
• Quantified type's kind mentions quantified type variable
type: ‘forall (r :: RuntimeRep). T r’
where the body of the forall has this kind: ‘TYPE r’
• In the type signature: foo :: T r
......@@ -52,3 +52,4 @@ test('T16326_Fail9', normal, compile_fail, [''])
test('T16326_Fail10', normal, compile_fail, [''])
test('T16326_Fail11', normal, compile_fail, [''])
test('T16326_Fail12', normal, compile_fail, [''])
test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
......@@ -7,7 +7,7 @@ pattern Pue :: a -> a1 -> (a, Ex) -- Defined at <interactive>:19:1
pattern Pur :: (Eq a, Num a) => a -> [a]
-- Defined at <interactive>:20:1
pattern Purp
:: (Eq a, Num a) => Show a1 => a -> a1 -> ([a], UnivProv a1)
:: (Eq a1, Num a1) => Show a2 => a1 -> a2 -> ([a1], UnivProv a2)
-- Defined at <interactive>:21:1
pattern Pure :: (Eq a, Num a) => a -> a1 -> ([a], Ex)
-- Defined at <interactive>:22:1
......@@ -32,10 +32,10 @@ pattern Pue :: forall {a}. () => forall {a1}. a -> a1 -> (a, Ex)
pattern Pur :: forall {a}. (Eq a, Num a) => a -> [a]
-- Defined at <interactive>:20:1
pattern Purp
:: forall {a} {a1}.
(Eq a, Num a) =>
Show a1 =>
a -> a1 -> ([a], UnivProv a1)
:: forall {a1} {a2}.
(Eq a1, Num a1) =>
Show a2 =>
a1 -> a2 -> ([a1], UnivProv a2)
-- Defined at <interactive>:21:1
pattern Pure
:: forall {a}. (Eq a, Num a) => forall {a1}. a -> a1 -> ([a], Ex)
......
......@@ -20,9 +20,9 @@ T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
T11213.hs:24:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
Pattern synonym with no type signature:
pattern Purp :: forall a a1.
(Eq a, Num a) =>
Show a1 => a -> a1 -> ([a], UnivProv a1)
pattern Purp :: forall a1 a2.
(Eq a1, Num a1) =>
Show a2 => a1 -> a2 -> ([a1], UnivProv a2)
T11213.hs:25:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
Pattern synonym with no type signature:
......
Subproject commit 07f2ca98fd4249dc6ebad053bd6aef90c814efe0
Subproject commit e7586f005aa89a45b0fc4f3564f0f17ab9f79d38
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment