This is the tracking ticket for the work I'm doing for my Master thesis on typechecking linearity in Core. UPDATE: A paper tackling this problem will be published at POPL26: "Lazy Linearity for a Core Functional Language". See also the announcement: https://alt-romes.github.io/posts/2025-11-26-lazy-linearity-popl26.html. ~~I'm currently finishing the soundness proof for the linear type system of a Core-like language, that annotates let and letrec bound variables as well as case binders with *usage environments*, as first proposed in the [Minicore document](https://gitlab.haskell.org/ghc/ghc/-/wikis/uploads/355cd9a03291a852a518b0cb42f960b4/minicore.pdf).~~ I haven't (yet?) addressed GADTs and multiplicity coercions. ~~The [(work in progress) dissertation](https://raw.githubusercontent.com/alt-romes/linear-core/master/report.pdf) motivates this issue and discusses the background, what I intend to do, and a tentative solution. Note that Chapter 3/4 are still much incomplete.~~ cc @monoidal