On Sun, Oct 01, 2006 at 08:05:15PM -0700, oleg@pobox.com wrote:
I have come to realize that irrefutable pattern matching of existentials may indeed be problematic. Let us consider the following existential data type
data FE = forall a. Typeable a => Foo a | forall a. Typeable a => Bar a
The following tests type and run (the latter raising the expected exception).
test1 = case (Foo ()) of Foo x -> show $ typeOf x test2 = case (Bar True) of Foo x -> show $ typeOf x
Let us suppose that irrefutable pattern matching of existentials is allowed. What would be the value of the expression
case (Bar True) of ~(Foo x) -> show $ typeOf x then?
Hopefully not "Bool". One might say that the expression ought to bottom out. However, what reason one may give for that outcome? The only binding in the above expression is of 'x', whose value is never demanded. Indeed, "show $ typeOf (undefined :: ())" yields the non-bottom value "()".
There is also the implicit dictionary argument of typeOf, and this is demanded, so the value should be _|_.