termination for FDs and ATs

[Iavor Diatchki]

Hello,

On 5/3/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
>
> If you now try to derive "D [Int]", you get
>
>              ||- D [Int]
>     subgoal: ||- C Int        -- via Instance
>     subgoal: ||- C (T [Int])  -- via Def. of T in F
>     subgoal: ||- D [Int]      -- Superclass

I do not follow this example.

If we are trying to prove `D [Int]` we use the instance to reduce the
problem to `C Int`, and then we fail because we cannot solve this
goal.

If we are trying to validate the second instance, then we need to
prove that the context of the instance is sufficient to discharge the
super class requirements:
C a |- C (T [a]), F [a]
We can solve `F [a]` using the instance, and (by using the definition
of `T`) `C (T [a])` becomes `C a`, so we can solve it by assumption.

-iavor