Hello cafe, I tried to play with some type level natural numbers, and it seems type level function is quite slow, for instance: (full source) https://gist.github.com/wangbj/5939aa7a30c3d756d98f5b5775e162a6 data Z data S n class KnownNat n where natSing :: n -> Integer instance KnownNat Z where natSing _ = 0 instance KnownNat n => KnownNat (S n) where natSing _ = 1 + natSing (undefined :: n) natVal :: KnownNat n => n -> Integer natVal = natSing natSing doesn't seems to know how to optimize when KnownNat is very big (i.e: 10000), I tried Peano Add/Mul, and they are very slow to be really useful. Is there any ways to improve this? How fully dependent typed language such as Adga/Idris handle this, do they have the same performance issue? Thanks baojun