It's possible if you have dependent types and are not afraid to (ab)use the type system. See section 2.4 of my thesis (link in bio) for a taste. You have to squint a bit but a system like that can ensure linearity.