Typing error when mixing dependent types and implicit types

[klinvill]

I'm not sure exactly why I'm seeing the error that I am, but I seem to be seeing an error when trying to say that a function with dependently typed arguments is of the same type as a function of the same shape with implicitly typed arguments (code below). It type checks ok if I change the dependently typed arguments to be of a static type. I get a different (slightly more informative) error message if I move the refinement into my functions argument.

It becomes even more informative if I print implicits, but it looks like the implicit type inferred is the unrefined type. The error message I get with print implicits (using the explicit refinement) is: (Error 19) Subtyping check failed; expected type protocol #nat #bytes #bytes; got type n: nat -> m: bytes{eq2 #(x: int{UInt.size x 32 \/ b2t (x >= 0)}) (length m) n} -> Prims.Tot (r: bytes{eq2 #(x: int{UInt.size x 32 \/ b2t (x >= 0)}) (length r) n}); The SMT solver could not prove the query. Use --query_stats for more details.

Does anyone know why I'm seeing these errors? Does the Type type not include refinements? Is there a way I need to change either my protocol type or my test_proto spec to make it type check as a protocol using dependent types?

module Test

open FStar.Bytes


type protocol (#args_1_type: Type) (#args_2_type: Type) (#result_type: Type) =
  args_1_type -> args_2_type -> result_type

// Using my dependent type here (lbytes n) results in the error: "(*?u11*) _ is not equal to the expected type n"
assume val test_proto (n: nat) (m: lbytes n) : Tot (lbytes n)

// Whereas if I just use the non-dependent type bytes, it type checks ok
//assume val test_proto (n: nat) (m: bytes) : Tot bytes

// If I make the refinement explicit here, I get a new error message that states that the SMT solver can't prove that test_proto is of type protocol
//assume val test_proto (n: nat) (m: bytes{length m == n}) : Tot (r: bytes{length r == n})

#push-options "--print_implicits"
let test_proto_wrapper : protocol = 
  test_proto
#pop-options

[aseemr]

Hi @klinvill:

The issue here is that while test_proto has a dependent type, the type protocol is not dependent. If we change the protocol type to:

type protocol (#args_1_type: Type) (#args_2_type: args_1_type → Type) (#result_type: args_1_type → Type) =
  n:args_1_type → args_2_type n → result_type n

to reflect the dependence of the type of the second argument and return type on the first argument, then it checks out. The refinement version also works with this.

(The error message (*?u11*) _ is not equal to the expected type n could be better.)

[klinvill]

Awesome, thanks Aseem! It looks like that type works even for types that aren't dependent (like below).

Is there a way to debug what that error message means if I see this elsewhere? Like a command line flag that would expand out what ?u11 is?

// Non-dependent type, but also type-checks with Aseem's suggested protocol type
assume val test_proto_2 (m: bytes) : Tot (bytes)

let test_proto_2_wrapper : protocol = 
  fun (_: unit) (m: bytes) ->
    test_proto_2 m