[Bug ada/113037] New: GNAT BUG DETECTED when instantiating generic package with Type_Invariant on a type derived from a generic type

[saulius.grazulis at bti dot vu.lt via Gcc-bugs]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=113037

            Bug ID: 113037
           Summary: GNAT BUG DETECTED when instantiating generic package
                    with Type_Invariant on a type derived from a generic
                    type
           Product: gcc
           Version: 14.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: ada
          Assignee: unassigned at gcc dot gnu.org
          Reporter: saulius.grazulis at bti dot vu.lt
                CC: dkm at gcc dot gnu.org
  Target Milestone: ---

Created attachment 56890
  --> https://gcc.gnu.org/bugzilla/attachment.cgi?id=56890&action=edit
A Minimal Working Example, for 'gnatchop'

When a generic package with a Type_Invariant on a declared type is
instantiated, a GNAT BUG DETECTED box is triggered:

+ gcc -v
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/home/saulius/install/gcc/gcc-13.2.0-git-master-d1647917006/libexec/gcc/x86_64-pc-linux-gnu/14.0.0/lto-wrapper
Target: x86_64-pc-linux-gnu
Configured with: ../gcc/configure
--prefix=/home/saulius/install/gcc/gcc-13.2.0-git-master-d1647917006
--enable-languages=c,c++,ada,fortran --disable-multilib --enable-shared
--enable-threads=posix --enable-__cxa_atexit --enable-clocale=gnu
Thread model: posix
Supported LTO compression algorithms: zlib
gcc version 14.0.0 20231214 (experimental) (GCC) 
+ uname -a
Linux tasmanijos-velnias 5.4.0-167-generic #184-Ubuntu SMP Tue Oct 31 09:21:49
UTC 2023 x86_64 x86_64 x86_64 GNU/Linux
+ lsb_release -a
No LSB modules are available.
Distributor ID: Linuxmint
Description:    Linux Mint 20.1
Release:        20.1
Codename:       ulyssa
+ gnatmake extended_euklidean_gen
gcc -c extended_euklidean_gen.adb
+===========================GNAT BUG DETECTED==============================+
| 14.0.0 20231214 (experimental) (x86_64-pc-linux-gnu) Assert_Failure
exp_util.adb:3693|
| Error detected at extended_euklidean_generic.ads:15:4
[extended_euklidean_gen.adb:12:4]|
| Compiling extended_euklidean_gen.adb                                     |
| Please submit a bug report; see https://gcc.gnu.org/bugs/ .              |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

extended_euklidean_gen.adb
extended_euklidean_generic.ads

compilation abandoned
gnatmake: "extended_euklidean_gen.adb" compilation error

$ cat extended_euklidean_gen.adb
pragma Ada_2022;

with Ada.Numerics.Big_Numbers.Big_Integers;
use Ada.Numerics.Big_Numbers.Big_Integers;

with Extended_Euklidean_Generic;

procedure Extended_Euklidean_Gen is

   type Number is new Big_Integer;

   package Extended_Euklidean is 
      new Extended_Euklidean_Generic (Number, 0, 1);

begin
   null;
end Extended_Euklidean_Gen;

$ cat extended_euklidean_generic.ads
generic
   type Number is private;
   Zero : Number;
   Unity : Number;
   with function "-" (A, B : Number) return Number is <>;
   with function ">" (A, B : Number) return Boolean is <>;

package Extended_Euklidean_Generic is

   type Positive_Number is new Number
     with Type_Invariant => Number (Positive_Number) > Zero;

   procedure GCD
     ( 
      A, B : in  Positive_Number; -- original numbers
      D    : out Positive_Number; -- GCD of the two numbers A and B
      M, N : out Number           -- Bézout coefficients: A * M + B * N = D
     );   

end Extended_Euklidean_Generic;

$ cat extended_euklidean_generic.adb
package body Extended_Euklidean_Generic is

   -- Test implementaion of the Extended Euclidean Algorithm.
   -- URL: https://en.wikipedia.org/wiki/Extended_Euclidean_algorithm

   procedure GCD
     ( 
      A, B : in  Positive_Number; -- original numbers
      D    : out Positive_Number; -- GCD of the two numbers A and B
      M, N : out Number           -- Bézout coefficients: A * M + B * N = D
     ) is
      P : Number := Unity; -- X = P*A + Q*B at any point
      Q : Number := Zero;
      S : Number := Zero;  -- Y = S*A + T*B at any point
      T : Number := Unity;
      X : Positive_Number := A; 
      Y : Positive_Number := B;
   begin
      while X /= Y loop
         if X > Y then
            X := X - Y;
            P := P - S;
            Q := Q - T;
         else
            Y := Y - X;
            S := S - P;
            T := T - Q;
         end if;
      end loop;
      D := X;
      M := P;
      N := Q;
      -- The naive computation of the N value can overflow:
      -- N := (X - P*A) / B;
      pragma Assert (X = Y);
      -- pragma Assert 
      --   (
      --    Long_Integer (D) =
      --      Long_Integer (A) * Long_Integer (M) + 
      --      Long_Integer (B) * Long_Integer (N)
      --   );
   end GCD;

end Extended_Euklidean_Generic;