dm4f: Cannot define continuations

[mtzguido]

The following code

module Bug713

let r = int
let cont (a:Type0) : Type = (a -> M r) -> M r

let return (a:Type0) (x:a) (p : a -> M r) : M r = p x

let bind (a:Type0) (b:Type0)
         (m : cont a) (f : a -> Tot (cont b)) (k : b -> M r) : M r =
         m (fun (x:a) -> f x k)

reifiable new_effect_for_free {
  CONT: Type -> Effect
  with repr = cont
     ; return = return
     ; bind = bind
}

Fails with

Error: Tm_ascribed is outside of the definition language: ((uu___:(uu___:a -> M (Prims.int)) -> M (Prims.int)) : Type)

Without annotating the type of cont, the error one gets is:

unknown(0,0-0,0) : Error
Variable "uu___#1870" not found

which might be a separate problem.

[msprotz]

I started looking at this specific example and then realized that you had made further progress on your branch. In particular, I suspect this example is broken because you did not provide M-style return type annotations for your combinators.

Can you let me know what the current status of this bug is?

[catalin-hritcu]

Here's the current status (pre artifact evaluation). With let mm:

[debug] mm#3033 is NOT a monadic let-binding
[debug] type of [head] is (uu___:(uu___:a -> M (Type)) -> M (Type))
[debug] length binders=1, length args=1
[debug]: final type of application is M[Type]
[debug] type of [head] is (uu___:a -> Tot (uu___:(uu___:b -> M (Type)) -> M (Type)))
[debug] length binders=2, length args=1
[debug]: final type of application is N[(uu___:(uu___:b -> M (Type)) -> M (Type))]
[debug] fx#3037 is NOT a monadic let-binding
[debug] type of [head] is (uu___:(uu___:b -> M (Type)) -> M (Type))
[debug] length binders=1, length args=1
[debug]: final type of application is M[Type]
./examples/bug-reports/bug715.fst(13,20-13,21) : Error
Expected expression of type "(uu___:(uu___:a -> M (Type)) -> M (Type))";
got expression "m" of type "(uu___:(uu___:a -> uu___:(uu___:Type -> Type) -> Type) -> uu___:(uu___:Type -> Type) -> Type)"

without let mm:

[debug] type of [head] is (uu___:(uu___:a -> M (Type)) -> M (Type))
[debug] length binders=1, length args=1
[debug]: final type of application is M[Type]
[debug] type of [head] is (uu___:a -> Tot (uu___:(uu___:b -> M (Type)) -> M (Type)))
[debug] length binders=2, length args=2
[debug]: final type of application is M[Type]
unknown(0,0-0,0) : Error
Variable "uu___#2279" not found

[msprotz]

Correct, this is the current status. Not sure I'll have the bandwidth to debug this before the artifact evaluation deadline, so I'm going to try to make the lift effect work instead before I go to bed.

[kyoDralliam]

Now working if you write it the exact way FStar expects it... There are still some issues if you don't add enough type annotations.