Commit 645444af authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

Use tcSplitForAllInvisTyVars (not tcSplitForAllTyVars) in more places

The use of `tcSplitForAllTyVars` in `tcDataFamInstHeader` was the immediate
cause of #18939, and replacing it with a new `tcSplitForAllInvisTyVars`
function (which behaves like `tcSplitForAllTyVars` but only splits invisible
type variables) fixes the issue. However, this led me to realize that _most_
uses of `tcSplitForAllTyVars` in GHC really ought to be
`tcSplitForAllInvisTyVars` instead. While I was in town, I opted to replace
most uses of `tcSplitForAllTys` with `tcSplitForAllTysInvis` to reduce the
likelihood of such bugs in the future.

I say "most uses" above since there is one notable place where we _do_ want
to use `tcSplitForAllTyVars`: in `GHC.Tc.Validity.forAllTyErr`, which produces
the "`Illegal polymorphic type`" error message if you try to use a higher-rank
`forall` without having `RankNTypes` enabled. Here, we really do want to split
all `forall`s, not just invisible ones, or we run the risk of giving an
inaccurate error message in the newly added `T18939_Fail` test case.

I debated at some length whether I wanted to name the new function
`tcSplitForAllInvisTyVars` or `tcSplitForAllTyVarsInvisible`, but in the end,
I decided that I liked the former better. For consistency's sake, I opted to
rename the existing `splitPiTysInvisible` and `splitPiTysInvisibleN` functions
to `splitInvisPiTys` and `splitPiTysInvisN`, respectively, so that they use the
same naming convention. As a consequence, this ended up requiring a `haddock`
submodule bump.

