+Consider this:
+
+ class C a b | a -> b
+ class D a b | a -> b
+
+ instance D a b => C a b -- Undecidable
+ -- (Not sure if it's crucial to this eg)
+ f :: C a b => a -> Bool
+ f _ = True
+
+ g :: C a b => a -> Bool
+ g = f
+
+Here f typechecks, but g does not!! Reason: before doing improvement,
+we reduce the (C a b1) constraint from the call of f to (D a b1).
+
+Here is a more complicated example:
+