[Git][ghc/ghc][master] Fix a buglet in tcSplitForAllTyVarsReqTVBindersN
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Sat Jan 18 07:54:36 UTC 2025
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
854c2f75 by Simon Peyton Jones at 2025-01-18T02:54:08-05:00
Fix a buglet in tcSplitForAllTyVarsReqTVBindersN
The problem was that an equation in `split` had two guards (one about
visiblity and one about `n_req`). So it fell thorugh if /either/
was False. But the next equation then assumed an invisible binder.
Simple bug, easily fixed. Fixes #25661.
- - - - -
7 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Types/Var.hs
- + testsuite/tests/polykinds/T25661.hs
- + testsuite/tests/polykinds/T25661.stderr
- testsuite/tests/polykinds/all.T
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -155,11 +155,13 @@ data Type
| ForAllTy -- See Note [ForAllTy]
{-# UNPACK #-} !ForAllTyBinder
- Type -- ^ A Π type.
- -- See Note [Why ForAllTy can quantify over a coercion variable]
- -- INVARIANT: If the binder is a coercion variable, it must
- -- be mentioned in the Type.
- -- See Note [Unused coercion variable in ForAllTy]
+ -- ForAllTyBinder: see GHC.Types.Var
+ -- Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility]
+ Type
+ -- INVARIANT: If the binder is a coercion variable, it must
+ -- be mentioned in the Type.
+ -- See Note [Unused coercion variable in ForAllTy]
+ -- See Note [Why ForAllTy can quantify over a coercion variable]
| FunTy -- ^ FUN m t1 t2 Very common, so an important special case
-- See Note [Function types]
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -120,13 +120,17 @@ tcFunBindMatches ctxt fun_name mult matches invis_pat_tys exp_ty
-- Makes sure that if the binding is unrestricted, it counts as
-- consuming its rhs Many times.
- do { traceTc "tcFunBindMatches 2" (vcat [ pprUserTypeCtxt ctxt, ppr invis_pat_tys
- , ppr pat_tys $$ ppr rhs_ty ])
+ do { traceTc "tcFunBindMatches 2" $
+ vcat [ text "ctxt:" <+> pprUserTypeCtxt ctxt
+ , text "arity:" <+> ppr arity
+ , text "invis_pat_tys:" <+> ppr invis_pat_tys
+ , text "pat_tys:" <+> ppr pat_tys
+ , text "rhs_ty:" <+> ppr rhs_ty ]
; tcMatches tcBody (invis_pat_tys ++ pat_tys) rhs_ty matches }
; return (wrap_fun, r) }
where
- herald = ExpectedFunTyMatches (NameThing fun_name) matches
+ herald = ExpectedFunTyMatches (NameThing fun_name) matches
funBindPrecondition :: MatchGroup GhcRn (LHsExpr GhcRn) -> Bool
funBindPrecondition (MG { mg_alts = L _ alts })
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1490,8 +1490,10 @@ tcSplitForAllTyVarsReqTVBindersN n_req ty
= split n_req ty ty []
where
split n_req _orig_ty (ForAllTy b@(Bndr _ argf) ty) bs
- | isVisibleForAllTyFlag argf, n_req > 0 = split (n_req - 1) ty ty (b:bs)
- | otherwise = split n_req ty ty (b:bs)
+ | isVisibleForAllTyFlag argf, n_req > 0 -- Split off a visible forall
+ = split (n_req - 1) ty ty (b:bs)
+ | isInvisibleForAllTyFlag argf -- Split off an invisible forall,
+ = split n_req ty ty (b:bs) -- even if n_req=0, i.e. the trailing ones
split n_req orig_ty ty bs | Just ty' <- coreView ty = split n_req orig_ty ty' bs
split n_req orig_ty _ty bs = (n_req, reverse bs, orig_ty)
@@ -1975,7 +1977,7 @@ isSigmaTy :: TcType -> Bool
-- forall a. blah
-- Eq a => blah
-- ?x::Int => blah
--- But not
+-- But NOT
-- forall a -> blah
isSigmaTy (ForAllTy (Bndr _ af) _) = isInvisibleForAllTyFlag af
isSigmaTy (FunTy { ft_af = af }) = isInvisibleFunArg af
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -648,6 +648,7 @@ data VarBndr var argf = Bndr var argf
-- A 'ForAllTyBinder' is the binder of a ForAllTy
-- It's convenient to define this synonym here rather its natural
-- home in "GHC.Core.TyCo.Rep", because it's used in GHC.Core.DataCon.hs-boot
+-- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility]
--
-- A 'TyVarBinder' is a binder with only TyVar
type ForAllTyBinder = VarBndr TyCoVar ForAllTyFlag
=====================================
testsuite/tests/polykinds/T25661.hs
=====================================
@@ -0,0 +1,38 @@
+{-# Language TypeFamilyDependencies #-}
+{-# Language RequiredTypeArguments #-}
+module T25661 where
+
+import Data.Kind
+import Control.Category (Category(id, (.)))
+import Prelude hiding (id, (.))
+
+type Cat :: Type -> Type
+type Cat k = k -> k -> Type
+-- type Op :: (k -> j -> Type) -> (j -> k -> Type)
+-- newtype Op cat b a = Op (cat a b)
+
+-- instance Category cat => Category (Op @k @k cat) where
+-- id = Op id
+-- Op f . Op g = Op (g . f)
+
+type NaturalTransformation :: Cat s -> Cat t -> Cat (s -> t)
+data NaturalTransformation src tgt f g where
+ -- NaturalTransformationId :: NaturalTransformation src tgt f f
+ NaturalTransformation :: (FunctorOf src tgt f, FunctorOf src tgt g) => { getNaturalTransformation :: forall x. f x `tgt` g x } -> NaturalTransformation src tgt f g
+
+type
+ FunctorOf :: Cat s -> Cat t -> (s -> t) -> Constraint
+class (NewFunctor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f
+instance (NewFunctor f, Source f ~ src, Target f ~ tgt) => FunctorOf src tgt f
+
+type
+ NewFunctor :: (s -> t) -> Constraint
+class (Category (Source f), Category (Target f)) => NewFunctor (f :: s -> t) where
+ type Source (f :: s -> t) :: Cat s
+ type Target (f :: s -> t) :: Cat t
+ newmap :: Source f a a' -> Target f (f a) (f a')
+
+
+newmapVis :: NewFunctor f => forall source -> source ~ Source f
+ => forall target -> target ~ Target f => source a a' -> target (f a) (f a')
+newmapVis source = undefined
=====================================
testsuite/tests/polykinds/T25661.stderr
=====================================
@@ -0,0 +1,17 @@
+T25661.hs:38:20: error: [GHC-91028]
+ • Couldn't match expected type ‘forall (target :: Cat t) ->
+ (target ~ Target f) => source a a' -> target (f a) (f a')’
+ with actual type ‘a0’
+ Cannot instantiate unification variable ‘a0’
+ with a type involving polytypes:
+ forall (target :: Cat t) ->
+ (target ~ Target f) => source a a' -> target (f a) (f a')
+ • In the expression: undefined
+ In an equation for ‘newmapVis’: newmapVis source = undefined
+ • Relevant bindings include
+ newmapVis :: forall (source :: Cat s) ->
+ (source ~ Source f) =>
+ forall (target :: Cat t) ->
+ (target ~ Target f) => source a a' -> target (f a) (f a')
+ (bound at T25661.hs:38:1)
+
=====================================
testsuite/tests/polykinds/all.T
=====================================
@@ -247,3 +247,4 @@ test('T24083', normal, compile_fail, [''])
test('T24083a', normal, compile, [''])
test('T24686', normal, compile_fail, [''])
test('T24686a', normal, compile_fail, [''])
+test('T25661', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/854c2f753dddeaa31d2988704cedf651f9fb7958
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/854c2f753dddeaa31d2988704cedf651f9fb7958
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/20250118/6232fd8e/attachment-0001.html>
More information about the ghc-commits
mailing list