Inferring implicits arguments in return position (and error localization)

[nikswamy]

fn initialize_context' (sid:sid_t) (uds:A.larray U8.t (US.v uds_len)) 
                       (#p:perm) (#uds_bytes:Ghost.erased (Seq.seq U8.t))
  requires A.pts_to uds #p uds_bytes
  returns _:option ctxt_hndl_t
  ensures A.pts_to uds #p uds_bytes
{
  rewrite emp as (session_state_perm InUse);
  let st = take_session_state sid InUse;
  match st 
  {
    None ->
    {
      with s. rewrite (session_state_perm s) as emp;
      None //#ctxt_hndl_t
    }
    
    Some st ->
    {
      admit()
    }
  }
}

• We should pass the expected type from the annotation to F* when elaborating the returned None . Currently, we fail to infer that instantiation and report a peroperly localized error ( - Could not infer implicit arguments in None).
• But, we also report an unresolved (universe) uvar in deep compress blaming the entire definition, which masks the localized error above.