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:[email protected]] On Behalf Of Joachim
| Breitner
| Sent: 26 July 2013 11:27
| To: [email protected]
| 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
| [email protected] • http://www.joachim-breitner.de/
| Jabber: [email protected] • GPG-Key: 0x4743206C
| Debian Developer: [email protected]
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
