Something stronger than IncoherentInstances needed (Univalent Classes?)

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Something stronger than IncoherentInstances needed (Univalent Classes?)

Joachim Breitner-2
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  -XMultiParamTypeClasses
Prelude> class Class a b where { method :: (a,b); method = undefined }
Prelude> instance Class a b => Class [a] [b]
Prelude> instance Class a a
Prelude> :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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130726/3fdb4a0a/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

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

Reply | Threaded
Open this post in threaded view
|

Something stronger than IncoherentInstances needed (Univalent Classes?)

Joachim Breitner-2
Hi,

Am Freitag, den 26.07.2013, 23:16 +0000 schrieb Simon Peyton-Jones:

> 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.

I thought about this as well, but after reading the docs (which document
what is happing right now) it seemed to me that this behavior was
intentional. But if it is ok to liberate the meaning of
IncoherentInstances, even better. I?ll put it on my TODO list for NT
stuff.

Greetings,
Joachim
--
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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130727/5ce31057/attachment.pgp>