AtIndex with destructed parameterised type

[1BAH]

import Derivation.DepTyCheck.Gen

%default total

data BoolableTy : Bool -> Type where
    T : BoolableTy True
    F : BoolableTy False

record Wrapper where
    constructor W
    Arg   : BoolableTy bool

data AtIndex : (wrap : Wrapper) ->
               (arg : BoolableTy predicate) ->
               Type where
    Here : {pred : Bool} -> {arg : BoolableTy pred} -> AtIndex (W arg) arg

atIndexGen : Fuel ->
            (v : Bool) ->
            (w : Wrapper) ->
            (arg   : BoolableTy v) ->
            Gen MaybeEmpty $ AtIndex w arg

Derivation fails with error:

[ build ] Error: While processing right hand side of atIndexGen. Error during reflection: While processing right hand side
[ build ] of $resolved15024,<AtIndex.AtIndex>[0, 1, 2, 3]. While processing right hand side
[ build ] of with block in $resolved15024,<AtIndex.AtIndex>[0, 1, 2, 3],<<AtIndex.Here>>. to_be_deceqed^^pred0 is not accessible in this context.

[buzden]

The problem is that bool argument in the record W must be runtime to be able for the wrapped BooleableTy to be tested on propositional equality with the unwrapped one. DepTyCheck should report this with an adequate error message and FC.

[GlebChili]

Bumping the issue! Just spent an nontrivial amount of time to figure out the problem with erased arguments.