Hello,
On 5/3/06, Stefan Wehr
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