Compiler error "No such variable"

[jinwoo]

Idris: 1.3.1 OS: macOS 10.14.4

data Tree a = E | T (Tree a) a (Tree a)

balTree : a -> Int -> Tree a
balTree x 0 = E
balTree x n
  = let n' = n - 1 in
        case n' `mod` 2 of
             0 => let next = balTree x (n' `div` 2) in
                      T next x next
             1 => let (l, r) = balTree2 (n' `div` 2) in
                      T l x r
  where
    balTree2 : Int -> (Tree a, Tree a)
    balTree2 m = (balTree x m, balTree x (m + 1))

Steps to Reproduce

Save the code above in a file Tree.idr and load it in Idris.

Expected Behavior

Must compile fine.

Observed Behavior

Get a compile error

Type checking ./Tree.idr
Tree.idr:7:14-23:
  |
7 |         case n' `mod` 2 of
  |              ~~~~~~~~~~
When checking right hand side of Main.case block in balTree at Tree.idr:7:14-23 with expected type
        Tree a

When checking an application of function Prelude.Interfaces.div:
        No such variable n'

Holes: Main.balTree

[jinwoo]

Please note that even though the highlight in the error message is around n' `mod` 2, the error actually comes from n' `div` 2 in the case branches. If I inline n' with (n - 1) in those branches, compilation succeeds. So it seems that n' is recognized in n' `mod` 2 but not in n' `div` 2.

balTree : a -> Int -> Tree a
balTree x 0 = E
balTree x n
  = let n' = n - 1 in
        case n' `mod` 2 of
             0 => let next = balTree x ((n - 1) `div` 2) in
                      T next x next
             1 => let (l, r) = balTree2 ((n - 1) `div` 2) in
                      T l x r
  where
    balTree2 : Int -> (Tree a, Tree a)
    balTree2 m = (balTree x m, balTree x (m + 1))