Hello, On 5/9/06, Stefan Wehr <[EMAIL PROTECTED]> 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
But there is also the equality `T [Int] = Int` which we could apply.
I think I see what you mean. Here is what I worked out in case anyone else didn't follow. The axioms from the above declarations are: 1. forall a. F [a] 2. forall a. F [a] => T [a] = a 3. forall a. D a => C (T a) /\ F a 4. forall a. C a => D [a] "proof" goal: D [Int] Using 4 with a = Int: goal: C Int Use (3 with a = [Int]) and (2 with a = Int) to get a new rule: 5. D [Int] /\ F [Int] => C Int /\ F [Int] Using 5 and projection: goal: F [Int], D [Int] Using 1 with a = Int: goal: D [Int] Now we are back to where we started. In this case we can notice this and give up, but in general this might be tricky. -Iavor _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org//mailman/listinfo/haskell-prime
