[Git][ghc/ghc][wip/sand-witch/lazy-skol] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jan 31 08:43:25 UTC 2024
Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC
Commits:
05745d57 by Simon Peyton Jones at 2024-01-30T22:24:21+00:00
Wibbles
- - - - -
5 changed files:
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -1,7 +1,6 @@
+{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE DeriveDataTypeable #-}
-
-{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE DeriveFunctor #-}
{-
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -287,15 +287,7 @@ tcExpr e@(OpApp {}) res_ty = tcApp e res_ty
tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty
tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty
tcExpr e@(HsRecSel {}) res_ty = tcApp e res_ty
-
--- tcApp can deal with HsExpanded (because we might find one at the
--- head of an application chain) but it is needlessly expensive to
--- treat every HsExpanded as a nullary application; it it gives less
--- good error messages because we infer the type of the head of the
--- appication chain. So we give it a case here.
-tcExpr (XExpr (HsExpanded orig expr)) res_ty
- = do { expr' <- tcExpr expr res_ty
- ; return (XExpr (ExpansionExpr (HsExpanded orig expr'))) }
+tcExpr e@(XExpr (HsExpanded {})) res_ty = tcApp e res_ty
tcExpr e@(HsOverLit _ lit) res_ty
= do { mb_res <- tcShortCutLit lit res_ty
=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -311,9 +311,7 @@ tcGRHSList :: forall body. AnnoBody body
-> [LGRHS GhcRn (LocatedA (body GhcRn))] -> ExpRhoType
-> TcM [LGRHS GhcTc (LocatedA (body GhcTc))]
tcGRHSList ctxt tc_body grhss res_ty
- = do { -- (usages, grhss') <- mapAndUnzipM (wrapLocSndMA tc_alt) grhss
- ; stuff <- mapM (wrapLocSndMA tc_alt) grhss
- ; let (usages, grhss') = unzip stuff
+ = do { (usages, grhss') <- mapAndUnzipM (wrapLocSndMA tc_alt) grhss
; tcEmitBindingUsage $ supUEs usages
; return grhss' }
where
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -469,7 +469,7 @@ mkInvisExpPatType (Bndr tv spec) = ExpForAllPatTy (Bndr tv (Invisible spec))
isVisibleExpPatType :: ExpPatType -> Bool
isVisibleExpPatType (ExpForAllPatTy (Bndr _ vis)) = isVisibleForAllTyFlag vis
-isVisibleExpPatType _ = True
+isVisibleExpPatType (ExpFunPatTy {}) = True
isExpFunPatType :: ExpPatType -> Bool
isExpFunPatType ExpFunPatTy{} = True
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -258,14 +258,16 @@ Suppose f :: (forall a. a->a) -> blah, and we have the application (f e)
Then we want to typecheck `e` pushing in the type `forall a. a->a`. But we
need to be careful:
-* In general, in (tcPolyExpr e (forall a b. rho), we skolemise `a` and `b`,
+* Roughly speaking, in (tcPolyExpr e (forall a b. rho)), we skolemise `a` and `b`,
and then call (tcExpr e rho)
-* But we must be careful if `e` is a type lambda (\@p @q -> blah). Then we want to
- line up the skolemised variables `a`,`b` with `p`,`q`.
+* But not quite! We must be careful if `e` is a type lambda (\ @p @q -> blah).
+ Then we want to line up the skolemised variables `a`,`b`
+ with `p`,`q`, so we can't just call (tcExpr (\ @p @q -> blah) rho)
* A very similar situation arises with
- (\@p @q -> blah) :: forall a b. rho
+ (\ @p @q -> blah) :: forall a b. rho
+ Again, we must line up `p`, `q` with the skolemised `a` and `b`.
* Another similar situation arises with
g :: forall a b. rho
@@ -273,13 +275,17 @@ need to be careful:
Here again when skolemising `a` and `b` we must be careful to match them up
with `p` and `q`.
-* Note that this only matters for /checking/. We don't do inference for
- (\@a -> blah), yet anyway.
+OK, so how exactly do we check @p binders in lambdas? First note that we only
+we only attempt to deal with @p binders when /checking/. We don't do inference for
+(\ @a -> blah), not yet anyway.
-There are two cases to consider:
- * Function LHS f @p x @q y = ...
- * Lambda \@p x @q y -> ...
- \cases { @p x @q y -> ... }
+For checking, there are two cases to consider:
+ * Function LHS, where the function has a type signature
+ f :: forall a. a -> forall b. [b] -> blah
+ f @p x @q y = ...
+
+ * Lambda \ @p x @q y -> ...
+ \cases { @p x @q y -> ... }
(\case p behaves like \cases { p -> ... }, and p is always a term pattern.)
Both ultimately handled by matchExpectedFunTys.
@@ -292,7 +298,7 @@ Both ultimately handled by matchExpectedFunTys.
* And then passes the (skolemised-variables ++ arg tys) on to `tcMatches`
* For the Lambda case there are two sub-cases:
- * An expression with a type signature: (\@a x y -> blah) :: hs_ty
+ * An expression with a type signature: (\ @a x y -> blah) :: hs_ty
This is handled by `GHC.Tc.Gen.Head.tcExprWithSig`, which kind-checks
the signature and hands off to `tcExprPolyCheck` vai `tcPolyLExprSig`
Note that the foralls at the top of hs_ty scope over the expression.
@@ -312,7 +318,7 @@ Both ultimately handled by matchExpectedFunTys.
The outer skolemisation in tcPolyExprCheck is done using
* tcSkolemiseCompleteSig when there is a user-written signature
- * tcSkolemiseGeneral when the polytpe just comes from the context e.g. (f e)
+ * tcSkolemiseGeneral when the polytype just comes from the context e.g. (f e)
The former just calls the latter, so the two cases differ only slightly:
* Both do shallow skolemisation
* Both go via checkConstraints, which uses implicationNeeded to decide whether
@@ -365,6 +371,10 @@ Some examples:
f x @p = rhs
`matchExpectedFunTys` does shallow skolemisation eagerly, so we'll skolemise the
forall a b. Then `tcMatchPats` will bind [p :-> a_sk], and discard `b_sk`.
+ Discarding the `b_sk` means that
+ f x @p = \ @q -> blah
+ or f x @p = let .. in \ @q -> blah
+ will both be rejected: this is Plan B2: skolemise at the "=".
* Suppose DeepSubsumption is on
f :: forall a. a -> forall b. b -> b -> forall z. z
@@ -426,7 +436,7 @@ tcSkolemiseCompleteSig (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = lo
tcSkolemiseExpectedType :: TcSigmaType
-> ([ExpPatType] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
--- Just ike tcSkolemiseCompleteSig, except that don't have a user-written
+-- Just like tcSkolemiseCompleteSig, except that we don't have a user-written
-- type signature, we only have a type comimg from the context.
-- Eg. f :: (forall a. blah) -> blah
-- In the call (f e) we will call tcSkolemiseExpectedType on (forall a.blah)
@@ -788,8 +798,8 @@ 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 synonyms in the returned 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'
@@ -906,7 +916,7 @@ mkFunTysMsg herald (n_val_args_in_call, fun_ty) env
{- Note [Reporting application arity errors]
---------------------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider f :: Int -> Int -> Int
and the call foo = f 3 4 5
We'd like to get an error like:
@@ -915,9 +925,9 @@ We'd like to get an error like:
• The function ‘f’ is applied to three value arguments,
but its type ‘Int -> Int -> Int’ has only two
-That is that `mkFunTysMsg` tries to do. But what is the "type of the function".
+That is what `mkFunTysMsg` tries to do. But what is the "type of the function".
Most obviously, we can report its full, polymorphic type; that is simple and
-expliciable. But sometimes a bit odd. Consider
+explicable. But sometimes a bit odd. Consider
f :: Bool -> t Int Int
foo = f True 5 10
We get this error:
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/05745d57d470568effd8c8f1f5c76b48e25188e4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/05745d57d470568effd8c8f1f5c76b48e25188e4
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/20240131/c054e84f/attachment-0001.html>
More information about the ghc-commits
mailing list