Dylan Thurston wrote:
On Thu, Jun 19, 2003 at 11:08:35AM -0500, Ed Komp wrote:
| type BaseType = Either Integer ( Either Bool () ) | | type Value = (Either Double BaseType) | | data Foo = forall x. (SubType x BaseType) => MkFoo x | | test :: Foo -> Value | test (MkFoo x) = inj x
'x' is the variable I am concerned about. Since it is an argument to MkFoo, we know that (SubType x BaseType) and we also know that:
NOT (SubType Double BaseType), so 'x' cannot be instantiated as Double.
I'm missing something. Why do we know NOT (SubType Double BaseType)? Nothing in the code above prevents you from having such an instance, does it?
Put another way, only with a "closed world" assumption could the compiler "know" that NOT (SubType Double BaseType). GHC deliberately eschews such an assumption, so that adding new instances doesn't change the semantics of a program. Dean