[ test ] Added regression tests for #2927

tests/Main.idr

@@ -272,7 +272,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        "import001", "import002", "import003", "import004", "import005", "import006",
        "import007", "import008",
        -- Implicit laziness, lazy evaluation
-       "lazy001", "lazy002",
+       "lazy001", "lazy002", "lazy003",
        -- Namespace blocks
        "namespace001", "namespace002", "namespace003", "namespace004",
        -- Parameters blocks

tests/idris2/lazy003/LiftedBot.idr

@@ -0,0 +1,28 @@
+import Data.List.Lazy
+
+import Debug.Trace
+
+showHead : Show a => LazyList a -> String
+showHead [] = "Empty"
+showHead (x::xs) = show x
+
+%inline
+(::) : Maybe a -> Lazy (LazyList a) -> LazyList a
+Nothing :: xs = xs
+Just x  :: xs = x :: xs
+
+bot : a
+bot = bot
+
+fufu : a -> Maybe a
+fufu = Just
+
+g : LazyList Nat
+g = [ fufu 6
+    , fufu bot
+    ]
+
+-- Note that this should finish in finite time, as tail containing
+-- `bot` is lazy and should never be computed
+main : IO Unit
+main = printLn $ showHead g

tests/idris2/lazy003/LiftedTrace.idr

@@ -0,0 +1,22 @@
+import Data.List.Lazy
+
+import Debug.Trace
+
+%default total
+
+%inline
+(::) : Maybe a -> Lazy (LazyList a) -> LazyList a
+Nothing :: xs = xs
+Just x  :: xs = x :: xs
+
+fufu : a -> Maybe a
+fufu = Just
+
+g : LazyList Nat
+g = trace "--- outmost ---"
+  [ fufu $ trace "pure 6" 6
+  , fufu $ trace "pure 5" 5
+  ]
+
+main : IO Unit
+main = printLn g

tests/idris2/lazy003/expected

@@ -0,0 +1,5 @@
+pure 6
+--- outmost ---
+pure 5
+[6, 5]
+"6"

tests/idris2/lazy003/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner -p contrib --exec main LiftedTrace.idr
+$1 --no-color --console-width 0 --no-banner -p contrib --exec main LiftedBot.idr