Note [Non-variable pattern bindings aren't linear]

GHC/Tc/Gen/Bind.hs:672 compiler 1 ticket

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

- (NVP1) 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). We do this with a
  dedicated test in decideGeneralisationPlan.
- (NVP2) 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. We do this by calling manyIfPats in tcPolyInfer. 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.
- (NVP3) LinearLet implies MonoLocalBinds to avoid the AbsBind case altogether.
- (NVP4) Wrinkle: even when other conditions (including MonoLocalBinds), GHC
  will generalise some binders, namely so-called closed binding groups. We need
  to make sure that the test for (NVP1) has priority over the test for closed
  binders.
- (NVP5) Wrinkle: Closed binding groups (NVP4) are usually fine to type with
  multiplicity Many. But there's one exception: when there's no binder at all,
  the binding group is considered closed. Even if the rhs contains arbitrary
  variables.

     f :: () %1 -> Bool
     f x = let !() = x in True

  If we consider `!() = x` as a generalisable group (which does nothing anyway),
  then (NVP2) will infer the pattern as multiplicity Many, and reject the
  function. We don't want that, see also #25428. So we take care not to
  generalise in this case, by excluding the no-binder case from automatic
  generalisation in decideGeneralisationPlan.

References 1

Referenced by 4