[Git][ghc/ghc][master] Better skolemisation
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu May 23 01:56:12 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
3d9e4ce6 by Simon Peyton Jones at 2024-05-22T21:54:43-04:00
Better skolemisation
As #24810 showed, it is (a little) better to skolemise en-bloc,
so that Note [Let-bound skolems] fires more often.
See Note [Skolemisation en bloc] in GHC.Tc.Utils.Instantiate.
- - - - -
10 changed files:
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Utils.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/GHC/Types/Var.hs
- + testsuite/tests/typecheck/should_compile/T24810.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -2369,8 +2369,8 @@ mkEtaForAllMCo (Bndr tcv vis) ty mco
(mkNomReflCo (varType tcv)) co)
-- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly
-- the (EtaInfo Invariant). (sym co) wraps a lambda that always has
- -- a ForAllTyFlag of coreTyLamForAllTyFlag; see wrinkle (FC4) in
- -- Note [ForAllCo] in GHC.Core.TyCo.Rep
+ -- a ForAllTyFlag of coreTyLamForAllTyFlag; see Note [Required foralls in Core]
+ -- in GHC.Core.TyCo.Rep
{-
************************************************************************
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1195,6 +1195,24 @@ among branches, but that doesn't quite concern us here.)
The Int in the AxiomInstCo constructor is the 0-indexed number
of the chosen branch.
+Note [Required foralls in Core]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the CoreExpr (Lam a e) where `a` is a TyVar, and (e::e_ty).
+It has type
+ forall a. e_ty
+Note the Specified visibility of (forall a. e_ty); the Core type just isn't able
+to express more than one visiblity, and we pick `Specified`. See `exprType` and
+`mkLamType` in GHC.Core.Utils, and `GHC.Type.Var.coreLamForAllTyFlag`.
+
+So how can we ever get a term of type (forall a -> e_ty)? Answer: /only/ via a
+cast built with ForAllCo. See `GHC.Tc.Types.Evidence.mkWpForAllCast`. This does
+not seem very satisfying, but it does the job.
+
+An alternative would be to put a visibility flag into `Lam` (a huge change),
+or into a `TyVar` (a more plausible change), but we leave that for the future.
+
+See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
+
Note [ForAllCo]
~~~~~~~~~~~~~~~
See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
@@ -1251,10 +1269,7 @@ Several things to note here
in the typing rule. See also Note [ForAllTy and type equality] in
GHC.Core.TyCo.Compare.
-(FC4) A lambda term (Lam a e) has type (forall a. ty), with visibility
- flag `GHC.Type.Var.coreTyLamForAllTyFlag`, not (forall a -> ty).
- See `GHC.Type.Var.coreTyLamForAllTyFlag` and `GHC.Core.Utils.mkLamType`.
- The only way to get a term of type (forall a -> ty) is to cast a lambda.
+(FC4) See Note [Required foralls in Core].
(FC5) In a /type/, in (ForAllTy cv ty) where cv is a CoVar, we insist that
`cv` must appear free in `ty`; see Note [Unused coercion variable in ForAllTy]
=====================================
compiler/GHC/Core/Utils.hs
=====================================
@@ -170,7 +170,7 @@ mkLamTypes :: [Var] -> Type -> Type
mkLamType v body_ty
| isTyVar v
= mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
- -- coreTyLamForAllTyFlag: see (FC4) in Note [ForAllCo]
+ -- coreTyLamForAllTyFlag: see Note [Required foralls in Core]
-- in GHC.Core.TyCo.Rep
| isCoVar v
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -7,7 +7,7 @@ module GHC.Tc.Types.Evidence (
-- * HsWrapper
HsWrapper(..),
- (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpVisTyLam,
+ (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpForAllCast,
mkWpEvLams, mkWpLet, mkWpFun, mkWpCastN, mkWpCastR, mkWpEta,
collectHsWrapBinders,
idHsWrapper, isIdHsWrapper,
@@ -258,20 +258,20 @@ mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
mkWpTyLams :: [TyVar] -> HsWrapper
mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
--- Construct a type lambda and cast its type
--- from `forall tv. res` to `forall tv -> res`.
+-- mkWpForAllCast [tv{vis}] constructs a cast
+-- forall tv. res ~R# forall tv{vis} res`.
+-- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep
--
--- (\ @tv -> e )
--- `cast` (forall (tv[spec]~[req] :: <*>_N). <res>_R -- ForAllCo is the evidence that...
--- :: (forall tv. res) ~R# (forall tv -> res)) -- invisible and visible foralls are representationally equal
---
-mkWpVisTyLam :: TyVar -> Type -> HsWrapper
-mkWpVisTyLam tv res =
- WpCast (mkForAllCo tv coreTyLamForAllTyFlag Required kind_co body_co)
- <.> WpTyLam tv
+-- It's a no-op if all binders are invisible;
+-- but in that case we refrain from calling it.
+mkWpForAllCast :: [ForAllTyBinder] -> Type -> HsWrapper
+mkWpForAllCast bndrs res_ty
+ = mkWpCastR (go bndrs)
where
- kind_co = mkNomReflCo (varType tv)
- body_co = mkRepReflCo res
+ go [] = mkRepReflCo res_ty
+ go (Bndr tv vis : bs) = mkForAllCo tv coreTyLamForAllTyFlag vis kind_co (go bs)
+ where
+ kind_co = mkNomReflCo (varType tv)
mkWpEvLams :: [Var] -> HsWrapper
mkWpEvLams ids = mk_co_lam_fn WpEvLam ids
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -11,7 +11,7 @@
-}
module GHC.Tc.Utils.Instantiate (
- topSkolemise,
+ topSkolemise, skolemiseRequired,
topInstantiate,
instantiateSigma,
instCall, instDFunType, instStupidTheta, instTyVarsWith,
@@ -75,7 +75,7 @@ import GHC.Tc.Errors.Types
import GHC.Tc.Zonk.Monad ( ZonkM )
import GHC.Types.Id.Make( mkDictFunId )
-import GHC.Types.Basic ( TypeOrKind(..), Arity )
+import GHC.Types.Basic ( TypeOrKind(..), Arity, VisArity )
import GHC.Types.Error
import GHC.Types.SourceText
import GHC.Types.SrcLoc as SrcLoc
@@ -145,22 +145,16 @@ newMethodFromName origin name ty_args
Note [Skolemisation]
~~~~~~~~~~~~~~~~~~~~
topSkolemise decomposes and skolemises a type, returning a type
-with no top level foralls or (=>)
+with no top level foralls or (=>).
Examples:
topSkolemise (forall a. Ord a => a -> a)
= ( wp, [a], [d:Ord a], a->a )
- where wp = /\a. \(d:Ord a). <hole> a d
+ where
+ wp = /\a. \(d:Ord a). <hole> a d
- topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b)
- = ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
- where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2
-
-This second example is the reason for the recursive 'go' function in
-topSkolemise: we remove successive layers of foralls and (=>). This
-is really just an optimisation; see wrinkle (SK1) in GHC.Tc.Utils.Unify
-Note [Skolemisation overview].
+For nested foralls, see Note [Skolemisation en-bloc]
In general,
if topSkolemise ty = (wrap, tvs, evs, rho)
@@ -168,6 +162,41 @@ In general,
then wrap e :: ty
and 'wrap' binds {tvs, evs}
+Note [Skolemisation en-bloc]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this case:
+
+ topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b)
+
+We /could/ return just
+ (wp, [a], [d:Ord a, forall b. Eq b => a -> b -> b)
+
+But in fact we skolemise "en-bloc", looping around (in `topSkolemise` for
+example) to skolemise the (forall b. Eq b =>). So in fact
+
+ topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b)
+ = ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
+ where
+ wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2
+
+This applies regardless of DeepSubsumption.
+
+Why do we do this "en-bloc" loopy thing? It is /nearly/ just an optimisation.
+But not quite! At the call site of `topSkolemise` (and its cousins) we
+use `checkConstraints` to gather constraints and build an implication
+constraint. So skolemising just one level at a time would lead to nested
+implication constraints. That is a bit less efficient, but there is /also/ a small
+user-visible effect: see Note [Let-bound skolems] in GHC.Tc.Solver.InertSet.
+Specifically, consider
+
+ forall a. Eq a => forall b. (a ~ [b]) => blah
+
+If we skolemise en-bloc, the equality (a~[b]) is like a let-binding and we
+don't treat it like a GADT pattern match, limiting unification. With nested
+implications, the inner one would be treated as having-given-equalities.
+
+This is also relevant when Required foralls are involved; see #24810, and
+the loop in `skolemiseRequired`.
-}
topSkolemise :: SkolemInfo
@@ -182,7 +211,7 @@ topSkolemise skolem_info ty
where
init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
- -- Why recursive? See Note [Skolemisation]
+ -- Why recursive? See Note [Skolemisation en-bloc]
go subst wrap tv_prs ev_vars ty
| (bndrs, theta, inner_ty) <- tcSplitSigmaTyBndrs ty
, let tvs = binderVars bndrs
@@ -202,6 +231,51 @@ topSkolemise skolem_info ty
= return (wrap, tv_prs, ev_vars, substTy subst ty)
-- substTy is a quick no-op on an empty substitution
+skolemiseRequired :: SkolemInfo -> VisArity -> TcSigmaType
+ -> TcM (VisArity, HsWrapper, [Name], [ForAllTyBinder], [EvVar], TcRhoType)
+-- Skolemise up to N required (visible) binders,
+-- plus any invisible ones "in the way",
+-- /and/ any trailing invisible ones.
+-- So the result has no top-level invisible quantifiers.
+-- Return the depleted arity.
+skolemiseRequired skolem_info n_req sigma
+ = go n_req init_subst idHsWrapper [] [] [] sigma
+ where
+ init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType sigma))
+
+ -- Why recursive? See Note [Skolemisation en-bloc]
+ go n_req subst wrap acc_nms acc_bndrs ev_vars ty
+ | (n_req', bndrs, inner_ty) <- tcSplitForAllTyVarsReqTVBindersN n_req ty
+ , not (null bndrs)
+ = do { (subst', bndrs1) <- tcInstSkolTyVarBndrsX skolem_info subst bndrs
+ ; let tvs1 = binderVars bndrs1
+ -- fix_up_vis: see Note [Required foralls in Core]
+ -- in GHC.Core.TyCo.Rep
+ fix_up_vis | n_req == n_req'
+ = idHsWrapper
+ | otherwise
+ = mkWpForAllCast bndrs1 (substTy subst' inner_ty)
+ ; go n_req' subst'
+ (wrap <.> fix_up_vis <.> mkWpTyLams tvs1)
+ (acc_nms ++ map (tyVarName . binderVar) bndrs)
+ (acc_bndrs ++ bndrs1)
+ ev_vars
+ inner_ty }
+
+ | (theta, inner_ty) <- tcSplitPhiTy ty
+ , not (null theta)
+ = do { ev_vars1 <- newEvVars (substTheta subst theta)
+ ; go n_req subst
+ (wrap <.> mkWpEvLams ev_vars1)
+ acc_nms
+ acc_bndrs
+ (ev_vars ++ ev_vars1)
+ inner_ty }
+
+ | otherwise
+ = return (n_req, wrap, acc_nms, acc_bndrs, ev_vars, substTy subst ty)
+ -- substTy is a quick no-op on an empty substitution
+
topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
-- Instantiate outer invisible binders (both Inferred and Specified)
-- If top_instantiate ty = (wrap, inner_ty)
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -67,7 +67,7 @@ module GHC.Tc.Utils.TcType (
--------------------------------
-- Splitters
getTyVar, getTyVar_maybe, getCastedTyVar_maybe,
- tcSplitForAllTyVarBinder_maybe,
+ tcSplitForAllTyVarBinder_maybe, tcSplitForAllTyVarsReqTVBindersN,
tcSplitForAllTyVars, tcSplitForAllInvisTyVars, tcSplitSomeForAllTyVars,
tcSplitForAllReqTVBinders, tcSplitForAllInvisTVBinders,
tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBinders,
@@ -1410,6 +1410,18 @@ tcSplitSomeForAllTyVars argf_pred ty
split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs
split orig_ty _ tvs = (reverse tvs, orig_ty)
+tcSplitForAllTyVarsReqTVBindersN :: Arity -> Type -> (Arity, [ForAllTyBinder], Type)
+-- Split off at most N /required/ (aka visible) binders, plus any invisible ones
+-- in the way, /and/ any trailing invisible ones
+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)
+ 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)
+
-- | Like 'tcSplitForAllTyVars', but only splits 'ForAllTy's with 'Required' type
-- variable binders. All split tyvars are annotated with '()'.
tcSplitForAllReqTVBinders :: Type -> ([TcReqTVBinder], Type)
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -350,8 +350,8 @@ Some wrinkles
The implication constraint will look like
forall a b. (Eq a, Ord b) => <constraints>
See the loop in GHC.Tc.Utils.Instantiate.topSkolemise.
- This is just an optimisation; it would be fine to generate one implication
- constraint for each nesting layer.
+ and Note [Skolemisation en-bloc] in that module
+
Some examples:
@@ -777,29 +777,40 @@ matchExpectedFunTys herald _ arity (Infer inf_res) thing_inside
; return (mkWpCastN co, result) }
matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
- = check 0 [] top_ty
+ = check arity [] top_ty
where
check :: VisArity -> [ExpPatType] -> TcSigmaType -> TcM (HsWrapper, a)
-- `check` is called only in the Check{} case
-- It collects rev_pat_tys in reversed order
- -- n_so_far is the number of /visible/ arguments seen so far:
- -- i.e. length (filterOut isExpForAllPatTyInvis rev_pat_tys)
-
- -- Do shallow skolemisation if there are top-level invisible quantifiers
- check n_so_far rev_pat_tys ty
- | isSigmaTy ty -- Type has invisible quantifiers
- = do { (wrap_gen, (wrap_res, result))
- <- tcSkolemiseGeneral Shallow ctx top_ty ty $ \tv_bndrs ty' ->
- let rev_pat_tys' = reverse (map (mkInvisExpPatType . snd) tv_bndrs)
- ++ rev_pat_tys
- in check n_so_far rev_pat_tys' ty'
- ; return (wrap_gen <.> wrap_res, result) }
-
- -- (n_so_far == arity): no more args
- -- rho_ty has no top-level quantifiers
- -- If there is deep subsumption, do deep skolemisation
- check n_so_far rev_pat_tys rho_ty
- | n_so_far == arity
+ -- n_req is the number of /visible/ arguments still needed
+
+ ----------------------------
+ -- Skolemise quantifiers, both visible (up to n_req) and invisible
+ -- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
+ check n_req rev_pat_tys ty
+ | isSigmaTy ty -- An invisible quantifier at the top
+ || (n_req > 0 && isForAllTy ty) -- A visible quantifier at top, and we need it
+ = do { rec { (n_req', wrap_gen, tv_nms, bndrs, given, inner_ty) <- skolemiseRequired skol_info n_req ty
+ ; let sig_skol = SigSkol ctx top_ty (tv_nms `zip` skol_tvs)
+ skol_tvs = binderVars bndrs
+ ; skol_info <- mkSkolemInfo sig_skol }
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ ; (ev_binds, (wrap_res, result))
+ <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
+ check n_req'
+ (reverse (map ExpForAllPatTy bndrs) ++ rev_pat_tys)
+ inner_ty
+ ; assertPpr (not (null bndrs && null given)) (ppr ty) $
+ -- The guard ensures that we made some progress
+ return (wrap_gen <.> mkWpLet ev_binds <.> wrap_res, result) }
+
+ ----------------------------
+ -- Base case: (n_req == 0): no more args
+ -- The earlier skolemisation ensurs that rho_ty has no top-level invisible quantifiers
+ -- If there is deep subsumption, do deep skolemisation now
+ check n_req rev_pat_tys rho_ty
+ | n_req == 0
= do { let pat_tys = reverse rev_pat_tys
; ds_flag <- getDeepSubsumptionFlag
; case ds_flag of
@@ -810,52 +821,34 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
-- They do not line up with binders in the Match
thing_inside pat_tys (mkCheckExpType rho_ty) }
- -- NOW do coreView. We didn't do it before, so that we do not unnecessarily
- -- unwrap a synonym in the returned rho_ty
- check n_so_far rev_pat_tys ty
- | Just ty' <- coreView ty = check n_so_far rev_pat_tys ty'
-
- -- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
- -- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
- -- NB: visible foralls "count" for the Arity argument; they correspond
- -- to syntactically visible patterns in the source program
- -- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
- check n_so_far rev_pat_tys ty
- | Just (Bndr tv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty
- = assertPpr (isVisibleForAllTyFlag vis) (ppr ty) $
- -- isSigmaTy case above has dealt with /invisible/ quantifiers,
- -- so this one must be /visible/ (= Required)
- do { let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
- -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
- -- in GHC.Tc.Utils.TcType
- ; rec { (subst', [tv']) <- tcInstSkolTyVarsX skol_info init_subst [tv]
- ; let tv_prs = [(tyVarName tv, tv')]
- ; skol_info <- mkSkolemInfo (SigSkol ctx top_ty tv_prs) }
- ; let body_ty' = substTy subst' body_ty
- pat_ty = ExpForAllPatTy (mkForAllTyBinder Required tv')
- ; (ev_binds, (wrap_res, result)) <- checkConstraints (getSkolemInfo skol_info) [tv'] [] $
- check (n_so_far+1) (pat_ty : rev_pat_tys) body_ty'
- ; let wrap_gen = mkWpVisTyLam tv' body_ty' <.> mkWpLet ev_binds
- ; return (wrap_gen <.> wrap_res, result) }
-
- check n_so_far rev_pat_tys (FunTy { ft_af = af, ft_mult = mult
- , ft_arg = arg_ty, ft_res = res_ty })
+ ----------------------------
+ -- Function types
+ check n_req rev_pat_tys (FunTy { ft_af = af, ft_mult = mult
+ , ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
- do { let arg_pos = n_so_far + 1
+ do { let arg_pos = arity - n_req + 1 -- 1 for the first argument etc
; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
- ; (wrap_res, result) <- check arg_pos
+ ; (wrap_res, result) <- check (n_req - 1)
(mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
res_ty
; let wrap_arg = mkWpCastN arg_co
fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
; return (fun_wrap, result) }
- check n_so_far rev_pat_tys ty@(TyVarTy tv)
+ ----------------------------
+ -- Type variables
+ check n_req rev_pat_tys ty@(TyVarTy tv)
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
- Indirect ty' -> check n_so_far rev_pat_tys ty'
- Flexi -> defer n_so_far rev_pat_tys ty }
+ Indirect ty' -> check n_req rev_pat_tys ty'
+ Flexi -> defer n_req rev_pat_tys ty }
+
+ ----------------------------
+ -- NOW do coreView. We didn't do it before, so that we do not unnecessarily
+ -- unwrap a synonym in the returned rho_ty
+ check n_req rev_pat_tys ty
+ | Just ty' <- coreView ty = check n_req rev_pat_tys ty'
-- In all other cases we bale out into ordinary unification
-- However unlike the meta-tyvar case, we are sure that the
@@ -872,14 +865,14 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
--
-- But in that case we add specialized type into error context
-- anyway, because it may be useful. See also #9605.
- check n_so_far rev_pat_tys res_ty
+ check n_req rev_pat_tys res_ty
= addErrCtxtM (mkFunTysMsg herald (arity, top_ty)) $
- defer n_so_far rev_pat_tys res_ty
+ defer n_req rev_pat_tys res_ty
------------
defer :: VisArity -> [ExpPatType] -> TcRhoType -> TcM (HsWrapper, a)
- defer n_so_far rev_pat_tys fun_ty
- = do { more_arg_tys <- mapM (new_check_arg_ty herald) [n_so_far + 1 .. arity]
+ defer n_req rev_pat_tys fun_ty
+ = do { more_arg_tys <- mapM (new_check_arg_ty herald) [arity - n_req + 1 .. arity]
; let all_pats = reverse rev_pat_tys ++ map mkCheckExpFunPatTy more_arg_tys
; res_ty <- newOpenFlexiTyVarTy
; result <- thing_inside all_pats (mkCheckExpType res_ty)
@@ -894,7 +887,7 @@ new_infer_arg_ty herald arg_pos -- position for error messages only
; return (mkScaled mult inf_hole) }
new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
-new_check_arg_ty herald arg_pos -- Position for error messages only
+new_check_arg_ty herald arg_pos -- Position for error messages only, 1 for first arg
= do { mult <- newFlexiTyVarTy multiplicityTy
; arg_ty <- newOpenFlexiFRRTyVarTy (FRRExpectedFunTy herald arg_pos)
; return (mkScaled mult arg_ty) }
=====================================
compiler/GHC/Types/Var.hs
=====================================
@@ -503,7 +503,7 @@ isSpecifiedForAllTyFlag _ = False
coreTyLamForAllTyFlag :: ForAllTyFlag
-- ^ The ForAllTyFlag on a (Lam a e) term, where `a` is a type variable.
-- If you want other ForAllTyFlag, use a cast.
--- See Note [ForAllCo] in GHC.Core.TyCo.Rep
+-- See Note [Required foralls in Core] in GHC.Core.TyCo.Rep
coreTyLamForAllTyFlag = Specified
instance Outputable ForAllTyFlag where
=====================================
testsuite/tests/typecheck/should_compile/T24810.hs
=====================================
@@ -0,0 +1,26 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RequiredTypeArguments, TypeAbstractions #-}
+
+module T24810 where
+
+import GHC.TypeLits
+
+-------------------------
+-- Example from the ticket
+showKnownChar :: forall c -> KnownChar c => IO ()
+showKnownChar c = print (charSing @c)
+
+withKnownChar_rta :: SChar c -> (forall c' -> c ~ c' => KnownChar c => r) -> r
+withKnownChar_rta (SChar @c) r = r c
+
+-- no type signature for example
+example = withKnownChar_rta (SChar @'a') (\c -> showKnownChar c)
+
+
+-------------------------
+-- Example with deeper nested skolemisation needed
+ex2 :: forall c. (forall a -> Eq a => forall b. (a ~ [b]) => c) -> c
+ex2 = ex2
+
+-- no type signature for foo
+foo = ex2 (\c -> True)
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -916,3 +916,4 @@ test('T24470b', normal, compile, [''])
test('T24566', [], makefile_test, [])
test('T23764', normal, compile, [''])
test('T23739a', normal, compile, [''])
+test('T24810', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d9e4ce68a55f6bc5246d2d77729676010e85bbd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/3d9e4ce68a55f6bc5246d2d77729676010e85bbd
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/20240522/4ea492f0/attachment-0001.html>
More information about the ghc-commits
mailing list