Very strange behavior of default effects

[jkzinzindohoue]

I was trying to push forward the tutorial with universes but I do not understand the following behaviors, which I believe is a bug, maybe related to #517:

module Test

val null: unit -> All unit
  (requires (fun h -> True))
  (ensures  (fun h r h' -> True))
let null () = ()

(* Fails *)
(* let test0 = assert(false); null () *)

(* Succeeds *)
let test1 () = assert(false); null ()

(* Succeeds *)
let test2 (u:unit) = assert(false); null ()

(* Fails *)
(* let test3 (u:unit) : All unit (requires (fun h -> True)) (ensures (fun h r h' -> True)) = assert(false); null() *)

(* Succeeds *)
let test3' () : All unit (requires (fun h -> True)) (ensures (fun h r h' -> True)) = assert(false); null()

(* Succeeds *)
let test4 (u:unit) : ML unit = assert(false); null()

(* Fails *)
(* let test5 (u:unit) : ML unit = assert(false) *)

val null2: unit -> Div unit
  (requires (True))
  (ensures  (fun r -> True))
let null2 () = ()

(* Succeeds *)
let test6 (u:unit) : ML unit = assert(false); null2()

val null3: unit -> Pure unit
  (requires (True))
  (ensures  (fun r -> True))
let null3 () = ()

(* Fails *)
(* let test7 (u:unit) : ML unit = assert(false); null3() *)

It goes through in many cases, although the call is after the assert(false). And All and ML seem to have different behaviours. And the presence/absence of the binder has some importance too.

[s-zanella]

See also #581 for a discussion on default effects

[catalin-hritcu]

@nikswamy just fixed this