Eager or lazy instantiation of implicits?

[msprotz]

Trying to use typeclasses a little... here is my minimal repro:

class block (index: Type0) = {
  // Astract footprint.
  state: index -> Type0;
  footprint: #i:index -> h:HS.mem -> s:state i -> B.loc;
}

trying to process this in the interactive mode gives me:

(Error) Failed to resolve implicit argument of type 'index' in the type of footprint ((#[FStar.Tactics.Typeclasses.tcresolve ()] d: Hacl.Streaming.Interface.block index)
  -> Prims.Tot
    (h: FStar.Monotonic.HyperStack.mem -> s: Mkblock?.state d (*?u10*) _
        -> Prims.Tot LowStar.Monotonic.Buffer.loc))

am I misusing the type class feature?

Thanks,

Jonathan

[mtzguido]

This is because we generate roughly the following for the footprint method:

let footprint' = fun (index:Type0) (#[tcresolve ()] d : block index) -> d.footprint

And it seems F* attempts to instantiate the implicit for d.footprint (the #i:index) eagerly. Adding an annotation would fix this, but the dependency makes it awkward. The underlying issue is this, I think:

assume val f : unit -> #i:int -> int

let g = f

let h () = f ()

g succeeds but h fails with Failed to resolve implicit argument ?3 of type int introduced for Instantiation of implicit argument. Possibly related to #1965.

[mtzguido]

EDIT: nevermind, that was stupid since then your typeclass is useless. I'm looking at fixing the instantiation code for this.

[mtzguido]

This should now be fixed in master, I did add the annotation for the methods since it wasn't as hard as I thought. Keeping this open since I think the instantiation behaviour is wrong (and I have some work on that too, but it'll probably take a while).