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 files changed, 43 insertions, 52 deletions

diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index f904bc2616..03164c5b25 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/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 }
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index e8954914e3..8bef4b4b8e 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -373,7 +373,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
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index c8d021a4fe..e827e1215d 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/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 $$
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index ccc25c209d..b9d460b8ec 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/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:
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index e8640a08dc..76ebb79e1e 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/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
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 145520045b..bf933127b8 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/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 =