diff --git a/tests/idris2/basic/basic044/expected b/tests/idris2/basic/basic044/expected index d93f23fa89..a67dfb45ec 100644 --- a/tests/idris2/basic/basic044/expected +++ b/tests/idris2/basic/basic044/expected @@ -117,33 +117,33 @@ Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3: $resolved6 $resolved7 -Target type : ?Vec.{a:4569}_[] +Target type : ?Vec.{a:4574}_[] LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4: (($resolved3 ((:: (fromInteger 0)) Nil)) Nil) (($resolved4 ((:: (fromInteger 0)) Nil)) Nil) (($resolved5 ((:: (fromInteger 0)) Nil)) Nil) -Target type : (Vec.Vec ?Vec.{a:4569}_[] ?Vec.{n:4568}_[]) +Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[]) LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5: (($resolved3 (fromInteger 0)) Nil) (($resolved4 (fromInteger 0)) Nil) (($resolved5 (fromInteger 0)) Nil) -Target type : ?Vec.{a:4572}_[] +Target type : ?Vec.{a:4577}_[] LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6: ($resolved1 0) ($resolved2 0) -With default. Target type : ?Vec.{a:4574}_[] +With default. Target type : ?Vec.{a:4579}_[] LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7: $resolved6 $resolved7 -Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[]) +Target type : (Vec.Vec ?Vec.{a:4579}_[] ?Vec.{n:4578}_[]) LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6: ($resolved1 0) ($resolved2 0) -With default. Target type : ?Vec.{a:4573}_[] +With default. Target type : ?Vec.{a:4578}_[] LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8: $resolved6 $resolved7 -Target type : (Vec.Vec ?Vec.{a:4572}_[] ?Vec.{n:4571}_[]) +Target type : (Vec.Vec ?Vec.{a:4577}_[] ?Vec.{n:4576}_[]) LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5: (($resolved4 (fromInteger 0)) Nil) Target type : (Prelude.Basics.List Prelude.Types.Nat) diff --git a/tests/idris2/data/record021/RecordParam.idr b/tests/idris2/data/record021/RecordParam.idr index ea48121873..8e05ea09b8 100644 --- a/tests/idris2/data/record021/RecordParam.idr +++ b/tests/idris2/data/record021/RecordParam.idr @@ -2,3 +2,5 @@ record Ok (ty : Type) where f : (x : ty) -> Type record Fail (ty : Type) where f : {x : ty} -> Type +record Fail2 (ty : Type) where + f : {x : ty} -> ty -> {y : ty} -> Type diff --git a/tests/idris2/error/error018/expected b/tests/idris2/error/error018/expected index eecd82d312..b57b4cd037 100644 --- a/tests/idris2/error/error018/expected +++ b/tests/idris2/error/error018/expected @@ -30,7 +30,7 @@ Issue1031-3:4:6--4:7 1/1: Building Issue1031-4 (Issue1031-4.idr) Error: While processing left hand side of nice. Unsolved holes: -Main.{dotTm:815} introduced at: +Main.{dotTm:820} introduced at: Issue1031-4:4:6--4:10 1 | %default total 2 | diff --git a/tests/idris2/evaluator/evaluator002/expected b/tests/idris2/evaluator/evaluator002/expected index 9a58fb3c9c..f114eeba77 100644 --- a/tests/idris2/evaluator/evaluator002/expected +++ b/tests/idris2/evaluator/evaluator002/expected @@ -1,89 +1,89 @@ 1/2: Building Lib (Lib.idr) -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2550} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2554} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2551} -LOG eval.stuck.outofscope:5: Stuck function: {_:2556} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2557} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2558} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2555} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2559} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2556} +LOG eval.stuck.outofscope:5: Stuck function: {_:2561} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2562} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2559} -LOG eval.stuck.outofscope:5: Stuck function: {_:2565} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2566} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2563} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2570} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2567} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2564} +LOG eval.stuck.outofscope:5: Stuck function: {_:2570} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2571} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2572} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2575} LOG eval.stuck.outofscope:5: Stuck function: Prelude.Types.List.reverse -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2585} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2586} -LOG eval.stuck.outofscope:5: Stuck function: {_:2589} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2590} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2591} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593} -LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2593} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2590} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{_:2591} +LOG eval.stuck.outofscope:5: Stuck function: {_:2594} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{b:2595} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598} +LOG eval.stuck.outofscope:5: Stuck function: Lib.{a:2598} LOG eval.stuck.outofscope:5: Stuck function: Lib.accMapAux 2/2: Building Main (Main.idr) -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595} -LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2595} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2599} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2602} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{b:2600} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2604} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2607} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2605} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} -LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2616} -LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2596} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2612} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2610} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} +LOG eval.stuck.outofscope:5: Stuck function: Main.{ty:2621} +LOG eval.stuck.outofscope:5: Stuck function: Main.{a:2601} LOG eval.stuck.outofscope:5: Stuck function: Lib.accMap Main> LOG eval.stuck:5: Stuck function: Lib.accMapAux LOG eval.stuck:5: Stuck function: Lib.accMapAux diff --git a/tests/idris2/evaluator/interpreter008/expected b/tests/idris2/evaluator/interpreter008/expected index 7849d94f57..55093bb3bb 100644 --- a/tests/idris2/evaluator/interpreter008/expected +++ b/tests/idris2/evaluator/interpreter008/expected @@ -1,6 +1,6 @@ 1/1: Building Issue2041 (Issue2041.idr) Error: Unsolved holes: -Main.{n:820} introduced at: +Main.{n:825} introduced at: Issue2041:5:17--5:19 1 | ex : {n : Nat} -> String 2 | ex {n} = "hello" ++ show n @@ -9,8 +9,8 @@ Issue2041:5:17--5:19 5 | main = putStrLn ex ^^ -Main> Encountered unimplemented hole Main.{n:820} -Warning: compiling hole Main.{n:820} +Main> Encountered unimplemented hole Main.{n:825} +Warning: compiling hole Main.{n:825} Main> Encountered unimplemented hole Main.{n:4} Warning: compiling hole Main.{n:4} Main> diff --git a/tests/idris2/interactive/interactive042/expected b/tests/idris2/interactive/interactive042/expected index 385ca5b84e..1859345e24 100644 --- a/tests/idris2/interactive/interactive042/expected +++ b/tests/idris2/interactive/interactive042/expected @@ -12,17 +12,17 @@ Main> 0 m : Nat ------------------------------ help : Vect (S (plus n m)) a Main> Main> a : Nat - eq : {a:822} = a + eq : {a:827} = a ------------------------------ a : Nat Main> 0 m : Nat 0 a : Type x : a - xs : Vect {n:871} a + xs : Vect {n:876} a ys : Vect m a 0 n : Nat ------------------------------ -help : Vect (S (plus {n:871} m)) a +help : Vect (S (plus {n:876} m)) a Main> Bye for now! 1/1: Building Issue35-2 (Issue35-2.idr) @@ -39,10 +39,10 @@ Issue35-2:2:13--2:14 1/1: Building Issue35-2 (Issue35-2.idr) Error: While processing right hand side of f. When unifying: - Either b {b:821} + Either b {b:826} and: - Either {b:821} b -Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b. + Either {b:826} b +Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b. Issue35-2:2:13--2:14 1 | f : { a, b : Type } -> Either a b -> Either b a @@ -51,10 +51,10 @@ Issue35-2:2:13--2:14 1/1: Building Issue35-2 (Issue35-2.idr) Error: While processing right hand side of f. When unifying: - Prelude.Either b {b:821} + Prelude.Either b {b:826} and: - Prelude.Either {b:821} b -Mismatch between: {b:821} (implicitly bound at Issue35-2:2:1--2:2) and b. + Prelude.Either {b:826} b +Mismatch between: {b:826} (implicitly bound at Issue35-2:2:1--2:2) and b. Issue35-2:2:13--2:14 1 | f : { a, b : Type } -> Either a b -> Either b a diff --git a/tests/idris2/misc/lazy003/expected b/tests/idris2/misc/lazy003/expected index 4c5174f352..99ec8a61c5 100644 --- a/tests/idris2/misc/lazy003/expected +++ b/tests/idris2/misc/lazy003/expected @@ -7,8 +7,8 @@ Refers to: Builtin.Unit Flags: covering Main> Main.f6 Arguments [] -Compile time tree: Delay (\u1, {u2:834} => u1) -Compiled: Delay Lazy (\u1=> \{u2:834}=> u1) +Compile time tree: Delay (\u1, {u2:839} => u1) +Compiled: Delay Lazy (\u1=> \{u2:839}=> u1) Refers to: Builtin.Unit Flags: covering Main> Main.switch3 @@ -19,7 +19,7 @@ Compiled: \ {arg:0} => let f = Force Lazy (Main.switch {arg:0}) in \{lamc:0}=> case {lamc:0} of { Builtin.MkPair {tag = 0} [cons] {e:2} {e:3} => case {e:3} of { Builtin.MkPair {tag = 0} [cons] {e:6} {e:7} => Builtin.MkPair {tag = 0} [cons] (f {e:2}) (Builtin.MkPair {tag = 0} [cons] (f {e:6}) (f {e:7}))} } -Refers to: Main.case block in switch3, Main.{_:980}, Main.switch, Builtin.Pair, Prelude.Types.Nat +Refers to: Main.case block in switch3, Main.{_:985}, Main.switch, Builtin.Pair, Prelude.Types.Nat Refers to (runtime): Main.switch, Builtin.MkPair Flags: covering Size change: