Totality check fails on simple structural recursion when it is not tail recusive

[uzytkownik]

Steps to Reproduce

Repro after cleaning up:

import Data.Erased
import Data.List

data Color = Red | Black

Eq Color where
  Red   == Red   = True
  Black == Black = True
  _     == _     = False

data Node : Type -> Type where
  NNode : Node v
  Bin   : (c : Color) -> (l : Node v) -> (m : v) -> (r : Node v) -> Node v

nodeBHeight : Node v -> Nat
nodeBHeight  NNode              =                   0
nodeBHeight (Bin Red   l _ _) =     nodeBHeight $ l
nodeBHeight (Bin Black l _ _) = S . nodeBHeight $ l

-- That one works                                                                                                                                                                             
nodeBHeight' : Node v -> Nat
nodeBHeight' = aux Z where
  aux n  NNode            = n
  aux n (Bin Red   l _ _) = aux    n  l
  aux n (Bin Black l _ _) = aux (S n) l

-- So does this:
nodeBHeight'' : Node v -> Nat
nodeBHeight''  NNode              =                   0
nodeBHeight'' (Bin Red   l _ _) =     nodeBHeight $ l
nodeBHeight'' (Bin Black l _ _) = nodeBHeight $ l

Expected Behavior

*src/Data/Map> :total nodeBHeight'
Data.Map.nodeBHeight' is Total
*src/Data/Map> :total nodeBHeight
Data.Map.nodeBHeight' is Total

Observed Behavior

*src/Data/Map> :total nodeBHeight'
Data.Map.nodeBHeight' is Total
*src/Data/Map> :total nodeBHeight
Data.Map.nodeBHeight is possibly not total due to recursive path:
    Data.Map.nodeBHeight, Data.Map.nodeBHeight, Data.Map.nodeBHeight