Proposal: fix "simple pattern binding" and "declaration group"

[dm-list-haskell-prime at scs.stanford.edu]

At Mon, 27 Jun 2011 15:02:33 +0100,
Paterson, Ross wrote:
> 
> > There is no a priori reason why b should depend on a in a pair of
> > bindings such as these:
> >
> >        a = const (\x -> x) b
> >        b = const (a :: Int -> Int) (a :: Bool -> Bool)
> 
> There is: section 3.16 says that in an expression type signature e::t,
> the type derived for e must be more specific than t.  To derive the
> type of e, in this case a, before matching it against t, we have no
> alternative but to use the definition of a.

I saw this, but I guess I didn't realize it was relevant to 4.5.1.
When I read 3.16, the following sentence:

	the declared type may be more specific than the principal type
	derivable from exp, but it is an error to give a type that is
	more general than, or not comparable to, the principal type

seemed so obvious that I just glossed over it.  There's actually an
important point here, which is that in order to infer the type of an
expression type-signature e :: t, you first must infer the type of e,
and only then check it against t.  If this is the intent, it would be
clearer to say "more specific than the principle type *derived* from
exp", rather than "derivable", since the derivation must actually
happen.

But in fact, the relation of expression type signatures to type
inference is even subtler.  Expression type signatures *can* affect
type inference in code such as the following:

	f1 () = 5 where { _ = f2; _ = n }
	f2 () = f1 () :: Rational         -- changes type of n to Rational
	n = f1 ()

I guess the rule is that expression type signatures can affect type
inference by resolving ambiguities or avoiding defaulting, but not in
any other way?  To understand that, you have to understand sections
4.5.1 and 4.5.2, meaning we've come full circle.

And there's another sentence in 4.5.2 that makes this harder to
understand:

	If the programmer supplies explicit type signatures for more
	than one variable in a declaration group, the contexts of
	these signatures must be identical up to renaming of the type
	variables.

This makes it sound like declaration type signatures don't break up
declaration groups.  I suppose the above sentence is technically
applicable for non-simple pattern bindings, but it would be clearer to
add something along of the lines of "... type signatures for more than
one variable (which can occur when a non-simple pattern binding binds
multiple variables)...".

> > Even if you don't think the report is ambiguous, it is at least prone
> > to misinterpretation, which is why a couple of examples would really
> > help at the end of 4.5.1.
> 
> Fair enough.  Perhaps the example on the H' page would help:
> 
> http://hackage.haskell.org/trac/haskell-prime/wiki/RelaxedDependencyAnalysis

Sure, that's a good example.  But it would also be nice to have an
example with an expression type signature, maybe with an explanation
that references 3.16 to make clear what is going on (and maybe with a
change of derivable -> derived in 3.16).

David