[ wip ] Cut prefixes deeper

src/Deriving/DepTyCheck/Gen/Core.idr

@@ -72,7 +72,7 @@ ConstructorDerivator => DerivatorCore where
       let genConParams = sig.generatedParams.asVect <&> \gv => getExpr $ index' conParams $ rewrite lengthCorrect in gv
       Right genConParams
     -- clean up prefixes of potential indices, we kinda depend here on fact that constructor expressions are already normalised
-    let genConParams = transpose . map cutAppPrefix . transpose $ genConParams
+    let genConParams = transpose . map (cutAppPrefix {n=sig.targetType.cons.length}) . transpose $ genConParams
 
     -- calculate which constructors are recursive and which are not
     consRecs <- logBounds "consRec" [sig] $ pure $ sig.targetType.cons `zipV` genConParams <&> \(con, genConIdxs) => do

src/Deriving/DepTyCheck/Util/Reflection.idr

@@ -147,8 +147,8 @@ reAppAny1 l $ NamedApp n e = namedApp l n e
 reAppAny1 l $ AutoApp e    = autoApp l e
 reAppAny1 l $ WithApp e    = IWithApp EmptyFC l e
 
-public export
-reAppAny : TTImp -> List AnyApp -> TTImp
+public export %inline
+reAppAny : Foldable f => TTImp -> f AnyApp -> TTImp
 reAppAny = foldl reAppAny1
 
 --- Specific expressions building helpers ---
@@ -584,25 +584,34 @@ namespace UpToRenaming
   [UpToRenaming] Eq TTImp where
     x == y = (x == y) @{UpToSubst @{empty}}
 
+[AppUpToRenaming] Eq AnyApp where
+  (==) = (==) @{UpToRenaming} `on` getExpr
+
 export
-cutAppPrefix : Vect n TTImp -> Vect n TTImp
+cutAppPrefix : {n : _} -> Vect n TTImp -> Vect n TTImp
+cutAppPrefix' : {n : _} -> Vect n AnyApp -> Vect n AnyApp
 cutAppPrefix [] = []
 cutAppPrefix {n=S k} xs@(_::_) = do
-  let unappXs = xs <&> map @{Compose} getExpr . unAppAny
-  let S Z = List.length . nub @{UpToRenaming} $ fst <$> unappXs.asList
+  let unappXs = xs <&> unAppAny
+  let heads = fst <$> unappXs
+  let S Z = List.length . nub @{UpToRenaming} $ heads.asList
     | _ => xs -- what is applied differs, to stop reduction
   let first::unappXs = snd <$> unappXs
-  let unappXs : Maybe $ Vect k $ Vect first.length TTImp = for unappXs $ \lst => do
+  let unappXs : Maybe $ Vect k $ Vect first.length AnyApp = for unappXs $ \lst => do
     let Yes lc = decEq first.length lst.length
       | No _ => Nothing
     rewrite lc
     Just lst.asVect
   let Just unappXs = unappXs
     | Nothing => xs -- different count of args in apps, stop reduction
   let unappXs = transpose $ first.asVect :: unappXs
-  let [unevenApp] = filter ((> 1) . List.length . nub @{UpToRenaming} . toList) unappXs.asList
-    | _ => xs -- either all equal, or no single reduction point
-  unevenApp
+  let [unevenApp] = filter ((> 1) . List.length . nub @{AppUpToRenaming} . toList) unappXs.asList
+    | [] => xs <&> \expr => Implicit (getFC expr) False -- all equal, erase it
+    | _  => map (uncurry reAppAny) $ zip heads $ transpose $ assert_total cutAppPrefix' <$> unappXs
+  cutAppPrefix $ assert_smaller xs $ map getExpr $ unevenApp
+cutAppPrefix' xs = do
+  let xs' = cutAppPrefix $ getExpr <$> xs
+  xs' `zip` xs <&> uncurry (mapExpr . const)
 
 -- Returns a list without duplications
 export