Generated code attempts to pattern match on function application

[UARTman]

When deriving the following generator:

module DerivedGen

import Data.Fin
import Deriving.DepTyCheck.Gen

%default total

public export
data X : Nat -> Type where
  MkX  : Fin rc -> X rc

public export
DecEq (X rc) where
  decEq (MkX xs) (MkX ys) = case (decEq xs ys) of
    Yes Refl => Yes Refl
    No up => No $ up . \case Refl => Refl

public export
f : X rc -> Fin rc

public export
data Y : X rc -> X rc -> Type where
  MkY : Y (MkX (f x)) x

checkedGen : Fuel -> (rc : Nat) -> (r1, r2 : X rc) -> Gen MaybeEmpty (Y r1 r2)
checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}}

DepTyCheck produces the following compilation error:

    Error during reflection: While processing right hand side of $resolved17300,<DerivedGen.Y>[0, 1, 2]. While processing left hand side of $resolved17362,<<DerivedGen.MkY>>. Can't match on f ?x (Not a constructor application or primitive).

    DerivedGen:23:17--23:18
     19 | f : X rc -> Fin rc
     20 | 
     21 | public export
     22 | data Y : X rc -> X rc -> Type where
     23 |   MkY : Y (MkX (f x)) x

This behavior should not occur. DepTyCheck should probably refuse to derive the generator.