termination for FDs and ATs

Iavor Diatchki iavor.diatchki at gmail.com
Wed May 3 17:03:48 EDT 2006


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

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.


More information about the Haskell-prime mailing list