[ prelude ] Make some higher-kinded functions be tc-inlined

libs/prelude/Prelude/Basics.idr

@@ -37,14 +37,14 @@ const : a -> b -> a
 const x = \value => x
 
 ||| Function composition.
-public export %inline
+public export %inline %tcinline
 (.) : (b -> c) -> (a -> b) -> a -> c
 (.) f g = \x => f (g x)
 
 ||| Composition of a two-argument function with a single-argument one.
 ||| `(.:)` is like `(.)` but the second argument and the result are two-argument functions.
 ||| This operator is also known as "blackbird operator".
-public export %inline
+public export %inline %tcinline
 (.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
 (.:) = (.) . (.)
 
@@ -61,7 +61,7 @@ public export %inline
 ||| ```idris example
 ||| sortBy (compare `on` fst).
 ||| ```
-public export
+public export %tcinline
 on : (b -> b -> c) -> (a -> b) -> a -> a -> c
 on f g = \x, y => g x `f` g y
 
@@ -69,14 +69,14 @@ infixl 0 `on`
 
 ||| Takes in the first two arguments in reverse order.
 ||| @ f the function to flip
-public export
+public export %tcinline
 flip : (f : a -> b -> c) -> b -> a -> c
-flip f x y = f y x
+flip f = \x, y => f y x
 
 ||| Function application.
-public export
+public export %tcinline
 apply : (a -> b) -> a -> b
-apply f a = f a
+apply f = \a => f a
 
 public export
 curry : ((a, b) -> c) -> a -> b -> c

tests/Main.idr

@@ -224,7 +224,7 @@ idrisTestsTotality = MkTestPool "Totality checking" [] Nothing
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
-       "total011", "total012", "total013"
+       "total011", "total012", "total013", "total014"
       ]
 
 -- This will only work with an Idris compiled via Chez or Racket, but at

tests/idris2/total014/FunCompTC.idr

@@ -0,0 +1,13 @@
+%default total
+
+data X : Type where
+  B : X
+  T : r -> (r -> X) -> X
+
+f_expl : (X -> X) -> X -> X
+f_expl f B       = f B
+f_expl f (T k g) = T k $ \n => f_expl f $ g n
+
+f_impl : (X -> X) -> X -> X
+f_impl f B       = f B
+f_impl f (T k g) = T k $ f_impl f . g

tests/idris2/total014/expected

@@ -0,0 +1 @@
+1/1: Building FunCompTC (FunCompTC.idr)

tests/idris2/total014/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner --check FunCompTC.idr