Richard raises a question about coherence below. (Coherence, not soundness.) But it's a coherence problem we already have. Given his Foo type, | > data Foo a where -- a's role is representational; this is NOT a GADT | > MkFoo :: Ord a => a -> Foo a suppose we define bar :: Foo T -> Bool bar (MkFoo x) = x>x At the use of (>) we have potentially two instances of (Ord T) available - one bound by the MkFoo constructor - one top-level instance and we could easily have more; et bar2 :: Foo T -> Foo T -> Bool bar2 (MkFoo x) (MkFoo y) = x>y These instances could potentially have different implementations if the (Foo T) values were constructed in different modules, each with its own (instance Ord T). So this isn't really a new problem, and it's one that doesn't seem too bad in practice. Simon | A question about the existing check: How does it treat constraints? For example, | say we have | | > data Foo a where -- a's role is representational; this is NOT a GADT | > MkFoo :: Ord a => a -> Foo a | > | > newtype Age = MkAge Int deriving Eq -- the Eq is to satisfy Ord's superclass | constraint | > instance Ord Age where | > (MkAge a) `compare` (MkAge b) = b `compare` a -- args are reversed | > | > fooInt :: Foo Int | > fooInt = MkFoo 5 | > | > fooAge :: Foo Age | > fooAge = coerce fooInt -- it seems this would be accepted | > | > confused :: Foo Age -> Ordering | > confused (MkFoo x) = x `compare` (MkAge 0) | | What will confused do? It has potentially two, conflicting instances for Ord to | hand: one in the global context; and one from pattern-matching MkFoo, which was | creating by coercing from Ord Int. I have a hard time seeing the solution to be | IncoherentInstances, because it's not clear which chunk of code would trigger the | need for that extension. | | Also, it's possible for there to be "abstract" classes, which don't export all of their | methods or use other tricks to prevent instances (non-exported superclasses, for | example) outside of the library. Are these checked for? | | Actually, come to think of it, the example I have above doesn't really interact with | the Safe Haskell check -- it's a problem regardless, unless I'm confused.