[Haskell-cafe] Problematic irrefutable pattern matching of existentials

[oleg at pobox.com]

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 "()". 

One may claim that the existential pattern match also binds an
implicit dictionary argument, which is demanded above. That
explanation is quite unsatisfactory, because it breaks the abstraction
of type classes. The dictionary passing is merely an _implementation
technique_ for type classes. Furthermore, it is not the only 
implementation technique: JHC and Chameleon, for example, use
intensional type analysis to implement typeclasses.


On a different note, Conor McBride wrote:
> It isn't necessary to perform
> constructor discrimination when it's statically known that exactly one
> constructor is possible, so those patterns can always be made
> irrefutable, with matching replaced by projection.

that is, in essence, the idea behind 
	`Tagless Staged Interpreters for Typed Languages'
	Pasalic, Taha, Sheard: ICFP02
It is well-written paper, with an excellent introduction and
motivation.

Incidentally, one can write their tagless staged interpreter in Haskell
as it is. No dependent types are necessary.