bad error: `Expected type Type0, got type Type0`

[mtzguido]

An example from @msprotz (use --include karamel/krmllib), not minimized yet

module J

module B = LowStar.Buffer
module U32 = FStar.UInt32
module S = FStar.Seq

open FStar.HyperStack.ST

let rec sum (s: S.seq U32.t): Ghost nat
  (requires True)
  (ensures fun _ -> True)
  (decreases S.length s)
= if S.eq s S.empty then 0 else U32.v (S.head s) + sum (S.tail s)

#set-options "--print_implicits --print_universes --print_full_names"

val sum_low2 (dst: B.buffer U32.t { B.len dst == 0ul }) (b: B.buffer U32.t) (len: U32.t { len == B.len b }): Stack bool
  (requires fun h0 ->
    B.live h0 b /\ B.live h0 dst)
  (ensures fun h0 r h1 ->
    let s = B.as_seq h0 b in
    if r then
      (* overflowed *)
      sum s > FStar.UInt.max_int 32 /\ B.(modifies loc_none h0 h1)
    else
      U32.v (B.get h1 dst 0) == sum s /\ B.(modifies (loc_buffer dst) h0 h1))

let sum_low2 = magic ()

* Error 19 at J.fst(146,25-152,76):
  - Subtyping check failed
  - Expected type Type0 got type Type0
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also LowStar.Monotonic.Buffer.fsti(247,21-247,35)

[mtzguido]

Minimized:

val sum_low2 () : Pure unit
  (requires True)
  (ensures  fun _ -> assert False; True)
let sum_low2 = magic ()