[fix #215] handle automatic projections from let pattern of tuples

[flupe]

The issue was coming from Agda inlining let bindings. This translation leaked our encoding for tuples.

The example from #215 now gets compiled properly, but:

• n-uples with n > 2 pattern-matched inside lets would still get compiled incorrectly because there is in fact no proper way to inline the let using projections (unless we also generate projections on the fly, like \(_, _, x) -> x).

  So let (x, y, z) = e in z would still compile to the incorrect snd (snd e). We probably need a reliable way to prevent such use of pattern-matching on let for n-uples, doesn't have to be now.

  We could compute the length of projection chains of Pair.fst and Pair.snd in the terms we get, the only issue being that the resulting error would not point to the location of the let, only the location of the problematic variable.

• The projection fst and snd of Pair probably shouldn't get exported from Haskell.Prim.Tuple so as to enforce that the only way they pop up in terms is through inlining of let bindings.

Feedback welcome.

[jespercockx]

n-uples with n > 2 pattern-matched inside lets would still get compiled incorrectly because there is in fact no proper way to inline the let using projections (unless we also generate projections on the fly, like (_, _, x) -> x).

As we discussed, maybe we should just bite the bullet and define n-tuples for n =< 10 by hand.