termination for FDs and ATs

[Iavor Diatchki]

Hello,

On 5/9/06, Stefan Wehr <mail at stefanwehr.de> wrote:
> >>     class C a
> >>     class F a where type T a
> >>     instance F [a] where type T [a] = a
> >>     class (C (T a), F a) => D a where m :: a -> Int
> >>     instance C a => D [a] where m _ = 42

> But there is also the equality `T [Int] = Int` which we could apply.
I think I see what you mean.  Here is what I worked out in case anyone
else didn't follow.
The axioms from the above declarations are:
1. forall a. F [a]
2. forall a. F [a] => T [a] = a
3. forall a. D a => C (T a) /\ F a
4. forall a. C a => D [a]
"proof"
goal: D [Int]
Using 4 with a = Int:
goal: C Int
Use (3 with a = [Int]) and (2 with a = Int) to get a new rule:
5. D [Int] /\ F [Int] => C Int /\ F [Int]
Using 5 and projection:
goal: F [Int], D [Int]
Using 1 with a = Int:
goal: D [Int]

Now we are back to where we started.  In this case we can notice this
and give up, but in general this might be tricky.

-Iavor