[Haskell-cafe] conflicting variable definitions in pattern

[wren ng thornton]

Conor McBride wrote:
> Rumblings about funny termination behaviour, equality
> for functions, and the complexity of unification (which
> isn't the proposal anyway)

But unification is what you get by adding non-linearity. Sure, all terms 
are ground; would you prefer I said "testing for membership in an 
element of the RATEG class"?


For more ickiness about RATEG, it's not closed under compliment and the 
emptiness problem is undecidable (so dead code elimination can't always 
work). Even restricting to the closed subset (aka "tree-automata with 
(dis-)equality constraints") leaves emptiness undecidable, though there 
are a couple still more restricted classes that are decidable.

cf ch.4 of TATA <http://tata.gforge.inria.fr/>

-- 
Live well,
~wren