ScopedSnocList: WIP: rewrites to Snock ANF and LambdaLift

src/Compiler/ANF.idr

@@ -264,7 +264,7 @@ toANF : LiftedDef -> Core ANFDef
 toANF (MkLFun args scope sc)
     = do v <- newRef Next (the Int 0)
          (iargs, vsNil) <- bindArgs args []
-         let vs : AVars args = rewrite sym (appendNilRightNeutral args) in
+         let vs : AVars args = rewrite sym (appendLinLeftNeutral args) in
                                       vsNil
          (iargs', vs) <- bindArgs scope vs
          pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)

src/Compiler/LambdaLift.idr

@@ -358,10 +358,10 @@ initUsed : {vars : _} -> Used vars
 initUsed {vars} = MkUsed (replicate (length vars) False)
 
 lengthDistributesOverAppend
-  : (xs, ys : List a)
-  -> length (xs ++ ys) = length xs + length ys
-lengthDistributesOverAppend [] ys = Refl
-lengthDistributesOverAppend (x :: xs) ys =
+  : (xs, ys : SnocList a)
+  -> length (ys ++ xs) = length xs + length ys
+lengthDistributesOverAppend [<] ys = Refl
+lengthDistributesOverAppend (xs :< x) ys =
   cong S $ lengthDistributesOverAppend xs ys
 
 weakenUsed : {outer : _} -> Used vars -> Used (vars ++ outer)
@@ -581,11 +581,18 @@ mutual
         LConCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)
     where
       dropConCase : LiftedConAlt (vars ++ outer) ->
-                    LiftedConAlt ((dropped vars unused) ++ outer)
+                    LiftedConAlt (dropped vars unused ++ outer)
       dropConCase (MkLConAlt n ci t args sc) =
-        let sc' = (rewrite sym $ appendAssociative args outer vars in sc)
-            droppedSc = dropUnused {vars=vars} {outer=outer++args} unused sc' in
-        MkLConAlt n ci t args (rewrite appendAssociative args outer (dropped vars unused) in droppedSc)
+        MkLConAlt n ci t args (?sdf droppedSc)
+        where
+          sc' : Lifted (vars ++ (outer ++ args))
+          sc' = (rewrite appendAssociative vars outer args in sc)
+
+          droppedSc : Lifted ((dropped vars unused ++ outer) ++ args)
+          droppedSc = do
+            rewrite sym $ appendAssociative (dropped vars unused) outer args
+            dropUnused {vars=vars} {outer=outer++args} unused sc'
+
   dropUnused {vars} {outer} unused (LConstCase fc sc alts def) =
     let alts' = map dropConstCase alts in
         LConstCase fc (dropUnused unused sc) alts' (map (dropUnused unused) def)