Derivation fails when adding S to an LTE parameter due to unnecessary generators with extraneous given parameters being derived

[elkcl]

Package collection used: nightly-250207

Derivation of genX fails here:

public export
record FI n where
    constructor MkFI
    v : Nat
    p : LTE v n

namespace VN
    public export
    data VN : Nat -> Type where
        Nil : VN 0
        (::) : Nat -> VN n -> VN (S n)

namespace HVF
    public export
    data HVF : (k : Nat) -> VN k -> Type where
        Nil : HVF 0 []
        (::) : FI n -> HVF k ns -> HVF (S k) (n :: ns)

public export
data X : Nat -> (n : Nat) -> FI n -> Type

namespace HVX
    public export
    data HVX : Nat -> (k : Nat) -> (ns : VN k) -> HVF k ns -> Type where
        Nil : HVX z 0 [] []
        (::) : forall z, n, ns, cs, c.
               X z n c -> 
               HVX z k ns cs -> 
               HVX z (S k) (n :: ns) (c :: cs)

public export
data X : Nat -> (n : Nat) -> FI n -> Type where
    MkX : forall z, n, kv, ns, cs.
          {0 kp : LTE (S kv) (n * z)} ->
          HVX z kv ns cs ->
          X z n (MkFI n Control.Relation.reflexive)

public export
genX : Fuel -> (z : Nat) -> Gen MaybeEmpty (n ** c ** X z n c)
genX = deriveGen

with the following error:

[ info ] Found local config at /home/elk/Development/deptycheck-bug-Skv/pack.toml
[ info ] Using package collection nightly-250207
[ build ] 1/1: Building Main (src/Main.idr)
[ build ] LOG deptycheck.derive.namesInfo:5: ____ start ____
[ build ] LOG deptycheck.derive.namesInfo:5: ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.type:5: Main.X[0] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.X[0] MkX __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.X[0] MkX ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.X[0] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.X[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.X[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Data.Nat.LTE[0, 1] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[0, 1] LTEZero __ start __
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[0, 1] LTEZero ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[0, 1] LTESucc __ start __
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[0, 1] LTESucc ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Data.Nat.LTE[0, 1] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Data.Nat.LTE[0, 1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Data.Nat.LTE[0, 1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Prelude.Types.Nat[] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] Z __ start __
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] Z ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] S __ start __
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] S ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Prelude.Types.Nat[] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Prelude.Types.Nat[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Prelude.Types.Nat[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVX.HVX[0, 1, 2, 3] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1, 2, 3] Nil __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1, 2, 3] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1, 2, 3] (::) __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1, 2, 3] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.HVX.HVX[0, 1, 2, 3] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.HVX.HVX[0, 1, 2, 3] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVX.HVX[0, 1, 2, 3] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVF.HVF[] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.HVF.HVF[] Nil __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVF.HVF[] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Main.HVF.HVF[] (::) __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVF.HVF[] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.HVF.HVF[] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.HVF.HVF[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVF.HVF[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.FI[] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.FI[] MkFI __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.FI[] MkFI ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.FI[] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.FI[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.FI[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.X[0, 1, 2] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.X[0, 1, 2] MkX __ start __
[ build ] Error: While processing right hand side of genX. Error during
[ build ] reflection: Argument #2 is not supported yet, argument expression: Main.MkFI {n = n} n (Data.Nat.reflexive {x = n}), reason: name `Data.Nat.reflexive` is not a constructor
[ build ] 
[ build ] Main:43:11--43:52
[ build ]  39 | data X : Nat -> (n : Nat) -> FI n -> Type where
[ build ]  40 |     MkX : forall z, n, kv, ns, cs.
[ build ]  41 |           {0 kp : LTE (S kv) (n * z)} ->
[ build ]  42 |           HVX z kv ns cs ->
[ build ]  43 |           X z n (MkFI n Control.Relation.reflexive)
[ build ]                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[ build ] 
[ fatal ] Error when executing system command.
          Command: "/home/elk/.pack/install/7ca34d1db6f7ea46fb16ea4df303fa97c50a7f6c/idris2/bin/idris2" "--build" "deptycheck-bug-Skv.ipkg"
          Error code: 1

However, if (S kv) in the type of the kp parameter of the MkX constructor is replaced with just kv, then the generator is successfully derived. Note that the failure occurs in the X[0, 1, 2] generator, that is derived only with (S kv) (and some other parameters become given as well, such as HVX[0, 1] turning into HVX[0, 1, 2, 3] when introducing (S kv)):

[ info ] Found local config at /home/elk/Development/deptycheck-bug-Skv/pack.toml
[ info ] Using package collection nightly-250207
[ build ] 1/1: Building Main (src/Main.idr)
[ build ] LOG deptycheck.derive.namesInfo:5: ____ start ____
[ build ] LOG deptycheck.derive.namesInfo:5: ^^^^  end  ^^^^
[ build ] LOG deptycheck.derive.type:5: Main.X[0] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.X[0] MkX __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.X[0] MkX ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.X[0] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.X[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.X[0] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVX.HVX[0, 1] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1] Nil __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1] Nil ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1] (::) __ start __
[ build ] LOG deptycheck.derive.consBody:5: Main.HVX.HVX[0, 1] (::) ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Main.HVX.HVX[0, 1] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Main.HVX.HVX[0, 1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Main.HVX.HVX[0, 1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Data.Nat.LTE[1] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[1] LTEZero __ start __
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[1] LTEZero ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[1] LTESucc __ start __
[ build ] LOG deptycheck.derive.consBody:5: Data.Nat.LTE[1] LTESucc ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Data.Nat.LTE[1] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Data.Nat.LTE[1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Data.Nat.LTE[1] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Prelude.Types.Nat[] ___ start ___
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] Z __ start __
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] Z ^^  end  ^^
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] S __ start __
[ build ] LOG deptycheck.derive.consBody:5: Prelude.Types.Nat[] S ^^  end  ^^
[ build ] LOG deptycheck.derive.consRec:5: Prelude.Types.Nat[] ___ start ___
[ build ] LOG deptycheck.derive.consRec:5: Prelude.Types.Nat[] ^^^  end  ^^^
[ build ] LOG deptycheck.derive.type:5: Prelude.Types.Nat[] ^^^  end  ^^^
[ build ] Now compiling the executable: deptycheck-bug-Skv

[buzden]

Local ordering changes too much with this addition, we should try to make is a bit more stable, maybe taking matchability of indices when they are about to be set as "given"