diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index f2c8e238cc6a9acc4cfc85ab5a89eb177e737d58..daae455c76e4c6133da308c5a4be69c8a97ddbcb 100644
--- a/compiler/GHC/Core.hs
+++ b/compiler/GHC/Core.hs
@@ -35,6 +35,8 @@ module GHC.Core (
         mkConApp, mkConApp2, mkTyBind, mkCoBind,
         varToCoreExpr, varsToCoreExprs,
 
+        mkBinds,
+
         isId, cmpAltCon, cmpAlt, ltAlt,
 
         -- ** Simple 'Expr' access functions and predicates
@@ -311,6 +313,17 @@ data Bind b = NonRec b (Expr b)
             | Rec [(b, (Expr b))]
   deriving Data
 
+-- | Helper function. You can use the result of 'mkBinds' with 'mkLets' for
+-- instance.
+--
+--   * @'mkBinds' 'Recursive' binds@ makes a single mutually-recursive
+--     bindings with all the rhs/lhs pairs in @binds@
+--   * @'mkBinds' 'NonRecursive' binds@ makes one non-recursive binding
+--     for each rhs/lhs pairs in @binds@
+mkBinds :: RecFlag -> [(b, (Expr b))] -> [Bind b]
+mkBinds Recursive binds = [Rec binds]
+mkBinds NonRecursive binds = map (uncurry NonRec) binds
+
 {-
 Note [Literal alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index 5af2893658059dc22488becaab04e404e3d532eb..e2ea89c42bb917805965a1fe983abeddaac3a44b 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -2862,7 +2862,7 @@ impliedXFlags
     , (LangExt.UnliftedDatatypes, turnOn, LangExt.DataKinds)
     , (LangExt.UnliftedDatatypes, turnOn, LangExt.StandaloneKindSignatures)
 
-    -- See Note [Destructuring AbsBinds aren't linear] in GHC.Tc.Gen.Bind
+    -- See Note [Non-variable pattern bindings aren't linear] in GHC.Tc.Gen.Bind
     , (LangExt.LinearTypes, turnOn, LangExt.MonoLocalBinds)
   ]
 
diff --git a/compiler/GHC/Hs/Binds.hs b/compiler/GHC/Hs/Binds.hs
index 30840ed25388c522d6bd1d04ee8c6ba4b860d10a..8ba92f8d2897a644e116fd4f8b005a6420ad1dcf 100644
--- a/compiler/GHC/Hs/Binds.hs
+++ b/compiler/GHC/Hs/Binds.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE AllowAmbiguousTypes #-} -- used to pass the phase to ppr_mult_ann since MultAnn is a type family
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
@@ -138,6 +139,10 @@ type instance XPSB         (GhcPass idL) GhcTc = NameSet
 
 type instance XXPatSynBind (GhcPass idL) (GhcPass idR) = DataConCantHappen
 
+type instance XMultAnn GhcPs = NoExtField
+type instance XMultAnn GhcRn = NoExtField
+type instance XMultAnn GhcTc = Mult
+
 -- ---------------------------------------------------------------------
 
 -- | Typechecked, generalised bindings, used in the output to the type checker.
@@ -508,6 +513,16 @@ plusHsValBinds (XValBindsLR (NValBinds ds1 sigs1))
 plusHsValBinds _ _
   = panic "HsBinds.plusHsValBinds"
 
+-- Used to print, for instance, let bindings:
+--   let %1 x = …
+pprHsMultAnn :: forall id. OutputableBndrId id => HsMultAnn (GhcPass id) -> SDoc
+pprHsMultAnn HsNoMultAnn = empty
+pprHsMultAnn (HsPct1Ann _) = text "%1"
+pprHsMultAnn (HsMultAnn _ p) = text"%" <> ppr p
+
+ppr_mult_ann :: forall id. OutputableBndrId id => MultAnn (GhcPass id) -> SDoc
+ppr_mult_ann = pprHsMultAnn . mult_ann
+
 instance (OutputableBndrId pl, OutputableBndrId pr)
          => Outputable (HsBindLR (GhcPass pl) (GhcPass pr)) where
     ppr mbind = ppr_monobind mbind
@@ -516,8 +531,9 @@ ppr_monobind :: forall idL idR.
                 (OutputableBndrId idL, OutputableBndrId idR)
              => HsBindLR (GhcPass idL) (GhcPass idR) -> SDoc
 
-ppr_monobind (PatBind { pat_lhs = pat, pat_rhs = grhss })
-  = pprPatBind pat grhss
+ppr_monobind (PatBind { pat_lhs = pat, pat_mult = mult_ann, pat_rhs = grhss })
+  = ppr_mult_ann @idL mult_ann
+    <+> pprPatBind pat grhss
 ppr_monobind (VarBind { var_id = var, var_rhs = rhs })
   = sep [pprBndr CasePatBind var, nest 2 $ equals <+> pprExpr (unLoc rhs)]
 ppr_monobind (FunBind { fun_id = fun,
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 54bbbd098593d7b1e92e1ad3f4d2acbea6c32921..18289f499cd883a52a4edb8dfaac27a6104a614e 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -108,6 +108,13 @@ deriving instance Data (HsPatSynDir GhcPs)
 deriving instance Data (HsPatSynDir GhcRn)
 deriving instance Data (HsPatSynDir GhcTc)
 
+deriving instance Data (MultAnn GhcPs)
+deriving instance Data (MultAnn GhcRn)
+deriving instance Data (MultAnn GhcTc)
+
+deriving instance Data (HsMultAnn GhcPs)
+deriving instance Data (HsMultAnn GhcRn)
+deriving instance Data (HsMultAnn GhcTc)
 -- ---------------------------------------------------------------------
 -- Data derivations from GHC.Hs.Decls ----------------------------------
 
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index e610e2daf8c348bab922cd3b305de943e095fe1f..78ded75d25c13be15cdffa87af7d396d9a204ec2 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -48,7 +48,8 @@ module GHC.Hs.Utils(
   mkMatchGroup, mkLamCaseMatchGroup, mkMatch, mkPrefixFunRhs, mkHsLam, mkHsIf,
   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
   mkHsDictLet, mkHsLams,
-  mkHsOpApp, mkHsDo, mkHsDoAnns, mkHsComp, mkHsCompAnns, mkHsWrapPat, mkHsWrapPatCo,
+  mkHsOpApp, mkHsDo, mkHsDoAnns, mkHsComp, mkHsCompAnns,
+  mkHsWrapPat, mkLHsWrapPat, mkHsWrapPatCo,
   mkLHsPar, mkHsCmdWrap, mkLHsCmdWrap,
   mkHsCmdIf, mkConLikeTc,
 
@@ -793,6 +794,9 @@ mkHsWrapPat :: HsWrapper -> Pat GhcTc -> Type -> Pat GhcTc
 mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p
                        | otherwise           = XPat $ CoPat co_fn p ty
 
+mkLHsWrapPat :: HsWrapper -> LPat GhcTc -> Type -> LPat GhcTc
+mkLHsWrapPat co_fn (L loc p) ty = L loc (mkHsWrapPat co_fn p ty)
+
 mkHsWrapPatCo :: TcCoercionN -> Pat GhcTc -> Type -> Pat GhcTc
 mkHsWrapPatCo co pat ty | isReflCo co = pat
                         | otherwise     = XPat $ CoPat (mkWpCastN co) pat ty
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 5693a798b851e5a5287d5415d6d1fbd376e14740..1ee8bb38cd891580026879b94ec923880e6131f2 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -295,7 +295,7 @@ dsProcExpr pat (L _ (HsCmdTop (CmdTopTc _unitTy cmd_ty ids) cmd)) = do
     let env_stk_expr = mkCorePairExpr (mkBigCoreVarTup env_ids) mkCoreUnitExpr
     fail_expr <- mkFailExpr (ArrowMatchCtxt ProcExpr) env_stk_ty
     var <- selectSimpleMatchVarL ManyTy pat
-    match_code <- matchSimply (Var var) (ArrowMatchCtxt ProcExpr) pat env_stk_expr fail_expr
+    match_code <- matchSimply (Var var) (ArrowMatchCtxt ProcExpr) ManyTy pat env_stk_expr fail_expr
     let pat_ty = hsLPatType pat
     let proc_code = do_premap meth_ids pat_ty env_stk_ty cmd_ty
                     (Lam var match_code)
@@ -963,7 +963,7 @@ dsCmdStmt ids local_vars out_ids (BindStmt _ pat cmd) env_ids = do
     fail_expr <- mkFailExpr (StmtCtxt (HsDoStmt (DoExpr Nothing))) out_ty
     pat_id    <- selectSimpleMatchVarL ManyTy pat
     match_code
-      <- matchSimply (Var pat_id) (StmtCtxt (HsDoStmt (DoExpr Nothing))) pat body_expr fail_expr
+      <- matchSimply (Var pat_id) (StmtCtxt (HsDoStmt (DoExpr Nothing))) ManyTy pat body_expr fail_expr
     pair_id   <- newSysLocalDs ManyTy after_c_ty
     let
         proj_expr = Lam pair_id (coreCasePair pair_id pat_id env_id match_code)
@@ -1198,7 +1198,7 @@ matchSimplys :: [CoreExpr]              -- Scrutinees
 matchSimplys [] _ctxt [] result_expr _fail_expr = return result_expr
 matchSimplys (exp:exps) ctxt (pat:pats) result_expr fail_expr = do
     match_code <- matchSimplys exps ctxt pats result_expr fail_expr
-    matchSimply exp ctxt pat match_code fail_expr
+    matchSimply exp ctxt ManyTy pat match_code fail_expr
 matchSimplys _ _ _ _ _ = panic "matchSimplys"
 
 -- List of leaf expressions, with set of variables bound in each
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 024f9377c7ea866e1299231f038f0db43f59fcff..b0960927a9451ed3ecc3d1333dab6065f38fafe4 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -702,6 +702,65 @@ tuple `t`, thus:
 See https://gitlab.haskell.org/ghc/ghc/wikis/strict-pragma for a more
 detailed explanation of the desugaring of strict bindings.
 
+Wrinkle 1: forcing linear variables
+
+Consider
+
+  let %1 !x = rhs in <body>
+==>
+  let x = rhs in x `seq` <body>
+
+In the desugared version x is used in both arguments of seq. This isn't
+recognised a linear. So we can't strictly speaking use seq. Instead, the code is
+really desugared as
+
+  let x = rhs in case x of x { _ -> <body> }
+
+The shadowing with the case-binder is crucial. The linear linter (see
+Note [Linting linearity] in GHC.Core.Lint) understands this as linear. This is
+what the seqVar function does.
+
+To be more precise, suppose x has multiplicity p, the fully annotated seqVar (in
+Core, p is really stored inside x) is
+
+  case x of %p x { _ -> <body> }
+
+In linear Core, case u of %p y { _ -> v } consumes u with multiplicity p, and
+makes y available with multiplicity p in v. Which is exactly what we want.
+
+Wrinkle 2: linear patterns
+
+Consider the following linear binding (linear lets are always non-recursive):
+
+  let
+     %1 f : g = rhs
+  in <body>
+
+The general case would desugar it to
+
+  let t = let tm = rhs
+              fm = case tm of fm:_ -> fm
+              gm = case tm of _:gm -> gm
+           in
+           (tm, fm, gm)
+
+  in let f = case t a of (_,fm,_) -> fm
+  in let g = case t a of (_,_,gm) -> gm
+  in let tm = case t a of (tm,_,_) -> tm
+  in tm `seq` <body>
+
+But all the case expression drop variables, which is prohibited by
+linearity. But because this is a non-recursive let (in particular we're
+desugaring a single binding), we can (and do) desugar the binding as a simple
+case-expression instead:
+
+  case rhs of {
+    (f:g) -> <body>
+  }
+
+This is handled by the special case: a non-recursive PatBind in
+GHC.HsToCore.Expr.ds_val_bind.
+
 Note [Strict binds checks]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 There are several checks around properly formed strict bindings. They
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index d972ee303b4d42a2e66e1f387102221683944361..7f44894f70e64f1767bd962c56b4d2d3c96b7ef8 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -88,7 +88,8 @@ dsLocalBinds (HsIPBinds _ binds)  body = dsIPBinds  binds body
 -- caller sets location
 dsValBinds :: HsValBinds GhcTc -> CoreExpr -> DsM CoreExpr
 dsValBinds (XValBindsLR (NValBinds binds _)) body
-  = foldrM ds_val_bind body binds
+  = do { dflags <- getDynFlags
+       ; foldrM (ds_val_bind dflags) body binds }
 dsValBinds (ValBinds {})       _    = panic "dsValBinds ValBindsIn"
 
 -------------------------
@@ -107,12 +108,12 @@ dsIPBinds (IPBinds ev_binds ip_binds) body
 
 -------------------------
 -- caller sets location
-ds_val_bind :: (RecFlag, LHsBinds GhcTc) -> CoreExpr -> DsM CoreExpr
+ds_val_bind :: DynFlags -> (RecFlag, LHsBinds GhcTc) -> CoreExpr -> DsM CoreExpr
 -- Special case for bindings which bind unlifted variables
 -- We need to do a case right away, rather than building
 -- a tuple and doing selections.
 -- Silently ignore INLINE and SPECIALISE pragmas...
-ds_val_bind (NonRecursive, hsbinds) body
+ds_val_bind _ (NonRecursive, hsbinds) body
   | [L loc bind] <- bagToList hsbinds
         -- Non-recursive, non-overloaded bindings only come in ones
         -- ToDo: in some bizarre case it's conceivable that there
@@ -146,13 +147,38 @@ ds_val_bind (NonRecursive, hsbinds) body
     is_polymorphic _ = False
 
 
-ds_val_bind (is_rec, binds) _body
+ds_val_bind _ (is_rec, binds) _body
   | anyBag (isUnliftedHsBind . unLoc) binds  -- see Note [Strict binds checks] in GHC.HsToCore.Binds
   = assert (isRec is_rec )
     errDsCoreExpr $ DsRecBindsNotAllowedForUnliftedTys (bagToList binds)
 
+-- Special case: a non-recursive PatBind. No dancing about with lets and seqs,
+-- we make a case immediately. Very important for linear types: let !pat can be
+-- linear, but selectors as used in the general case aren't. So the general case
+-- would transform a linear definition into a non-linear one. See Wrinkle 2
+-- Note [Desugar Strict binds] in GHC.HsToCore.Binds.
+ds_val_bind dflags (NonRecursive, hsbinds) body
+  | [L _loc (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = MultAnn{mult_ext=mult}
+                     , pat_ext = (ty, (rhs_tick, _var_ticks))})] <- bagToList hsbinds
+        -- Non-recursive, non-overloaded bindings only come in ones
+  , pat' <- decideBangHood dflags pat
+  , isBangedLPat pat'
+  = do { rhss_nablas <- pmcGRHSs PatBindGuards grhss
+        ; rhs_expr <- dsGuarded grhss ty rhss_nablas
+        ; let rhs' = mkOptTickBox rhs_tick rhs_expr
+        ; let body_ty = exprType body
+        ; error_expr <- mkErrorAppDs pAT_ERROR_ID body_ty (ppr pat')
+        ; matchSimply rhs' PatBindRhs mult pat' body error_expr }
+    -- This is the one place where matchSimply is given a non-ManyTy
+    -- multiplicity argument.
+    --
+    -- In this form, there isn't a natural place for the var_ticks. In
+    -- mkSelectorBinds, the ticks are around the selector function but there
+    -- aren't any selection functions as we make a single pattern-match. Is this a
+    -- problem?
+
 -- Ordinary case for bindings; none should be unlifted
-ds_val_bind (is_rec, binds) body
+ds_val_bind _ (is_rec, binds) body
   = do  { massert (isRec is_rec || isSingletonBag binds)
                -- we should never produce a non-recursive list of multiple binds
 
diff --git a/compiler/GHC/HsToCore/ListComp.hs b/compiler/GHC/HsToCore/ListComp.hs
index 697ca0e877faf7df260e63e6cd1c9ba43b517f01..2e0e3b7f0359a636616f3fc9ea8761745e063c59 100644
--- a/compiler/GHC/HsToCore/ListComp.hs
+++ b/compiler/GHC/HsToCore/ListComp.hs
@@ -284,7 +284,7 @@ deBindComp pat core_list1 quals core_list2 = do
         letrec_body = App (Var h) core_list1
 
     rest_expr <- deListComp quals core_fail
-    core_match <- matchSimply (Var u2) (StmtCtxt (HsDoStmt ListComp)) pat rest_expr core_fail
+    core_match <- matchSimply (Var u2) (StmtCtxt (HsDoStmt ListComp)) ManyTy pat rest_expr core_fail
 
     let
         rhs = Lam u1 $
@@ -372,7 +372,7 @@ dfBindComp c_id n_id (pat, core_list1) quals = do
     core_rest <- dfListComp c_id b quals
 
     -- build the pattern match
-    core_expr <- matchSimply (Var x) (StmtCtxt (HsDoStmt ListComp))
+    core_expr <- matchSimply (Var x) (StmtCtxt (HsDoStmt ListComp)) ManyTy
                 pat core_rest (Var b)
 
     -- now build the outermost foldr, and return
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 05e5becb53c2ed07d316a250268f73f49d1c14f7..d5c30d14629bf14f5d5991ce6cd2739b7084f5d5 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -890,6 +890,7 @@ matchEquations ctxt vars eqns_info rhs_ty
 -- pattern. It returns an expression.
 matchSimply :: CoreExpr                 -- ^ Scrutinee
             -> HsMatchContext GhcTc     -- ^ Match kind
+            -> Mult                     -- ^ Scaling factor of the case expression
             -> LPat GhcTc               -- ^ Pattern it should match
             -> CoreExpr                 -- ^ Return this if it matches
             -> CoreExpr                 -- ^ Return this if it doesn't
@@ -903,15 +904,15 @@ matchSimply :: CoreExpr                 -- ^ Scrutinee
 --     match is awkward
 --   * And we still export 'matchSinglePatVar', so not much is gained if we
 --     don't also implement it in terms of 'matchWrapper'
-matchSimply scrut hs_ctx pat result_expr fail_expr = do
+matchSimply scrut hs_ctx mult pat result_expr fail_expr = do
     let
       match_result = cantFailMatchResult result_expr
       rhs_ty       = exprType fail_expr
         -- Use exprType of fail_expr, because won't refine in the case of failure!
-    match_result' <- matchSinglePat scrut hs_ctx pat rhs_ty match_result
+    match_result' <- matchSinglePat scrut hs_ctx pat mult rhs_ty match_result
     extractMatchResult match_result' fail_expr
 
-matchSinglePat :: CoreExpr -> HsMatchContext GhcTc -> LPat GhcTc
+matchSinglePat :: CoreExpr -> HsMatchContext GhcTc -> LPat GhcTc -> Mult
                -> Type -> MatchResult CoreExpr -> DsM (MatchResult CoreExpr)
 -- matchSinglePat ensures that the scrutinee is a variable
 -- and then calls matchSinglePatVar
@@ -920,17 +921,12 @@ matchSinglePat :: CoreExpr -> HsMatchContext GhcTc -> LPat GhcTc
 -- Used for things like [ e | pat <- stuff ], where
 -- incomplete patterns are just fine
 
-matchSinglePat (Var var) ctx pat ty match_result
+matchSinglePat (Var var) ctx pat _ ty match_result
   | not (isExternalName (idName var))
   = matchSinglePatVar var Nothing ctx pat ty match_result
 
-matchSinglePat scrut hs_ctx pat ty match_result
-  = do { var           <- selectSimpleMatchVarL ManyTy pat
-                            -- matchSinglePat is only used in matchSimply, which
-                            -- is used in list comprehension, arrow notation,
-                            -- and to create field selectors. All of which only
-                            -- bind unrestricted variables, hence the 'Many'
-                            -- above.
+matchSinglePat scrut hs_ctx pat mult ty match_result
+  = do { var           <- selectSimpleMatchVarL mult pat
        ; match_result' <- matchSinglePatVar var (Just scrut) hs_ctx pat ty match_result
        ; return $ bindNonRec var scrut <$> match_result'
        }
diff --git a/compiler/GHC/HsToCore/Match.hs-boot b/compiler/GHC/HsToCore/Match.hs-boot
index 5a55463d4c6f9825c32df0deaa310930f39aa0a3..5ee1fbd0d666a4c0c11431e194b28caec18f640f 100644
--- a/compiler/GHC/HsToCore/Match.hs-boot
+++ b/compiler/GHC/HsToCore/Match.hs-boot
@@ -5,7 +5,7 @@ import GHC.Types.Var ( Id )
 import GHC.Tc.Utils.TcType  ( Type )
 import GHC.HsToCore.Monad ( DsM, EquationInfo, MatchResult )
 import GHC.Core ( CoreExpr )
-import GHC.Hs   ( LPat, HsMatchContext, MatchGroup, LHsExpr )
+import GHC.Hs   ( LPat, HsMatchContext, MatchGroup, LHsExpr, Mult )
 import GHC.Hs.Extension ( GhcTc )
 
 match   :: [Id]
@@ -22,6 +22,7 @@ matchWrapper
 matchSimply
         :: CoreExpr
         -> HsMatchContext GhcTc
+        -> Mult
         -> LPat GhcTc
         -> CoreExpr
         -> CoreExpr
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index 248e408b72500e0be3697398315fac7be409c6db..07b875e858fa2819fda452b60d052a36ce6ba3b3 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -250,6 +250,9 @@ wrapBind new old body   -- NB: this function must deal with term
   | new==old    = body  -- variables, type variables or coercion variables
   | otherwise   = Let (NonRec new (varToCoreExpr old)) body
 
+-- Used to force variables when desugaring strict binders. It's crucial that the
+-- variable is shadowed by the case binder. See Wrinkle 1 in
+-- Note [Desugar Strict binds] in GHC.HsToCore.Binds.
 seqVar :: Var -> CoreExpr -> CoreExpr
 seqVar var body = mkDefaultCase (Var var) var body
 
@@ -751,7 +754,7 @@ mkSelectorBinds ticks pat ctx val_expr
        ; let mk_bind tick bndr_var
                -- (mk_bind sv bv)  generates  bv = case sv of { pat -> bv }
                -- Remember, 'pat' binds 'bv'
-               = do { rhs_expr <- matchSimply (Var val_var) ctx pat'
+               = do { rhs_expr <- matchSimply (Var val_var) ctx ManyTy pat'
                                        (Var bndr_var)
                                        (Var bndr_var)  -- Neat hack
                       -- Neat hack: since 'pat' can't fail, the
@@ -766,7 +769,7 @@ mkSelectorBinds ticks pat ctx val_expr
   | otherwise                          -- General case (C)
   = do { tuple_var  <- newSysLocalDs ManyTy tuple_ty
        ; error_expr <- mkErrorAppDs pAT_ERROR_ID tuple_ty (ppr pat')
-       ; tuple_expr <- matchSimply val_expr ctx pat
+       ; tuple_expr <- matchSimply val_expr ctx ManyTy pat
                                    local_tuple error_expr
        ; let mk_tup_bind tick binder
                = (binder, mkOptTickBox tick $
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index b171a961112227cb834851efd81480fb996275af..ae30baad8c61b6fb113f67b7a27afcb8575c3af0 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -2553,7 +2553,18 @@ decl_no_th :: { LHsDecl GhcPs }
 
         | infixexp     opt_sig rhs  {% runPV (unECP $1) >>= \ $1 ->
                                        do { let { l = comb2 $1 $> }
-                                          ; r <- checkValDef l $1 $2 $3;
+                                          ; r <- checkValDef l $1 (HsNoMultAnn, $2) $3;
+                                        -- Depending upon what the pattern looks like we might get either
+                                        -- a FunBind or PatBind back from checkValDef. See Note
+                                        -- [FunBind vs PatBind]
+                                          ; cs <- getCommentsFor l
+                                          ; return $! (sL (commentsA l cs) $ ValD noExtField r) } }
+        | PREFIX_PERCENT atype infixexp     opt_sig rhs  {% runPV (unECP $3) >>= \ $3 ->
+                                       do { let { l = comb2 $3 $> }
+                                          ; r <- checkValDef l $3 (mkMultAnn (hsTok $1) $2, $4) $5;
+                                        -- parses bindings of the form %p x or
+                                        -- %p x :: sig
+                                        --
                                         -- Depending upon what the pattern looks like we might get either
                                         -- a FunBind or PatBind back from checkValDef. See Note
                                         -- [FunBind vs PatBind]
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 9821dadc393528f3709ccda68a4dfe1d7dac7325..c6e304479439642399f702b3c09ad99e63e297bf 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -75,6 +75,7 @@ module GHC.Parser.PostProcess (
         mkBangTy,
         UnpackednessPragma(..),
         mkMultTy,
+        mkMultAnn,
 
         -- Token location
         mkTokenLocation,
@@ -139,8 +140,7 @@ import GHC.Types.TyThing
 import GHC.Core.Type    ( Specificity(..) )
 import GHC.Builtin.Types( cTupleTyConName, tupleTyCon, tupleDataCon,
                           nilDataConName, nilDataConKey,
-                          listTyConName, listTyConKey,
-                          unrestrictedFunTyCon )
+                          listTyConName, listTyConKey, unrestrictedFunTyCon )
 import GHC.Types.ForeignCall
 import GHC.Types.SrcLoc
 import GHC.Types.Unique ( hasKey )
@@ -742,7 +742,7 @@ mkPatSynMatchGroup (L loc patsyn_name) (L ld decls) =
     fromDecl (L loc decl@(ValD _ (PatBind _
                                  -- AZ: where should these anns come from?
                          pat@(L _ (ConPat noAnn ln@(L _ name) details))
-                               rhs))) =
+                               _ rhs))) =
         do { unless (name == patsyn_name) $
                wrongNameBindingErr (locA loc) decl
            ; match <- case details of
@@ -1313,17 +1313,17 @@ patIsRec e = e == mkUnqual varName (fsLit "rec")
 
 checkValDef :: SrcSpan
             -> LocatedA (PatBuilder GhcPs)
-            -> Maybe (AddEpAnn, LHsType GhcPs)
+            -> (HsMultAnn GhcPs, Maybe (AddEpAnn, LHsType GhcPs))
             -> Located (GRHSs GhcPs (LHsExpr GhcPs))
             -> P (HsBind GhcPs)
 
-checkValDef loc lhs (Just (sigAnn, sig)) grhss
+checkValDef loc lhs (mult, Just (sigAnn, sig)) grhss
         -- x :: ty = rhs  parses as a *pattern* binding
   = do lhs' <- runPV $ mkHsTySigPV (combineLocsA lhs sig) lhs sig [sigAnn]
                         >>= checkLPat
-       checkPatBind loc [] lhs' grhss
+       checkPatBind loc [] lhs' grhss mult
 
-checkValDef loc lhs Nothing g
+checkValDef loc lhs (HsNoMultAnn, Nothing) g
   = do  { mb_fun <- isFunLhs lhs
         ; case mb_fun of
             Just (fun, is_infix, pats, ann) ->
@@ -1331,7 +1331,12 @@ checkValDef loc lhs Nothing g
                            fun is_infix pats g
             Nothing -> do
               lhs' <- checkPattern lhs
-              checkPatBind loc [] lhs' g }
+              checkPatBind loc [] lhs' g HsNoMultAnn }
+
+checkValDef loc lhs (mult_ann, Nothing) ghrss
+        -- %p x = rhs  parses as a *pattern* binding
+  = do lhs' <- checkPattern lhs
+       checkPatBind loc [] lhs' ghrss mult_ann
 
 checkFunBind :: SrcStrictness
              -> SrcSpan
@@ -1373,9 +1378,10 @@ checkPatBind :: SrcSpan
              -> [AddEpAnn]
              -> LPat GhcPs
              -> Located (GRHSs GhcPs (LHsExpr GhcPs))
+             -> HsMultAnn GhcPs
              -> P (HsBind GhcPs)
 checkPatBind loc annsIn (L _ (BangPat (EpAnn _ ans cs) (L _ (VarPat _ v))))
-                        (L _match_span grhss)
+                        (L _match_span grhss) HsNoMultAnn
       = return (makeFunBind v (L (noAnnSrcSpan loc)
                 [L (noAnnSrcSpan loc) (m (EpAnn (spanAsAnchor loc) (ans++annsIn) cs) v)]))
   where
@@ -1386,9 +1392,11 @@ checkPatBind loc annsIn (L _ (BangPat (EpAnn _ ans cs) (L _ (VarPat _ v))))
                   , m_pats = []
                  , m_grhss = grhss }
 
-checkPatBind loc annsIn lhs (L _ grhss) = do
+checkPatBind loc annsIn lhs (L _ grhss) mult = do
   cs <- getCommentsFor loc
-  return (PatBind (EpAnn (spanAsAnchor loc) annsIn cs) lhs grhss)
+  let mult_ann = MultAnn{mult_ext=NoExtField, mult_ann=mult}
+  return (PatBind (EpAnn (spanAsAnchor loc) annsIn cs) lhs mult_ann grhss)
+
 
 checkValSigLhs :: LHsExpr GhcPs -> P (LocatedN RdrName)
 checkValSigLhs (L _ (HsVar _ lrdr@(L _ v)))
@@ -3195,6 +3203,16 @@ mkMultTy pct t@(L _ (HsTyLit _ (HsNumTy (SourceText (unpackFS -> "1")) 1))) arr
     locOfPct1 = token_location_widenR (getLoc pct) (locA (getLoc t))
 mkMultTy pct t arr = HsExplicitMult pct t arr
 
+mkMultAnn :: LHsToken "%" GhcPs -> LHsType GhcPs -> HsMultAnn GhcPs
+mkMultAnn pct t@(L _ (HsTyLit _ (HsNumTy (SourceText (unpackFS -> "1")) 1)))
+  -- See #18888 for the use of (SourceText "1") above
+  = HsPct1Ann (L locOfPct1 HsTok)
+  where
+    -- The location of "%" combined with the location of "1".
+    locOfPct1 :: TokenLocation
+    locOfPct1 = token_location_widenR (getLoc pct) (locA (getLoc t))
+mkMultAnn pct t = HsMultAnn pct t
+
 mkTokenLocation :: SrcSpan -> TokenLocation
 mkTokenLocation (UnhelpfulSpan _) = NoTokenLoc
 mkTokenLocation (RealSrcSpan r mb) = TokenLoc (EpaSpan (RealSrcSpan r mb))
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index c3cc596850d7792ebef196d2195ee1d849897de8..c67b1e2fb30135fbb7099bd6ac8ba9b9ad721661 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -442,11 +442,12 @@ rnBindLHS :: NameMaker
           -- (i.e., any free variables of the pattern)
           -> RnM (HsBindLR GhcRn GhcPs)
 
-rnBindLHS name_maker _ bind@(PatBind { pat_lhs = pat })
+rnBindLHS name_maker _ bind@(PatBind { pat_lhs = pat, pat_mult = pat_mult })
   = do
       -- we don't actually use the FV processing of rnPatsAndThen here
       (pat',pat'_fvs) <- rnBindPat name_maker pat
-      return (bind { pat_lhs = pat', pat_ext = pat'_fvs })
+      (pat_mult', mult'_fvs) <- rnMultAnn pat_mult
+      return (bind { pat_lhs = pat', pat_ext = pat'_fvs `plusFV` mult'_fvs, pat_mult = pat_mult' })
                 -- We temporarily store the pat's FVs in bind_fvs;
                 -- gets updated to the FVs of the whole bind
                 -- when doing the RHS below
@@ -711,6 +712,20 @@ makeMiniFixityEnv decls = foldlM add_one_sig emptyFsEnv decls
      }
 
 
+-- | Multiplicity annotations are a simple wrapper around types. As such,
+-- renaming them is a straightforward wrapper around 'rnLHsType'.
+rnHsMultAnn :: HsMultAnn GhcPs -> RnM (HsMultAnn GhcRn, FreeVars)
+rnHsMultAnn HsNoMultAnn = return $ (HsNoMultAnn, emptyFVs)
+rnHsMultAnn (HsPct1Ann x) = return $ (HsPct1Ann x, emptyFVs)
+rnHsMultAnn (HsMultAnn x p) = do
+  (p', freeVars') <- rnLHsType PatCtx p
+  return $ (HsMultAnn x p', freeVars')
+
+rnMultAnn :: MultAnn GhcPs -> RnM (MultAnn GhcRn, FreeVars)
+rnMultAnn (MultAnn{mult_ext=none, mult_ann=ann}) = do
+  (ann', freeVars') <- rnHsMultAnn ann
+  return $ (MultAnn{mult_ext=none, mult_ann=ann'}, freeVars')
+
 {- *********************************************************************
 *                                                                      *
                 Pattern synonym bindings
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 21280a1fde733af75485426d3a3bf512454ede50..411b5457a292db22bcbb0389da9ad5a95710ae7a 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -155,17 +155,17 @@ tc_cmd env (HsCmdPar x lpar cmd rpar) res_ty
         ; return (HsCmdPar x lpar cmd' rpar) }
 
 tc_cmd env (HsCmdLet x tkLet binds tkIn (L body_loc body)) res_ty
-  = do  { (binds', body') <- tcLocalBinds binds         $
-                             setSrcSpan (locA body_loc) $
-                             tc_cmd env body res_ty
+  = do  { (binds', _, body') <- tcLocalBinds binds         $
+                                setSrcSpan (locA body_loc) $
+                                tc_cmd env body res_ty
         ; return (HsCmdLet x tkLet binds' tkIn (L body_loc body')) }
 
 tc_cmd env in_cmd@(HsCmdCase x scrut matches) (stk, res_ty)
   = addErrCtxt (cmdCtxt in_cmd) $ do
     do { (scrut', scrut_ty) <- tcInferRho scrut
        ; hasFixedRuntimeRep_syntactic (FRRArrow $ ArrowCmdCase) scrut_ty
-       ; matches' <- tcCmdMatches env scrut_ty matches (stk, res_ty)
-       ; return (HsCmdCase x scrut' matches') }
+       ; (mult_co_wrap, matches') <- tcCmdMatches env scrut_ty matches (stk, res_ty)
+       ; return (HsCmdCase x (mkLHsWrap mult_co_wrap scrut') matches') }
 
 tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty    -- Ordinary 'if'
   = do  { pred' <- tcCheckMonoExpr pred boolTy
@@ -317,7 +317,7 @@ tcCmdMatches :: CmdEnv
              -> TcTypeFRR -- ^ Type of the scrutinee.
              -> MatchGroup GhcRn (LHsCmd GhcRn)  -- ^ case alternatives
              -> CmdType
-             -> TcM (MatchGroup GhcTc (LHsCmd GhcTc))
+             -> TcM (HsWrapper, MatchGroup GhcTc (LHsCmd GhcTc))
 tcCmdMatches env scrut_ty matches (stk, res_ty)
   = tcMatchesCase match_ctxt (unrestricted scrut_ty) matches (mkCheckExpType res_ty)
   where
@@ -366,8 +366,8 @@ tcCmdMatchLambda env
     pg_ctxt    = PatGuard match_ctxt
 
     tc_grhss (GRHSs x grhss binds) stk_ty res_ty
-        = do { (binds', grhss') <- tcLocalBinds binds $
-                                   mapM (wrapLocMA (tc_grhs stk_ty res_ty)) grhss
+        = do { (binds', _, grhss') <- tcLocalBinds binds $
+                                      mapM (wrapLocMA (tc_grhs stk_ty res_ty)) grhss
              ; return (GRHSs x grhss' binds') }
 
     tc_grhs stk_ty res_ty (GRHS x guards body)
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 958c07933818487eaa6cc84fc3af515874eec7c7..9c4263c49c15e3445c401842c1ff00ecade7c0dd 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -45,7 +45,8 @@ import GHC.Tc.Utils.Unify
 import GHC.Tc.Solver
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Constraint
-
+import GHC.Core.Predicate
+import GHC.Core.UsageEnv ( bottomUE )
 import GHC.Tc.Gen.HsType
 import GHC.Tc.Gen.Pat
 import GHC.Tc.Utils.TcMType
@@ -53,8 +54,6 @@ import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
 import GHC.Tc.Utils.TcType
 import GHC.Tc.Validity (checkValidType, checkEscapingKind)
 import GHC.Tc.Zonk.TcType
-
-import GHC.Core.Predicate ( getEqPredTys_maybe )
 import GHC.Core.Reduction ( Reduction(..) )
 import GHC.Core.Multiplicity
 import GHC.Core.FamInstEnv( normaliseType )
@@ -63,7 +62,7 @@ import GHC.Core.Coercion( mkSymCo )
 import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
 import GHC.Core.TyCo.Ppr( pprTyVars )
 
-import GHC.Builtin.Types ( mkConstraintTupleTy )
+import GHC.Builtin.Types ( mkConstraintTupleTy, multiplicityTy, oneDataConTy  )
 import GHC.Builtin.Types.Prim
 import GHC.Unit.Module
 
@@ -195,7 +194,14 @@ tcTopBinds :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
 -- The TcLclEnv has an extended type envt for the new bindings
 tcTopBinds binds sigs
   = do  { -- Pattern synonym bindings populate the global environment
-          (binds', (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs getEnvs
+          (binds', wrap, (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs getEnvs
+        ; massertPpr (isIdHsWrapper wrap)
+                     (text "Non-identity multiplicity wrapper at toplevel:" <+> ppr wrap)
+          -- The wrapper (`wrap`) is always the identity because toplevel
+          -- binders are unrestricted (and `tcSubmult _ ManyTy` returns the
+          -- identity wrapper). Therefore it's safe to drop it altogether.
+          --
+          -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
         ; specs <- tcImpPrags sigs   -- SPECIALISE prags for imported Ids
 
         ; complete_matches <- restoreEnvs (tcg_env, tcl_env) $ tcCompleteSigs sigs
@@ -250,16 +256,18 @@ tcHsBootSigs binds sigs
     tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
 
 ------------------------
+
+-- Why an HsWrapper? See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 tcLocalBinds :: HsLocalBinds GhcRn -> TcM thing
-             -> TcM (HsLocalBinds GhcTc, thing)
+             -> TcM (HsLocalBinds GhcTc, HsWrapper, thing)
 
 tcLocalBinds (EmptyLocalBinds x) thing_inside
   = do  { thing <- thing_inside
-        ; return (EmptyLocalBinds x, thing) }
+        ; return (EmptyLocalBinds x, idHsWrapper, thing) }
 
 tcLocalBinds (HsValBinds x (XValBindsLR (NValBinds binds sigs))) thing_inside
-  = do  { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
-        ; return (HsValBinds x (XValBindsLR (NValBinds binds' sigs)), thing) }
+  = do  { (binds', wrapper, thing) <- tcValBinds NotTopLevel binds sigs thing_inside
+        ; return (HsValBinds x (XValBindsLR (NValBinds binds' sigs)), wrapper, thing) }
 tcLocalBinds (HsValBinds _ (ValBinds {})) _ = panic "tcLocalBinds"
 
 tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
@@ -271,7 +279,10 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
         ; (ev_binds, result) <- checkConstraints (IPSkol ips)
                                   [] given_ips thing_inside
 
-        ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , result) }
+        -- We don't have linear implicit parameters, yet. So the wrapper can be
+        -- the identity.
+        -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
+        ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , idHsWrapper, result) }
   where
     ips = [ip | (L _ (IPBind _ (L _ ip) _)) <- ip_binds]
 
@@ -297,10 +308,11 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
     toDict ipClass x ty = mkHsWrap $ mkWpCastR $
                           wrapIP $ mkClassPred ipClass [x,ty]
 
+-- Why an HsWrapper? See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 tcValBinds :: TopLevelFlag
            -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
            -> TcM thing
-           -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
+           -> TcM ([(RecFlag, LHsBinds GhcTc)], HsWrapper, thing)
 
 tcValBinds top_lvl binds sigs thing_inside
   = do  {   -- Typecheck the signatures
@@ -319,7 +331,7 @@ tcValBinds top_lvl binds sigs thing_inside
         -- For the moment, let bindings and top-level bindings introduce
         -- only unrestricted variables.
         ; tcExtendSigIds top_lvl poly_ids $
-     do { (binds', (extra_binds', thing))
+     do { (binds', wrapper, (extra_binds', thing))
               <- tcBindGroups top_lvl sig_fn prag_fn binds $
                  do { thing <- thing_inside
                        -- See Note [Pattern synonym builders don't yield dependencies]
@@ -328,15 +340,17 @@ tcValBinds top_lvl binds sigs thing_inside
                     ; let extra_binds = [ (NonRecursive, builder)
                                         | builder <- patsyn_builders ]
                     ; return (extra_binds, thing) }
-        ; return (binds' ++ extra_binds', thing) }}
+        ; return (binds' ++ extra_binds', wrapper, thing) }}
   where
     patsyns = getPatSynBinds binds
     prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
 
 ------------------------
+
+-- Why an HsWrapper? See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
              -> [(RecFlag, LHsBinds GhcRn)] -> TcM thing
-             -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
+             -> TcM ([(RecFlag, LHsBinds GhcTc)], HsWrapper, thing)
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 -- Here a "strongly connected component" has the straightforward
@@ -345,16 +359,16 @@ tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
 
 tcBindGroups _ _ _ [] thing_inside
   = do  { thing <- thing_inside
-        ; return ([], thing) }
+        ; return ([], idHsWrapper, thing) }
 
 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
   = do  { -- See Note [Closed binder groups]
           type_env <- getLclTypeEnv
         ; let closed = isClosedBndrGroup type_env (snd group)
-        ; (group', (groups', thing))
+        ; (group', outer_wrapper, (groups', inner_wrapper, thing))
                 <- tc_group top_lvl sig_fn prag_fn group closed $
                    tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
-        ; return (group' ++ groups', thing) }
+        ; return (group' ++ groups', outer_wrapper <.> inner_wrapper, thing) }
 
 -- Note [Closed binder groups]
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -377,7 +391,7 @@ tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
 tc_group :: forall thing.
             TopLevelFlag -> TcSigFun -> TcPragEnv
          -> (RecFlag, LHsBinds GhcRn) -> IsGroupClosed -> TcM thing
-         -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
+         -> TcM ([(RecFlag, LHsBinds GhcTc)], HsWrapper, thing)
 
 -- Typecheck one strongly-connected component of the original program.
 -- We get a list of groups back, because there may
@@ -391,9 +405,9 @@ tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) closed thing_inside
                  [bind] -> bind
                  []     -> panic "tc_group: empty list of binds"
                  _      -> panic "tc_group: NonRecursive binds is not a singleton bag"
-       ; (bind', thing) <- tc_single top_lvl sig_fn prag_fn bind closed
+       ; (bind', wrapper, thing) <- tc_single top_lvl sig_fn prag_fn bind closed
                                      thing_inside
-       ; return ( [(NonRecursive, bind')], thing) }
+       ; return ( [(NonRecursive, bind')], wrapper, thing) }
 
 tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
   =     -- To maximise polymorphism, we do a new
@@ -404,8 +418,8 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     do  { traceTc "tc_group rec" (pprLHsBinds binds)
         ; whenIsJust mbFirstPatSyn $ \lpat_syn ->
             recursivePatSynErr (locA $ getLoc lpat_syn) binds
-        ; (binds1, thing) <- go sccs
-        ; return ([(Recursive, binds1)], thing) }
+        ; (binds1, wrapper, thing) <- go sccs
+        ; return ([(Recursive, binds1)], wrapper, thing) }
                 -- Rec them all together
   where
     mbFirstPatSyn = find (isPatSyn . unLoc) binds
@@ -415,14 +429,15 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     sccs :: [SCC (LHsBind GhcRn)]
     sccs = stronglyConnCompFromEdgedVerticesUniq (mkEdges sig_fn binds)
 
-    go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTc, thing)
+    go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTc, HsWrapper, thing)
     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
                          -- recursive bindings must be unrestricted
                          -- (the ids added to the environment here are the name of the recursive definitions).
-                        ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn closed ids1
-                                                            (go sccs)
-                        ; return (binds1 `unionBags` binds2, thing) }
-    go []         = do  { thing <- thing_inside; return (emptyBag, thing) }
+                        ; ((binds2, inner_wrapper, thing), outer_wrapper) <-
+                              tcExtendLetEnv top_lvl sig_fn closed ids1
+                              (go sccs)
+                        ; return (binds1 `unionBags` binds2, outer_wrapper <.> inner_wrapper, thing) }
+    go []         = do  { thing <- thing_inside; return (emptyBag, idHsWrapper, thing) }
 
     tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
     tc_scc (CyclicSCC binds) = tc_sub_group Recursive    binds
@@ -441,13 +456,13 @@ recursivePatSynErr loc binds
 tc_single :: forall thing.
             TopLevelFlag -> TcSigFun -> TcPragEnv
           -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
-          -> TcM (LHsBinds GhcTc, thing)
+          -> TcM (LHsBinds GhcTc, HsWrapper, thing)
 tc_single _top_lvl sig_fn prag_fn
           (L loc (PatSynBind _ psb))
           _ thing_inside
   = do { (aux_binds, tcg_env) <- tcPatSynDecl (L loc psb) sig_fn prag_fn
        ; thing <- setGblEnv tcg_env thing_inside
-       ; return (aux_binds, thing)
+       ; return (aux_binds, idHsWrapper, thing)
        }
 
 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
@@ -455,10 +470,8 @@ tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
                                       NonRecursive NonRecursive
                                       closed
                                       [lbind]
-         -- since we are defining a non-recursive binding, it is not necessary here
-         -- to define an unrestricted binding. But we do so until toplevel linear bindings are supported.
-       ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
-       ; return (binds1, thing) }
+       ; (thing, wrapper) <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
+       ; return (binds1, wrapper, thing) }
 
 ------------------------
 type BKey = Int -- Just number off the bindings
@@ -494,7 +507,7 @@ tcPolyBinds :: TopLevelFlag -> TcSigFun -> TcPragEnv
                                -- dependencies based on type signatures
             -> IsGroupClosed   -- Whether the group is closed
             -> [LHsBind GhcRn]  -- None are PatSynBind
-            -> TcM (LHsBinds GhcTc, [TcId])
+            -> TcM (LHsBinds GhcTc, [Scaled TcId])
 
 -- Typechecks a single bunch of values bindings all together,
 -- and generalises them.  The bunch may be only part of a recursive
@@ -517,11 +530,13 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
     ; dflags   <- getDynFlags
     ; let plan = decideGeneralisationPlan dflags top_lvl closed sig_fn bind_list
     ; traceTc "Generalisation plan" (ppr plan)
-    ; result@(_, poly_ids) <- case plan of
+    ; result@(_, scaled_poly_ids) <- case plan of
          NoGen              -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
          InferGen           -> tcPolyInfer rec_tc prag_fn sig_fn bind_list
          CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
 
+    ; let poly_ids = map scaledThing scaled_poly_ids
+
     ; mapM_ (\ poly_id ->
         hasFixedRuntimeRep_syntactic (FRRBinder $ idName poly_id) (idType poly_id))
         poly_ids
@@ -542,10 +557,10 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise
 -- subsequent error messages
-recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTc, [Id])
+recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTc, [Scaled Id])
 recoveryCode binder_names sig_fn
   = do  { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
-        ; let poly_ids = map mk_dummy binder_names
+        ; let poly_ids = map (Scaled ManyTy) $ map mk_dummy binder_names
         ; return (emptyBag, poly_ids) }
   where
     mk_dummy name
@@ -575,7 +590,7 @@ tcPolyNoGen     -- No generalisation whatsoever
                    -- dependencies based on type signatures
   -> TcPragEnv -> TcSigFun
   -> [LHsBind GhcRn]
-  -> TcM (LHsBinds GhcTc, [TcId])
+  -> TcM (LHsBinds GhcTc, [Scaled TcId])
 
 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
   = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
@@ -584,9 +599,9 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
        ; mono_ids' <- mapM tc_mono_info mono_infos
        ; return (binds', mono_ids') }
   where
-    tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
+    tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id, mbi_mono_mult = mult })
       = do { _specs <- tcSpecPrags mono_id (lookupPragEnv prag_fn name)
-           ; return mono_id }
+           ; return $ Scaled mult mono_id }
            -- NB: tcPrags generates error messages for
            --     specialisation pragmas for non-overloaded sigs
            -- Indeed that is why we call it here!
@@ -602,7 +617,7 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
 tcPolyCheck :: TcPragEnv
             -> TcIdSigInfo     -- Must be a complete signature
             -> LHsBind GhcRn   -- Must be a FunBind
-            -> TcM (LHsBinds GhcTc, [TcId])
+            -> TcM (LHsBinds GhcTc, [Scaled TcId])
 -- There is just one binding,
 --   it is a FunBind
 --   it has a complete type signature,
@@ -615,6 +630,7 @@ tcPolyCheck prag_fn
   = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
 
        ; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
+       ; mult <- tcMultAnn HsNoMultAnn
        ; (wrap_gen, (wrap_res, matches'))
              <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
                 tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
@@ -629,7 +645,7 @@ tcPolyCheck prag_fn
                 --    See Note [Relevant bindings and the binder stack]
 
                 setSrcSpanA bind_loc $
-                tcMatchesFun (L nm_loc (idName mono_id)) matches
+                tcMatchesFun (L nm_loc (idName mono_id)) mult matches
                              (mkCheckExpType rho_ty)
 
        -- We make a funny AbsBinds, abstracting over nothing,
@@ -664,7 +680,7 @@ tcPolyCheck prag_fn
                                  , abs_binds    = unitBag (L bind_loc bind')
                                  , abs_sig      = True }
 
-       ; return (unitBag abs_bind, [poly_id]) }
+       ; return (unitBag abs_bind, [Scaled mult poly_id]) }
 
 tcPolyCheck _prag_fn sig bind
   = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
@@ -708,18 +724,50 @@ it's all cool; each signature has distinct type variables from the renamer.)
 *                                                                      *
 ********************************************************************* -}
 
+{- Note [Non-variable pattern bindings aren't linear]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A fundamental limitation of the typechecking algorithm is that we cannot have a
+binding which, at the same time,
+- is linear in its rhs
+- is a non-variable pattern
+- binds variables to polymorphic or qualified types
+
+A detailed explanation can be found at:
+https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst#let-bindings-and-polymorphism
+
+To address this we to do a few things
+
+- When a pattern is annotated with a multiplicity annotation `let %q pat = rhs
+  in body` (note: multiplicity-annotated bindings are always parsed as a
+  PatBind, see Note [Multiplicity annotations] in Language.Haskell.Syntax.Binds),
+  then the let is never generalised (we use the NoGen plan).
+- Whenever the typechecker infers an AbsBind *and* the inner binding is a
+  non-variable PatBind, then the multiplicity of the binding is inferred to be
+  Many. This is a little infelicitous: sometimes the typechecker infers an
+  AbsBind where it didn't need to. This may cause some programs to be spuriously
+  rejected, when NoMonoLocalBinds is on.
+- LinearLet implies MonoLocalBinds to avoid the AbsBind case altogether.
+
+-}
+
 tcPolyInfer
   :: RecFlag       -- Whether it's recursive after breaking
                    -- dependencies based on type signatures
   -> TcPragEnv -> TcSigFun
   -> [LHsBind GhcRn]
-  -> TcM (LHsBinds GhcTc, [TcId])
+  -> TcM (LHsBinds GhcTc, [Scaled TcId])
 tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
   = do { (tclvl, wanted, (binds', mono_infos))
              <- pushLevelAndCaptureConstraints  $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
        ; apply_mr <- checkMonomorphismRestriction mono_infos bind_list
+
+       -- AbsBinds which are PatBinds can't be linear.
+       -- See Note [Non-variable pattern bindings aren't linear]
+       ; binds' <- manyIfPats binds'
+
        ; traceTc "tcPolyInfer" (ppr apply_mr $$ ppr (map mbi_sig mono_infos))
 
        ; let name_taus  = [ (mbi_poly_name info, idType (mbi_mono_id info))
@@ -732,8 +780,9 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
             <- captureConstraints $ simplifyInfer tclvl infer_mode sigs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
-       ; exports <- checkNoErrs $
+       ; scaled_exports <- checkNoErrs $
                     mapM (mkExport prag_fn residual insoluble qtvs inferred_theta) mono_infos
+       ; let exports = map scaledThing scaled_exports
 
          -- NB: *after* the checkNoErrs call above. This ensures that we don't get an error
          -- cascade in case mkExport runs into trouble. In particular, this avoids duplicate
@@ -743,7 +792,8 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
        ; emitConstraints residual
 
        ; loc <- getSrcSpanM
-       ; let poly_ids = map abe_poly exports
+       ; let scaled_poly_ids = [ Scaled p (abe_poly export) | Scaled p export <- scaled_exports]
+             poly_ids = map scaledThing scaled_poly_ids
              abs_bind = L (noAnnSrcSpan loc) $ XHsBindsLR $
                         AbsBinds { abs_tvs = qtvs
                                  , abs_ev_vars = givens, abs_ev_binds = [ev_binds]
@@ -751,8 +801,20 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn bind_list
                                  , abs_sig = False }
 
        ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
-       ; return (unitBag abs_bind, poly_ids) }
+       ; return (unitBag abs_bind, scaled_poly_ids) }
          -- poly_ids are guaranteed zonked by mkExport
+  where
+    manyIfPat bind@(L _ (PatBind{pat_lhs=(L _ (VarPat{}))}))
+      = return bind
+    manyIfPat (L loc pat@(PatBind {pat_mult=MultAnn{mult_ext=pat_mult}, pat_lhs=lhs, pat_ext =(pat_ty,_)}))
+      = do { mult_co_wrap <- tcSubMult NonLinearPatternOrigin ManyTy pat_mult
+           -- The wrapper checks for correct multiplicities.
+           -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
+           ; let lhs' = mkLHsWrapPat mult_co_wrap lhs pat_ty
+           ; return $ L loc pat {pat_lhs=lhs'}
+           }
+    manyIfPat bind = return bind
+    manyIfPats binds' = traverse manyIfPat binds'
 
 checkMonomorphismRestriction :: [MonoBindInfo] -> [LHsBind GhcRn] -> TcM Bool
 -- True <=> apply the MR
@@ -860,7 +922,7 @@ mkExport :: TcPragEnv
                                         --          when typechecking the bindings
          -> [TyVar] -> TcThetaType      -- Both already zonked
          -> MonoBindInfo
-         -> TcM ABExport
+         -> TcM (Scaled ABExport)
 -- Only called for generalisation plan InferGen, not by CheckGen or NoGen
 --
 -- mkExport generates exports with
@@ -877,7 +939,8 @@ mkExport :: TcPragEnv
 mkExport prag_fn residual insoluble qtvs theta
          (MBI { mbi_poly_name = poly_name
               , mbi_sig       = mb_sig
-              , mbi_mono_id   = mono_id })
+              , mbi_mono_id   = mono_id
+              , mbi_mono_mult = mono_mult })
   = do  { mono_ty <- liftZonkM $ zonkTcType (idType mono_id)
         ; poly_id <- mkInferredPolyId residual insoluble qtvs theta poly_name mb_sig mono_ty
 
@@ -907,7 +970,8 @@ mkExport prag_fn residual insoluble qtvs theta
 
         ; localSigWarn poly_id mb_sig
 
-        ; return (ABE { abe_wrap = wrap
+        ; return (Scaled mono_mult $
+                  ABE { abe_wrap = wrap
                         -- abe_wrap :: (forall qtvs. theta => mono_ty) ~ idType poly_id
                       , abe_poly  = poly_id
                       , abe_mono  = mono_id
@@ -1284,7 +1348,8 @@ The signatures have been dealt with already.
 
 data MonoBindInfo = MBI { mbi_poly_name :: Name
                         , mbi_sig       :: Maybe TcIdSigInst
-                        , mbi_mono_id   :: TcId }
+                        , mbi_mono_id   :: TcId
+                        , mbi_mono_mult :: Mult }
 
 tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking purposes
                         -- i.e. the binders are mentioned in their RHSs, and
@@ -1301,7 +1366,9 @@ tcMonoBinds is_rec sig_fn no_gen
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
   , Nothing <- sig_fn name   -- ...with no type signature
   = setSrcSpanA b_loc    $
-    do  { ((co_fn, matches'), rhs_ty')
+    do  { mult <- tcMultAnn HsNoMultAnn
+
+        ; ((co_fn, matches'), rhs_ty')
             <- tcInferFRR (FRRBinder name) $ \ exp_ty ->
                           -- tcInferFRR: the type of a let-binder must have
                           -- a fixed runtime rep. See #23176
@@ -1309,8 +1376,8 @@ tcMonoBinds is_rec sig_fn no_gen
                           -- We extend the error context even for a non-recursive
                           -- function so that in type error messages we show the
                           -- type of the thing whose rhs we are type checking
-                       tcMatchesFun (L nm_loc name) matches exp_ty
-       ; mono_id <- newLetBndr no_gen name ManyTy rhs_ty'
+                       tcMatchesFun (L nm_loc name) mult matches exp_ty
+       ; mono_id <- newLetBndr no_gen name mult rhs_ty'
 
         ; return (unitBag $ L b_loc $
                      FunBind { fun_id = L nm_loc mono_id,
@@ -1318,27 +1385,55 @@ tcMonoBinds is_rec sig_fn no_gen
                                fun_ext = (co_fn, []) },
                   [MBI { mbi_poly_name = name
                        , mbi_sig       = Nothing
-                       , mbi_mono_id   = mono_id }]) }
+                       , mbi_mono_id   = mono_id
+                       , mbi_mono_mult = mult }]) }
 
 -- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings]
 tcMonoBinds is_rec sig_fn no_gen
-           [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })]
+           [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = MultAnn{mult_ann=mult_ann} })]
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
   , all (isNothing . sig_fn) bndrs
   = addErrCtxt (patMonoBindsCtxt pat grhss) $
-    do { (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty ->
+    do { mult <- tcMultAnn mult_ann
+
+       ; (grhss', pat_ty) <- tcInferFRR FRRPatBind $ \ exp_ty ->
                           -- tcInferFRR: the type of each let-binder must have
                           -- a fixed runtime rep. See #23176
-                             tcGRHSsPat grhss exp_ty
+                             tcGRHSsPat mult grhss exp_ty
 
        ; let exp_pat_ty :: Scaled ExpSigmaTypeFRR
-             exp_pat_ty = unrestricted (mkCheckExpType pat_ty)
-       ; (pat', mbis) <- tcLetPat (const Nothing) no_gen pat exp_pat_ty $
-                         mapM lookupMBI bndrs
+             exp_pat_ty = Scaled mult (mkCheckExpType pat_ty)
+       ; (_, (pat', mbis)) <- tcCollectingUsage $
+                         tcLetPat (const Nothing) no_gen pat exp_pat_ty $ do
+                           tcEmitBindingUsage bottomUE
+                           mapM lookupMBI bndrs
+            -- What's happening here? Typing pattern-matching (either from case
+            -- expression or equation) and typing bindings (let or where) have a
+            -- different control flow: for pattern-matching, the rhs is typed
+            -- within the `thing_inside` argument. The type-checker walks down
+            -- the pattern, and when finally it is done, all variables have been
+            -- added to the environment, thing_inside is called. So, when
+            -- type-checking patterns, the check for the correctness of
+            -- multiplicity is generated in the VarPat case. This is quite
+            -- natural.
+            --
+            -- Bindings, however, have a more complex control flow for our
+            -- purpose: we collect all the variables as we go down, then return
+            -- them (here as `mapM lookupMBI bndrs`), and in a subsequent
+            -- computation (rather than an inner computation), the rhs is
+            -- type-checked. This poses a problem here: we're calling
+            -- `tcLetPat`, which will verify the proper usage of the introduced
+            -- variable when reaching the `VarPat` case. But there is no actual
+            -- usage of variable in the `thing_inside`. This would always
+            -- fail. So we emit a `bottomUE`, which is compatible with every
+            -- usage. So that we can bypass the check in VarPat. Then we use
+            -- `tcCollectingUsage` to throw the `bottomUE` away, since it would
+            -- let us bypass many linearity checks.
 
        ; return ( unitBag $ L b_loc $
                      PatBind { pat_lhs = pat', pat_rhs = grhss'
-                             , pat_ext = (pat_ty, ([],[])) }
+                             , pat_ext = (pat_ty, ([],[]))
+                             , pat_mult = MultAnn {mult_ext=mult, mult_ann=mult_ann} }
 
                 , mbis ) }
   where
@@ -1446,8 +1541,8 @@ switch to inference when we have no signature for any of the binders.
 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
 
 data TcMonoBind         -- Half completed; LHS done, RHS not done
-  = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
-  | TcPatBind [MonoBindInfo] (LPat GhcTc) (GRHSs GhcRn (LHsExpr GhcRn))
+  = TcFunBind  MonoBindInfo  SrcSpan Mult (MatchGroup GhcRn (LHsExpr GhcRn))
+  | TcPatBind [MonoBindInfo] (LPat GhcTc) Mult (HsMultAnn GhcRn) (GRHSs GhcRn (LHsExpr GhcRn))
               TcSigmaTypeFRR
 
 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
@@ -1466,32 +1561,32 @@ tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name
     --           Just g = ...f...
     -- Hence always typechecked with InferGen
     do { mono_info <- tcLhsSigId no_gen (name, sig)
-       ; return (TcFunBind mono_info (locA nm_loc) matches) }
+       ; mult <- tcMultAnn HsNoMultAnn
+       ; return (TcFunBind mono_info (locA nm_loc) mult matches) }
 
   | otherwise  -- No type signature
   = do { mono_ty <- newOpenFlexiTyVarTy
-       ; mono_id <- newLetBndr no_gen name ManyTy mono_ty
-          -- This ^ generates a binder with Many multiplicity because all
-          -- let/where-binders are unrestricted. When we introduce linear let
-          -- binders, we will need to retrieve the multiplicity information.
+       ; mult <- tcMultAnn HsNoMultAnn
+       ; mono_id <- newLetBndr no_gen name mult mono_ty
        ; let mono_info = MBI { mbi_poly_name = name
                              , mbi_sig       = Nothing
-                             , mbi_mono_id   = mono_id }
-       ; return (TcFunBind mono_info (locA nm_loc) matches) }
+                             , mbi_mono_id   = mono_id
+                             , mbi_mono_mult = mult}
+       ; return (TcFunBind mono_info (locA nm_loc) mult matches) }
 
-tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
+tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_mult = MultAnn{mult_ann=mult_ann} })
   = -- See Note [Typechecking pattern bindings]
     do  { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
 
         ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
                              [ (mbi_poly_name mbi, mbi_mono_id mbi)
                              | mbi <- sig_mbis ]
-
+        ; mult <- tcMultAnn mult_ann
             -- See Note [Typechecking pattern bindings]
         ; ((pat', nosig_mbis), pat_ty)
             <- addErrCtxt (patMonoBindsCtxt pat grhss) $
                tcInferFRR FRRPatBind $ \ exp_ty ->
-               tcLetPat inst_sig_fun no_gen pat (unrestricted exp_ty) $
+               tcLetPat inst_sig_fun no_gen pat (Scaled mult exp_ty) $
                  -- The above inferred type get an unrestricted multiplicity. It may be
                  -- worth it to try and find a finer-grained multiplicity here
                  -- if examples warrant it.
@@ -1503,7 +1598,7 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
                                 | mbi <- mbis, let id = mbi_mono_id mbi ]
                            $$ ppr no_gen)
 
-        ; return (TcPatBind mbis pat' grhss pat_ty) }
+        ; return (TcPatBind mbis pat' mult mult_ann grhss pat_ty) }
   where
     bndr_names = collectPatBinders CollNoDictBinders pat
     (nosig_names, sig_names) = partitionWith find_sig bndr_names
@@ -1526,7 +1621,8 @@ lookupMBI name
   = do { mono_id <- tcLookupId name
        ; return (MBI { mbi_poly_name = name
                      , mbi_sig       = Nothing
-                     , mbi_mono_id   = mono_id }) }
+                     , mbi_mono_id   = mono_id
+                     , mbi_mono_mult = idMult mono_id }) }
 
 -------------------
 tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
@@ -1535,7 +1631,8 @@ tcLhsSigId no_gen (name, sig)
        ; mono_id <- newSigLetBndr no_gen name inst_sig
        ; return (MBI { mbi_poly_name = name
                      , mbi_sig       = Just inst_sig
-                     , mbi_mono_id   = mono_id }) }
+                     , mbi_mono_id   = mono_id
+                     , mbi_mono_mult = idMult mono_id }) }
 
 ------------
 newSigLetBndr :: LetBndrSpec -> Name -> TcIdSigInst -> TcM TcId
@@ -1551,18 +1648,18 @@ newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind GhcTc)
 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
-                 loc matches)
+                 loc mult matches)
   = tcExtendIdBinderStackForRhs [info]  $
     tcExtendTyVarEnvForRhs mb_sig       $
     do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
-        ; (co_fn, matches') <- tcMatchesFun (L (noAnnSrcSpan loc) (idName mono_id))
+        ; (co_fn, matches') <- tcMatchesFun (L (noAnnSrcSpan loc) (idName mono_id)) mult
                                  matches (mkCheckExpType $ idType mono_id)
         ; return ( FunBind { fun_id = L (noAnnSrcSpan loc) mono_id
                            , fun_matches = matches'
                            , fun_ext = (co_fn, [])
                            } ) }
 
-tcRhs (TcPatBind infos pat' grhss pat_ty)
+tcRhs (TcPatBind infos pat' mult mult_ann grhss pat_ty)
   = -- When we are doing pattern bindings we *don't* bring any scoped
     -- type variables into scope unlike function bindings
     -- Wny not?  They are not completely rigid.
@@ -1570,10 +1667,20 @@ tcRhs (TcPatBind infos pat' grhss pat_ty)
     tcExtendIdBinderStackForRhs infos        $
     do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
-                    tcGRHSsPat grhss (mkCheckExpType pat_ty)
+                    tcGRHSsPat mult grhss (mkCheckExpType pat_ty)
 
         ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
-                           , pat_ext = (pat_ty, ([],[])) } )}
+                           , pat_ext = (pat_ty, ([],[]))
+                           , pat_mult = MultAnn{mult_ext=mult, mult_ann=mult_ann} } )}
+
+
+-- | @'tcMultAnn' ann@ takes an optional multiplicity annotation. If
+-- present the multiplicity is returned, otherwise a fresh unification variable
+-- is generated so that multiplicity can be inferred.
+tcMultAnn :: HsMultAnn GhcRn -> TcM Mult
+tcMultAnn (HsPct1Ann _) = return oneDataConTy
+tcMultAnn (HsMultAnn _ p) = tcCheckLHsType p (TheKind multiplicityTy)
+tcMultAnn HsNoMultAnn = newFlexiTyVarTy multiplicityTy
 
 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
 tcExtendTyVarEnvForRhs Nothing thing_inside
@@ -1601,8 +1708,8 @@ getMonoBindInfo :: [LocatedA TcMonoBind] -> [MonoBindInfo]
 getMonoBindInfo tc_binds
   = foldr (get_info . unLoc) [] tc_binds
   where
-    get_info (TcFunBind info _ _)    rest = info : rest
-    get_info (TcPatBind infos _ _ _) rest = infos ++ rest
+    get_info (TcFunBind info _ _ _)    rest = info : rest
+    get_info (TcPatBind infos _ _ _ _ _) rest = infos ++ rest
 
 
 {- Note [Relevant bindings and the binder stack]
@@ -1643,7 +1750,7 @@ and suppose t :: T.  Which of these pattern bindings are ok?
 * (E2) is fine, despite the existential pattern, because
   q::Int, and nothing escapes.
 
-* Even (E3) is fine.  The existential pattern binds a dictionary
+* Even (E3) is fine.  The existential pattern bindings a dictionary
   for (Integral a) which the view pattern can use to convert the
   a-valued field to an Integer, so r :: Integer.
 
@@ -1764,6 +1871,9 @@ decideGeneralisationPlan dflags top_lvl closed sig_fn lbinds
       | isTopLevel top_lvl             = True
         -- See Note [Always generalise top-level bindings]
 
+      | has_mult_anns_and_pats = False
+        -- See Note [Non-variable pattern bindings aren't linear]
+
       | IsGroupClosed _ True <- closed = True
         -- The 'True' means that all of the group's
         -- free vars have ClosedTypeId=True; so we can ignore
@@ -1788,6 +1898,11 @@ decideGeneralisationPlan dflags top_lvl closed sig_fn lbinds
     has_partial_sig nm = case sig_fn nm of
       Just (TcIdSig (PartialSig {})) -> True
       _                              -> False
+    has_mult_anns_and_pats = any has_mult_ann_and_pat lbinds
+    has_mult_ann_and_pat (L _ (PatBind{pat_mult=MultAnn{mult_ann=HsNoMultAnn}})) = False
+    has_mult_ann_and_pat (L _ (PatBind{pat_lhs=(L _ (VarPat{}))})) = False
+    has_mult_ann_and_pat (L _ (PatBind{})) = True
+    has_mult_ann_and_pat _ = False
 
 isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
 isClosedBndrGroup type_env binds
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index c20fa8405da9a16dee501afe28a000f5ec9c4302..215f7401e71296e6840c2ddc2b3c36d109f393a1 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -348,9 +348,11 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty
 -}
 
 tcExpr (HsLet x tkLet binds tkIn expr) res_ty
-  = do  { (binds', expr') <- tcLocalBinds binds $
-                             tcMonoExpr expr res_ty
-        ; return (HsLet x tkLet binds' tkIn expr') }
+  = do  { (binds', wrapper, expr') <- tcLocalBinds binds $
+                                      tcMonoExpr expr res_ty
+          -- The wrapper checks for correct multiplicities.
+          -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
+        ; return (HsLet x tkLet binds' tkIn (mkLHsWrap wrapper expr')) }
 
 tcExpr (HsCase x scrut matches) res_ty
   = do  {  -- We used to typecheck the case alternatives first.
@@ -374,8 +376,8 @@ tcExpr (HsCase x scrut matches) res_ty
 
         ; traceTc "HsCase" (ppr scrut_ty)
         ; hasFixedRuntimeRep_syntactic FRRCase scrut_ty
-        ; matches' <- tcMatchesCase match_ctxt (Scaled mult scrut_ty) matches res_ty
-        ; return (HsCase x scrut' matches') }
+        ; (mult_co_wrap, matches') <- tcMatchesCase match_ctxt (Scaled mult scrut_ty) matches res_ty
+        ; return (HsCase x (mkLHsWrap mult_co_wrap scrut') matches') }
  where
     match_ctxt = MC { mc_what = x,
                       mc_body = tcBody }
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 7c433f556043ec122ed7a5ad84c588f26546a3ad..28be511a81c9c0b707d09c09892ec73b5cfec525 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -96,31 +96,29 @@ same number of arguments before using @tcMatches@ to do the work.
 -}
 
 tcMatchesFun :: LocatedN Name -- MatchContext Id
+             -> Mult -- The multiplicity of the binder
              -> MatchGroup GhcRn (LHsExpr GhcRn)
              -> ExpRhoType    -- Expected type of function
              -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
                                 -- Returns type of body
-tcMatchesFun fun_name matches exp_ty
+tcMatchesFun fun_name mult matches exp_ty
   = do  {  -- Check that they all have the same no of arguments
            -- Location is in the monad, set the caller so that
            -- any inter-equation error messages get some vaguely
            -- sensible location.        Note: we have to do this odd
            -- ann-grabbing, because we don't always have annotations in
            -- hand when we call tcMatchesFun...
-          traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty $$ ppr arity)
+          traceTc "tcMatchesFun" (ppr fun_name $$ ppr mult $$ ppr exp_ty $$ ppr arity)
         ; checkArgCounts what matches
 
-        ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
-             -- NB: exp_type may be polymorphic, but
-             --     matchExpectedFunTys can cope with that
-          tcScalingUsage ManyTy $
-          -- toplevel bindings and let bindings are, at the
-          -- moment, always unrestricted. The value being bound
-          -- must, accordingly, be unrestricted. Hence them
-          -- being scaled by Many. When let binders come with a
-          -- multiplicity, then @tcMatchesFun@ will have to take
-          -- a multiplicity argument, and scale accordingly.
-          tcMatches match_ctxt pat_tys rhs_ty matches }
+        ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
+               -- NB: exp_type may be polymorphic, but
+               --     matchExpectedFunTys can cope with that
+            tcScalingUsage mult $
+               -- Makes sure that if the binding is unrestricted, it counts as
+               -- consuming its rhs Many times.
+            tcMatches match_ctxt pat_tys rhs_ty matches
+        ; return (wrapper <.> mult_co_wrap, r) }
   where
     arity  = matchGroupArity matches
     herald = ExpectedFunTyMatches (NameThing (unLoc fun_name)) matches
@@ -145,7 +143,7 @@ tcMatchesCase :: (AnnoBody body, Outputable (body GhcTc)) =>
              -> Scaled TcSigmaTypeFRR -- ^ Type of scrutinee
              -> MatchGroup GhcRn (LocatedA (body GhcRn)) -- ^ The case alternatives
              -> ExpRhoType                               -- ^ Type of the whole case expression
-             -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
+             -> TcM (HsWrapper, MatchGroup GhcTc (LocatedA (body GhcTc)))
                 -- Translated alternatives
                 -- wrapper goes from MatchGroup's ty to expected ty
 
@@ -159,31 +157,38 @@ tcMatchLambda :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys
               -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
 tcMatchLambda herald match_ctxt match res_ty
   =  do { checkArgCounts (mc_what match_ctxt) match
-        ; matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty -> do
+        ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty ->
             -- checking argument counts since this is also used for \cases
-            tcMatches match_ctxt pat_tys rhs_ty match }
+            tcMatches match_ctxt pat_tys rhs_ty match
+        ; return (wrapper <.> mult_co_wrap, r) }
   where
     n_pats | isEmptyMatchGroup match = 1   -- must be lambda-case
            | otherwise               = matchGroupArity match
 
 -- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
 
-tcGRHSsPat :: GRHSs GhcRn (LHsExpr GhcRn) -> ExpRhoType
+tcGRHSsPat :: Mult -> GRHSs GhcRn (LHsExpr GhcRn) -> ExpRhoType
            -> TcM (GRHSs GhcTc (LHsExpr GhcTc))
 -- Used for pattern bindings
-tcGRHSsPat grhss res_ty
-  = tcScalingUsage ManyTy $
-      -- Like in tcMatchesFun, this scaling happens because all
-      -- let bindings are unrestricted. A difference, here, is
-      -- that when this is not the case, any more, we will have to
-      -- make sure that the pattern is strict, otherwise this will
-      -- desugar to incorrect code.
-    tcGRHSs match_ctxt grhss res_ty
+tcGRHSsPat mult grhss res_ty
+  = tcScalingUsage mult $ do
+    { (mult_co_wrapper, r) <- tcGRHSs match_ctxt grhss res_ty
+    ; return $ mkWrap mult_co_wrapper r }
   where
     match_ctxt :: TcMatchCtxt HsExpr -- AZ
     match_ctxt = MC { mc_what = PatBindRhs,
                       mc_body = tcBody }
 
+    mkWrap wrap grhss@(GRHSs { grhssGRHSs = L loc (GRHS x guards body) : rhss }) =
+      grhss { grhssGRHSs = L loc (GRHS x guards (mkLHsWrap wrap body)) : rhss }
+    mkWrap _ (GRHSs { grhssGRHSs = [] }) = panic "tcGRHSsPat: empty GHRSs"
+    mkWrap _ _ = panic "tcGRHSsPat: non-empty extensions"
+    -- Should be the following but it warns of redundant pattern and I couldn't
+    -- find a way to silence them
+    --
+    -- mkWrap _ (GRHSs { grhssGRHSs = L _ (XGRHS absent) : _ }) = dataConCantHappen absent
+    -- mkWrap _ (XGRHSs absent) = dataConCantHappen absent
+
 {- *********************************************************************
 *                                                                      *
                 tcMatch
@@ -215,7 +220,7 @@ tcMatches :: (AnnoBody body, Outputable (body GhcTc)) =>
           -> [ExpPatType]             -- ^ Expected pattern types.
           -> ExpRhoType               -- ^ Expected result-type of the Match.
           -> MatchGroup GhcRn (LocatedA (body GhcRn))
-          -> TcM (MatchGroup GhcTc (LocatedA (body GhcTc)))
+          -> TcM (HsWrapper, MatchGroup GhcTc (LocatedA (body GhcTc)))
 
 tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
                                   , mg_ext = origin })
@@ -226,20 +231,22 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
   = do { tcEmitBindingUsage bottomUE
        ; pat_tys <- mapM scaledExpTypeToType (filter_out_forall_pat_tys pat_tys)
        ; rhs_ty  <- expTypeToType rhs_ty
-       ; return (MG { mg_alts = L l []
-                    , mg_ext = MatchGroupTc pat_tys rhs_ty origin
-                    }) }
+       ; return (idHsWrapper, MG { mg_alts = L l []
+                                 , mg_ext = MatchGroupTc pat_tys rhs_ty origin
+                                 }) }
 
   | otherwise
   = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
