arthuraa / extructures

Finite sets and maps for Coq with extensional equality
MIT License
29 stars 6 forks source link

ssreflect.phant error #10

Closed jgrosso closed 3 years ago

jgrosso commented 3 years ago

Disclaimer: I'm relatively new to Coq (and haven't yet learned the details of mathcomp or SSReflect)—as such, if this turns out to be an issue on my end, I apologize in advance.

I'm getting an error when trying to create an alias for a specific type of finite map:

From extructures Require Import fmap.

(* I'm using [nat] here as an example; I've tried other types too, but unfortunately to no avail. *)
Definition type_substitution : Type := {fmap nat -> nat}.

(* Error:
The term "ssreflect.Phant (nat -> nat)" has type "ssreflect.phant (nat -> nat)"
while it is expected to have type "ssreflect.phant (?T -> ?S)".
*)

Environment: coq 8.13.1, coq-mathcomp-ssreflect 1.12.0, coq-deriving 0.1.0, coq-extructures 0.2.2.

arthuraa commented 3 years ago

Fix

From extructures Require Import ord fmap.
Definition type_substitution : Type := {fmap nat -> nat}.

Explanation

The fmap type requires the keys of the map to be sorted according to some order relation. This order relation is given by an instance of the ord class. Basic types like nat are already declared as instances of ord, but you need to import the ord module to make them visible. (You can also define ord instances for your own data types, if you need to -- check ord.v for some examples on how to do this.)

More generally, when using some MathComp class (eqType, choiceType, etc.), directly or indirectly, it is a good idea to import the module where it is defined. This will bring into scope many instances for common types, avoiding the error that you saw.

Hope this helps!

jgrosso commented 3 years ago

I could have sworn I tried that :-P So sorry for the bother, and thank you for the help!