Something stronger than IncoherentInstances needed (Univalent Classes?)

Simon Peyton-Jones simonpj at
Sat Jul 27 01:16:59 CEST 2013


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


|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at] On Behalf Of Joachim
|  Breitner
|  Sent: 26 July 2013 11:27
|  To: ghc-devs at
|  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
|  --
|  Joachim “nomeata” Breitner
|    mail at joachim-breitner.de
|    Jabber: nomeata at  • GPG-Key: 0x4743206C
|    Debian Developer: nomeata at

More information about the ghc-devs mailing list