[ refactor ] Add information about determination directions

src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr

@@ -77,9 +77,11 @@ namespace NonObligatoryExts
             let Yes lengthCorrect = decEq ty.args.length args.length
               | No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"
             _ <- ensureTyArgsNamed ty
-            pure $ MkTypeApp ty $ rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
-              expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
-              expr            => Right expr
+            let as = rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of
+                       expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs
+                       expr            => Right expr
+            let determinedBy = fromList $ mapMaybe (lookup' conArgIdxs) $ rights as.asList >>= allVarNames
+            pure $ MkTypeApp ty determinedBy as
 
       -- Compute left-to-right need of generation when there are non-trivial types at the left
       argsTypeApps <- for con.args.asVect $ analyseTypeApp . type
@@ -100,7 +102,7 @@ namespace NonObligatoryExts
             genForOneArg genedArg = do
 
               -- Get info for the `genedArg`
-              let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps
+              let MkTypeApp typeOfGened _ argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps
 
               -- Acquire the set of arguments that are already present
               presentArguments <- get
@@ -167,14 +169,14 @@ namespace NonObligatoryExts
       -------------------------------------------------
 
       -- Determine which arguments need to be generated in a left-to-right manner
-      let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\((MkTypeApp _ as), _) => any isRight as) $ toListI argsTypeApps
+      let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\((MkTypeApp _ _ as), _) => any isRight as) $ toListI argsTypeApps
 
       --------------------------------------------------------------------------------
       -- Preparation of input for the left-to-right phase (1st right-to-left phase) --
       --------------------------------------------------------------------------------
 
       -- Acquire those variables that appear in non-trivial type expressions, i.e. those which needs to be generated before the left-to-right phase
-      let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ as) => rights (toList as) >>= allVarNames
+      let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ _ as) => rights (toList as) >>= allVarNames
       let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR
 
       -- Find rightmost arguments among `preLTR`
@@ -229,9 +231,16 @@ namespace NonObligatoryExts
           MkTypeApp :
             (type : TypeInfo) ->
             (0 _ : AllTyArgsNamed type) =>
+            (determinedBy : SortedSet $ Fin con.args.length) ->
             (argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) ->
             TypeApp
 
+        argsDeterminedBy : TypeApp -> SortedSet $ Fin con.args.length
+        argsDeterminedBy $ MkTypeApp {determinedBy, _} = determinedBy
+
+        argsCanDetermine : TypeApp -> SortedSet $ Fin con.args.length
+        argsCanDetermine $ MkTypeApp {argTypes, determinedBy, _} = fromList (lefts argTypes.asList) `difference` determinedBy
+
   ||| Best effort non-obligatory tactic tries to use as much external generators as possible
   ||| but discards some there is a conflict between them.
   ||| All possible non-conflicting layouts may be produced in the generated values list.