Exponential compile time

[nicolabotta]

I have ran again into what could be an instance of #172. In contrast to #172, however, compilation time seems to be exponential in |n| both for lists:

> module Main

> import Data.Fin

> %default total

> tail : (Fin (S n) -> a) -> (Fin n -> a)
> tail f = f . FS

> myToList : (Fin n -> a) -> List a
> myToList {n =   Z} _ = Nil
> myToList {n = S m} f = (f FZ) :: myToList (tail f)

> n : Nat
> n = 3200

> f : Fin n -> Bool
> f k = False

> xs : List Bool
> xs = myToList f

> main : IO ()
> main = putStrLn (show n)

and for vectors:

> module Main

> import Data.Fin
> import Data.Vect

> %default total

> tail : (Fin (S n) -> a) -> (Fin n -> a)
> tail f = f . FS

> toVect : (Fin n -> a) -> Vect n a
> toVect {n =   Z} _ = Nil
> toVect {n = S m} f = (f FZ) :: toVect (tail f)

> n : Nat
> n = 1600

> xs : Vect n Bool
> xs = toVect (\ k => False)

> main : IO ()
> main = putStrLn (show n)

Memory requirements at compile time seem to be linear in |n| in both cases. Execution takes constant time, as one would expect.

[ahmadsalim]

I think this is indeed a duplicate of #172, which seems to be a major issue.