[project @ 2004-10-04 15:51:00 by simonpj]

[project @ 2004-10-04 15:51:00 by simonpj]
------------------------------------
	Part-fix an awkward interaction
	between case-of-case and GADTs
	------------------------------------

Consider
	data T a where
	  MkT :: a -> b -> T a

	f = /\a. \(w::a).
	   case (case ...) of
		  MkT a' b (p::a') (q::b) -> [p,w]

The danger is that we'll make a join point

	j a' p = [p,w]

and that's ill-typed, because (p::a') but (w::a).

Solution so far: don't abstract over a', because the type refinement
maps [a' -> a] .  Ultimately that won't work when real refinement goes on.

Then we must abstract over any refined free variables.  Hmm.  Maybe we
could just abstract over *all* free variables, thereby lambda-lifting
the join point?   We should try this.