-
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