Sorry, I forgot to enclose the message I promised. Here it is. -----Original Message----- From: Simon Peyton-Jones Sent: 04 November 2002 14:20 To: 'Tim Sheard (Tim Sheard)' Cc: 'Ian Lynagh'; 'Oege de Moor (Oege de Moor)'; Simon Peyton-Jones Subject: Patterns and types Tim We claim to allow you to write splices in (a) types and (b) patterns. I'm very dubious about (b). Consider] x = 4 y :: Patt y = [p| ... |] f $y = x Question: where is x bound? It looks as though x can be bound by the spliced-in pattern or by the top-level binding. You can't tell without knowing what $y expands to. We argue in our paper against non-top-level declaration splices because that would lead to ambiguity of exactly this sort. It turns out that it's very inconvenient to implement pattern splices in GHC, for exactly this reason. We can't figure out the binding structure till we expand the splice. We can't expand the splice till typechecking time. But the renamer currently fixes the binding structure before type checking. Changing this would be a big upheaval. Conclusion: pattern splices are hard to implement, and dubious from a programming point of view. I propose to drop them, for now at least. Type splices have some similar echoes. Consider y :: Type y = [t| a -> a |] f :: $y What is f polymorphic in? The trouble concerns Haskell's implicit quantification. I guess there are three possibilities: a) $y expands to "a -> a", and that is implicitly universally quantified to "forall a. a->a". b) The implicit quantification happens at the [t| ...|] brackets, so that $y expands to "forall a. a->a" c) $y expands to "a -> a" with no implicit quantification anywhere. I'm pretty sure that we should adopt (b). After all, we want a lexical-scoping rule for TH, so we have to say where 'a' is bound. That would still in principle allow y :: Type y = return (Tvar "a" `Arrow` Tvar "a") Since it's the renamer that does implicit quantification, it'd be quite awkward to make the implicit quantification at the splice site "see" the free variables 'a'. The link with the pattern stuff is this. If you see f :: $y -> b then what are the implicit for-alls? My answer: the implicit for-alls are just for "b", not for any free vars of $y. Simon