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

**URL:** <https://discourse.haskell.org/t/ann-linear-locks-locking-primitives-free-of-deadlocks/14112>\
**Category:** Announcements\
**Created:** [May 14, 2026, 7:48pm UTC](https://discourse.haskell.org/t/ann-linear-locks-locking-primitives-free-of-deadlocks/14112 "2026-05-14T19:48:50Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![dcastro](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/dcastro/32/4026_2.png) [@dcastro](https://discourse.haskell.org/u/dcastro)\
**Post date:** [May 14, 2026, 7:48pm UTC](https://discourse.haskell.org/t/ann-linear-locks-locking-primitives-free-of-deadlocks/14112/1 "2026-05-14T19:48:50Z")

</div>

[linear-locks](https://hackage.haskell.org/package/linear-locks) provides locking primitives that are statically guaranteed not to lead to deadlocks.

It achieves this by breaking one of the [Coffman conditions for deadlocks](https://en.wikipedia.org/wiki/Deadlock_(computer_science)#Prevention): the “circular wait” condition. `linear-locks` ensures locks are always acquired in a consistent order.

tl;dr: Each lock is assigned a “level”, tracked at the type level. When you enter a “lock scope”, you’re given a key that can acquire locks of level 0 or above. When you acquire a lock of level `n`, the key is consumed and you’re given a new key of level `n+1`, capable of acquiring locks of level `n+1` or above. This ensures locks are always acquired in order of increasing level, preventing circular waits.

The package ports the ideas of the [Surelock](https://notes.brooklynzelenka.com/Blog/Surelock) Rust crate to Linear Haskel. As such, it relies heavily on `LinearTypes` and is meant to be used with `linear-base`. Keys are linearly typed to ensure they cannot be reused and do not escape the “lock scope”. “Guards” (which represent ownership over acquired locks) are also linearly typed to ensure they are (1) always released and (2) cannot be used after being released.

- [Hackage](https://hackage.haskell.org/package/linear-locks)
- [GitHub](https://github.com/dcastro/linear-locks)

---

<div class="post-metadata">

**Author:** ![Leary](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/leary/32/4348_2.png) [@Leary](https://discourse.haskell.org/u/Leary)\
**Post date:** [May 15, 2026, 4:50am UTC](https://discourse.haskell.org/t/ann-linear-locks-locking-primitives-free-of-deadlocks/14112/2 "2026-05-15T04:50:35Z")

</div>

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

```haskell
-- 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

```