Re: termination for FDs and ATs

9 May 2006


      Iavor Diatchki  wrote::
...
Hello,
On 5/3/06, Stefan Wehr  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