[Haskell] Re: Rebindable syntax for monads and arrows

[Simon Peyton-Jones]

| You can to do this with GADTs:
| 
| data MyVec a where
|   MkMyVec :: (FinSet a) => Vec a -> MyVec a
| 
| instance Monad MyVec where
|   return a = MkMyVec (vreturn a)
|   etc.
| 
| GADTs are scheduled for version 6.4 of GHC. The version of GHC now in
| CVS does not currently allow this however, see GHC bug #1097046.

I'm not sure how to fix this bug, or even if it is a bug.  Let me
explain why. 

Usually GHC is reluctant to perform context reduction by applying
instance declarations.  Two reasons:
1.  Postponing context reduction give more opportunities for sharing
2.  With overlapping instance declarations, eager context reduction may
	select an instance declaration "too early"; later, more type
information
	may be available.

In fact, when you force context reduction by giving a type signature,
GHC complains if (2) applies with its "the instance selected depends on
the instantiation of x" message.

Now, suppose we have

  f x = case x of
	  MkMyVec x -> <rhs>

where (x::MyVec a) the <rhs> gives a constraint (Foo [a]).  And suppose
we have

	instance (Eq a, MyVec a) => Foo [a]

then you may say that f should get type
	f :: Eq a => MyVec a -> ...
because the MyVec part gets discharged by the MkMyVec pattern match,
leaving only the Eq a part.  Fine.  Now suppose there's an overlapping
instance declaration for Foo, say Foo [Char].  Then GHC would decline to
select the Foo [a] instance, so we'd infer the type
	f :: Foo [a] => MyVec a -> ....

There would be no error message in either case, just a different type
inferred.  A programmer might well find this odd.  Sometimes the MyVec
constraints are handled by the MkMyVec constructor, and sometimes they
aren't.

The root of the difficulty is that the MkMyVec constructor captures
constraints that mention no existentially-quantified type variable, so
it'd make perfect sense to float them outwards.  (In contrast,
constraints mentioning existentially-quantified type variables *must* be
dealt with at the pattern match.)

Here's one idea.  If you specify a type signature for 'f' then matters
are much clearer.  In my example, if you specify
	f :: Eq a => MyVec a -> ...
then it's absolutely clear what constraints are available at the pattern
match (namely Eq a, MyVec a), and we solve all the constraints there.
So the rule would be: 
	
	constraints are always solved *lazily* when inferring, so we'd
infer
		f :: Foo [a] => MyVec a -> ...
		even without any overlap 
	
	but they are solved *eagerly* when checking against a
user-supplied type sig
	so when checking
		f :: Eq a => MyVec a => ...
	we'd accept the program.  (If there were overlapping instances,
we'd complain about them.)

But I suspect that programmers will prefer a more woolly rule that does
as much constraint solving as it can (provided all instance selection is
uniquely determined).  That would give the slightly surprising behaviour
I describe above if an overlapping instance declaration was added.

Thoughts anyone? 

Simon