
" Pattern synonym declarations can only occur in the top level of a module. In particular, they are not allowed as local definitions. " says the User Guide. And the 2016 paper says likewise. But there's no explanation why. PattSyns are not necessarily declared in the same module as the underlying Datatype, so there can be a region of scope with the data constructor but without the PattSyn. If PattSyns are declared in the same module as their datatype, you can export the PattSyns but not the data constructors -- indeed that's a common way to keep the Datatype implementation abstract. Or (unusually) you can export the data constructors but not PattSyns. So there seems to be no close tie-up of Datatype/constructors and PattSyns. Then why couldn't a PattSyn be declared in local scope only? The builder function behind a PattSyn is just like any other function, so could be local(?) The paper's Implementation section 7 says the matcher also is an "ordinary function". Relatedly, PattSyns can in effect be overloaded: define the PattSyn in terms of a ViewPattern function. That can be a method of some class. Then why not more directly declare PattSyns within a class? [I have a feeling I answered a similar question on some forum, saying the PattSyn has to follow around its data constructors, like a dog on a lead. Can't find that now. If that was me, I apologise and withdraw.] AntC