termination for FDs and ATs

[Stefan Wehr]

Iavor Diatchki <iavor.diatchki at gmail.com> wrote::

> 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.

But there is also the equality `T [Int] = Int` which we could apply.
Manuel pointed out in his reply that the inference algorithm doesn't
do that, so you are right with respect to the algorithm. But it's
still unclear if the algorithm is complete.

Stefan