Mixing effects and dependent tuple types

[landonf]

Originally ran into this trying to mix the Stack effect with a dependent record type; narrowed the reproduction case down to:

type pos = (len:nat & (n:nat { n <= len }))

let id (p:pos): Div pos (requires (True)) (ensures (fun _ -> True)) = p

let get_offset (p:pos) = Mkdtuple2?._2 (id p)

Fails with:

DepTypeBug.fst(8,2-8,22): (Error 54) (*?u12*) _ is not equal to the expected type b

I'm required to state: Not a Contribution.

[catalin-hritcu]

~Looks like a bug to me~. Here is a slightly simpler reproduction:

type ints = _:int & int
let id (p:ints) : Dv ints = p
let get_offset (p:ints) : Dv int = dsnd (id p)

This still fails even when fully annotated:

let get_offset (p:ints) : Dv int = dsnd u#0 u#0 #int #(fun _ -> int) (id p)

It works again when changing the effect of id from Dv to Tot.

[catalin-hritcu]

Actually, nevermind the bug part, this might be an inherent limitation to the way effects and dependent types are mixed in F*. In particular, the type of dsnd (id p) is (fun _ -> int) (dfst (id p)), which depending on the evaluation strategy may require evaluating id p, which is potentially divergent.

The rule of thumb in F is that types can't depend on effectful / divergent computations. So while the error message should for sure be better, it could be that such programs have to be rejected in F.

[landonf]

Given that first binding the tuple to a temporary variable works, e.g. let p = id p in dsnd p; shouldn't that be equivalent to dsnd (id p) after (beta?) reduction?

let get_offset (p:ints) : Dv int = let p = id p in dsnd p

[msprotz]

I chatted about this with @nikswamy the other day. It has to do with i) a bad error message and ii) an actual issue with a type variable that would escape its scope, hence requiring you to hoist the argument as a let-binding.

The conclusion was that improving the error message was de rigueur

[mtzguido]

The errors are currently better, though not great.

- Bound variable
  'projectee#5'
  escapes because of impure applications in the type of
  'Mkdtuple2?._2'
- Add explicit let-bindings to avoid this

and

- Bound variable
  't#10747'
  escapes because of impure applications in the type of
  'dsnd'
- Add explicit let-bindings to avoid this