Do not treat free variables passed to a single constructor as determining

[buzden]

Consider the case where

record R where
  constructor MkR
  n : Nat
  b : Bool

data Y : R -> Type where
  Y1 : Y $ MkR 5 True
  Y2 : Y $ MkR a False

f, g : Nat -> Nat

data X : Type where
  X1 : Fin (f n) -> Y (MkR n True) -> X
  X2 : Fin (g n) -> Y (MkR n _) -> X

Currently we treat n as determining for both explicit arguments of X1, however knowing that MkR is the only constructor for R we can say that the second one can be used for generating n. But this leads to a redesign of an internal derivation task.

However, we can easily support a subset of this feature, when all of variables passed to the only constructor are free, like in X2. This requires only a slightly more complicated pattern matching on the result of generation.