Bad resugaring of operator when implicits are on

[mtzguido]

module BadResugaredOp

#set-options "--print_implicits"

let op_Plus #a (x y : a) = (x,y)

let _ = 1 + 1

$ ../pristine/bin/fstar.exe BadResugaredOp.fst --dump_module BadResugaredOp
[...]
Exports: [
#set-options "--print_implicits"
let op_Plus #a x y = FStar.Pervasives.Native.Mktuple2 #a #a x y
private
let _ = (Prims.int + 1) 1
]

Verified module: BadResugaredOp
All verification conditions discharged successfully

The (Prims.int + 1) is bogus