instance inference

[Simon Peyton-Jones]

Ross, and Martin,

Thanks!  But I'm not certain that your fix is correct.  Let's ask
Martin.  I've added comments below.

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org
[mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Ross Paterson
| Sent: 06 February 2006 11:36
| To: Simon Peyton-Jones; glasgow-haskell-users at haskell.org
| Subject: Re: instance inference
| 
| A patch implementing a relaxed termination constraint is at
| 
| 	http://www.soi.city.ac.uk/~ross/instance-termination.patch
| 
| Here is the description:
| 
|  With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4
|  requires that instances be of the following form:
| 
|   (1-GHC) each assertion in the context must constrain distinct
variables
|       mentioned in the head, and
| 
|   (2-GHC) at least one argument of the head must be a non-variable
type.

Yes, (1-GHC) certainly contradicts the FD paper that Martin and I wrote.
I think (1) should be:

   (1-fixed) Each assertion in the context must constrain type
variables, and 
   those type variables must all be mentioned in the head.

That is, there is no requirement that the type variables should be
distinct (they can be repeated).  But they must all appear in the HEAD.
Do you agree, Martin?  For example
	class D a b | a -> b 
	instance C a b b a => D a b where ...
is fine.


Now, you propose something new and interesting:

|  This patch replaces these rules with the requirement that each
|  assertion in the context satisfy
| 
|   (1-Ross) no variable has more occurrences in the assertion than in
the
|       head, and
| 
|   (2-Ross) the assertion has fewer constructors and variables (taken
together
|       and counting repetitions) than the head.
| 
|  This allows all instances permitted by the old rule, plus such
|  instances as
| 
|         instance C a
|         instance Show (s a) => Show (Sized s a)
|         instance (Eq a, Show b) => C2 a b
|         instance C2 Int a => C3 Bool [a]
|         instance C2 Int a => C3 [a] b
|         instance C4 a a => C4 [a] [a]
| 
|  but still ensures that under any substitution assertions in the
context
|  will be smaller than the head, so context reduction must terminate.

Your (1-Ross) ensures that every variable in the assertion does occur in
the head.  But I'm not sure that the size-reduction argument is
watertight in the presence of fundeps.  (E.g. in example 15 it *looks*
as if the size goes down, but it doesn't.) 

I bet Martin could tell us if it's watertight though.  

It certainly looks useful. However, notice that (1-Ross) is more also
more restrictive than (1-fixed), because it rules out the C/D example I
give above.  So is it a win?  

Simon