On Wed, Oct 14, 2009 at 7:33 AM,
<oleg@okmij.org> wrote:
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.
Sorry, I wasn't precise enough.
I didn't mean to say that *every* program which requires "undecidable"
instance won't terminate.
Rather, take any of the properties which imply decidability. Then,
there *exists* a program which satisfies the negated property and this
program won't terminate.
As you show, for specific cases we can argue that "undecidable" instances
are decidable. You can even argue that the Add/Mult example is decidable,
assuming we never generate loopy type constraints.
-Martin
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.