[ANN] linear-locks: locking primitives free of deadlocks

This is a cool idea, but I don’t think it really requires LinearTypes. Sketch:

-- Compile-time proof tokens.
type (<) :: k -> k -> ZeroBitType

(~) :: l < m -> m < n -> l < n

-- Newtype over IO, annotated by "lock level" and "acquisition level".
type Scoped :: k -> k -> Type -> Type

run :: (forall k (l :: k). Scoped l l b) -> IO b

fork :: Scoped l a () -> Scoped l a ThreadId

-- Newtype over MVar, annotated by level.
type Lock :: k -> Type -> Type

-- Create a new lock level and corresponding lock.
new
  :: b
  -> (forall m. l < m -> Lock m b -> Scoped m a r)
  -> Scoped l a r

-- Given that the acquisition level is less than the level of the lock,
-- acquire it in a scope of the corresponding acquisition level.
with
  :: a < m
  -> Lock m b
  -> (b -> Scoped l m (b, r))
  -> Scoped l a r