[ fix ] issue idris-lang#2288 (idris-lang#2289)

libs/prelude/Prelude/Types.idr

@@ -455,10 +455,18 @@ Foldable List where
 
   foldMap f = foldl (\acc, elem => acc <+> f elem) neutral
 
+-- tail recursive O(n) implementation of `(>>=)` for `List`
+public export
+listBind : List a -> (a -> List b) -> List b
+listBind as f = go Nil as
+  where go : List b -> List a -> List b
+        go xs []        = reverse xs
+        go xs (y :: ys) = go (reverseOnto xs (f y)) ys
+
 public export
 Applicative List where
   pure x = [x]
-  fs <*> vs = concatMap (\f => map f vs) fs
+  fs <*> vs = listBind fs (\f => map f vs)
 
 public export
 Alternative List where
@@ -467,7 +475,7 @@ Alternative List where
 
 public export
 Monad List where
-  m >>= f = concatMap f m
+  (>>=) = listBind
 
 public export
 Traversable List where

tests/prelude/bind001/bind.idr

@@ -0,0 +1,14 @@
+import Data.SnocList
+
+iterateTR : Nat -> (a -> a) -> a -> List a
+iterateTR n f = go n Lin
+  where go : Nat -> SnocList a -> a -> List a
+        go 0     sx _ = sx <>> Nil
+        go (S k) sx v = go k (sx :< v) (f v)
+
+main : IO ()
+main = do
+  -- this checks that *bind* still behaves correctly
+  printLn $ [1..4] >>= (\n => iterateTR n (+1) 1)
+  -- this verifies that *bind* runs in linear time
+  printLn . length $ [1..5000] >>= (\n => iterateTR n (+1) n)

tests/prelude/bind001/expected

@@ -0,0 +1,4 @@
+1/1: Building bind (bind.idr)
+Main> [1, 1, 2, 1, 2, 3, 1, 2, 3, 4]
+12502500
+Main> Bye for now!

tests/prelude/bind001/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/prelude/bind001/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner bind.idr < input