Martin Sulzmann wrote:
"Undecidable" instances means that there exists a program for which there's an infinite reduction sequence.
I believe this may be too strong of a statement. There exists patently terminating type families that still require undecidable instances in GHC. Here is an example:
{-# LANGUAGE TypeFamilies #-}
type family I x :: * type instance I x = x
type family B x :: * type instance B x = I x
GHC 6.8.3 complaints: Application is no smaller than the instance head in the type family application: I x (Use -fallow-undecidable-instances to permit this) In the type synonym instance declaration for `B' But there cannot possibly be any diverging reduction sequence here, can it? The type family I is the identity, and the type family B is its alias. There is no recursion. The fact that type families are open is not relevant here: our type families I and B are effectively closed, because one cannot define any more instance for I and B (or risk overlap, which is rightfully not supported for type families). The reason GHC complains is because it checks termination instance-by-instance. To see the termination in the above program, one should consider instances I and B together. Then we will see that I does not refer to B, so there are no loops. But this global termination check -- for a set of instances -- is beyond the abilities of GHC. This is arguably the right decision: after all, GHCi is not a full-blown theorem prover. Thus there are perfectly decidable type programs that require undecidable instances. Indeed, there is no reason to be afraid of that extension.