FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.7k stars 234 forks source link

Bad expected type on typeclass constraint #3498

Open mtzguido opened 1 month ago

mtzguido commented 1 month ago
module X

class usage_type (s:string) = {
  data_t: Type0;
  ps_data_t: data_t;
}

val get_data: s:string -> {|ut:usage_type s|} -> ut.data_t
let get_data s #ut = ut.ps_data_t

instance usage_string : usage_type "TLS.SigKey" = {
  data_t = int;
  ps_data_t = 42;
}

let test () : int =
  get_data "TLS.SigKey" #_

Minimized from an example from @TWal, somehow we get the error:

* Error 228 at X.fst(16,0-17,26):
  - Could not solve typeclass constraint `Type0`
  - See also FStar.Tactics.Typeclasses.fst(297,6-300,7)

1 error was reported (see above)

at the entrypoint of tcresolve (this should be clearer btw, the tactics aborts quickly since the goal is not a typeclass constraint, and that should be reflected in the error). Somehow the #_ was expected to have type Type0, instead of usage_type "TLS.SigKey". This incantation makes it work:

let test () : int =
  get_data "TLS.SigKey" #((_ by (FStar.Tactics.Typeclasses.tcresolve ())) <: usage_type "TLS.SigKey")