Advice about TcDeriv

[Simon Peyton-Jones]

| Questions:
|  * Will this annotation have other, possibly unwanted effects?

The role annotation will have exactly the *right* effect; in particular, it'll prevent you saying
	class Foo a where
	   foo :: Set a -> Set a

	instance Foo Int where ...
	newtype Age = MkAge Int deriving( Foo )

|  * Should we also simplify constraints like (NT Age a) to (NT Int a)
| automatically and built-in, or do we still want the user to first tell
| us that we should do so?

I think we should automatically simplify it.

|  * What about the “only do it if constructors are in scope” idea – if
| the typechecker creates these instances on the fly, it might do so for
| modules where the constructors are not in scope (either because they are
| private, or simply because they have not been imported).

It'll simplify (NT Age a) to (NT Int a) when, and only when, MkAge is in scope.  So visibility of the data constructor says just when you want that instance to work.  I think that seems fine to me.

Simon

| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 20 August 2013 08:37
| To: ghc-devs
| Subject: Re: Advice about TcDeriv
| 
| Good morning,
| 
| Am Dienstag, den 20.08.2013, 07:24 +0000 schrieb Simon Peyton-Jones:
| > The more I think about this, the more I wonder if we shouldn't treat
| > NT in a similar way that we treat (~); that is, with built-in rules.
| > The point is, we use
| >    (a) roles, and
| >    (b) visibility of the data constructor
| > to control abstraction via existence/visibility of the instance. We
| > don't really need a third mechanism
| >    (c) the presence or absence of a 'deriving' clause
| >
| > Instead, it can syntactically be a class, but be treateded rather like
| > the SingI class which has an infinite number of instances -- that is,
| > the type checker has a built-in way of simplifying NT constraints.
| >
| > For example, the typechecker simplifies
| > 	[s] ~ [t]
| > to
| > 	s ~ t
| > (This is just unification.)  Similarly it can simplify
| > 	NT [s] [t]
| > to
| > 	NT s t
| > (in a role-aware way, of course).
| >
| > I think this will end up being a lot simpler than trying to push it
| > through the full 'deriving' mechanism.
| >
| > Does that make sense?
| 
| it is certainly true that there are many obstacles when trying to use
| the normal class mechanisms here.
| 
| One of the main reason we wanted to use (standalone) deriving instances
| (or even the NT type constructor idea earlier) was to give library
| authors a way to communicate their abstractions, to avoid the coercion
| between (Set Int) and (Set (Down Int)). But thanks to Richard’s role
| annotation, this can be prevented by annotating the Set’s type variables
| with @N. So far so good.
| 
| Questions:
|  * Will this annotation have other, possibly unwanted effects?
|  * Should we also simplify constraints like (NT Age a) to (NT Int a)
| automatically and built-in, or do we still want the user to first tell
| us that we should do so?
|  * What about the “only do it if constructors are in scope” idea – if
| the typechecker creates these instances on the fly, it might do so for
| modules where the constructors are not in scope (either because they are
| private, or simply because they have not been imported).
| 
| 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