Simon said > This is a tricky one. Here's what is going on.
I believe there's nothing tricky going on. Your type annotation g :: (F a b,D b (T r)) => (a,T r) g = f is simply incorrect. Keep in mind that GHC does NOT improve type annotations. For example, g :: (F a b, C (T r)) => (a,T r) g = f type checks. (I "replaced" D b (T r) by C (T r) ) I understand that it might sound reasonable to accept g :: (F a b,D b (T r)) => (a,T r) g = f Indeed, depending on how we define subsumption among type schemes forall a b t. (F a b,D b t) => (a,t) -- inferred "subsumes" forall a b r. (F a b,D b (T r)) => (a,T r) -- annotated wrt the instance and FD. However, for GHCs evidence translation scheme we need a more restrictive subsumption check (because GHC never "improves" user-provided type annotations). > > Consider an instance decl like: > > instance (Lte a b l,If l b a c) => Max a b c > > (This is a real example.) Notice that "l" is used on the LHS of the > > => but not the RHS. The idea is that "l" will get unified by a > > functional dependency. But if such a unification re-starts the > > solving process from scratch, we just get into an infinite loop (apply > > instance decl, apply fds, unify, start again, apply instance decl > > again, etc). > Well, there might not be any immediate problem here. The only danger with instance (Lte a b l,If l b a c) => Max a b c is that we need to uniquely determine l given a, b and c. (If we can't then type inference (i.e. subsumption checking) might become incomplete) However, if there's a FD such as class Lte a b l | a b -> l then things should work out. We only get into trouble in case we find instance Lte a b l => Lte [a] [b] [l] By trouble I mean, type inference might become undecidable. To conclude, class Max a b c class Lte a b l | a b -> l class If l b a c instance (Lte a b l,If l b a c) => Max a b c is safe (i.e. type inference is sound and decidable). Things become unsafe if we add instance Lte a b l => Lte [a] [b] [l] Why and how to fix this problem is subject of current investigations. Will let you know once a readable version is available. Martin _______________________________________________ Glasgow-haskell-bugs mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
