Dot avoidance

dot.idr

data T : Nat -> Type where
    C : .(n : Nat) -> T n

f : (n : Nat) -> T n -> Bool
f    Z  (C    Z ) = True
f (S n) (C (S n)) = f n (C n)

main : IO ()
main = print $ f 3 (C 3)

{-
Main.C: inaccessible arguments reachable:
  n from Main.f arg# 1

Main.f {e0} {e1} =
	case {e1} of 
	| 0 => Prelude.Bool.True
	| _ => let {e3} = LMinus (ATInt ITBig)({e1}, 1) in Main.f(____, {e3})

-}