We've seen several examples now, from Ralf, Alex, and others, where it is
useful to relax the proposed restriction:
The types in an instance-declaration context must all be type variables.
(Item 10 in Simon's list:
http://www.dcs.gla.ac.uk/~simonpj/multi-param.html)
Hugs and GHC are currently taking different positions on this. The
latest version of the Hugs type checker (in Hugs 1.3c) does not restrict
the types appearing in instance contexts or heads (other than ensuring
that they are valid and appropriately kinded). GHC imposes restrictions
that limit its expressiveness but also guarantee decidability (i.e., that
type checking will terminate).
Without the restriction, it is easy to come up with examples that could
lead to non-termination. For example, try to establish Foo Maybe Int
using the following:
instance Foo f (f a) => Foo f a where ...
Or, if you want an example with at least one non-tyvar in the instance head,
then try to establish Bar Maybe [Int] using:
instance Bar f [f a] => Bar f [a] where ...
My hope is that, over a period of time, the two systems will converge on
some happy compromise between the current extremes that offers the
advantages
of both. From my perspective, it is a definite policy to leave this part
of the design space open for further exploration. There is good reason to
believe that a suitable compromise can be reached. For example, in both
of the instance decls above, the types on the left of the => arrow are
strictly larger than those on the right (an extra type application and
variable in each case). On the other hand, in Alex's example:
instance (Set s n, Num (s n), POrd (s n)) => Num [s n] where ...
the types in the three context constraints contain strictly smaller types
than those in the head. Likewise, in Ralf's example:
instance (PriorityQueue q a, PriorityQueue p a, Show (p a))
=> PriorityQueue (ControlBy q p) a where ...
the only compound type in the context is (p a), which is strictly smaller
than (Control q p) in the head.
Looking at the `size' of types is, of course, a generalization of Simon's
suggestion that contexts might be allowed to constrain only proper sub-
expressions of types in the context. (Proper sub-expressions are, by
definition, smaller in size.) However, it is still too strict to allow
useful things like: instance Monad m => Functor m where ..., so there is
still some work to be done ...
I hope this helps, at least to explain the current background!
Mark
