Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error in type reflection #5

Open
ejgallego opened this issue Mar 14, 2024 · 0 comments
Open

Error in type reflection #5

ejgallego opened this issue Mar 14, 2024 · 0 comments

Comments

@ejgallego
Copy link

Dear @thierry-martinez ,

I've seen that the recommended setup produces some type errors often; most of them seem like maybe a one-off typo somewhere?

For example, given this interface:

(* Petanque.Agent *)

module State : sig
  type t = int

  val goals : t -> string option
end

module Start_error : sig
  type t = string
end

(** [start uri thm] start a new proof for theorem [thm] in file
    [uri]. Note that uri is expected to be in the [file:///]
    format. *)
val start : uri:string -> thm:string -> (State.t, Start_error.t) Result.t

module Run_error : sig
  type t = string
end

(** [run_tac st tac] tries to run [tac] over state [st] *)
val run_tac : st:State.t -> tac:string -> (State.t, Run_error.t) Result.t

We get on import:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
ImportError: File "_none_", line 1:
Error: This expression has type
         (Petanque.Agent.State.t, Petanque.Agent.Start_error.t) Result.t =
           (Petanque.Agent.State.t, Petanque.Agent.Start_error.t) result
       but an expression was expected of type (string, string) result
       Type Petanque.Agent.State.t = int is not compatible with type string 

Thanks a lot for this package and for the help!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant