Reference counting as implemented in Koka or Lean requires a heap that is acyclic, or at least a heap that can be partitioned into a DAG of compact regions, each of which are collected as one. Lazy evaluation and more generally mutability is fundamentally at odds with that, because it introduces cycles in the heap.
If you want Lean’s RC, you have to give up on thunk update. E.g.,
ones :: [Int]
ones = 1:ones
main = print $ ones !! 100000
will no longer operate in constant space, but rather needs to allocate each cons cell anew.
Of course, in this case you could simply allocate ones
into a compact region and maintain the DAGs-of-regions invariant. In general, it is difficult to predict statically how big a region must become to eliminate all cycles. You could declare the whole heap one big region, but then you can only free it at the end of the program, e.g., you lose precision/space safety.
Is it worth giving up on laziness and unrestricted mutability to have a simple and efficient GC algorithm? Perhaps it is! Time will tell and we surely will have a good comparison in a few years of time.