Strange error in show for datatype

[Thomas Hallgren]

  Simon Peyton-Jones wrote:

>...
>	msg :: forall a.  Show a => String
>
>Urk!  What "Show" dictionary should Hugs use when evaluating "msg"?
>
>You may say "it doesn't matter", but in general that's not the case.  
>In the case of class Num, for example, we might have
>
>	expr = 3+4
>	msg = show expr
>
>and then the type involved really does matter.
>
>I wonder if the following is true.  Given the ambiguous type
>
>	forall a.  Show a => T	(where a does not appear in T)
>
>it's OK to pass the bottom dictionary. ...
>
Type systems with subtyping have what is needed to determine when the 
choice of dictinionary "doesn't matter".

In type systems with subtyping, the most general type is the minimal 
type. This means that type variables that occur only positively (in 
covariant positions) can be minimized (and that negative variables can 
be maximized). If there is an empty type, Empty say, which is a subtype 
of all other types, then the type

    forall a . Show a => T

is just as general as the type

    Show Empty => T

since a occurs only positively in Show a => T, taking into account the 
occurences of a in the definition of the Show class. The requirement 
that a does not appear in T is overly restrictive. This simplification 
can be made as long as all occurences of a in T are positive.

Assuming a language with subtyping that simplifes types in this way, 
expressions like

    show undefined
    show []
    show Nothing
    show (Left False)

would no longer be ambiguously overloaded. If the prelude provides

    instance Show Empty -- no methods need to be defined

then types of the above expressions would all reduce to String, and they 
would all compute to the expected results (i.e., the result you would 
get by manually disambiguating the types, e.g., show ([]::[Int])).

The same trick applies to the Eq class, so that, e.g., [] == [] would be 
unambiguous and compute to True.

So, obviously, the next version of Haskell should have a type system 
with subtyping, don't you agree? :-) 

Thomas Hallgren

PS In some previous version of Haskell (1.3?), the Prelude defined an 
empty type called Void, but it has since been removed. Apparently, 
people didn't see the potential of Void...

PPS For those who are afraid of subtypes :-), I think you can use the 
information about variance of type variables used in subtype inference, 
to determine when the choice of dictinonary "doesn't matter", without 
introducing subtyping in the languange...