On Thu, Oct 24, 2013 at 11:23 AM, Stijn van Drongelen wrote:

Hi,

As far as I know, you're referring to the Paterson Conditions. Condition 'b' kind of corresponds to "at least one of the types is shrinking", while condition 'a' corresponds to "all the other are not growing", so the rules are already formulated in the way you suggest. The Paterson Conditions are also not the issue here; the Coverage Condition is.

...

The equivalent code using type families doesn't need undecidable instances in my ghc-7.6.2.

This is because (I think) type family instances are not subject to the Coverage Condition. In principle, type families are to type classes as functions are to relations. Functional dependencies may be used to make type classes more 'function-like'. I guess(!) the Coverage Condition is trying to capture this notion.

I don't know why it's formulated in this way, because in Alejandro's example, the classes really look 'function-like'.

Kind regards,

Stijn van Drongelen

Hi Stijn, Thanks for clarifying the issue. There is an example of why the coverage condition is needed on line 512 of (github doesn't handle line numbers in lhs correctly unfortunately): https://github.com/ghc/ghc/blob/9a04e1c7257f93f0c1cadc56a5e2a177574f6871/com... It doesn't seem possible to write a type for that function with just a type family; you need a class Mul to get into an infinite loop while looking for instances. So it seems appropriate that the coverage condition does not apply to type families. Regards, Adam