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 - (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
- Multiplicity annotations Language.Haskell.Syntax.Binds
Referenced by 4
- GHC.Tc.Gen.Bind call site ×3
- GHC.Driver.Flags call site