Joachim Good point. There is something odd about this. "IncoherentInstances" is meant to say "I don't care which path you take to proving this constraint". So if we have instance C Int a instance C b Int and we try to solve (C Int Int) we should arbitrarily pick either. But we don't. So I rather think that IncoherentInstances should be modified so it really does what it says. (In effect, it'd become what you mean by univalent classes, but per-instance.) If you need something short term, you could just bake in (NT a a) instance into the solver Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of Joachim | Breitner | Sent: 26 July 2013 11:27 | To: ghc-devs@haskell.org | Subject: Something stronger than IncoherentInstances needed (Univalent | Classes?) | | Hi, | | in the context of the newtype wrapper I have an instance selection problem where | even IncoherentInstances is not liberal enough. Consider this example: | | Prelude> :set -XFlexibleInstances -XIncoherentInstances | Prelude> -XMultiParamTypeClasses class Class a b where { method :: | Prelude> (a,b); method = undefined } instance Class a b => Class [a] [b] | Prelude> instance Class a a :t method :: ([a],[a]) | | <interactive>:1:1: | Overlapping instances for Class [a1] [a1] | arising from a use of `method' | Matching instances: | instance [incoherent] Class a b => Class [a] [b] | -- Defined at <interactive>:4:10 | instance [incoherent] Class a a -- Defined at <interactive>:5:10 | In the expression: method :: ([a], [a]) | | As none of the two instances are more specific than the other, the typechecker | stops despite the incoherent flag. | | My suggestion is to add another flag, this time to the class declaration, marking | the class as univalent (different naming suggestions welcome, of course), | indicating that it will generally not matter which instance is selected, and in the | case of overlap the typechecker should just pick any matching instance. | | Would such a feature be welcome? | | I could imagine that it might be more useful in other settings as well, e.g. if type | classes are pure predicates about types, without any methods. | | Greetings, | Joachim | | PS: I will be on a summer school the next two week. I have written down the | status of the newtype coercion implementation at | http://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers#Status | | -- | Joachim “nomeata” Breitner | mail@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org