Filter GADT case splits on whether or not the index matches the inferred index

[ProofOfKeags]

I am not sure whether to classify this as a bug or feature request but I encountered this today:

type JobMetadata :: AppTmpStatus -> Type
data JobMetadata a where
    Install ::StoreApp -> StoreAppVersionInfo -> JobMetadata 'Installing
    Backup ::JobMetadata 'CreatingBackup
    Restore ::JobMetadata 'RestoringBackup
    StopApp ::JobMetadata 'StoppingT
    RestartApp ::JobMetadata 'RestartingT

installInfo :: JobMetadata 'Installing -> (StoreApp, StoreAppVersionInfo)
installInfo = _

I got excited and attempted to use the tactics engine to autoderive "installInfo" for me but it got stuck. Confused, I decided to just do a case split and it put all of the cases into my editor instead of just the first one, which is telling me why it got stuck. I am not sure exactly how much context is available to the plugin at that site, but I think in theory it should be able to limit it down to the only constructor that will produce that GADT at that type index.