Invalid pattern matching translation on nullary constructors

[4ever2]

In some cases pattern matching gets "optimized" during translation in cases that match on nullary constructors and return the same constructor. I.e. we get

match x
  case CONSTRUCTOR1 -> x

rather than

match x 
  case CONSTRUCTOR1 -> CONSTRUCTOR1

This is problematic for the typed targets if the inductive type contains type variables, since the constructor matched and the constructor returned could have different type variables.
This only seems to happen in some cases, for example it happens in the map example but not in the double example.

map : {A B : Set} -> (A → B) → List A → List B
map f empty = empty
...

double : Nat → Nat
double zero = zero
...