-       ; let (usages,matches') = unzip umatches
+       ; let (usages, wmatches) = unzip umatches
+       ; let (wrappers, matches') = unzip wmatches
+       ; let wrapper = mconcat wrappers
        ; tcEmitBindingUsage $ supUEs usages
        ; pat_tys  <- mapM readScaledExpType (filter_out_forall_pat_tys pat_tys)
        ; rhs_ty   <- readExpType rhs_ty
        ; traceTc "tcMatches" (ppr matches' $$ ppr pat_tys $$ ppr rhs_ty)
-       ; return (MG { mg_alts   = L l matches'
-                    , mg_ext    = MatchGroupTc pat_tys rhs_ty origin
-                    }) }
+       ; return (wrapper, MG { mg_alts   = L l matches'
+                             , mg_ext    = MatchGroupTc pat_tys rhs_ty origin
+                             }) }
   where
     -- We filter out foralls because we have no use for them in HsToCore.
     filter_out_forall_pat_tys :: [ExpPatType] -> [Scaled ExpSigmaTypeFRR]
@@ -253,20 +260,21 @@ tcMatch :: (AnnoBody body) => TcMatchCtxt body
         -> [ExpPatType]          -- Expected pattern types
         -> ExpRhoType            -- Expected result-type of the Match.
         -> LMatch GhcRn (LocatedA (body GhcRn))
-        -> TcM (LMatch GhcTc (LocatedA (body GhcTc)))
+        -> TcM (HsWrapper, LMatch GhcTc (LocatedA (body GhcTc)))
 
 tcMatch ctxt pat_tys rhs_ty match
-  = wrapLocMA (tc_match ctxt pat_tys rhs_ty) match
+  = do { (L loc (wrapper, r)) <- wrapLocMA (tc_match ctxt pat_tys rhs_ty) match
+       ; return (wrapper, L loc r) }
   where
     tc_match ctxt pat_tys rhs_ty
              match@(Match { m_pats = pats, m_grhss = grhss })
       = add_match_ctxt match $
-        do { (pats', grhss') <- tcPats (mc_what ctxt) pats pat_tys $
+        do { (pats', (wrapper, grhss')) <- tcPats (mc_what ctxt) pats pat_tys $
                                 tcGRHSs ctxt grhss rhs_ty
-           ; return (Match { m_ext = noAnn
-                           , m_ctxt = mc_what ctxt
-                           , m_pats = filter_out_type_pats pats'
-                           , m_grhss = grhss' }) }
+           ; return (wrapper, Match { m_ext = noAnn
+                                    , m_ctxt = mc_what ctxt
+                                    , m_pats = filter_out_type_pats pats'
+                                    , m_grhss = grhss' }) }
 
         -- For (\x -> e), tcExpr has already said "In the expression \x->e"
         --     so we don't want to add "In the lambda abstraction \x->e"
@@ -288,7 +296,7 @@ tcMatch ctxt pat_tys rhs_ty match
 -------------
 tcGRHSs :: AnnoBody body
         => TcMatchCtxt body -> GRHSs GhcRn (LocatedA (body GhcRn)) -> ExpRhoType
-        -> TcM (GRHSs GhcTc (LocatedA (body GhcTc)))
+        -> TcM (HsWrapper, GRHSs GhcTc (LocatedA (body GhcTc)))
 
 -- Notice that we pass in the full res_ty, so that we get
 -- good inference from simple things like
@@ -297,12 +305,13 @@ tcGRHSs :: AnnoBody body
 -- but we don't need to do that any more
 
 tcGRHSs ctxt (GRHSs _ grhss binds) res_ty
-  = do  { (binds', ugrhss)
-            <- tcLocalBinds binds $
-               mapM (tcCollectingUsage . wrapLocMA (tcGRHS ctxt res_ty)) grhss
-        ; let (usages, grhss') = unzip ugrhss
-        ; tcEmitBindingUsage $ supUEs usages
-        ; return (GRHSs emptyComments grhss' binds') }
+  = do  { (binds', wrapper, grhss')
+            <- tcLocalBinds binds $ do
+               { ugrhss <- mapM (tcCollectingUsage . wrapLocMA (tcGRHS ctxt res_ty)) grhss
+               ; let (usages, grhss') = unzip ugrhss
+               ; tcEmitBindingUsage $ supUEs usages
+               ; return grhss' }
+        ; return (wrapper, GRHSs emptyComments grhss' binds') }
 
 -------------
 tcGRHS :: TcMatchCtxt body -> ExpRhoType -> GRHS GhcRn (LocatedA (body GhcRn))
@@ -403,7 +412,7 @@ tcStmtsAndThen _ _ [] res_ty thing_inside
 -- LetStmts are handled uniformly, regardless of context
 tcStmtsAndThen ctxt stmt_chk (L loc (LetStmt x binds) : stmts)
                                                              res_ty thing_inside
-  = do  { (binds', (stmts',thing)) <- tcLocalBinds binds $
+  = do  { (binds', _, (stmts',thing)) <- tcLocalBinds binds $
               tcStmtsAndThen ctxt stmt_chk stmts res_ty thing_inside
         ; return (L loc (LetStmt x binds') : stmts', thing) }
 
diff --git a/compiler/GHC/Tc/Gen/Match.hs-boot b/compiler/GHC/Tc/Gen/Match.hs-boot
index 80790f2f9c1a78e271b387802475b131ee993296..c6f91bfdca8d2b2f2b530eda0df86ead354a7d58 100644
--- a/compiler/GHC/Tc/Gen/Match.hs-boot
+++ b/compiler/GHC/Tc/Gen/Match.hs-boot
@@ -1,5 +1,5 @@
 module GHC.Tc.Gen.Match where
-import GHC.Hs           ( GRHSs, MatchGroup, LHsExpr )
+import GHC.Hs           ( GRHSs, MatchGroup, LHsExpr, Mult )
 import GHC.Tc.Types.Evidence  ( HsWrapper )
 import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType )
 import GHC.Tc.Types     ( TcM )
@@ -7,11 +7,13 @@ import GHC.Hs.Extension ( GhcRn, GhcTc )
 import GHC.Parser.Annotation ( LocatedN )
 import GHC.Types.Name (Name)
 
-tcGRHSsPat    :: GRHSs GhcRn (LHsExpr GhcRn)
+tcGRHSsPat    :: Mult
+              -> GRHSs GhcRn (LHsExpr GhcRn)
               -> ExpRhoType
               -> TcM (GRHSs GhcTc (LHsExpr GhcTc))
 
 tcMatchesFun :: LocatedN Name
+             -> Mult
              -> MatchGroup GhcRn (LHsExpr GhcRn)
              -> ExpSigmaType
              -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 037db0fa3a334b997e77dd9b935311c024ecc97a..bb1a6ab6d3ff6aa7e958e2171e80945eddd3512e 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -97,8 +97,28 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
              penv = PE { pe_lazy = True
                        , pe_ctxt = ctxt
                        , pe_orig = PatOrigin }
-
-       ; tc_lpat pat_ty penv pat thing_inside }
+       ; dflags <- getDynFlags
+       ; mult_co_wrap <- manyIfLazy dflags pat
+       -- The wrapper checks for correct multiplicities.
+       -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
+       ; (pat', r) <- tc_lpat pat_ty penv pat thing_inside
+       ; pat_ty' <- readExpType (scaledThing pat_ty)
+       ; return (mkLHsWrapPat mult_co_wrap pat' pat_ty', r) }
+  where
+    -- The logic is partly duplicated from decideBangHood in
+    -- GHC.HsToCore.Utils. Ugh…
+    manyIfLazy dflags lpat
+      | xopt LangExt.Strict dflags = xstrict lpat
+      | otherwise = not_xstrict lpat
+      where
+        xstrict (L _ (LazyPat _ _)) = checkManyPattern pat_ty
+        xstrict (L _ (ParPat _ _ p _)) = xstrict p
+        xstrict _ = return WpHole
+
+        not_xstrict (L _ (BangPat _ _)) = return WpHole
+        not_xstrict (L _ (VarPat _ _)) = return WpHole
+        not_xstrict (L _ (ParPat _ _ p _)) = not_xstrict p
+        not_xstrict _ = checkManyPattern pat_ty
 
 -----------------
 tcPats :: HsMatchContext GhcTc
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index b41c1ff215e066295b9e5cdd46b97682c17aebde..1227991fac121d10eae86588c3e72709cfd5119d 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -2061,7 +2061,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind
                                           , sig_loc  = getLocA hs_sig_ty }
 
 
-       ; (tc_bind, [inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
+       ; (tc_bind, [Scaled _ inner_id]) <- tcPolyCheck no_prag_fn inner_meth_sig meth_bind
 
        ; let export = ABE { abe_poly  = local_meth_id
                           , abe_mono  = inner_id
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index 4dd971db4ea6d99e5eb5a84cee90def28e85410a..555ae12861c8678f4f72d6ad9cac34a4be1324b4 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -843,10 +843,10 @@ when typechecking the [d| .. |] quote, and typecheck them later.
 tcRecSelBinds :: [(Id, LHsBind GhcRn)] -> TcM TcGblEnv
 tcRecSelBinds sel_bind_prs
   = tcExtendGlobalValEnv [sel_id | (L _ (XSig (IdSig sel_id))) <- sigs] $
-    do { (rec_sel_binds, tcg_env) <- discardWarnings $
-                                     -- See Note [Impredicative record selectors]
-                                     setXOptM LangExt.ImpredicativeTypes $
-                                     tcValBinds TopLevel binds sigs getGblEnv
+    do { (rec_sel_binds, _, tcg_env) <- discardWarnings $
+                                       -- See Note [Impredicative record selectors]
+                                       setXOptM LangExt.ImpredicativeTypes $
+                                       tcValBinds TopLevel binds sigs getGblEnv
        ; return (tcg_env `addTypecheckedBinds` map snd rec_sel_binds) }
   where
     sigs = [ L (noAnnSrcSpan loc) (XSig $ IdSig sel_id)
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index b2c1003a9b0c28b70c6e72fc9c8ff9d1d7459c81..e50af8cca5e4cfa29c5bda05384b8d8f0feb7069 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -1,6 +1,7 @@
 -- (c) The University of Glasgow 2006
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TupleSections #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}  -- instance MonadThings is necessarily an
                                        -- orphan
 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]
@@ -70,6 +71,7 @@ module GHC.Tc.Utils.Env(
 
 import GHC.Prelude
 
+
 import GHC.Driver.Env
 import GHC.Driver.Env.KnotVars
 import GHC.Driver.DynFlags
@@ -87,13 +89,16 @@ import GHC.Iface.Load
 import GHC.Tc.Errors.Types
 import GHC.Tc.Utils.Monad
 import GHC.Tc.Utils.TcType
+import {-# SOURCE #-} GHC.Tc.Utils.TcMType ( tcCheckUsage )
 import GHC.Tc.Types.LclEnv
+import GHC.Tc.Types.Evidence (HsWrapper, idHsWrapper, (<.>))
 
 import GHC.Core.InstEnv
 import GHC.Core.DataCon ( DataCon, dataConTyCon, flSelector )
 import GHC.Core.PatSyn  ( PatSyn )
 import GHC.Core.ConLike
 import GHC.Core.TyCon
+import GHC.Core.TyCo.Rep
 import GHC.Core.Type
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Class
@@ -574,17 +579,17 @@ tcExtendSigIds top_lvl sig_ids thing_inside
 
 
 tcExtendLetEnv :: TopLevelFlag -> TcSigFun -> IsGroupClosed
-                  -> [TcId] -> TcM a -> TcM a
+                  -> [Scaled TcId] -> TcM a -> TcM (a, HsWrapper)
 -- Used for both top-level value bindings and nested let/where-bindings
 -- Adds to the TcBinderStack too
 tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
                ids thing_inside
-  = tcExtendBinderStack [TcIdBndr id top_lvl | id <- ids] $
+  = tcExtendBinderStack [TcIdBndr id top_lvl | Scaled _ id <- ids] $
     tc_extend_local_env top_lvl
           [ (idName id, ATcId { tct_id   = id
                               , tct_info = mk_tct_info id })
-          | id <- ids ]
-    thing_inside
+          | Scaled _ id <- ids ] $
+    foldr check_usage ((, idHsWrapper) <$> thing_inside) scaled_names
   where
     mk_tct_info id
       | type_closed && isEmptyNameSet rhs_fvs = ClosedLet
@@ -594,6 +599,11 @@ tcExtendLetEnv top_lvl sig_fn (IsGroupClosed fvs fv_type_closed)
         rhs_fvs     = lookupNameEnv fvs name `orElse` emptyNameSet
         type_closed = isTypeClosedLetBndr id &&
                       (fv_type_closed || hasCompleteSig sig_fn name)
+    scaled_names = [Scaled p (idName id) | Scaled p id <- ids ]
+    check_usage :: Scaled Name -> TcM (a, HsWrapper) -> TcM (a, HsWrapper)
+    check_usage (Scaled p id) thing_inside = do
+      ((res, inner_wrap), outer_wrap) <- tcCheckUsage id p thing_inside
+      return $ (res, outer_wrap <.> inner_wrap)
 
 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
 -- For lambda-bound and case-bound Ids
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs-boot b/compiler/GHC/Tc/Utils/TcMType.hs-boot
new file mode 100644
index 0000000000000000000000000000000000000000..62fbb9330d091c4292bdac9eeb110a6bc60d1b47
--- /dev/null
+++ b/compiler/GHC/Tc/Utils/TcMType.hs-boot
@@ -0,0 +1,8 @@
+module GHC.Tc.Utils.TcMType where
+
+import GHC.Tc.Types
+import GHC.Types.Name
+import GHC.Core.TyCo.Rep
+import GHC.Tc.Types.Evidence
+
+tcCheckUsage :: Name -> Mult -> TcM a -> TcM (a, HsWrapper)
diff --git a/compiler/GHC/Tc/Zonk/Type.hs b/compiler/GHC/Tc/Zonk/Type.hs
index 74bda6e147883b6edb4bdf9e3d6c05c23ad98f94..f9b4da15e4f1ef4a1517a4f872dc140f1e0867c9 100644
--- a/compiler/GHC/Tc/Zonk/Type.hs
+++ b/compiler/GHC/Tc/Zonk/Type.hs
@@ -718,11 +718,14 @@ zonk_lbind = wrapLocZonkMA zonk_bind
 
 zonk_bind :: HsBind GhcTc -> ZonkTcM (HsBind GhcTc)
 zonk_bind bind@(PatBind { pat_lhs = pat, pat_rhs = grhss
+                        , pat_mult = mult_ann
                         , pat_ext = (ty, ticks)})
   = do  { new_pat   <- don'tBind $ zonkPat pat            -- Env already extended
         ; new_grhss <- zonkGRHSs zonkLExpr grhss
         ; new_ty    <- zonkTcTypeToTypeX ty
+        ; new_mult  <- onMultExt zonkTcTypeToTypeX mult_ann
         ; return (bind { pat_lhs = new_pat, pat_rhs = new_grhss
+                       , pat_mult = new_mult
                        , pat_ext = (new_ty, ticks) }) }
 
 zonk_bind (VarBind { var_ext = x
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 4c9f1cd793f0b33e98fd3b47498cafac0241adf9..5ae01c473b8feb440ab03d415cd61727eacf8548 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -224,6 +224,7 @@ cvtDec (TH.ValD pat body ds)
           PatBind { pat_lhs = pat'
                   , pat_rhs = GRHSs emptyComments body' ds'
                   , pat_ext = noAnn
+                  , pat_mult = MultAnn{mult_ext=NoExtField, mult_ann=HsNoMultAnn}
                   } }
 
 cvtDec (TH.FunD nm cls)
diff --git a/compiler/Language/Haskell/Syntax/Binds.hs b/compiler/Language/Haskell/Syntax/Binds.hs
index 7ac866cfb288874ea45b7cdaa68b1849127b8ed4..094ed1214f3b021824495f487eea35701f87f234 100644
--- a/compiler/Language/Haskell/Syntax/Binds.hs
+++ b/compiler/Language/Haskell/Syntax/Binds.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -28,6 +29,7 @@ import {-# SOURCE #-} Language.Haskell.Syntax.Expr
 import {-# SOURCE #-} Language.Haskell.Syntax.Pat
   ( LPat )
 
+import Language.Haskell.Syntax.Concrete
 import Language.Haskell.Syntax.Extension
 import Language.Haskell.Syntax.Type
 
@@ -41,6 +43,7 @@ import GHC.Types.SourceText (StringLiteral)
 import Data.Void
 import Data.Bool
 import Data.Maybe
+import Data.Functor
 
 {-
 ************************************************************************
@@ -162,6 +165,23 @@ other interesting cases. Namely,
     Just x = e
     (x) = e
     x :: Ty = e
+
+Note [Multiplicity annotations]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Multiplicity annotation are stored in the pat_mult field on PatBinds. The type
+of the pat_mult field is given by the type family MultAnn: it changes depending
+on the phase. Before typechecking, MultAnn is Maybe (HsMultAnn) where Nothing
+means that there was no annotation in the original file. After typechecking
+MultAnn is Mult: the typechecker infers a multiplicity when there is no
+annotation.
+
+We don't need to store a multiplicity on FunBinds:
+- let %1 x = … is parsed as a PatBind. So we don't need an annotation before
+  typechecking.
+- the multiplicity that the typechecker infers is stored in the binder's Var for
+  the desugarer to use. It's only relevant for strict FunBinds, see Wrinkle 1 in
+  Note [Desugar Strict binds] in GHC.HsToCore.Binds as, in Core, let expressions
+  don't have multiplicity annotations.
 -}
 
 -- | Haskell Binding with separate Left and Right id's
@@ -219,6 +239,8 @@ data HsBindLR idL idR
   | PatBind {
         pat_ext    :: XPatBind idL idR,
         pat_lhs    :: LPat idL,
+        pat_mult   :: MultAnn idL,
+        -- ^ See Note [Multiplicity annotations].
         pat_rhs    :: GRHSs idR (LHsExpr idR)
     }
 
@@ -264,6 +286,25 @@ data PatSynBind idL idR
    | XPatSynBind !(XXPatSynBind idL idR)
 
 
+-- | Multiplicity annotations, on binders, are always resolved (to a unification
+-- variable if there is no annotation) during type-checking. The resolved
+-- multiplicity is stored in the `mult_ext` field.
+type family XMultAnn pass
+
+data MultAnn pass
+  = MultAnn { mult_ext :: XMultAnn pass, mult_ann :: HsMultAnn (NoGhcTc pass)}
+
+-- | Multiplicity annotations at parse time. In particular `%1` is
+-- special-cased.
+data HsMultAnn pass
+  = HsNoMultAnn
+  | HsPct1Ann !(LHsToken "%1" pass)
+  | HsMultAnn !(LHsToken "%" pass) (LHsType pass)
+
+onMultExt :: Functor f => (XMultAnn pass -> f (XMultAnn pass)) -> MultAnn pass -> f (MultAnn pass)
+onMultExt f (MultAnn{mult_ext=x, mult_ann=ann}) =
+  f x <&> (\y -> MultAnn{mult_ext = y, mult_ann = ann})
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/docs/users_guide/9.10.1-notes.rst b/docs/users_guide/9.10.1-notes.rst
index fc50645c4366941382c45534440b08fb1056e3de..1a68d6191de7d6d9cbba858761946ae90b218a59 100644
--- a/docs/users_guide/9.10.1-notes.rst
+++ b/docs/users_guide/9.10.1-notes.rst
@@ -17,6 +17,17 @@ Language
     x = idv (type Int) 42
 
   This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
+- With :extension:`LinearTypes`, ``let`` and ``where`` bindings can
+  now be linear. So the following now typechecks::
+
+    f :: A %1 -> B
+    g :: B %1 -> C
+
+    h :: A %1 -> C
+    h x = g y
+      where
+        y = f x
+
 
 - Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
   of promoted data types in kinds, even when :extension:`DataKinds` was not
diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst
index e08a52e4d19848a4ca4a00c8d26011350a44e9eb..8f9d51bcf6f74ab842079aae032a4d5510110892 100644
--- a/docs/users_guide/exts/linear_types.rst
+++ b/docs/users_guide/exts/linear_types.rst
@@ -5,6 +5,9 @@ Linear types
 
 .. extension:: LinearTypes
     :shortdesc: Enable linear types.
+        Implies :extension:`MonoLocalBinds`.
+
+    :implies: :extension:`MonoLocalBinds`
 
     :since: 9.0.1
     :status: Experimental
@@ -63,6 +66,83 @@ signature to a function, it will be inferred as being a regular
 function of type ``a -> b``. The same principle holds for
 representation polymorphism (see :ref:`representation-polymorphism-defaulting`).
 
+Expressions
+-----------
+
+When defining a function either as a lambda ``\x -> u`` or with
+equations ``f x = u``, the multiplicity of the variable ``x`` will be
+inferred from the context. For equations, the context will typically
+be a type signature. For instance here is a linear function
+
+::
+
+    f :: (a -> b) %1 -> a -> b
+    f g x = g x
+
+In this example, ``g`` must be used linearly while ``x`` is
+unrestricted.
+
+Bindings
+~~~~~~~~
+
+Let and where bindings can be linear as well, the multiplicity of
+bindings is typically inferred
+
+::
+
+    f :: A %1 -> B
+    g :: B %1 -> C
+
+    h :: A %1 -> C
+    h x = g y
+      where
+        y = f x
+
+If you don't want, or aren't able, to rely on inference, let and where
+bindings can be annotated with a multiplicity
+
+::
+
+    f :: A %1 -> B
+    g :: B %1 -> C
+
+    h :: A %1 -> C
+    h x = g y
+      where
+        %1 y = f x
+
+The precise rules are, that you can annotate a binding with a
+multiplicity if:
+
+- The binding is not top-level
+- The binding is non-recursive
+- The binding is a pattern binding (including a simple variable)
+  ``p=e`` (you can't write ``let %1 f x = u``, instead write ``let %1
+  f = \x -> u``)
+- Either ``p`` is of the form ``!p'`` or ``p`` is a variable. In
+  particular neither ``x@y`` nor ``(x)`` are covered by “is a
+  variable”
+
+When there's no multiplicity annotation, the multiplicity is inferred
+as follows:
+
+- Toplevel bindings are inferred as having multiplicity ``Many``
+- Recursive bindings are inferred as having multiplicity ``Many``
+- Lazy non-variable pattern bindings are inferred as having
+  multiplicity ``Many`` (note that in let- and where-bindings,
+  patterns are lazy by default, so that ``let (x,y) = rhs`` always
+  have multiplicity ``Many``, whereas ``let !(x,y) = rhs`` can have
+  multiplicity ``1``).
+- In all other cases, including function bindings ``let f x1...xn = rhs``,
+  the multiplicity is inferred from the term.
+
+When ``-XMonoLocalBinds`` is on, the following also holds:
+
+- Multiplicity-annotated non-variable pattern-bindings (such as
+  ``let %1 !(x,y) = rhs``) are never generalised.
+- Non-variable pattern bindings which are inferred as polymorphic or
+  qualified are inferred as having multiplicity ``Many``.
+
 Data types
 ----------
 By default, all fields in algebraic data types are linear (even if
@@ -157,36 +237,12 @@ missing pieces.
 - Multiplicity polymorphism is incomplete and experimental. You may
   have success using it, or you may not. Expect it to be really unreliable.
   (Multiplicity multiplication is not supported yet.)
-- There is currently no support for multiplicity annotations such as
-  ``x :: a %p``, ``\(x :: a %p) -> ...``.
+- There is currently no support for multiplicity annotations on
+  function arguments such as ``\(%p x :: a) -> ...``, only on
+  let-bound variables.
 - A ``case`` expression may consume its scrutinee ``One`` time,
   or ``Many`` times. But the inference is still experimental, and may
   over-eagerly guess that it ought to consume the scrutinee ``Many`` times.
-- All ``let`` and ``where`` statements consume their right hand side
-  ``Many`` times. That is, the following will not type check:
-
-  ::
-
-      g :: A %1 -> (A, B)
-      h :: A %1 -> B %1 -> C
-
-      f :: A %1 -> C
-      f x =
-        let (y, z) = g x in h y z
-
-  This can be worked around by defining extra functions which are
-  specified to be linear, such as:
-
-  ::
-
-      g :: A %1 -> (A, B)
-      h :: A %1 -> B %1 -> C
-
-      f :: A %1 -> C
-      f x = f' (g x)
-        where
-          f' :: (A, B) %1 -> C
-          f' (y, z) = h y z
 - There is no support for linear pattern synonyms.
 - ``@``-patterns and view patterns are not linear.
 - The projection function for a record with a single linear field should be
diff --git a/testsuite/tests/linear/should_compile/LinearLet.hs b/testsuite/tests/linear/should_compile/LinearLet.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2cc310725af7be80acd286d0bc0a8edd9e43aa67
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearLet.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearLet where
+
+import GHC.Types
+
+f :: a -> a
+f x = let %1 y = x in y
+
+f' :: a %1 -> a
+f' x = let %1 y = x in y
+
+f'' :: a %1 -> a
+f'' x = let y = x in y
+
+g :: a -> (a, a, a)
+g x = let %'Many y = x in (x, x, x)
+
+h :: a %1 -> a
+h x = y
+  where %1 y = x
+
+h' :: a %1 -> a
+h' x = y
+  where y = x
+
+i :: Maybe a %1 -> a
+i x = let %1 !(Just y) = x in y
+
+j :: (a, b) %1 -> (b, a)
+j x = let !(y, z) = x in (z, y)
+
+-- The non-variable pattern let binding cannot be linear because it's inferred as
+-- polymorphic. See Note [Non-variable pattern bindings aren't linear] in GHC.Tc.Gen.Bind
+--
+-- The local let binding is inferred as polymorphic despite MonoLocalBinds
+-- because it is closed. This behaviour is not very problematic (this will never
+-- need to be linear), but can be a little surprising.
+k :: a -> (a, Bool)
+k x = let !(f, b) = ((\y -> y), b) in (f x, b)
+
+-- let !y = (without a multiplicity annotation) uses the same code path as let y =
+-- (FunBind) not that of pattern bindings (PatBind). The desugaring of a strict
+-- pattern involves `seq`, with which we need to be careful when dealing with
+-- linear types.
+l :: a %1 -> a
+l x = let !y = x in y
diff --git a/testsuite/tests/linear/should_compile/LinearLetPoly.hs b/testsuite/tests/linear/should_compile/LinearLetPoly.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d0d967bfc73ec52e354ec3e14ed775c35d51d3e7
--- /dev/null
+++ b/testsuite/tests/linear/should_compile/LinearLetPoly.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE NoMonoLocalBinds #-}
+
+module LinearLet where
+
+-- Tests behaviour of linear lets in presence of -XNoMonoLocalBinds. These are a
+-- little bit of a corner case, as it's recommended to use -XMonoLocalBinds with
+-- -XLinearTypes (indeed LinearTypes implies MonoLocalBinds).
+
+-- Because the multiplicity annotation on the let, `y` is given a monomorphic
+-- type. Otherwise it would run afoul of Note [Non-variable pattern bindings aren't linear] in GHC.Tc.Gen.Bind
+f :: Maybe a %1 -> a
+f x = let %1 !(Just y) = x in y
+
+-- Variable pattern bindings can be generalised.
+g :: Bool -> Int
+g b =
+  case b of
+  True -> f 0
+  False -> f (\x -> x) 1
+  where
+    %1 f = (\x -> x)
diff --git a/testsuite/tests/linear/should_compile/all.T b/testsuite/tests/linear/should_compile/all.T
index 39d0f82d5f8b9f66833736c65c265bfb4091d2b4..3c7ef5dcbb709be90249568864503d68492f956e 100644
--- a/testsuite/tests/linear/should_compile/all.T
+++ b/testsuite/tests/linear/should_compile/all.T
@@ -43,3 +43,5 @@ test('T22546', normal, compile, [''])
 test('T23025', normal, compile, ['-dlinear-core-lint'])
 test('LinearRecUpd', normal, compile, [''])
 test('T23814', normal, compile, [''])
+test('LinearLet', normal, compile, [''])
+test('LinearLetPoly', normal, compile, [''])
diff --git a/testsuite/tests/linear/should_fail/LinearLet.hs b/testsuite/tests/linear/should_fail/LinearLet1.hs
similarity index 100%
rename from testsuite/tests/linear/should_fail/LinearLet.hs
rename to testsuite/tests/linear/should_fail/LinearLet1.hs
diff --git a/testsuite/tests/linear/should_fail/LinearLet.stderr b/testsuite/tests/linear/should_fail/LinearLet1.stderr
similarity index 81%
rename from testsuite/tests/linear/should_fail/LinearLet.stderr
rename to testsuite/tests/linear/should_fail/LinearLet1.stderr
index 5ee468376b7abbded6d58bc0ee9c08543f32c697..61136962b0263ebfa2b5ab3bbddce8aaad325bc4 100644
--- a/testsuite/tests/linear/should_fail/LinearLet.stderr
+++ b/testsuite/tests/linear/should_fail/LinearLet1.stderr
@@ -1,5 +1,5 @@
 
-LinearLet.hs:5:3: error: [GHC-18872]
+LinearLet1.hs:5:3: error: [GHC-18872]
     • Couldn't match type ‘Many’ with ‘One’
         arising from multiplicity of ‘x’
     • In an equation for ‘f’: f x = let y = x in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet10.hs b/testsuite/tests/linear/should_fail/LinearLet10.hs
new file mode 100644
index 0000000000000000000000000000000000000000..74874c454af57e6d7518f18c1b2837983958da6f
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet10.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+
+module LinearLet10 where
+
+-- Test for well-kindedness of multiplicity annotations
+f :: a -> a
+f x = let %Int y = x in y
diff --git a/testsuite/tests/linear/should_fail/LinearLet10.stderr b/testsuite/tests/linear/should_fail/LinearLet10.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..34294f2e440aa7b20659a21b41f84bf26099bac5
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet10.stderr
@@ -0,0 +1,6 @@
+
+LinearLet10.hs:7:12: error: [GHC-83865]
+    • Expected kind ‘GHC.Types.Multiplicity’, but ‘Int’ has kind ‘*’
+    • In the type ‘Int’
+      In a pattern binding: y = x
+      In the expression: let %Int y = x in y
diff --git a/testsuite/tests/linear/should_fail/LinearLet2.hs b/testsuite/tests/linear/should_fail/LinearLet2.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4570b095f1b0ce53fd77391e094b7b5a4d106137
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet2.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet2 where
+
+f :: a -> (a, a)
+f x = let %1 y = x in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet2.stderr b/testsuite/tests/linear/should_fail/LinearLet2.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..d442c84c26d5d605cda761e9b208e73807cee239
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet2.stderr
@@ -0,0 +1,6 @@
+
+LinearLet2.hs:5:7: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘y’
+    • In the expression: let %1 y = x in (y, y)
+      In an equation for ‘f’: f x = let %1 y = x in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet3.hs b/testsuite/tests/linear/should_fail/LinearLet3.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1dd90980b6288ea1906c8b7cd7a98fc9f7a9afa6
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet3.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet3 where
+
+f :: a -> (a, a)
+f x = let %1 y = x ; %1 z = y in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet3.stderr b/testsuite/tests/linear/should_fail/LinearLet3.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..e4e43dfc773dc3837b59fd8b59218c50b108de76
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet3.stderr
@@ -0,0 +1,15 @@
+
+LinearLet3.hs:5:7: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘z’
+    • In the expression:
+        let
+          %1 y = x
+          %1 z = y
+        in (y, y)
+      In an equation for ‘f’:
+          f x
+            = let
+                %1 y = x
+                %1 z = y
+              in (y, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet4.hs b/testsuite/tests/linear/should_fail/LinearLet4.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d91c662bf18a2da9e85c50fcea398b991d4c5e9d
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet4.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet4 where
+
+import GHC.Types
+
+f :: a -> (a, a)
+f x = let %1 y = x ; %'Many z = y in (z, z)
diff --git a/testsuite/tests/linear/should_fail/LinearLet4.stderr b/testsuite/tests/linear/should_fail/LinearLet4.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..9ba84fa3516de01bc78eb07e41a1a08db720e70f
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet4.stderr
@@ -0,0 +1,15 @@
+
+LinearLet4.hs:7:7: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘y’
+    • In the expression:
+        let
+          %1 y = x
+          %'Many z = y
+        in (z, z)
+      In an equation for ‘f’:
+          f x
+            = let
+                %1 y = x
+                %'Many z = y
+              in (z, z)
diff --git a/testsuite/tests/linear/should_fail/LinearLet5.hs b/testsuite/tests/linear/should_fail/LinearLet5.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8474831e3b43ab4598c8f6f87b602b0196ec235f
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet5.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet5 where
+
+f :: a -> (a, a)
+f x = let %1 y = x ; %1 z = y in (z, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet5.stderr b/testsuite/tests/linear/should_fail/LinearLet5.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..662a33e350e9d39ef1666dfd9b73d6ec3cdd2588
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet5.stderr
@@ -0,0 +1,15 @@
+
+LinearLet5.hs:5:7: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘y’
+    • In the expression:
+        let
+          %1 y = x
+          %1 z = y
+        in (z, y)
+      In an equation for ‘f’:
+          f x
+            = let
+                %1 y = x
+                %1 z = y
+              in (z, y)
diff --git a/testsuite/tests/linear/should_fail/LinearLet6.hs b/testsuite/tests/linear/should_fail/LinearLet6.hs
new file mode 100644
index 0000000000000000000000000000000000000000..37ee2afa5a1ac7c068882f3a998b95f93d340de3
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet6.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet6 where
+
+-- Should fail because the pattern is lazy and there is no clear interpretation
+-- of linear lazy patterns.
+f :: Maybe a %1 -> a
+f x = let (Just y) = x in y
+
+g :: Maybe a %1 -> a
+g x = y
+  where
+    (Just y) = x
+
+h :: Maybe a %1 -> a
+h x = let %1 (Just y) = x in y
diff --git a/testsuite/tests/linear/should_fail/LinearLet6.stderr b/testsuite/tests/linear/should_fail/LinearLet6.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..545b61162c0320e6c611fb0fe604dca62d2fad97
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet6.stderr
@@ -0,0 +1,21 @@
+
+LinearLet6.hs:7:3: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘f’: f x = let (Just y) = x in y
+
+LinearLet6.hs:10:3: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘g’:
+          g x
+            = y
+            where
+                (Just y) = x
+
+LinearLet6.hs:15:14: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from a non-linear pattern
+    • In a pattern binding: (Just y) = x
+      In the expression: let %1 (Just y) = x in y
+      In an equation for ‘h’: h x = let %1 (Just y) = x in y
diff --git a/testsuite/tests/linear/should_fail/LinearLet7.hs b/testsuite/tests/linear/should_fail/LinearLet7.hs
new file mode 100644
index 0000000000000000000000000000000000000000..05e497a5d85f466f983656ae8284e34b743b730a
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet7.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet7 where
+
+-- Should fail because recursive lets should never be linear
+f :: a -> a
+f x = let %1 g = \y -> g y in g x
diff --git a/testsuite/tests/linear/should_fail/LinearLet7.stderr b/testsuite/tests/linear/should_fail/LinearLet7.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..260ca28b7abbd8a82a139a41a4df12a21bbbc216
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet7.stderr
@@ -0,0 +1,13 @@
+
+LinearLet7.hs:6:14: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘g’
+    • In a pattern binding: g = \ y -> g y
+      In the expression: let %1 g = \ y -> ... in g x
+      In an equation for ‘f’: f x = let %1 g = ... in g x
+
+LinearLet7.hs:6:14: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from a non-linear pattern
+    • In the expression: let %1 g = \ y -> ... in g x
+      In an equation for ‘f’: f x = let %1 g = ... in g x
diff --git a/testsuite/tests/linear/should_fail/LinearLet8.hs b/testsuite/tests/linear/should_fail/LinearLet8.hs
new file mode 100644
index 0000000000000000000000000000000000000000..67e561b703e190c2875b5475dbe6404c94e08e79
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet8.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE LinearTypes #-}
+module LinearLet8 where
+
+-- Unbound multiplicity annotation
+f :: a %1 -> a
+f x = let %p y = x in y
diff --git a/testsuite/tests/linear/should_fail/LinearLet8.stderr b/testsuite/tests/linear/should_fail/LinearLet8.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..7a60b992400a255a4350c7e9f8fc3f30e479767b
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet8.stderr
@@ -0,0 +1,3 @@
+
+LinearLet8.hs:6:12: error: [GHC-76037]
+    Not in scope: type variable ‘p’
diff --git a/testsuite/tests/linear/should_fail/LinearLet9.hs b/testsuite/tests/linear/should_fail/LinearLet9.hs
new file mode 100644
index 0000000000000000000000000000000000000000..6618106c07214d6c04afd21158ce63418b8706aa
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet9.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE NoMonoLocalBinds #-}
+
+module LinearLet where
+
+import GHC.Types
+
+-- See Note [Non-variable pattern bindings aren't linear] in GHC.Tc.Gen.Bind
+
+-- In k, the type-checker, assigns a polymorphic type to `f`. This doesn't
+-- admit a linear desugaring.
+k :: a -> (a, Bool)
+k x = let %1 !(f, b) = ((\y -> y), b) in (f x, b)
+
+-- i could, in principled, be desugared linearly. Because it doesn't, in fact,
+-- have polymorphic variables. But it's still inferred as an AbsBinds. It looks
+-- difficult to avoid, but equally difficult to specify.
+i :: (a, b) %1 -> (b, a)
+i x = let !(y, z) = x in (z, y)
+
+
+-- f is given a monomorphic type because of the multiplicity annotation. Because
+-- the multiplicity annotation is %Many, f could be inferred to have a
+-- polymorphic type: it wouldn't endanger type safety. If this behaviour
+-- changes, the documentation should change to reflect the new behaviour.
+j :: (Int, Bool)
+j = let %Many !(Just f) = Just (\x -> x) in (f (0::Int), f True)
diff --git a/testsuite/tests/linear/should_fail/LinearLet9.stderr b/testsuite/tests/linear/should_fail/LinearLet9.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..231cbb73656ccb74d0beab1370b096a21bf69061
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearLet9.stderr
@@ -0,0 +1,32 @@
+
+LinearLet9.hs:14:16: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘f’
+    • In the pattern: (f, b)
+      In the pattern: !(f, b)
+      In a pattern binding: !(f, b) = ((\ y -> y), b)
+
+LinearLet9.hs:14:19: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘b’
+    • In the pattern: (f, b)
+      In the pattern: !(f, b)
+      In a pattern binding: !(f, b) = ((\ y -> y), b)
+
+LinearLet9.hs:20:3: error: [GHC-18872]
+    • Couldn't match type ‘Many’ with ‘One’
+        arising from multiplicity of ‘x’
+    • In an equation for ‘i’: i x = let !(y, z) = x in (z, y)
+
+LinearLet9.hs:28:58: error: [GHC-83865]
+    • Couldn't match expected type ‘Bool’ with actual type ‘Int’
+    • In the expression: f True
+      In the expression: (f (0 :: Int), f True)
+      In the expression:
+        let %Many !(Just f) = Just (\ x -> x) in (f (0 :: Int), f True)
+
+LinearLet9.hs:28:60: error: [GHC-83865]
+    • Couldn't match expected type ‘Int’ with actual type ‘Bool’
+    • In the first argument of ‘f’, namely ‘True’
+      In the expression: f True
+      In the expression: (f (0 :: Int), f True)
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
index f98692689c41a4a87f419247c04130b6aee8e9d8..08cc41e0ea44365c485600a6e94073d9b5558ca6 100644
--- a/testsuite/tests/linear/should_fail/all.T
+++ b/testsuite/tests/linear/should_fail/all.T
@@ -10,7 +10,6 @@ test('Linear9', normal, compile_fail, [''])
 test('LinearNoExt', normal, compile_fail, [''])
 test('LinearNoExtU', normal, compile_fail, [''])
 test('LinearAsPat', normal, compile_fail, [''])
-test('LinearLet', normal, compile_fail, [''])
 test('LinearLazyPat', normal, compile_fail, [''])
 test('LinearRecordUpdate', normal, compile_fail, [''])
 test('LinearSeq', normal, compile_fail, [''])
@@ -42,3 +41,13 @@ test('T20083', normal, compile_fail, ['-XLinearTypes'])
 test('T19361', normal, compile_fail, [''])
 test('T21278', normal, compile_fail, ['-XLinearTypes'])
 test('T23814fail', normal, compile_fail, [''])
+test('LinearLet1', normal, compile_fail, [''])
+test('LinearLet2', normal, compile_fail, [''])
+test('LinearLet3', normal, compile_fail, [''])
+test('LinearLet4', normal, compile_fail, [''])
+test('LinearLet5', normal, compile_fail, [''])
+test('LinearLet6', normal, compile_fail, [''])
+test('LinearLet7', normal, compile_fail, [''])
+test('LinearLet8', normal, compile_fail, [''])
+test('LinearLet9', normal, compile_fail, [''])
+test('LinearLet10', normal, compile_fail, [''])
diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs
index ffb48ee27bc2e1245f557b52fe0098af207aa1ee..82f45854edd9bb5d66a788515a40c3fad062752f 100644
--- a/utils/check-exact/ExactPrint.hs
+++ b/utils/check-exact/ExactPrint.hs
@@ -2331,10 +2331,10 @@ instance ExactPrint (HsBind GhcPs) where
           _ -> fid
     return (FunBind x fun_id' matches')
 
-  exact (PatBind x pat grhss) = do
+  exact (PatBind x pat q grhss) = do
     pat' <- markAnnotated pat
     grhss' <- markAnnotated grhss
-    return (PatBind x pat' grhss')
+    return (PatBind x pat' q grhss')
   exact (PatSynBind x bind) = do
     bind' <- markAnnotated bind
     return (PatSynBind x bind')
diff --git a/utils/check-exact/Transform.hs b/utils/check-exact/Transform.hs
index 4d70d06933bccc51e2a21f5f2aa9ddd7b3410562..885156301ca79c4e091d86ef57f01b0b9ae1a99f 100644
--- a/utils/check-exact/Transform.hs
+++ b/utils/check-exact/Transform.hs
@@ -926,7 +926,7 @@ hsDeclsPatBindD x = error $ "hsDeclsPatBindD called for:" ++ showGhc x
 -- for 'hsDecls' \/ 'replaceDecls'. 'hsDeclsPatBind' \/ 'replaceDeclsPatBind' is
 -- idempotent.
 hsDeclsPatBind :: LHsBind GhcPs -> [LHsDecl GhcPs]
-hsDeclsPatBind (L _ (PatBind _ _ (GRHSs _ _grhs lb))) = hsDeclsLocalBinds lb
+hsDeclsPatBind (L _ (PatBind _ _ _ (GRHSs _ _grhs lb))) = hsDeclsLocalBinds lb
 hsDeclsPatBind x = error $ "hsDeclsPatBind called for:" ++ showGhc x
 
 -- -------------------------------------
@@ -948,11 +948,11 @@ replaceDeclsPatBindD x _ = error $ "replaceDeclsPatBindD called for:" ++ showGhc
 -- idempotent.
 replaceDeclsPatBind :: (Monad m) => LHsBind GhcPs -> [LHsDecl GhcPs]
                     -> TransformT m (LHsBind GhcPs)
-replaceDeclsPatBind (L l (PatBind x a (GRHSs xr rhss binds))) newDecls
+replaceDeclsPatBind (L l (PatBind x a p (GRHSs xr rhss binds))) newDecls
     = do
         logTr "replaceDecls PatBind"
         binds'' <- replaceDeclsValbinds WithWhere binds newDecls
-        return (L l (PatBind x a (GRHSs xr rhss binds'')))
+        return (L l (PatBind x a p (GRHSs xr rhss binds'')))
 replaceDeclsPatBind x _ = error $ "replaceDeclsPatBind called for:" ++ showGhc x
 
 -- ---------------------------------------------------------------------