[fixed entailment
mail@stefanwehr.de**20050613042209
 
 entailment could not deal with something like
 
 Elem T = Int ||- Num (Elem T)
 
 The problem was solved by normalizing (Elem T) before
 running entail
 
] {
hunk ./Entailment.hs 81
-entail' ps (CC p) = 
-    do supers <- mapM bySuper (classConstraints ps)
+entail' ps (CC cc@(ClassConstraint c ts)) = 
+    do ts' <- mapM (\t -> runUF (toEqDefs ps) (normalise t)) ts
+       let p = ClassConstraint c ts'
+       debug ("checking entailment of class constraint " ++ showPpr' cc 
+             ++ ", so normalizing rhs first. Result: " ++ showPpr' p)
+       supers <- mapM bySuper (classConstraints ps)
hunk ./Entailment.hs 95
-    do let ps' = mapMaybe toEqDef ps
+    do let ps' = toEqDefs ps
hunk ./Entailment.hs 100
-    where toEqDef (CC _) = Nothing
-          toEqDef (EC e) = Just $ EqualityDefinition [] e
+
+toEqDefs :: [Constraint] -> [EqualityDefinition]
+toEqDefs ps = mapMaybe toEqDef ps
+
+toEqDef (CC _) = Nothing
+toEqDef (EC e) = Just $ EqualityDefinition [] e
addfile ./tests/examples/Collects.out
hunk ./tests/examples/Collects.out 1
+42
addfile ./tests/examples/Collects.phc
hunk ./tests/examples/Collects.phc 1
+-- Eq
+
+class Eq a where {
+  eq :: a -> a -> Bool;
+}
+
+instance Eq Int where {
+  eq x y = x == y;
+}
+
+-- Float
+
+data Float = MkFloat Int;
+
+instance Eq Float where {
+  eq (MkFloat x) (MkFloat y) = eq x y;
+}
+
+-- Num
+
+class Num a where {
+  zero :: a;
+  add  :: a -> a -> a;
+}
+
+instance Num Int where {
+  zero    = 0;
+  add x y =  x + y;
+}
+
+instance Num Float where {
+  zero                        = MkFloat 0;
+  add (MkFloat x) (MkFloat y) = MkFloat (x + y);
+}
+
+sum :: Num a => List a -> a;
+sum l = case l of 
+          Nil       -> zero;
+	  Cons x xs -> add x (sum xs);
+        ;
+
+--
+
+class Collects c where {
+  type Elem c;
+  empty  :: c;
+  insert :: Elem c -> c -> c;
+  toList :: c -> List (Elem c);
+}
+
+instance Eq e => Collects (List e) where {
+  type Elem (List e) = e;
+  empty    = Nil;
+  insert   = Cons;
+  toList c = c;
+}
+
+data BitSet = MkBitSet;
+
+instance Collects BitSet where {
+  type Elem BitSet = Char;
+  empty = MkBitSet;
+  insert = insert;
+  toList = toList;
+}
+
+--sumColl :: Collects c, Elem c = Int => c -> Int;  -- ERROR (now ok)
+--sumColl :: Collects c, Elem c = Int => c -> Elem c;  -- ERROR (now ok)
+--sumColl :: Collects c, Num (Elem c) => c -> Elem c;  -- ok (still ok)
+--sumColl :: List Int -> Int;  -- ok (still ok)
+sumColl c = sum (toList c);
+--sumColl = sumColl;
+
+main = 42;
+
}