Type inference for int constants worse in pulse functions

[JonasAlaif]

The following snippet highlights the issue:

open Pulse.Lib.Pervasives

#lang-pulse

val rnat (p: FStar.Seq.seq nat): slprop

let works = rnat seq![0]

fn foo_works ()
  requires emp
  ensures  rnat seq![0 <: nat]

fn foo ()
  requires emp
  ensures  rnat seq![0]

I get a Assertion failed error (also not a very intuitive error, e.g. seq int is not a subtype of seq nat would be better). The error is due to seq![0] typing as FStar.Seq.seq int in the Pulse postcondition (this also happens in the body of a pulse function).

This happens even when using seq![x; x; 0] with x: nat or when writing out the seq! as conss. The surprising thing to me is that it works in the F* code but not pulse.