Something stronger than IncoherentInstances needed (Univalent Classes?)

[Simon Peyton-Jones]

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 at haskell.org] On Behalf Of Joachim
|  Breitner
|  Sent: 26 July 2013 11:27
|  To: ghc-devs at 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 at joachim-breitner.de • http://www.joachim-breitner.de/
|    Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
|    Debian Developer: nomeata at debian.org