[Git][ghc/ghc][wip/T24810] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri May 17 06:50:39 UTC 2024
Simon Peyton Jones pushed to branch wip/T24810 at Glasgow Haskell Compiler / GHC
Commits:
d9babc57 by Simon Peyton Jones at 2024-05-16T23:35:02+01:00
Wibbles
- - - - -
5 changed files:
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/typecheck/should_compile/T24810.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -205,8 +205,7 @@ topSkolemise skolem_info ty
skolemiseRequired :: SkolemInfo -> VisArity -> TcSigmaType
-> TcM (VisArity, HsWrapper, [Name], [ForAllTyBinder], [EvVar], TcSigmaType)
-- Skolemise up to N required (visible) binders, plus any invisible ones
--- "in the way". Stop as soon as you have found the n'th, so there might still
--- be some invisible foralls/qual-tys in the returned type
+-- "in the way", and any trailing invisible ones.
-- Return the depleted arity
skolemiseRequired skolem_info n_req sigma
= go n_req init_subst idHsWrapper [] [] [] sigma
@@ -215,8 +214,7 @@ skolemiseRequired skolem_info n_req sigma
-- Why recursive? See Note [Skolemisation]
go n_req subst wrap acc_nms acc_bndrs ev_vars ty
- | n_req > 0
- , (n_req', bndrs, inner_ty) <- tcSplitForAllTyVarsReqTVBindersN n_req 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
@@ -227,8 +225,7 @@ skolemiseRequired skolem_info n_req sigma
ev_vars
inner_ty }
- | n_req > 0
- , (theta, inner_ty) <- tcSplitPhiTy ty
+ | (theta, inner_ty) <- tcSplitPhiTy ty
, not (null theta)
= do { ev_vars1 <- newEvVars (substTheta subst theta)
; go n_req subst
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -1412,15 +1412,15 @@ tcSplitSomeForAllTyVars argf_pred 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 invisibl ones
tcSplitForAllTyVarsReqTVBindersN n_req ty
= split n_req ty ty []
where
- split 0 orig_ty _ty bs = (0, reverse bs, orig_ty)
split n_req _orig_ty (ForAllTy b@(Bndr _ argf) ty) bs
- | isVisibleForAllTyFlag argf = split (n_req - 1) ty ty (b: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)
+ 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 '()'.
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -786,38 +786,8 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
-- 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) }
-
- ----------------------------
- -- Base case: (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
- = do { let pat_tys = reverse rev_pat_tys
- ; ds_flag <- getDeepSubsumptionFlag
- ; case ds_flag of
- Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
- ; return (idHsWrapper, res) }
- Deep -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
- -- "_" drop the /deeply/-skolemise binders
- -- 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'
-
----------------------------
- -- Visible forall
+ -- Skolemise quantifiers
--
-- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
-- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
@@ -825,9 +795,9 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
-- 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
- | isForAllTy ty -- isSigmaTy case above has dealt with /invisible/ quantifiers,
- -- so this one must be /visible/ (= Required)
- , let n_req = arity - n_so_far -- Must be n_req > 0
+ | let n_req = arity - n_so_far
+ , isSigmaTy ty -- Invisible quantifier at the top
+ || (n_req > 0 && isForAllTy ty) -- 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
@@ -840,9 +810,30 @@ matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
check (arity - n_req')
(reverse pat_tys ++ rev_pat_tys)
inner_ty
- ; assertPpr (n_req' < n_req) (ppr ty) $ -- Some progress
+ ; assertPpr (not (null bndrs && null given)) (ppr ty) $ -- Some progress
return (wrap_gen <.> mkWpLet ev_binds <.> wrap_res, result) }
+ ----------------------------
+ -- Base case: (n_so_far == arity): no more args
+ -- rho_ty has no top-level invisible quantifiers
+ -- If there is deep subsumption, do deep skolemisation
+ check n_so_far rev_pat_tys rho_ty
+ | n_so_far == arity
+ = do { let pat_tys = reverse rev_pat_tys
+ ; ds_flag <- getDeepSubsumptionFlag
+ ; case ds_flag of
+ Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
+ ; return (idHsWrapper, res) }
+ Deep -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
+ -- "_" drop the /deeply/-skolemise binders
+ -- 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'
+
----------------------------
-- Function types
check n_so_far rev_pat_tys (FunTy { ft_af = af, ft_mult = mult
=====================================
testsuite/tests/typecheck/should_compile/T24810.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T24810 where
+
+import GHC.TypeLits
+
+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
+example = withKnownChar_rta (SChar @'a') (\c -> showKnownChar c)
=====================================
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/d9babc5722116535352294c2e3b6941808b96129
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d9babc5722116535352294c2e3b6941808b96129
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/20240517/f6e7ab13/attachment-0001.html>
More information about the ghc-commits
mailing list