ScopedSnocList: Fix CI

Co-authored-by: Viktor Yudov <[email protected]>
idris-lang · Feb 7, 2025 · b2542e3 · b2542e3
1 parent 7fc2f3a
commit b2542e3
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr
@@ -478,7 +478,7 @@ mutual
                                 -- the RHS
                         then do log "compiler.newtype.world" 50 "Inlining case on \{show n} (no world)"
 
-                                sc' : CExp (vars <>< args) <- toCExpTree n sc
+                                sc' <- toCExpTree n sc
                                 let sc'' : CExp (vars ++ cast args)
                                 := rewrite sym $ fishAsSnocAppend vars args in sc'
 
@@ -493,7 +493,7 @@ mutual
                                 let (s, env) : (_, SubstCEnv (cast args) (vars :< MN "eff" 0))
                                         = mkSubst 0 (CLocal fc First) pos args
 
-                                sc' : CExp (vars <>< args) <- toCExpTree n sc
+                                sc' <- toCExpTree n sc
 
                                 let sc'' : CExp (vars ++ cast args)
                                     := rewrite sym $ fishAsSnocAppend vars args in sc'

diff --git a/src/Core/Name/Scoped.idr b/src/Core/Name/Scoped.idr
@@ -4,7 +4,7 @@ import Core.Name
 import Core.Name.CompatibleVars
 
 import Data.SnocList
-import Data.SnocList.HasLength
+import Libraries.Data.SnocList.HasLength
 import Libraries.Data.SnocList.SizeOf
 import Libraries.Data.List.SizeOf