Fixes #18939.
parent d61adb3d
Pipeline #27508 failed with stages
in 387 minutes and 55 seconds
......@@ -76,7 +76,7 @@ module GHC.Core.Type (
coAxNthLHS,
stripCoercionTy,
splitPiTysInvisible, splitPiTysInvisibleN,
splitInvisPiTys, splitInvisPiTysN,
invisibleTyBndrCount,
filterOutInvisibleTypes, filterOutInferredTypes,
partitionInvisibleTypes, partitionInvisibles,
......@@ -1559,7 +1559,7 @@ splitForAllTyCoVars ty = split ty ty []
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
-- | Splits the longest initial sequence of ForAllTys' that satisfy
-- | Splits the longest initial sequence of 'ForAllTy's that satisfy
-- @argf_pred@, returning the binders transformed by @argf_pred@
splitSomeForAllTyCoVarBndrs :: (ArgFlag -> Maybe af) -> Type -> ([VarBndr TyCoVar af], Type)
splitSomeForAllTyCoVarBndrs argf_pred ty = split ty ty []
......@@ -1716,12 +1716,12 @@ invisibleTyBndrCount :: Type -> Int
-- Includes invisible predicate arguments; e.g. for
-- e.g. forall {k}. (k ~ *) => k -> k
-- returns 2 not 1
invisibleTyBndrCount ty = length (fst (splitPiTysInvisible ty))
invisibleTyBndrCount ty = length (fst (splitInvisPiTys ty))
-- Like splitPiTys, but returns only *invisible* binders, including constraints
-- Stops at the first visible binder
splitPiTysInvisible :: Type -> ([TyCoBinder], Type)
splitPiTysInvisible ty = split ty ty []
-- | Like 'splitPiTys', but returns only *invisible* binders, including constraints.
-- Stops at the first visible binder.
splitInvisPiTys :: Type -> ([TyCoBinder], Type)
splitInvisPiTys ty = split ty ty []
where
split _ (ForAllTy b res) bs
| Bndr _ vis <- b
......@@ -1732,11 +1732,11 @@ splitPiTysInvisible ty = split ty ty []
| Just ty' <- coreView ty = split orig_ty ty' bs
split orig_ty _ bs = (reverse bs, orig_ty)
splitPiTysInvisibleN :: Int -> Type -> ([TyCoBinder], Type)
-- Same as splitPiTysInvisible, but stop when
-- - you have found 'n' TyCoBinders,
splitInvisPiTysN :: Int -> Type -> ([TyCoBinder], Type)
-- ^ Same as 'splitInvisPiTys', but stop when
-- - you have found @n@ 'TyCoBinder's,
-- - or you run out of invisible binders
splitPiTysInvisibleN n ty = split n ty ty []
splitInvisPiTysN n ty = split n ty ty []
where
split n orig_ty ty bs
| n == 0 = (reverse bs, orig_ty)
......
......@@ -316,7 +316,7 @@ dsPrimCall :: Id -> Coercion -> ForeignCall
dsPrimCall fn_id co fcall = do
let
ty = coercionLKind co
(tvs, fun_ty) = tcSplitForAllTyVars ty
(tvs, fun_ty) = tcSplitForAllInvisTyVars ty
(arg_tys, io_res_ty) = tcSplitFunTys fun_ty
args <- newSysLocalsDs arg_tys -- no FFI levity-polymorphism
......@@ -489,7 +489,7 @@ dsFExportDynamic id co0 cconv = do
where
ty = coercionLKind co0
(tvs,sans_foralls) = tcSplitForAllTyVars ty
(tvs,sans_foralls) = tcSplitForAllInvisTyVars ty
([Scaled arg_mult arg_ty], fn_res_ty) = tcSplitFunTys sans_foralls
Just (io_tc, res_ty) = tcSplitIOType_maybe fn_res_ty
-- Must have an IO type; hence Just
......
......@@ -1389,4 +1389,4 @@ quantifyType ty = ( filter isTyVar $
tyCoVarsOfTypeWellScoped rho
, rho)
where
(_tvs, rho) = tcSplitForAllTyVars ty
(_tvs, rho) = tcSplitForAllInvisTyVars ty
......@@ -2568,13 +2568,13 @@ kcCheckDeclHeader_sig kisig name flav
split_invis :: Kind -> Maybe Kind -> ([TyCoBinder], Kind)
split_invis sig_ki Nothing =
-- instantiate all invisible binders
splitPiTysInvisible sig_ki
splitInvisPiTys sig_ki
split_invis sig_ki (Just res_ki) =
-- subtraction a la checkExpectedKind
let n_res_invis_bndrs = invisibleTyBndrCount res_ki
n_sig_invis_bndrs = invisibleTyBndrCount sig_ki
n_inst = n_sig_invis_bndrs - n_res_invis_bndrs
in splitPiTysInvisibleN n_inst sig_ki
in splitInvisPiTysN n_inst sig_ki
-- A quantifier from a kind signature zipped with a user-written binder for it.
data ZippedBinder =
......
......@@ -950,7 +950,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
tc_kind_sig (Just hs_kind)
= do { sig_kind <- tcLHsKindSig data_ctxt hs_kind
; lvl <- getTcLevel
; let (tvs, inner_kind) = tcSplitForAllTyVars sig_kind
; let (tvs, inner_kind) = tcSplitForAllInvisTyVars sig_kind
; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs
-- Perhaps surprisingly, we don't need the skolemised tvs themselves
; return (substTy subst inner_kind) }
......
......@@ -223,8 +223,8 @@ check_inst sig_inst = do
skol_info = InstSkol
-- Based off of tcSplitDFunTy
(tvs, theta, pred) =
case tcSplitForAllTyVars ty of { (tvs, rho) ->
case splitFunTys rho of { (theta, pred) ->
case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
case splitFunTys rho of { (theta, pred) ->
(tvs, theta, pred) }}
origin = InstProvidedOrigin (tcg_semantic_mod tcg_env) sig_inst
(skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
......
......@@ -464,7 +464,7 @@ tcInstType inst_tyvars id
subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho)
; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
where
(tyvars, rho) = tcSplitForAllTyVars (idType id)
(tyvars, rho) = tcSplitForAllInvisTyVars (idType id)
(theta, tau) = tcSplitPhiTy rho
tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
......
......@@ -60,7 +60,7 @@ module GHC.Tc.Utils.TcType (
-- These are important because they do not look through newtypes
getTyVar,
tcSplitForAllTyVarBinder_maybe,
tcSplitForAllTyVars, tcSplitSomeForAllTyVars,
tcSplitForAllTyVars, tcSplitForAllInvisTyVars, tcSplitSomeForAllTyVars,
tcSplitForAllReqTVBinders, tcSplitForAllInvisTVBinders,
tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBinders,
tcSplitPhiTy, tcSplitPredFunTy_maybe,
......@@ -1223,12 +1223,17 @@ tcSplitForAllTyVarBinder_maybe (ForAllTy tv ty) = ASSERT( isTyVarBinder tv ) Jus
tcSplitForAllTyVarBinder_maybe _ = Nothing
-- | Like 'tcSplitPiTys', but splits off only named binders,
-- returning just the tycovars.
-- returning just the tyvars.
tcSplitForAllTyVars :: Type -> ([TyVar], Type)
tcSplitForAllTyVars ty
= ASSERT( all isTyVar (fst sty) ) sty
where sty = splitForAllTyCoVars ty
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Invisible'
-- type variable binders.
tcSplitForAllInvisTyVars :: Type -> ([TyVar], Type)
tcSplitForAllInvisTyVars ty = tcSplitSomeForAllTyVars isInvisibleArgFlag ty
-- | Like 'tcSplitForAllTyVars', but only splits a 'ForAllTy' if @argf_pred argf@
-- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and
-- @argf_pred@ is a predicate over visibilities provided as an argument to this
......@@ -1284,9 +1289,11 @@ tcSplitPhiTy ty
Just (pred, ty) -> split ty (pred:ts)
Nothing -> (reverse ts, ty)
-- | Split a sigma type into its parts.
-- | Split a sigma type into its parts. This only splits /invisible/ type
-- variable binders, as these are the only forms of binder that the typechecker
-- will implicitly instantiate.
tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy ty = case tcSplitForAllTyVars ty of
tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
......@@ -1469,9 +1476,9 @@ tcSplitDFunTy :: Type -> ([TyVar], [Type], Class, [Type])
-- the latter specifically stops at PredTy arguments,
-- and we don't want to do that here
tcSplitDFunTy ty
= case tcSplitForAllTyVars ty of { (tvs, rho) ->
case splitFunTys rho of { (theta, tau) ->
case tcSplitDFunHead tau of { (clas, tys) ->
= case tcSplitForAllInvisTyVars ty of { (tvs, rho) ->
case splitFunTys rho of { (theta, tau) ->
case tcSplitDFunHead tau of { (clas, tys) ->
(tvs, map scaledThing theta, clas, tys) }}}
tcSplitDFunHead :: Type -> (Class, [Type])
......@@ -1489,7 +1496,7 @@ tcSplitMethodTy :: Type -> ([TyVar], PredType, Type)
-- tcSplitMethodTy just peels off the outer forall and
-- that first predicate
tcSplitMethodTy ty
| (sel_tyvars,sel_rho) <- tcSplitForAllTyVars ty
| (sel_tyvars,sel_rho) <- tcSplitForAllInvisTyVars ty
, Just (first_pred, local_meth_ty) <- tcSplitPredFunTy_maybe sel_rho
= (sel_tyvars, first_pred, local_meth_ty)
| otherwise
......
......@@ -924,7 +924,7 @@ forAllTyErr env rank ty
, vcat [ hang herald 2 (ppr_tidy env ty)
, suggestion ] )
where
(tvs, _theta, _tau) = tcSplitSigmaTy ty
(tvs, _rho) = tcSplitForAllTyVars ty
herald | null tvs = text "Illegal qualified type:"
| otherwise = text "Illegal polymorphic type:"
suggestion = case rank of
......
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
module T18939_Compile where
import Data.Kind
data family Hm :: forall a -> a -> Type
data instance Hm :: forall a -> a -> Type
......@@ -726,6 +726,7 @@ test('T18323', normal, compile, [''])
test('T18585', normal, compile, [''])
test('T18831', normal, compile, [''])
test('T18920', normal, compile, [''])
test('T18939_Compile', normal, compile, [''])
test('T15942', normal, compile, [''])
test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
test('T17186', normal, compile, [''])
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE PolyKinds #-}
module T18939_Fail where
data F (f :: forall a -> a)
T18939_Fail.hs:5:1: error:
• Illegal polymorphic type: forall a -> a
Perhaps you intended to use RankNTypes
• In the data type declaration for ‘F’
......@@ -583,6 +583,7 @@ test('T18714', normal, compile_fail, [''])
test('T18723a', normal, compile_fail, [''])
test('T18723b', normal, compile_fail, [''])
test('T18723c', normal, compile_fail, [''])
test('T18939_Fail', normal, compile_fail, [''])
test('too-many', normal, compile_fail, [''])
test('T18640a', normal, compile_fail, [''])
test('T18640b', normal, compile_fail, [''])
......
Subproject commit ad9cbad7312a64e6757c32bd9488c55ba4f2fec9
Subproject commit 4d0498d503bd51b7d7626497580232685a2691a1
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