Scoping bug leading to a 'Fatal error'

[dorchard]

on main

data Cost (r : Q) a where
    MkCost : (() [r] -> a) -> Cost r a

return : forall {a : Type} . a -> Cost 0 a
return x = MkCost (\([()] : () [0]) -> x)

bind : forall {a b : Type, n m : Q} . (a -> Cost n b) -> Cost m a -> Cost (n + m) b
bind f (MkCost k) = MkCost (\([p] : (() [n + m])) -> let (MkCost k') = f (k [p]) in k' [p])

produces:

(base) dorchard@edud49c granule % gr thursday.gr 
Checking ex.gr...
Fatal error: ex.gr:
Looking up a variable '(Id "r.1" "r.1")' in [((Id "r.0" "r.0"),SFloat <symbolic> :: SFloat),((Id "r.2" "r.2"),SFloat <symbolic> :: SFloat),((Id "n" "n`2"),SFloat <symbolic> :: SFloat),((Id "m" "m`3"),SFloat <symbolic> :: SFloat)]