[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 6 commits: Bump transformers submodule to 0.6.0.6
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Feb 1 12:50:52 UTC 2023
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
22089f69 by Ben Gamari at 2023-01-31T20:46:27-05:00
Bump transformers submodule to 0.6.0.6
Fixes #22862.
- - - - -
f0eefa3c by Cheng Shao at 2023-01-31T20:47:03-05:00
compiler: properly handle non-word-sized CmmSwitch scrutinees in the wasm NCG
Currently, the wasm NCG has an implicit assumption: all CmmSwitch
scrutinees are 32-bit integers. This is not always true; #22864 is one
counter-example with a 64-bit scrutinee. This patch fixes the logic by
explicitly converting the scrutinee to a word that can be used as a
br_table operand. Fixes #22871. Also includes a regression test.
- - - - -
9f95db54 by Simon Peyton Jones at 2023-02-01T08:55:08+00:00
Improve treatment of type applications in patterns
This patch fixes a subtle bug in the typechecking of type
applications in patterns, e.g.
f (MkT @Int @a x y) = ...
See Note [Type applications in patterns] in GHC.Tc.Gen.Pat.
This fixes #19847, #22383, #19577, #21501
- - - - -
e739c68c by Simon Peyton Jones at 2023-02-01T07:50:38-05:00
Treat existentials correctly in dubiousDataConInstArgTys
Consider (#22849)
data T a where
MkT :: forall k (t::k->*) (ix::k). t ix -> T @k a
Then dubiousDataConInstArgTys MkT [Type, Foo] should return
[Foo (ix::Type)]
NOT [Foo (ix::k)]
A bit of an obscure case, but it's an outright bug, and the fix is easy.
- - - - -
d97009fc by Matthew Pickering at 2023-02-01T07:50:38-05:00
Bump supported LLVM range from 10 through 15 to 11 through 16
LLVM 15 turns on the new pass manager by default, which we have yet to
migrate to so for new we pass the `-enable-new-pm-0` flag in our
llvm-passes flag.
LLVM 11 was the first version to support the `-enable-new-pm` flag so we
bump the lowest supported version to 11.
Our CI jobs are using LLVM 12 so they should continue to work despite
this bump to the lower bound.
Fixes #21936
- - - - -
407703c3 by Matthew Pickering at 2023-02-01T07:50:38-05:00
Bump DOCKER_REV to use alpine image without LLVM installed
alpine_3_12 only supports LLVM 10, which is now outside the supported
version range.
- - - - -
23 changed files:
- .gitlab-ci.yml
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Opt/WorkWrap/Utils.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Wasm/ControlFlow/FromCmm.hs
- configure.ac
- libraries/transformers
- llvm-passes
- + testsuite/tests/cmm/should_run/T22871.hs
- + testsuite/tests/cmm/should_run/T22871.stdout
- + testsuite/tests/cmm/should_run/T22871_cmm.cmm
- testsuite/tests/cmm/should_run/all.T
- + testsuite/tests/gadt/T19847.hs
- + testsuite/tests/gadt/T19847a.hs
- + testsuite/tests/gadt/T19847a.stderr
- + testsuite/tests/gadt/T19847b.hs
- testsuite/tests/gadt/all.T
- + testsuite/tests/simplCore/should_compile/T22849.hs
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/typecheck/should_compile/T19577.hs
- + testsuite/tests/typecheck/should_compile/T21501.hs
- + testsuite/tests/typecheck/should_compile/T22383.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
.gitlab-ci.yml
=====================================
@@ -2,7 +2,7 @@ variables:
GIT_SSL_NO_VERIFY: "1"
# Commit of ghc/ci-images repository from which to pull Docker images
- DOCKER_REV: 2d59d551647d102c4af44f257c520a94f04ea3f6
+ DOCKER_REV: 572353e0644044fe3a5465bba4342a9a0b0eb60e
# Sequential version number of all cached things.
# Bump to invalidate GitLab CI cache.
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -441,6 +441,7 @@ data DataCon
-- INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders is
-- exactly the set of tyvars (*not* covars) of dcExTyCoVars unioned
-- with the set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
+ -- So dcUserTyVarBinders is a subset of (dcUnivTyVars ++ dcExTyCoVars)
-- See Note [DataCon user type variable binders]
dcUserTyVarBinders :: [InvisTVBinder],
=====================================
compiler/GHC/Core/Opt/WorkWrap/Utils.hs
=====================================
@@ -707,7 +707,7 @@ Worker/wrapper will unbox
* is an algebraic data type (not a newtype)
* is not recursive (as per 'isRecDataCon')
* has a single constructor (thus is a "product")
- * that may bind existentials
+ * that may bind existentials (#18982)
We can transform
> data D a = forall b. D a b
> f (D @ex a b) = e
@@ -1272,16 +1272,25 @@ also unbox its components. That is governed by the `usefulSplit` mechanism.
-}
-- | Exactly 'dataConInstArgTys', but lacks the (ASSERT'ed) precondition that
--- the 'DataCon' may not have existentials. The lack of cloning the existentials
--- compared to 'dataConInstExAndArgVars' makes this function \"dubious\";
--- only use it where type variables aren't substituted for!
+-- the 'DataCon' may not have existentials. The lack of cloning the
+-- existentials this function \"dubious\"; only use it where type variables
+-- aren't substituted for! Why may the data con bind existentials?
+-- See Note [Which types are unboxed?]
dubiousDataConInstArgTys :: DataCon -> [Type] -> [Type]
dubiousDataConInstArgTys dc tc_args = arg_tys
where
- univ_tvs = dataConUnivTyVars dc
- ex_tvs = dataConExTyCoVars dc
- subst = extendSubstInScopeList (zipTvSubst univ_tvs tc_args) ex_tvs
- arg_tys = map (GHC.Core.Type.substTy subst . scaledThing) (dataConRepArgTys dc)
+ univ_tvs = dataConUnivTyVars dc
+ ex_tvs = dataConExTyCoVars dc
+ univ_subst = zipTvSubst univ_tvs tc_args
+ (full_subst, _) = substTyVarBndrs univ_subst ex_tvs
+ arg_tys = map (substTy full_subst . scaledThing) $
+ dataConRepArgTys dc
+ -- NB: use substTyVarBndrs on ex_tvs to ensure that we
+ -- substitute in their kinds. For example (#22849)
+ -- Consider data T a where
+ -- MkT :: forall k (t::k->*) (ix::k). t ix -> T @k a
+ -- Then dubiousDataConInstArgTys MkT [Type, Foo] should return
+ -- [Foo (ix::Type)], not [Foo (ix::k)]!
findTypeShape :: FamInstEnvs -> Type -> TypeShape
-- Uncover the arrow and product shape of a type
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -72,9 +72,12 @@ import Control.Arrow ( second )
import Control.Monad
import GHC.Data.FastString
import qualified Data.List.NonEmpty as NE
+
import GHC.Data.List.SetOps ( getNth )
import Language.Haskell.Syntax.Basic (FieldLabelString(..))
+import Data.List( partition )
+
{-
************************************************************************
* *
@@ -315,6 +318,11 @@ type Checker inp out = forall r.
, r -- Result of thing inside
)
+tcMultiple_ :: Checker inp () -> PatEnv -> [inp] -> TcM r -> TcM r
+tcMultiple_ tc_pat penv args thing_inside
+ = do { (_, res) <- tcMultiple tc_pat penv args thing_inside
+ ; return res }
+
tcMultiple :: Checker inp out -> Checker [inp] [out]
tcMultiple tc_pat penv args thing_inside
= do { err_ctxt <- getErrCtxt
@@ -861,10 +869,10 @@ tcConPat :: PatEnv -> LocatedN Name
tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
= do { con_like <- tcLookupConLike con_name
; case con_like of
- RealDataCon data_con -> tcDataConPat penv con_lname data_con
- pat_ty arg_pats thing_inside
- PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
- pat_ty arg_pats thing_inside
+ RealDataCon data_con -> tcDataConPat con_lname data_con pat_ty
+ penv arg_pats thing_inside
+ PatSynCon pat_syn -> tcPatSynPat con_lname pat_syn pat_ty
+ penv arg_pats thing_inside
}
-- Warn when pattern matching on a GADT or a pattern synonym
@@ -880,12 +888,11 @@ warnMonoLocalBinds
-- In #20485 this was made into a warning.
}
-tcDataConPat :: PatEnv -> LocatedN Name -> DataCon
+tcDataConPat :: LocatedN Name -> DataCon
-> Scaled ExpSigmaTypeFRR -- Type of the pattern
- -> HsConPatDetails GhcRn -> TcM a
- -> TcM (Pat GhcTc, a)
-tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
- arg_pats thing_inside
+ -> Checker (HsConPatDetails GhcRn) (Pat GhcTc)
+tcDataConPat (L con_span con_name) data_con pat_ty_scaled
+ penv arg_pats thing_inside
= do { let tycon = dataConTyCon data_con
-- For data families this is the representation tycon
(univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
@@ -921,21 +928,15 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
-- Why "super"? See Note [Binding when looking up instances]
-- in GHC.Core.InstEnv.
- ; let arg_tys' = substScaledTys tenv arg_tys
- pat_mult = scaledMult pat_ty_scaled
+ ; let arg_tys' = substScaledTys tenv arg_tys
+ pat_mult = scaledMult pat_ty_scaled
arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
+ con_like = RealDataCon data_con
-- This check is necessary to uphold the invariant that 'tcConArgs'
-- is given argument types with a fixed runtime representation.
-- See test case T20363.
- ; zipWithM_
- ( \ i arg_sty ->
- hasFixedRuntimeRep_syntactic
- (FRRDataConPatArg data_con i)
- (scaledThing arg_sty)
- )
- [1..]
- arg_tys'
+ ; checkFixedRuntimeRep data_con arg_tys'
; traceTc "tcConPat" (vcat [ text "con_name:" <+> ppr con_name
, text "univ_tvs:" <+> pprTyVars univ_tvs
@@ -947,11 +948,15 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
, text "pat_ty:" <+> ppr pat_ty
, text "arg_tys':" <+> ppr arg_tys'
, text "arg_pats" <+> ppr arg_pats ])
+
+ ; (univ_ty_args, ex_ty_args) <- splitConTyArgs con_like arg_pats
+
; if null ex_tvs && null eq_spec && null theta
then do { -- The common case; no class bindings etc
-- (see Note [Arrows and patterns])
- (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled
- tenv penv arg_pats thing_inside
+ (arg_pats', res) <- tcConTyArgs tenv penv univ_ty_args $
+ tcConValArgs con_like arg_tys_scaled
+ penv arg_pats thing_inside
; let res_pat = ConPat { pat_con = header
, pat_args = arg_pats'
, pat_con_ext = ConPatTc
@@ -974,8 +979,11 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
; given <- newEvVars theta'
; (ev_binds, (arg_pats', res))
- <- checkConstraints (getSkolemInfo skol_info) ex_tvs' given $
- tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside
+ <- -- See Note [Type applications in patterns] (W4)
+ tcConTyArgs tenv penv univ_ty_args $
+ checkConstraints (getSkolemInfo skol_info) ex_tvs' given $
+ tcConTyArgs tenv penv ex_ty_args $
+ tcConValArgs con_like arg_tys_scaled penv arg_pats thing_inside
; let res_pat = ConPat
{ pat_con = header
@@ -991,11 +999,10 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
; return (mkHsWrapPat wrap res_pat pat_ty, res)
} }
-tcPatSynPat :: PatEnv -> LocatedN Name -> PatSyn
+tcPatSynPat :: LocatedN Name -> PatSyn
-> Scaled ExpSigmaType -- ^ Type of the pattern
- -> HsConPatDetails GhcRn -> TcM a
- -> TcM (Pat GhcTc, a)
-tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
+ -> Checker (HsConPatDetails GhcRn) (Pat GhcTc)
+tcPatSynPat (L con_span con_name) pat_syn pat_ty penv arg_pats thing_inside
= do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
; (subst, univ_tvs') <- newMetaTyVars univ_tvs
@@ -1018,23 +1025,27 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
prov_theta' = substTheta tenv prov_theta
req_theta' = substTheta tenv req_theta
+ con_like = PatSynCon pat_syn
; when (any isEqPred prov_theta) warnMonoLocalBinds
; mult_wrap <- checkManyPattern pat_ty
-- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
- ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty'
- ; traceTc "tcPatSynPat" (ppr pat_syn $$
- ppr pat_ty $$
- ppr ty' $$
- ppr ex_tvs' $$
- ppr prov_theta' $$
- ppr req_theta' $$
- ppr arg_tys')
+ ; (univ_ty_args, ex_ty_args) <- splitConTyArgs con_like arg_pats
- ; prov_dicts' <- newEvVars prov_theta'
+ ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty'
+ ; traceTc "tcPatSynPat" $
+ vcat [ text "Pat syn:" <+> ppr pat_syn
+ , text "Expected type:" <+> ppr pat_ty
+ , text "Pat res ty:" <+> ppr ty'
+ , text "ex_tvs':" <+> pprTyVars ex_tvs'
+ , text "prov_theta':" <+> ppr prov_theta'
+ , text "req_theta':" <+> ppr req_theta'
+ , text "arg_tys':" <+> ppr arg_tys'
+ , text "univ_ty_args:" <+> ppr univ_ty_args
+ , text "ex_ty_args:" <+> ppr ex_ty_args ]
; req_wrap <- instCall (OccurrenceOf con_name) (mkTyVarTys univ_tvs') req_theta'
-- Origin (OccurrenceOf con_name):
@@ -1055,11 +1066,16 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
, text "bad_arg_tys:" <+> ppr bad_arg_tys ]
; traceTc "checkConstraints {" Outputable.empty
+ ; prov_dicts' <- newEvVars prov_theta'
; (ev_binds, (arg_pats', res))
- <- checkConstraints (getSkolemInfo skol_info) ex_tvs' prov_dicts' $
- tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
-
+ <- -- See Note [Type applications in patterns] (W4)
+ tcConTyArgs tenv penv univ_ty_args $
+ checkConstraints (getSkolemInfo skol_info) ex_tvs' prov_dicts' $
+ tcConTyArgs tenv penv ex_ty_args $
+ tcConValArgs con_like arg_tys_scaled penv arg_pats $
+ thing_inside
; traceTc "checkConstraints }" (ppr ev_binds)
+
; let res_pat = ConPat { pat_con = L con_span $ PatSynCon pat_syn
, pat_args = arg_pats'
, pat_con_ext = ConPatTc
@@ -1073,6 +1089,14 @@ tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
; pat_ty <- readExpType (scaledThing pat_ty)
; return (mkHsWrapPat (wrap <.> mult_wrap) res_pat pat_ty, res) }
+checkFixedRuntimeRep :: DataCon -> [Scaled TcSigmaTypeFRR] -> TcM ()
+checkFixedRuntimeRep data_con arg_tys
+ = zipWithM_ check_one [1..] arg_tys
+ where
+ check_one i arg_ty = hasFixedRuntimeRep_syntactic
+ (FRRDataConPatArg data_con i)
+ (scaledThing arg_ty)
+
{- Note [Call-stack tracing of pattern synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
@@ -1187,84 +1211,128 @@ Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
error messages; it's a purely internal thing
-}
-{-
-Note [Typechecking type applications in patterns]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-How should we typecheck type applications in patterns, such as
+{- Note [Type applications in patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type applications in patterns are enabled by -XTypeAbstractions.
+For example:
f :: Either (Maybe a) [b] -> blah
f (Left @x @[y] (v::Maybe x)) = blah
-It's quite straightforward, and very similar to the treatment of
-pattern signatures.
+How should we typecheck them? The basic plan is pretty simple, and is
+all done in tcConTyArgs. For each type argument:
-* Step 1: bind the newly-in-scope type variables x and y to fresh
- unification variables, say x0 and y0.
+* Step 1:
+ * bind the newly-in-scope type variables (here `x` or `y`) to
+ unification variables, say `x0` or `y0`
-* Step 2: typecheck those type arguments, @x and @[y], to get the
- types x0 and [y0].
+ * typecheck the type argument, `@x` or `@[y]` to get the
+ types `x0` or `[y0]`.
-* Step 3: Unify those types with the type arguments we expect,
- in this case (Maybe a) and [b]. These unifications will
- (perhaps after the constraint solver has done its work)
+ This step is done by `tcHsPatSigType`, similar to the way we
+ deal with pattern signatures.
+
+* Step 2: Unify those types with the type arguments we expect from
+ the context, in this case (Maybe a) and [b]. These unifications
+ will (perhaps after the constraint solver has done its work)
unify x0 := Maybe a
y0 := b
Thus we learn that x stands for (Maybe a) and y for b.
-Wrinkles:
-
-* Surprisingly, we can discard the coercions arising from
- these unifications. The *only* thing the unification does is
- to side-effect those unification variables, so that we know
- what type x and y stand for; and cause an error if the equality
- is not soluble. It's a bit like a constraint arising
- from a functional dependency, where we don't use the evidence.
-
-* Exactly the same works for existential arguments
- data T where
- MkT :: a -> a -> T
- f :: T -> blah
- f (MkT @x v w) = ...
- Here we create a fresh unification variable x0 for x, and
- unify it with the fresh existential variable bound by the pattern.
-
-* Note that both here and in pattern signatures the unification may
- not even end up unifying the variable. For example
- type S a b = a
- f :: Maybe a -> Bool
- f (Just @(S a b) x) = True :: b
- In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no
- effect on the unification variable b0, to which 'b' is bound.
- Later, in the RHS, we find that b0 must be Bool, and unify it there.
- All is fine.
+* Step 3: Extend the lexical context to bind `x` to `x0` and
+ `y` to `y0`, and typecheck the body of the pattern match.
+
+However there are several quite tricky wrinkles.
+
+(W1) Surprisingly, we can discard the coercions arising from
+ these unifications. The *only* thing the unification does is
+ to side-effect those unification variables, so that we know
+ what type x and y stand for; and cause an error if the equality
+ is not soluble. It's a bit like a constraint arising
+ from a functional dependency, where we don't use the evidence.
+
+(W2) Note that both here and in pattern signatures the unification may
+ not even end up unifying the variable. For example
+ type S a b = a
+ f :: Maybe a -> Bool
+ f (Just @(S a b) x) = True :: b
+ In Step 2 we will unify (S a0 b0 ~ a), which succeeds, but has no
+ effect on the unification variable b0, to which 'b' is bound.
+ Later, in the RHS, we find that b0 must be Bool, and unify it there.
+ All is fine.
+
+(W3) The order of the arguments to the /data constructor/ may differ from
+ the order of the arguments to the /type constructor/. Example
+ data T a b where { MkT :: forall c d. (c,d) -> T d c }
+ f :: T Int Bool -> blah
+ f (MkT @x @y p) = ...
+ The /first/ type argument to `MkT`, namely `@x` corresponds to the
+ /second/ argument to `T` in the type `T Int Bool`. So `x` is bound
+ to `Bool` -- not to `Int`!. That is why splitConTyArgs uses
+ conLikeUserTyVarBinders to match up with the user-supplied type arguments
+ in the pattern, not dataConUnivTyVars/dataConExTyVars.
+
+(W4) A similar story works for existentials, but it is subtly different
+ (#19847). Consider
+ data T a where { MkT :: forall a b. a -> b -> T a }
+ f :: T Int -> blah
+ f (MkT @x @y v w) = blah
+ Here we create a fresh unification variables x0,y0 for x,y and
+ unify x0~Int, y0~b, where b is the fresh existential variable bound by
+ the pattern. But
+ * (x0~Int) must be /outside/ the implication constraint
+ * (y0~b) must be /inside/ it
+ (and hence x0 and y0 themselves must have different levels).
+ Thus:
+ x0[1]~Int, (forall[2] b. (y0[2]~b, ...constraints-from-blah...))
+
+ We need (x0~Int) /outside/ so that it can influence the type of the
+ pattern in an inferred setting, e.g.
+ g :: T _ -> blah
+ g (MkT @Int @y v w) = blah
+ Here we want to infer `g` to have type `T Int -> blah`. If the
+ (x0~Int) was inside the implication, and the the constructor bound
+ equality constraints, `x0` would be untouchable. This was the root
+ cause of #19847.
+
+ We need (y0~b) to be /inside/ the implication, so that `b` is in
+ scope. In fact, we may actually /need/ equalities bound by the
+ implication to prove the equality constraint we generate.
+ Example data T a where
+ MkT :: forall p q. T (p,q)
+ f :: T (Int,Bool) -> blah
+ f (MkT @Int @Bool) = ...
+ We get the implication
+ forall[2] p q. (p,q)~(Int,Bool) => (p ~ Int, q ~ Bool, ...)
+ where the Given comes from the GADT match, while (p~Int, q~Bool)
+ comes from matching the type arguments.
+
+ Wow. That's all quite subtle! See the long discussion on #19847. We
+ must treat universal and existential arguments separately, even though
+ they are all mixed up (W3). The function splitConTyArgs separates the
+ universals from existentials; and we build the implication between
+ typechecking the two sets:
+ tcConTyArgs ... univ_ty_args $
+ checkConstraints ... $
+ tcConTyArgs ... ex_ty_args $
+ ..typecheck body..
+ You can see this code shape in tcDataConPat and tcPatSynPat.
+
+ Where pattern synonyms are involved, this two-level split may not be
+ enough. See #22328 for the story.
-}
-tcConArgs :: ConLike
- -> [Scaled TcSigmaTypeFRR]
- -> Subst -- Instantiating substitution for constructor type
- -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
-tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
+tcConValArgs :: ConLike
+ -> [Scaled TcSigmaTypeFRR]
+ -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+tcConValArgs con_like arg_tys penv con_args thing_inside = case con_args of
PrefixCon type_args arg_pats -> do
+ -- NB: type_args already dealt with
+ -- See Note [Type applications in patterns]
{ checkTc (con_arity == no_of_args) -- Check correct arity
(arityErr (text "constructor") con_like con_arity no_of_args)
- -- forgetting to filter out inferred binders led to #20443
- ; let con_spec_binders = filter ((== SpecifiedSpec) . binderFlag) $
- conLikeUserTyVarBinders con_like
- ; checkTc (type_args `leLength` con_spec_binders)
- (TcRnTooManyTyArgsInConPattern con_like (length con_spec_binders) (length type_args))
-
; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
- ; (type_args', (arg_pats', res))
- <- tcMultiple tcConTyArg penv type_args $
- tcMultiple tcConArg penv pats_w_tys thing_inside
-
- -- This unification is straight from Figure 7 of
- -- "Type Variables in Patterns", Haskell'18
- ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
- binderVars con_spec_binders)
- -- OK to drop coercions here. These unifications are all about
- -- guiding inference based on a user-written type annotation
- -- See Note [Typechecking type applications in patterns]
+ ; (arg_pats', res) <- tcMultiple tcConArg penv pats_w_tys thing_inside
; return (PrefixCon type_args arg_pats', res) }
where
@@ -1321,23 +1389,72 @@ tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
-- dataConFieldLabels will be empty (and each field in the pattern
-- will generate an error below).
-tcConTyArg :: Checker (HsConPatTyArg GhcRn) TcType
-tcConTyArg penv (HsConPatTyArg _ rn_ty) thing_inside
+
+splitConTyArgs :: ConLike -> HsConPatDetails GhcRn
+ -> TcM ( [(HsConPatTyArg GhcRn, TyVar)] -- Universals
+ , [(HsConPatTyArg GhcRn, TyVar)] ) -- Existentials
+-- See Note [Type applications in patterns] (W4)
+-- This function is monadic only because of the error check
+-- for too many type arguments
+splitConTyArgs con_like (PrefixCon type_args _)
+ = do { checkTc (type_args `leLength` con_spec_bndrs)
+ (TcRnTooManyTyArgsInConPattern con_like
+ (length con_spec_bndrs) (length type_args))
+ ; if null ex_tvs -- Short cut common case
+ then return (bndr_ty_arg_prs, [])
+ else return (partition is_universal bndr_ty_arg_prs) }
+ where
+ ex_tvs = conLikeExTyCoVars con_like
+ con_spec_bndrs = [ tv | Bndr tv SpecifiedSpec <- conLikeUserTyVarBinders con_like ]
+ -- conLikeUserTyVarBinders: see (W3) in
+ -- Note [Type applications in patterns]
+ -- SpecifiedSpec: forgetting to filter out inferred binders led to #20443
+
+ bndr_ty_arg_prs = type_args `zip` con_spec_bndrs
+ -- The zip truncates to length(type_args)
+
+ is_universal (_, tv) = not (tv `elem` ex_tvs)
+ -- See Note [DataCon user type variable binders] in GHC.Core.DataCon
+ -- especially INVARIANT(dataConTyVars).
+
+splitConTyArgs _ (RecCon {}) = return ([], []) -- No type args in RecCon
+splitConTyArgs _ (InfixCon {}) = return ([], []) -- No type args in InfixCon
+
+tcConTyArgs :: Subst -> PatEnv -> [(HsConPatTyArg GhcRn, TyVar)]
+ -> TcM a -> TcM a
+tcConTyArgs tenv penv prs thing_inside
+ = tcMultiple_ (tcConTyArg tenv) penv prs thing_inside
+
+tcConTyArg :: Subst -> Checker (HsConPatTyArg GhcRn, TyVar) ()
+tcConTyArg tenv penv (HsConPatTyArg _ rn_ty, con_tv) thing_inside
= do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind
-- AnyKind is a bit suspect: it really should be the kind gotten
-- from instantiating the constructor type. But this would be
-- hard to get right, because earlier type patterns might influence
-- the kinds of later patterns. In any case, it all gets checked
- -- by the calls to unifyType in tcConArgs, which will also unify
- -- kinds.
+ -- by the calls to unifyType below which unifies kinds
+
; case NE.nonEmpty sig_ibs of
Just sig_ibs_ne | inPatBind penv ->
addErr (TcRnCannotBindTyVarsInPatBind sig_ibs_ne)
_ -> pure ()
+
+ -- This unification is straight from Figure 7 of
+ -- "Type Variables in Patterns", Haskell'18
+ -- OK to drop coercions here. These unifications are all about
+ -- guiding inference based on a user-written type annotation
+ -- See Note [Type applications in patterns] (W1)
+ ; _ <- unifyType Nothing arg_ty (substTyVar tenv con_tv)
+
; result <- tcExtendNameTyVarEnv sig_wcs $
tcExtendNameTyVarEnv sig_ibs $
thing_inside
- ; return (arg_ty, result) }
+ -- NB: Because we call tConTyArgs twice, once for universals and
+ -- once for existentials; so this brings things into scope
+ -- "out of left-right order". But it doesn't matter; the renamer
+ -- has dealt with all that.
+
+ ; return ((), result) }
tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc)
tcConArg penv (arg_pat, Scaled arg_mult arg_ty)
=====================================
compiler/GHC/Wasm/ControlFlow/FromCmm.hs
=====================================
@@ -75,7 +75,7 @@ flowLeaving platform b =
let (offset, target_labels) = switchTargetsToTable targets
(lo, hi) = switchTargetsRange targets
default_label = switchTargetsDefault targets
- scrutinee = smartPlus platform e offset
+ scrutinee = smartExtend platform $ smartPlus platform e offset
range = inclusiveInterval (lo+toInteger offset) (hi+toInteger offset)
in Switch scrutinee range target_labels default_label
CmmCall { cml_cont = Nothing, cml_target = e } -> TailCall e
@@ -314,6 +314,14 @@ structuredControl platform txExpr txBlock g =
nodeBody :: CmmBlock -> CmmActions
nodeBody (BlockCC _first middle _last) = middle
+-- | A CmmSwitch scrutinee may have any width, but a br_table operand
+-- must be exactly word sized, hence the extension here. (#22871)
+smartExtend :: Platform -> CmmExpr -> CmmExpr
+smartExtend p e | w0 == w1 = e
+ | otherwise = CmmMachOp (MO_UU_Conv w0 w1) [e]
+ where
+ w0 = cmmExprWidth p e
+ w1 = wordWidth p
smartPlus :: Platform -> CmmExpr -> Int -> CmmExpr
smartPlus _ e 0 = e
=====================================
configure.ac
=====================================
@@ -554,8 +554,8 @@ AC_SUBST(InstallNameToolCmd)
# tools we are looking for. In the past, GHC supported a number of
# versions of LLVM simultaneously, but that stopped working around
# 3.5/3.6 release of LLVM.
-LlvmMinVersion=10 # inclusive
-LlvmMaxVersion=15 # not inclusive
+LlvmMinVersion=11 # inclusive
+LlvmMaxVersion=16 # not inclusive
AC_SUBST([LlvmMinVersion])
AC_SUBST([LlvmMaxVersion])
sUPPORTED_LLVM_VERSION_MIN=$(echo \($LlvmMinVersion\) | sed 's/\./,/')
=====================================
libraries/transformers
=====================================
@@ -1 +1 @@
-Subproject commit 2745db6c374c7e830a0f8fdeb8cc39bd8f054f36
+Subproject commit ceff1dcd7893f7ab4abb6e66bcd248abd86c8886
=====================================
llvm-passes
=====================================
@@ -1,5 +1,5 @@
[
-(0, "-mem2reg -globalopt -lower-expect"),
-(1, "-O1 -globalopt"),
-(2, "-O2")
+(0, "-enable-new-pm=0 -mem2reg -globalopt -lower-expect"),
+(1, "-enable-new-pm=0 -O1 -globalopt"),
+(2, "-enable-new-pm=0 -O2")
]
=====================================
testsuite/tests/cmm/should_run/T22871.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE GHCForeignImportPrim #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnliftedFFITypes #-}
+
+import Data.Foldable
+import GHC.Exts
+import GHC.Int
+
+foreign import prim "foo" foo :: Int64# -> Int64#
+
+main :: IO ()
+main = for_ [0, 42, 114514] $ \(I64# x#) -> print $ I64# (foo x#)
=====================================
testsuite/tests/cmm/should_run/T22871.stdout
=====================================
@@ -0,0 +1,3 @@
+233
+84
+1919810
=====================================
testsuite/tests/cmm/should_run/T22871_cmm.cmm
=====================================
@@ -0,0 +1,16 @@
+#include "Cmm.h"
+
+foo (I64 x) {
+ switch [0 .. 114514] (x) {
+ case 0: { return (233 :: I64); }
+ case 1: { return (333 :: I64); }
+ case 2: { return (666 :: I64); }
+ case 3: { return (1989 :: I64); }
+ case 4: { return (1997 :: I64); }
+ case 5: { return (2012 :: I64); }
+ case 6: { return (2019 :: I64); }
+ case 7: { return (2022 :: I64); }
+ case 114514: { return (1919810 :: I64); }
+ default: { return (x * (2 :: I64)); }
+ }
+}
=====================================
testsuite/tests/cmm/should_run/all.T
=====================================
@@ -25,3 +25,12 @@ test('ByteSwitch',
],
multi_compile_and_run,
['ByteSwitch', [('ByteSwitch_cmm.cmm', '')], ''])
+
+test('T22871',
+ [ extra_run_opts('"' + config.libdir + '"')
+ , omit_ways(['ghci'])
+ , js_skip
+ , when(arch('i386'), skip) # x86 NCG panics with "iselExpr64(i386)"
+ ],
+ multi_compile_and_run,
+ ['T22871', [('T22871_cmm.cmm', '')], ''])
=====================================
testsuite/tests/gadt/T19847.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE GADTs, PatternSynonyms, ViewPatterns, ScopedTypeVariables #-}
+
+module T19847 where
+
+import Data.Kind
+import Type.Reflection
+
+pattern Is :: forall (b :: Type) (a :: Type). Typeable b => (a ~ b) => TypeRep a
+pattern Is <- (eqTypeRep (typeRep @b) -> Just HRefl)
+ where Is = typeRep
+
+def :: TypeRep a -> a
+def x = case x of
+ Is @Int -> 10
+ Is @Bool -> False
=====================================
testsuite/tests/gadt/T19847a.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE LambdaCase, GADTs, ScopedTypeVariables, TypeAbstractions #-}
+
+module T19847a where
+
+data T a b c where
+ MkT :: forall c y x b. (x~y, c~[x], Ord x) => x -> y -> T (x,y) b c
+
+f :: forall b c. (T (Int,Int) b c -> Bool) -> (b,c)
+f = error "urk"
+
+h = f (\case { MkT @_ @_ @_ @Int p q -> True })
+-- Check that the @Int argument can affect
+-- the type at which `f` is instantiated
+-- So h :: forall c. (Int,c)
=====================================
testsuite/tests/gadt/T19847a.stderr
=====================================
@@ -0,0 +1,12 @@
+TYPE SIGNATURES
+ f :: forall b c. (T (Int, Int) b c -> Bool) -> (b, c)
+ h :: forall {c}. (Int, c)
+TYPE CONSTRUCTORS
+ data type T{4} :: forall {k}. * -> k -> * -> *
+ roles nominal nominal phantom nominal
+DATA CONSTRUCTORS
+ MkT :: forall {k} c y x (b :: k).
+ (x ~ y, c ~ [x], Ord x) =>
+ x -> y -> T (x, y) b c
+Dependent modules: []
+Dependent packages: [base-4.18.0.0]
=====================================
testsuite/tests/gadt/T19847b.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeAbstractions, GADTs #-}
+
+module T19847b where
+
+import Data.Kind
+
+data T (a :: Type) b where
+ MkT4 :: forall a b. b ~ a => T a b
+
+foo x = (case x of MkT4 @Bool -> ()) :: ()
=====================================
testsuite/tests/gadt/all.T
=====================================
@@ -126,3 +126,6 @@ test('SynDataRec', normal, compile, [''])
test('T20485', normal, compile, [''])
test('T20485a', normal, compile, [''])
test('T22235', normal, compile, [''])
+test('T19847', normal, compile, [''])
+test('T19847a', normal, compile, ['-ddump-types'])
+test('T19847b', normal, compile, [''])
=====================================
testsuite/tests/simplCore/should_compile/T22849.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs #-}
+
+module T22849 where
+
+data Foo a where
+ Foo :: Foo Int
+
+data Bar a = Bar a (Foo a)
+
+data Some t = forall ix. Some (t ix)
+
+instance Show (Some Bar) where
+ show (Some (Bar v t)) = case t of
+ Foo -> show v
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -453,7 +453,7 @@ test('T22375', normal, compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeab
test('T21851_2', [grep_errmsg(r'wwombat') ], multimod_compile, ['T21851_2', '-O -dno-typeable-binds -dsuppress-uniques'])
# Should not inline m, so there shouldn't be a single YES
test('T22317', [grep_errmsg(r'ANSWER = YES') ], compile, ['-O -dinline-check m -ddebug-output'])
-
+test('T22849', normal, compile, ['-O'])
test('T22634', normal, compile, ['-O -fcatch-nonexhaustive-cases'])
test('T22494', [grep_errmsg(r'case') ], compile, ['-O -ddump-simpl -dsuppress-uniques'])
test('T22491', normal, compile, ['-O2'])
@@ -472,3 +472,4 @@ test('T22611', [when(wordsize(32), skip), grep_errmsg(r'\$salterF') ], compile,
test('T22715_2', normal, multimod_compile, ['T22715_2', '-v0 -O -fspecialise-aggressively'])
test('T22802', normal, compile, ['-O'])
test('T15205', normal, compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-uniques'])
+
=====================================
testsuite/tests/typecheck/should_compile/T19577.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T19577 where
+
+data SBool (b :: Bool) where
+ STrue :: forall b. (b ~ 'True) => SBool b
+ SFalse :: forall b. (b ~ 'False) => SBool b
+
+class Blah b where
+ blah :: SBool b
+
+instance Blah 'True where
+ blah = STrue
+
+foo :: Blah b => (SBool b -> Int) -> Int
+foo f = f blah
+
+bar = foo (\(STrue @True) -> 42)
=====================================
testsuite/tests/typecheck/should_compile/T21501.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE MonoLocalBinds, PatternSynonyms, ViewPatterns, TypeAbstractions #-}
+
+module T21501 where
+
+import Data.Kind
+import Type.Reflection
+
+pattern TypeApp ::
+ forall {k1} {k2} (f :: k1 -> k2) (result :: k2).
+ Typeable f =>
+ forall (arg :: k1).
+ result ~ f arg =>
+ TypeRep arg ->
+ TypeRep result
+pattern TypeApp arg_rep <- App (eqTypeRep (typeRep @f) -> Just HRefl) arg_rep
+
+f :: TypeRep (a :: Type) -> String
+f (TypeApp @[] rep) = show rep
+
+{- Expected type: TypeRep k (a::k)
+ Instantiate at k10 k20 (f0 :: k10 -> k20) (result0 :: k20)
+ Unify (TypeRep k (a::k) ~ TypeRep k20 (result :: k20)
+ Unify f0 ~ []
+-}
=====================================
testsuite/tests/typecheck/should_compile/T22383.hs
=====================================
@@ -0,0 +1,83 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase, ScopedTypeVariables #-}
+
+module T22383 where
+
+import Data.Kind (Type)
+import Data.Proxy (Proxy(Proxy))
+
+-- | @IsType k@ witnesses that @k ~ Type at .
+data IsType k where
+ IsType :: IsType Type
+
+---------------------
+-- Using a GADT
+---------------------
+
+data FromType where
+ FromType :: forall (f :: Type -> Type). FromType
+
+-- | @FunRep (f b)@ witnesses that @b :: Type at .
+data FunRep a where
+ AppK ::
+ forall (k :: Type) (f :: k -> Type) (b :: k).
+ IsType k ->
+ Proxy f ->
+ FunRep (f b)
+
+-- Could not deduce: k ~ *
+isMaybeF :: forall (a :: Type). FunRep a -> FromType
+isMaybeF = \case
+ AppK @_ @f @_ t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType @f
+
+-- Could not deduce: k ~ *
+isMaybeG :: forall (a :: Type). FunRep a -> FromType
+isMaybeG = \case
+ AppK @_ @f @_ t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType @g
+
+-- Works fine
+isMaybeH :: forall (a :: Type). FunRep a -> FromType
+isMaybeH = \case
+ AppK @_ @f @_ t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType @h
+
+
+---------------------
+-- Not using a GADT
+---------------------
+
+data FunRep2 a where
+ AppK2 ::
+ forall k (b :: k).
+ IsType k ->
+ Proxy k ->
+ FunRep2 b
+
+data FromType2 where
+ FromType2 :: forall (b :: Type). FromType2
+
+-- Could not deduce: k ~ *
+isMaybeF2 :: forall k (a :: k). FunRep2 a -> FromType2
+isMaybeF2 = \case
+ AppK2 @_ @f t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType2 @f
+
+-- Works fine
+isMaybeG2 :: forall k (a :: k). FunRep2 a -> FromType2
+isMaybeG2 = \case
+ AppK2 @_ @f t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType2 @g
+
+-- Works fine
+isMaybeH2 :: forall k (a :: k). FunRep2 a -> FromType2
+isMaybeH2 = \case
+ AppK2 @_ @f t (Proxy @g :: Proxy h) ->
+ case t of
+ IsType -> FromType2 @h
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -854,3 +854,6 @@ test('T22310', normal, compile, [''])
test('T22331', normal, compile, [''])
test('T22516', normal, compile, [''])
test('T22647', normal, compile, [''])
+test('T19577', normal, compile, [''])
+test('T22383', normal, compile, [''])
+test('T21501', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/133344e0dbff97baafbd45377e3d3595f6f9232d...407703c34ffb649bbcf87a3218304342fd48ac16
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/133344e0dbff97baafbd45377e3d3595f6f9232d...407703c34ffb649bbcf87a3218304342fd48ac16
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/20230201/e509f808/attachment-0001.html>
More information about the ghc-commits
mailing list