type families & type-level recursion

[Manuel M T Chakravarty]

Peter Gavin:
> Manuel M T Chakravarty wrote:
>> Peter Gavin:
>>> > instance ( NaturalT n
>>> >          , zero ~ (n :==: D0)
>>> >          , zero ~ True )
>>> >   => TestIter n True where
>>> >     testIter _ _ = ""
>> I am wondering why you are writing (zero ~ (n :==: D0), zero ~  
>> True) instead os just (True ~ (n :==: D0)) - after all zero appears  
>> nowhere else.
> [..]
>
> Well, it's not happening in this instance, but I had some other code  
> that would give me compilation warnings unless I flattened  
> everything out like that.  I don't recall what the message exactly  
> was anymore, but I'd never seen it before. I guess I just got into  
> the habit of doing that without really thinking about it.

The earlier problems you head may have been due to a bug in the  
preliminary versions.  If you find that it makes a difference in the  
current implementation, then please let us know.

Cheers,
Manuel