[Haskell-cafe] Re: Problematic irrefutable pattern matching of existentials

[Ross Paterson]

On Sun, Oct 01, 2006 at 08:05:15PM -0700, oleg at 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 _|_.