Problems in k_foralle: #1 Unresolved implicit argument

[catalin-hritcu]

This problem appears in micro-fstar.fst in the k_foralle proof. After a bit of local simplification the code looks like this:

(* This takes forever to typecheck and fails without the assert;
   plus this fails without the explicit type annotation on k' in KTApp
   (Unresolved implicit argument). *)
val k_foralle : #g:env -> #t1:typ -> #t2:typ ->
                =hk1:kinding g t1 KType ->
                =hk2:kinding (eextend t1 g) t2 KType ->
                Tot (kinding g (TTApp (TConst TcForallE) t1)
                               (KKArr (KTArr t1 KType) KType))
let k_foralle g t1 t2 hk1 hk2 =
  let gwf = kinding_ewf hk1 in
  (* assert(KKArr (KTArr t1 KType) KType =  *)
  (*        ktsubst_beta t1 (KKArr (KTArr (TVar 0) KType) KType)); *)
  KTApp (KKArr (KTArr (TVar 0) KType) KType) (KConst TcForallE gwf) hk1 (magic())

I've put a lot of effort into reproducing this in a smaller setting, but so far without any success. Basically the same code in bug237.fst works just fine.

[catalin-hritcu]

The minimal counterexample for this looks like this:

type knd =
  | KType : knd
  | KKArr : knd -> knd

val ktsubst_beta : knd -> Tot knd
let ktsubst_beta k = k

val tconsts : unit -> Tot knd
let tconsts () = KKArr KType

type kinding : k:knd -> Type =
| KConst : kinding (tconsts())
| KTApp : #k':knd -> hk1:kinding (KKArr k') -> kinding (ktsubst_beta k')

val k_foralle : u:unit -> Tot (kinding KType)
let k_foralle () =  KTApp (* KType *) KConst
(* Problem: without the annotation and the explicit k' in KTApp
   this causes "Unresolved implicit argument" *)

[nikswamy]

cf #227

As mentioned there, we are not yet doing full reduction, in particular, no delta steps when trying to unify expressions.

I've been putting off enhancing the expression reducer ... I guess I should just do it.