[Haskell-cafe] (no subject)

[oleg at okmij.org]

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.