I guess there's no way to avoid this problem if the type you're eliminating is a record though, since pattern matching is desugared to projections? If so it'd explain why in some cases I get a big performance improvement by using a custom record type instead of just nesting sigmas. - Andrea