WIPwip/more-linear-lint

3 files changed, 21 insertions, 4 deletions

diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index bcb9953359..504631c734 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -980,9 +980,16 @@ lintIdOcc var nargs
         ; ensureEqTys occ_ty bndr_ty $
           mkBndrOccTypeMismatchMsg bndr var bndr_ty occ_ty
 
+        ; lf <- getLintFlags
+        ; let occ_mult  = varMult var
+              bndr_mult = varMult bndr
+          -- TODO: check if it can be enabled for all passes
+        ; when (lf_check_linearity lf) $
+          ensureEqTys occ_mult bndr_mult $
+          mkBndrOccMultMismatchMsg bndr var bndr_mult occ_mult
+
           -- Check for a nested occurrence of the StaticPtr constructor.
           -- See Note [Checking StaticPtrs].
-        ; lf <- getLintFlags
         ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $
             checkL (idName var /= makeStaticName) $
               text "Found makeStatic nested in an expression"
@@ -3256,6 +3263,13 @@ mkBndrOccTypeMismatchMsg bndr var bndr_ty var_ty
          , text "Occurrence:" <+> ppr var <+> dcolon <+> ppr var_ty
          , text "  Before subst:" <+> ppr (idType var) ]
 
+mkBndrOccMultMismatchMsg :: Var -> Var -> LintedType -> LintedType -> SDoc
+mkBndrOccMultMismatchMsg bndr var bndr_mult var_mult
+  = vcat [ text "Mismatch in multiplicity between binder and occurrence"
+         , text "Binder:" <+> ppr bndr <+> text "%" <+> ppr bndr_mult
+         , text "Occurrence:" <+> ppr var <+> text "%" <+> ppr var_mult
+         , text "  Before subst:" <+> ppr (idMult var) ]
+
 mkBadJoinPointRuleMsg :: JoinId -> JoinArity -> CoreRule -> SDoc
 mkBadJoinPointRuleMsg bndr join_arity rule
   = vcat [ text "Join point has rule with wrong number of arguments"
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index 5d060cb7cd..8c54b7d5be 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -79,7 +79,6 @@ import GHC.Utils.Misc
 import GHC.Types.Unique.Supply
 import GHC.Types.Unique
 import GHC.Types.Unique.FM
-import GHC.Types.Unique.Set
 import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
@@ -633,6 +632,8 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
 -- | This checks if the substitution satisfies the invariant from
 -- Note [The substitution invariant].
 checkValidSubst :: HasDebugCallStack => TCvSubst -> [Type] -> [Coercion] -> a -> a
+checkValidSubst _ _ _ x = x
+{-
 checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
   = assertPpr (isValidTCvSubst subst)
               (text "in_scope" <+> ppr in_scope $$
@@ -658,7 +659,7 @@ checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
                  shallowTyCoVarsOfCos cos)
                 `delListFromUniqSet_Directly` substDomain
   tysCosFVsInScope = needInScope `varSetInScope` in_scope
-
+-}
 
 -- | Substitute within a 'Type'
 -- The substitution has to satisfy the invariants described in
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index 333929c956..165ff540a8 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -65,6 +65,7 @@ import GHC.Core.TyCon
 import GHC.Core.DataCon
 import GHC.Core.PatSyn
 import GHC.Core.Type
+import GHC.Core.Subst
 import GHC.Core.Coercion
 import GHC.Builtin.Types
 import GHC.Types.Basic
@@ -377,7 +378,8 @@ mkDataConCase var ty alts@(alt1 :| _)
               -- Upholds the invariant that the binders of a case expression
               -- must be scaled by the case multiplicity. See Note [Case
               -- expression invariants] in CoreSyn.
-            return (Alt (DataAlt con) rep_ids' (mkLets binds body))
+                updateMults = substExpr (extendInScopeList emptySubst rep_ids')
+            return $ Alt (DataAlt con) rep_ids' (updateMults $ mkLets binds body)
 
     mk_default :: MatchResult (Maybe CoreAlt)
     mk_default