"Unmatched actual" in instantiation of a generic package

General
1

I’m trying to instantiate a generic hash map package in SPARK. The instantiation compiles as legal Ada, but SPARK is giving me the additional error

error: unmatched actual in instantiation of “Formal_Hashed_Maps” declared at a-cfhama.ads:33
package Boolean_Maps is new Ada.Containers.Formal_Hashed_Maps(Module_ID_Type, Boolean, Hash_Func, Equivalent_Key, Standard.“=”);

with a red underline under Module_ID_Type.

Module_ID_Type is defined in a non-generic package as type Module_ID_Type is new Positive range 1..255. I’m using the GNAT compiler. The code compiles and works as expected.

What does this error mean?

Thanks.

2

It seems you’re using incompatible versions of GNAT and GNATprove. With the FSF 12.1 release that you can install directly or through Alire, the following code is accepted by both GNAT and GNATprove:

with Ada.Containers; use Ada.Containers;
with Ada.Containers.Formal_Hashed_Maps;

package Hashmap  with SPARK_Mode Is
   type Module_ID_Type is new Positive range 1..255;
   function Hash_Func (X : Module_ID_Type) return Hash_Type is (0);
   function Equivalent_Key (X, Y : Module_ID_Type) return Boolean is (True);
   package Boolean_Maps is new Ada.Containers.Formal_Hashed_Maps(Module_ID_Type, Boolean, Hash_Func, Equivalent_Key, Standard."=");
end;