Agda: Simplifying recursive definitions involving Thunk

I'm trying to implement a type that represents a (possibly) infinite path on an infinite binary tree. The definition currently resembles that of Conat in the stdlib.

open import Size
open import Codata.Thunk

data BinaryTreePath (i : Size) : Set where
  here : BinaryTreePath i
  branchL : Thunk BinaryTreePath i → BinaryTreePath i
  branchR : Thunk BinaryTreePath i → BinaryTreePath i

zero : ∀ {i} → BinaryTreePath i
zero = branchL λ where .force → zero

infinity : ∀ {i} → BinaryTreePath i
infinity = branchR λ where .force → infinity

Now I want to define a value which has longer repeating parts, e.g. LRRL. The best I can write right now is the following (which gets tedious quickly).

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 =
  branchL λ where .force → branchR λ where .force → branchR λ where .force → branchL λ where .force → sqrt2

-- or --

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL λ where
  .force → branchR λ where
    .force → branchR λ where
      .force → branchL λ where
        .force → sqrt2

The goal

Define branchL' and branchR' so that the following passes type check and termination check.

sqrt2 : ∀ {i} → BinaryTreePath i
sqrt2 = branchL' (branchR' (branchR' (branchL' sqrt2)))

The things I tried so far

Wrapping the part in a regular function doesn't work:

branchL' : (∀ {i} → BinaryTreePath i) → (∀ {j} → BinaryTreePath j)
branchL' path = branchL λ where .force → path

zero' : ∀ {i} → BinaryTreePath i
zero' = branchL' zero'
--               ^^^^^ Termination checking failed

So I tried wrapping into a macro, but I can't find how to construct the term branchL λ where .force → path when path is given as a Term. The following doesn't work either:

open import Agda.Builtin.Reflection
open import Data.Unit
open import Data.List

macro
  branchL' : Term → Term → TC ⊤
  branchL' v hole = do
    path ← unquoteTC v
    term ← quoteTC (branchL λ where .force → path)
    --                                       ^^^^ error
    unify hole term

{- error message:
Cannot instantiate the metavariable _32 to solution BinaryTreePath
.j since it contains the variable .j which is not in scope of the
metavariable or irrelevant in the metavariable but relevant in the
solution
when checking that the expression path' has type BinaryTreePath .j
-}