[ preformance ] implementation of unpack is inefficient

[stefan-hoeck]

Steps to Reproduce

Typecheck the following example (this is a slightly adjusted example from a question on discord):

module Printf

import Data.String

%default total

data Format = FInt Format        -- %d
            | FString Format     -- %s
            | FOther Char Format
            | FEnd

format : List Char -> Format 
format Nil = FEnd
format ('%' :: 'd' :: xs) = FInt (format xs)
format ('%' :: 's' :: xs) = FString (format xs)
format (x :: xs) = FOther x (format xs)


0 InterpFormat : Format -> Type 
InterpFormat (FInt f)     = Int    -> InterpFormat f
InterpFormat (FString f)  = String -> InterpFormat f
InterpFormat (FOther _ f) = InterpFormat f
InterpFormat FEnd         = String

formatString : String -> Format 
formatString s = format (unpack s)

toFunction : (fmt : Format) -> String -> InterpFormat fmt
toFunction (FInt x) str     = \y => toFunction x (str ++ show y)
toFunction (FString x) str  = \y => toFunction x (str ++ y)
toFunction (FOther c x) str = toFunction x (str ++ singleton c)
toFunction FEnd str         = str

printf : (s : String) -> InterpFormat (formatString s)
printf s = toFunction (formatString s) ""

message : String
message = printf "My name is %s and I am %d years old"

Expected Behavior

Fails with a type error after a short time.

Observed Behavior

Consumes all my system's memory and dies after a couple of minutes.

The reason seems to be the implementation of unpack: For shorter messages, it produces a very large syntax tree (at least quadratic w.r.t. to the length of the string). It was pretty straight forward to come up with a different implementation of unpack that performs much better at compile time. I'll submit a PR in a moment.