[Git][ghc/ghc][wip/T20666] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Jan 3 16:29:56 UTC 2023
Simon Peyton Jones pushed to branch wip/T20666 at Glasgow Haskell Compiler / GHC
Commits:
50968773 by Simon Peyton Jones at 2023-01-03T16:30:11+00:00
Wibbles
- - - - -
3 changed files:
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Validity.hs
- testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
Changes:
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -136,11 +136,12 @@ module GHC.Tc.Utils.TcType (
PatersonSize(..), PatersonSizeFailure(..),
ltPatersonSize,
pSizeZero, pSizeOne,
- pSizeType, pSizeTypeX,
+ pSizeType, pSizeTypeX, pSizeTypes,
pSizeClassPred, pSizeClassPredX,
pSizeTyConApp,
noMoreTyVars, allDistinctTyVars,
TypeSize, sizeType, sizeTypes, scopedSort,
+ isTerminatingClass, isStuckTypeFamily,
--------------------------------
-- Reexported from Kind
@@ -2354,8 +2355,8 @@ described in #15177, which contains a number of examples.
The suspicious bits are the calls to filterOutInvisibleTypes.
See also #11833.
-Note [Paterson size for type family applications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [PatersonSize for type family applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A type-family application has infinite size (PS_TyFam);
see (PC3) in Note [Paterson conditions] in GHC.Tc.Validity.
@@ -2438,6 +2439,9 @@ addPSize (PS_Vanilla { ps_tvs = tvs1, ps_size = s1 })
pSizeType :: Type -> PatersonSize
pSizeType = pSizeTypeX emptyVarSet
+pSizeTypes :: [Type] -> PatersonSize
+pSizeTypes = pSizeTypesX emptyVarSet pSizeZero
+
-- Free variables of a type, retaining repetitions, and expanding synonyms
-- This ignores coercions, as coercions aren't user-written
pSizeTypeX :: VarSet -> Type -> PatersonSize
@@ -2446,10 +2450,7 @@ pSizeTypeX bvs (TyVarTy tv)
| tv `elemVarSet` bvs = pSizeOne
| otherwise = PS_Vanilla { ps_tvs = [tv], ps_size = 1 }
pSizeTypeX _ (LitTy {}) = pSizeOne
-
-pSizeTypeX bvs (TyConApp tc tys)
- | isTypeFamilyTyCon tc = pSizeTyFamApp tc
- | otherwise = pSizeTyConAppX bvs tc tys
+pSizeTypeX bvs (TyConApp tc tys) = pSizeTyConAppX bvs tc tys
pSizeTypeX bvs (AppTy fun arg) = pSizeTypeX bvs fun `addPSize` pSizeTypeX bvs arg
pSizeTypeX bvs (FunTy _ w arg res) = pSizeTypeX bvs w `addPSize` pSizeTypeX bvs arg `addPSize`
pSizeTypeX bvs res
@@ -2458,11 +2459,8 @@ pSizeTypeX bvs (ForAllTy (Bndr tv _) ty) = pSizeTypeX bvs (tyVarKind tv) `addPSi
pSizeTypeX bvs (CastTy ty _) = pSizeTypeX bvs ty
pSizeTypeX _ (CoercionTy {}) = pSizeOne
-pSizeTyFamApp :: TyCon -> PatersonSize
--- See Note [PatersonSize for type family applications]
-pSizeTyFamApp tc
- | tc `hasKey` errorMessageTypeErrorFamKey = pSizeZero
- | otherwise = PS_TyFam tc
+pSizeTypesX :: VarSet -> PatersonSize -> [Type] -> PatersonSize
+pSizeTypesX bvs sz tys = foldr (addPSize . pSizeTypeX bvs) sz tys
pSizeTyConApp :: TyCon -> [Type] -> PatersonSize
pSizeTyConApp = pSizeTyConAppX emptyVarSet
@@ -2470,7 +2468,15 @@ pSizeTyConApp = pSizeTyConAppX emptyVarSet
pSizeTyConAppX :: VarSet -> TyCon -> [Type] -> PatersonSize
-- Open question: do we count all args, or just the visible ones?
-- See Note [Invisible arguments and termination]
-pSizeTyConAppX bvs _tc tys = foldr (addPSize . pSizeTypeX bvs) pSizeOne tys
+pSizeTyConAppX bvs tc tys
+ | isTypeFamilyTyCon tc = pSizeTyFamApp tc
+ | otherwise = pSizeTypesX bvs pSizeOne tys
+
+pSizeTyFamApp :: TyCon -> PatersonSize
+-- See Note [PatersonSize for type family applications]
+pSizeTyFamApp tc
+ | isStuckTypeFamily tc = pSizeZero
+ | otherwise = PS_TyFam tc
pSizeClassPred :: Class -> [Type] -> PatersonSize
pSizeClassPred = pSizeClassPredX emptyVarSet
@@ -2480,10 +2486,16 @@ pSizeClassPredX bvs cls tys
| isTerminatingClass cls -- See (PS1) in Note [The PatersonSize of a type]
= pSizeZero
| otherwise
- = foldr (addPSize . pSizeTypeX bvs) pSizeOne $
+ = pSizeTypesX bvs pSizeOne $
filterOutInvisibleTypes (classTyCon cls) tys
-- filterOutInvisibleTypes Yuk! See Note [Invisible arguments and termination]
+isStuckTypeFamily :: TyCon -> Bool
+-- Special "stuck" type familes do not reduce to anything
+isStuckTypeFamily tc
+ = tc `hasKey` errorMessageTypeErrorFamKey
+ || tc `hasKey` anyTyConKey
+
-- | When this says "True", ignore this class constraint during
-- a termination check
-- See (PS1) in Note [The PatersonSize of a type]
=====================================
compiler/GHC/Tc/Validity.hs
=====================================
@@ -1913,14 +1913,14 @@ mkInstSizeError ps_failure head_pred pred
pp_pred = text "constraint" <+> quotes (ppr pred)
main_msg = case ps_failure of
- PSF_Size -> hang (text "The" <+> pp_pred)
- 2 (sep [ text "is no smaller than", text "the" <+> pp_head ])
- PSF_TyVar tvs -> hang (occMsg tvs)
- 2 (sep [ text "in the" <+> pp_pred
- , text "than in the" <+> pp_head ])
PSF_TyFam tc -> -- See (PC3) of Note [Paterson conditions]
hang (text "Illegal use of type family" <+> quotes (ppr tc))
2 (text "in the" <+> pp_pred)
+ PSF_TyVar tvs -> hang (occMsg tvs)
+ 2 (sep [ text "in the" <+> pp_pred
+ , text "than in the" <+> pp_head ])
+ PSF_Size -> hang (text "The" <+> pp_pred)
+ 2 (sep [ text "is no smaller than", text "the" <+> pp_head ])
occMsg :: [TyVar] -> SDoc
occMsg tvs = text "Variable" <> plural tvs <+> quotes (pprWithCommas ppr tvs)
@@ -2149,10 +2149,10 @@ checkFamInstRhs :: TyCon -> [Type] -- LHS
checkFamInstRhs lhs_tc lhs_tys famInsts
= mapMaybe check famInsts
where
- lhs_size = pSizeTyConApp lhs_tc lhs_tys
+ lhs_size = pSizeTypes lhs_tys
check (tc, tys)
- | let call_size = pSizeTyConApp tc tys
- , Just ps_failure <- call_size `ltPatersonSize` lhs_size
+ | not (stuckTypeFamily tc)
+ , Just ps_failure <- pSizeTypes tys `ltPatersonSize` lhs_size
= Just $ mkFamSizeError ps_failure (TyConApp lhs_tc lhs_tys) (TyConApp tc tys)
| otherwise
= Nothing
@@ -2167,14 +2167,14 @@ mkFamSizeError ps_failure lhs fam_call
pp_call = text "type-family application" <+> quotes (ppr fam_call)
main_msg = case ps_failure of
- PSF_Size -> hang (text "The" <+> pp_call)
- 2 (sep [ text "is no smaller than", text "the" <+> pp_lhs ])
- PSF_TyVar tvs -> hang (occMsg tvs)
- 2 (sep [ text "in the" <+> pp_call
- , text "than in the" <+> pp_lhs ])
PSF_TyFam tc -> -- See (PC3) of Note [Paterson conditions]
hang (text "Illegal nested use of type family" <+> quotes (ppr tc))
2 (text "in the arguments of the" <+> pp_call)
+ PSF_TyVar tvs -> hang (occMsg tvs)
+ 2 (sep [ text "in the" <+> pp_call
+ , text "than in the" <+> pp_lhs ])
+ PSF_Size -> hang (text "The" <+> pp_call)
+ 2 (sep [ text "is no smaller than", text "the" <+> pp_lhs ])
-----------------
checkFamPatBinders :: TyCon
=====================================
testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
=====================================
@@ -1,4 +1,17 @@
+TyFamUndec.hs:6:15: error:
+ • Variable ‘b’ occurs more often
+ in the type-family application ‘T (b, b)’
+ than in the LHS of the family instance ‘T (a, [b])’
+ (Use UndecidableInstances to permit this)
+ • In the type instance declaration for ‘T’
+
+TyFamUndec.hs:7:15: error:
+ • The type-family application ‘T (a, Maybe b)’
+ is no smaller than the LHS of the family instance ‘T (a, Maybe b)’
+ (Use UndecidableInstances to permit this)
+ • In the type instance declaration for ‘T’
+
TyFamUndec.hs:8:15: error:
• Illegal nested use of type family ‘T’
in the arguments of the type-family application ‘T (a, T b)’
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5096877337cc23f64d25d70ba399b93d804e8258
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5096877337cc23f64d25d70ba399b93d804e8258
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230103/1f624c36/attachment-0001.html>
More information about the ghc-commits
mailing list