Skip to content
  • Simon Peyton Jones's avatar
    [project @ 2004-10-04 15:51:00 by simonpj] · f469905a
    Simon Peyton Jones authored
    ------------------------------------
    	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.
    f469905a