[Git][ghc/ghc][wip/T18412] Improve typechecking of NPlusK patterns
Simon Peyton Jones
gitlab at gitlab.haskell.org
Tue Jul 14 15:43:34 UTC 2020
Simon Peyton Jones pushed to branch wip/T18412 at Glasgow Haskell Compiler / GHC
Commits:
e37cbc69 by Simon Peyton Jones at 2020-07-14T16:41:03+01:00
Improve typechecking of NPlusK patterns
This patch (due to Richard Eisenberg) improves
documentation of the wrapper returned by tcSubMult
(see Note [Wrapper returned from tcSubMult] in
GHC.Tc.Utils.Unify).
And, more substantially, it cleans up the multiplicity
handling in the typechecking of NPlusKPat
- - - - -
6 changed files:
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/Env.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/HsToCore/Binds.hs
=====================================
@@ -1141,6 +1141,7 @@ dsHsWrapper (WpCast co) = ASSERT(coercionRole co == Representational)
return $ \e -> mkCastDs e co
dsHsWrapper (WpEvApp tm) = do { core_tm <- dsEvTerm tm
; return (\e -> App e core_tm) }
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
dsHsWrapper (WpMultCoercion co) = do { when (not (isReflexiveCo co)) $
errDs (text "Multiplicity coercions are currently not supported")
; return $ \e -> e }
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -365,7 +365,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty
; mult_wrap <- tcSubMult AppOrigin Many (scaledMult arg2_sigma)
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
--
-- When ($) becomes multiplicity-polymorphic, then the above check will
-- need to go. But in the meantime, it would produce ill-typed
=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -343,7 +343,7 @@ tc_lpats tys penv pats
(zipEqual "tc_lpats" pats tys)
--------------------
--- See Note [tcSubMult's wrapper] in TcUnify.
+-- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
checkManyPattern :: Scaled a -> TcM HsWrapper
checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin Many (scaledMult pat_ty)
@@ -358,7 +358,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
{ (wrap, id) <- tcPatBndr penv name pat_ty
; (res, mult_wrap) <- tcCheckUsage name (scaledMult pat_ty) $
tcExtendIdEnv1 name id thing_inside
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
; pat_ty <- readExpType (scaledThing pat_ty)
; return (mkHsWrapPat (wrap <.> mult_wrap) (VarPat x (L l id)) pat_ty, res) }
@@ -372,7 +372,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
LazyPat x pat -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
; (pat', (res, pat_ct))
<- tc_lpat pat_ty (makeLazy penv) pat $
captureConstraints thing_inside
@@ -390,14 +390,14 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
WildPat _ -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
; res <- thing_inside
; pat_ty <- expTypeToType (scaledThing pat_ty)
; return (mkHsWrapPat mult_wrap (WildPat pat_ty) pat_ty, res) }
AsPat x (L nm_loc name) pat -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
; (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
; (pat', res) <- tcExtendIdEnv1 name bndr_id $
tc_lpat (pat_ty `scaledSet`(mkCheckExpType $ idType bndr_id))
@@ -414,7 +414,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
ViewPat _ expr pat -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
--
-- It should be possible to have view patterns at linear (or otherwise
-- non-Many) multiplicity. But it is not clear at the moment what
@@ -586,7 +586,7 @@ Fortunately that's what matchExpectedFunTySigma returns anyway.
-- When there is no negation, neg_lit_ty and lit_ty are the same
NPat _ (L l over_lit) mb_neg eq -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
--
-- It may be possible to refine linear pattern so that they work in
-- linear environments. But it is not clear how useful this is.
@@ -630,10 +630,6 @@ There are two bits of rebindable syntax:
lit1_ty and lit2_ty could conceivably be different.
var_ty is the type inferred for x, the variable in the pattern.
-If the pushed-down pattern type isn't a tau-type, the two pat_ty's
-above could conceivably be different specializations. So we use
-expTypeToType on pat_ty before proceeding.
-
Note that we need to type-check the literal twice, because it is used
twice, and may be used at different types. The second HsOverLit stored in the
AST is used for the subtraction operation.
@@ -643,16 +639,16 @@ AST is used for the subtraction operation.
NPlusKPat _ (L nm_loc name)
(L loc lit) _ ge minus -> do
{ mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
- ; pat_ty <- expTypeToType (scaledThing pat_ty)
- ; let orig = LiteralOrigin lit
+ -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
+ ; let pat_exp_ty = scaledThing pat_ty
+ orig = LiteralOrigin lit
; (lit1', ge')
- <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho]
+ <- tcSyntaxOp orig ge [SynType pat_exp_ty, SynRho]
(mkCheckExpType boolTy) $
\ [lit1_ty] _ ->
newOverloadedLit lit (mkCheckExpType lit1_ty)
; ((lit2', minus_wrap, bndr_id), minus')
- <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $
+ <- tcSyntaxOpGen orig minus [SynType pat_exp_ty, SynRho] SynAny $
\ [lit2_ty, var_ty] _ ->
do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
; (wrap, bndr_id) <- setSrcSpan nm_loc $
@@ -662,6 +658,7 @@ AST is used for the subtraction operation.
-- minus_wrap is applicable to minus'
; return (lit2', wrap, bndr_id) }
+ ; pat_ty <- readExpType pat_exp_ty
-- The Report says that n+k patterns must be in Integral
-- but it's silly to insist on this in the RebindableSyntax case
; unlessM (xoptM LangExt.RebindableSyntax) $
@@ -984,7 +981,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
req_theta' = substTheta tenv req_theta
; mult_wrap <- checkManyPattern pat_ty
- -- See Note [tcSubMult's wrapper] in TcUnify.
+ -- 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 $$
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -229,18 +229,10 @@ data HsWrapper
| WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
-- so that the identity coercion is always exactly WpHole
- | WpMultCoercion Coercion
- -- Note [Checking multiplicity coercions]
- -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
- -- This wrapper can be returned from tcSubMult.
- -- It is used in case a variable is used with multiplicity m1,
- -- we need it with multiplicity m2 and we have a coercion c :: m1 ~ m2.
- -- Compiling such code would require multiplicity coercions in Core,
- -- which we don't have. If the desugarer sees WpMultCoercion
- -- with a non-reflexive coercion, it gives an error.
- -- This is a temporary measure, as we don't really know yet exactly
- -- what multiplicity coercions should be. But it serves as a good
- -- approximation for the first iteration for the first iteration of linear types.
+
+ | WpMultCoercion Coercion -- Require that a Coercion be reflexive; otherwise,
+ -- error in the desugarer. See GHC.Tc.Utils.Unify
+ -- Note [Wrapper returned from tcSubMult]
-- Cannot derive Data instance because SDoc is not Data (it stores a function).
-- So we do it manually:
=====================================
compiler/GHC/Tc/Utils/Env.hs
=====================================
@@ -628,7 +628,8 @@ tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things
-- | @tcCheckUsage name mult thing_inside@ runs @thing_inside@, checks that the
-- usage of @name@ is a submultiplicity of @mult@, and removes @name@ from the
--- usage environment. See also Note [tcSubMult's wrapper] in TcUnify.
+-- usage environment. See also Note [Wrapper returned from tcSubMult] in
+-- GHC.Tc.Utils.Unify, which applies to the wrapper returned from this function.
tcCheckUsage :: Name -> Mult -> TcM a -> TcM (a, HsWrapper)
tcCheckUsage name id_mult thing_inside
= do { (local_usage, result) <- tcCollectingUsage thing_inside
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -762,29 +762,29 @@ to a UserTypeCtxt of GenSigCtxt. Why?
ambiguity check, but we don't need one for each level within it,
and GHC.Tc.Utils.Unify.alwaysBuildImplication checks the UserTypeCtxt.
See Note [When to build an implication]
--}
+Note [Wrapper returned from tcSubMult]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There is no notion of multiplicity coercion in Core, therefore the wrapper
+returned by tcSubMult (and derived functions such as tcCheckUsage and
+checkManyPattern) is quite unlike any other wrapper: it checks whether the
+coercion produced by the constraint solver is trivial, producing a type error
+is it is not. This is implemented via the WpMultCoercion wrapper, as desugared
+by GHC.HsToCore.Binds.dsHsWrapper, which does the reflexivity check.
+
+This wrapper needs to be placed in the term; otherwise, checking of the
+eventual coercion won't be triggered during desugaring. But it can be put
+anywhere, since it doesn't affect the desugared code.
+
+Why do we check this in the desugarer? It's a convenient place, since it's
+right after all the constraints are solved. We need the constraints to be
+solved to check whether they are trivial or not. Plus there is precedent for
+type errors during desuraging (such as the levity polymorphism
+restriction). An alternative would be to have a kind of constraint which can
+only produce trivial evidence, then this check would happen in the constraint
+solver.
+-}
--- Note [tcSubMult's wrapper]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~
--- There is no notion of multiplicity coercion in Core, therefore the wrapper
--- returned by tcSubMult (and derived function such as tcCheckUsage and
--- checkManyPattern) is quite unlike any other wrapper: it checks whether the
--- coercion produced by the constraint solver is trivial and disappears (it
--- produces a type error is the constraint is not trivial). See [Checking
--- multiplicity coercions] in TcEvidence.
---
--- This wrapper need to be placed in the term, otherwise checking of the
--- eventual coercion won't be triggered during desuraging. But it can be put
--- anywhere, since it doesn't affect the desugared code.
---
--- Why do we check this in the desugarer? It's a convenient place, since it's
--- right after all the constraints are solved. We need the constraints to be
--- solved to check whether they are trivial or not. Plus there are precedent for
--- type errors during desuraging (such as the levity polymorphism
--- restriction). An alternative would be to have a kind of constraints which can
--- only produce trivial evidence, then this check would happen in the constraint
--- solver.
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcSubMult origin w_actual w_expected
| Just (w1, w2) <- isMultMul w_actual =
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e37cbc69a81f7fc07cb87cd8b3adeab377c3c52b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e37cbc69a81f7fc07cb87cd8b3adeab377c3c52b
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/20200714/7aecaa60/attachment-0001.html>
More information about the ghc-commits
mailing list