Partial `let` is translated to partial pattern match

[antalsz]

If I translate

module TestMatch where

bad_let :: [a] -> a
bad_let xs = let (_,[x]) = (xs,xs) in x

bad_fun :: [a] -> a
bad_fun xs = let [x] = xs in x

good_match :: [a] -> a
good_match [x] = x

with

stack exec -- hs-to-coq --iface-dir base --edits base/edits TestMatch.hs

I get (reordered)

Definition bad_let {a} : list a -> a :=
  fun xs => let 'pair _ (cons x nil) := pair xs xs in x.

Definition bad_fun {a} : list a -> a :=
  fun '(cons x nil) => x.

Definition good_match {a} : list a -> a :=
  fun arg_0__ =>
    match arg_0__ with
    | cons x nil => x
    | _ => GHC.Err.patternFailure
    end.

The first two definitions translate to failing incomplete pattern matches (I believe bad_fun is still fun followed by match, just with sugar on the output), whereas the third does not.

The expected behavior is that all the functions look like good_match.