[ test ] Added regression tests for #2927

tests/Main.idr

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

tests/idris2/misc/lazy005/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/misc/lazy005/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/misc/lazy005/expected

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

tests/idris2/misc/lazy005/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+idris2 -p contrib --exec main LiftedTrace.idr
+idris2 -p contrib --exec main LiftedBot.idr