Recursion on TypeNats

[Barney Hilken]

> 
> because you haven't helped write a patch change it yet :) 
> 
> -Carter
> 

Would this be possible with the new type checker plugins? 

btw, your example gives me

    Nested type family application
      in the type family application: U (n - 1)
    (Use UndecidableInstances to permit this)
    In the equations for closed type family ‘U’
    In the type family declaration for ‘U’
Failed, modules loaded: none.