TypeFamilies vs. FunctionalDependencies & type-level recursion

[AntC]

 <oleg at ...> writes:

> 
> 
> I don't think Overlapping Instances will be in Haskell' any time soon
> since there are doubts about the soundness. Overlapping
> instances are clearly unsound with type functions. Whether they are
> sound with functional dependencies is not clear, but there are warning
> signs:
> 
> 	http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
> 
I have now worked through that post in detail, thank you. And replied (on the 
cafe http://www.haskell.org/pipermail/haskell-cafe/2012-May/101417.html )

As SPJ says there, I don't expect there's any real difference in the fundeps 
approach compared to type families. And as a matter of taste, I find type 
families more easy to understand and reason about, and more *functional*.

But I don't see in SPJ's post any real doubts about soundness, just 
restrictions that would have to be imposed. He concludes "I believe that 
if ..., then overlap of type families would be fine."

The only onerous restriction is that overlapping instances would have to be in 
a single module. And I don't think that is needed under my proposal to dis-
overlap overlaps.

As a matter of interest, how would the TTypeable approach address those 
examples? Particularly the existentials (examples 3 and 4). How would it look 
inside the GADTs to discharge the constraints (or apply the type functions)?

I notice example 4 (and 1) 'exploits' separate compilation/imported 
overlapping instances to arrive at unsoundness. How does TTypeable handle 
imported instances?

AntC