Ill-typed VC

[mtzguido]

open FStar.Exn

exception DivZero

let test0 (#a:Type u#0) () : Exn a (requires True) (ensures fun (r : result a) -> r == E DivZero) =
  FStar.Exn.raise DivZero;
  ()

let test1 (#a:Type u#1) () : Exn a (requires True) (ensures fun (r : result a) -> r == E DivZero) =
  FStar.Exn.raise DivZero;
  ()

The second function fails. Turning on enough debugging shows:

Encoding query formula {: forall (a: Type u#1)
  (_: Prims.unit)
  (p: FStar.Pervasives.ex_post u#1 a)
  (_:
  _:
  Prims.unit
    { forall (r: FStar.Pervasives.result u#1 a).
        Prims.eq2 u#1
          #(FStar.Pervasives.result u#1 a)
          r
          (FStar.Pervasives.E u#1 #a Clase08.Eff.DivZero) ==>
        p r })
  (r: FStar.Pervasives.result u#0 Prims.unit)
  (_:
  _:
  Prims.unit
    { Prims.eq2 u#0
        #(FStar.Pervasives.result u#0 Prims.unit)
        r
        (FStar.Pervasives.E u#0 #Prims.unit Clase08.Eff.DivZero) })
  (_:
  _:
  Prims.unit
    { ~(exists (ra1: Prims.unit).
          Prims.eq2 u#0
            #(FStar.Pervasives.result u#0 Prims.unit)
            r
            (FStar.Pervasives.V u#0 #Prims.unit ra1)) })
  (e: Prims.exn)
  (_:
  _:
  Prims.unit
    { Prims.eq2 u#0
        #(FStar.Pervasives.result u#0 Prims.unit)
        r
        (FStar.Pervasives.E u#0 #Prims.unit e) }).
  Prims.auto_squash u#0 (p (FStar.Pervasives.E u#0 #a e))  // !!!!!!
} Done encoding
Z3 says: unknown
Z3 says: unknown
Z3 says: unknown
Z3 says: unknown
* Error 19 at Clase08.Eff.fst(12,2-13,4):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also /home/guido/r/fstar/pristine/stage2/out/lib/fstar/ulib/FStar.Pervasives.fsti(403,19-403,31)

Note the ill-typed application of p in the goal: the u#0 should be u#1.