Update test output

Results consistent with Idris 2 behaviour
edwinb · May 15, 2023 · 9d90dff · 9d90dff
1 parent 74d70b3
commit 9d90dff
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Core/Unify/Unify.idr b/src/Core/Unify/Unify.idr
@@ -444,8 +444,6 @@ parameters {auto c : Ref Ctxt Defs} {auto u : Ref UST UState}
   unifyNotMetavar : {vars : _} ->
           UnifyInfo -> FC -> Env Term vars ->
           Value f vars -> Value f' vars -> Core UnifyResult
-  unifyNotMetavar mode fc env (VAs _ _ _ x) y = unifyNoEta mode fc env !(expand x) y
-  unifyNotMetavar mode fc env x (VAs _ _ _ y) = unifyNoEta mode fc env x !(expand y)
   -- Unifying applications means we're stuck and need to postpone, since we've
   -- already checked convertibility
   -- In 'match' or 'search'  mode, we can nevertheless unify the arguments
@@ -504,6 +502,8 @@ parameters {auto c : Ref Ctxt Defs} {auto u : Ref UST UState}
       = if !(convert env x y)
            then pure success
            else postpone fc mode "Postponing application (right)" env x y
+  unifyNotMetavar mode fc env (VAs _ _ _ x) y = unifyNoEta mode fc env !(expand x) y
+  unifyNotMetavar mode fc env x (VAs _ _ _ y) = unifyNoEta mode fc env x !(expand y)
   unifyNotMetavar mode fc env x_in y_in
       = do x <- expand x_in
            y <- expand y_in

diff --git a/tests/yaffle/case001/expected b/tests/yaffle/case001/expected
@@ -12,6 +12,6 @@ Yaffle> Main.ctestS ==>
 	Runtime: \({arg:0} : [__]) => let {sc:0} : Main.Nat = (Main.S (Main.plus {arg:0}[0] {arg:0}[0])) in case  {sc:0}[0] : Main.Nat of [Main.S {e:0} => case  {e:0}[0] : Main.Nat of [Main.Z => {arg:0}[2], _ => (Main.plus {e:0}[0] {e:0}[0])]]
 	[covering]
 	[Main.plus: [Just (0, Same), Just (0, Same)], Main.plus: [Nothing, Nothing]]
-	total
+	not covering due to call to function Main.case block in ctestS
 
 Yaffle> Bye for now!