Polymorphic components, so far

[Simon Peyton-Jones]

| > | * Pattern matching on polymorphic fields.  This does not appear to be
| > | too controversial, although Atze  had some reservations about this
| > | design choice.
...
| So far, most replys seemed to agree that this is not a big
| restriction.  Could you give more details on how you think that should
| work?   If we follow the current rules for pattern simplification,
| then this feature might be a bit confusing.  Here is an example:
|
| > data T = C (forall a. [a->a])
| >
| > f (C (f:fs)) = ...
| >
| > f x = case x of
| >         C y -> case y of
| >                  f : fs -> ...
| >                  _ -> undefined
|
| Notice that in the translation, when we 'case' on the 'y' the list
| gets instantiated, so that 'f' is monomorphic.  There is nothing wrong
| with that but I think that the may be more confusing than useful.

Indeed; if you are going to match 'y' against a constructor, you must instantiate.  The translation is untyped so I don't think that's a problem.  Indeed, you can regard the translation as specifying both the static and dynamic semantics.  That is
        f (C (f:fs)) = ...
is well-typed iff
        f x = case x of { C y -> case y of { f:fs ->... }}
is well-typed (as a Haskell source program).

Indeed, *not* allowing y to be polymorphic amounts to a special case of this rule that says "f (C (f:fs)) is well-typed iff ... UNLESS one of the variables bound is polymorphic.  It seems simpler to be uniform, no?

The only difficulty in implementation is maintaining the translation into System F, but I know a tidy way to do that now.  And GHC is the only compiler that does that anyway.

Simon