[ prelude ] Make able to implement provably total showPrec recursively

libs/prelude/Prelude/Show.idr

@@ -67,7 +67,7 @@ interface Show ty where
 
 ||| Surround a `String` with parentheses depending on a condition.
 ||| @ b whether to add parentheses
-export
+public export
 showParens : (b : Bool) -> String -> String
 showParens False s = s
 showParens True  s = "(" ++ s ++ ")"
@@ -83,7 +83,7 @@ showParens True  s = "(" ++ s ++ ")"
 ||| Show a => Show (Ann a) where
 |||   showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x
 ||| ```
-export
+public export
 showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String
 showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs)
 
@@ -92,7 +92,7 @@ showCon d conName shownArgs = showParens (d >= App) (conName ++ shownArgs)
 |||
 ||| This adds a space to the front so the results can be directly concatenated.
 ||| See `showCon` for details and an example.
-export
+public export %tcinline
 showArg : Show a => (x : a) -> String
 showArg x = " " ++ showPrec App x
 

tests/idris2/total/total020/Check.idr

@@ -1,5 +1,7 @@
 %default total
 
+--- Functor-related ---
+
 data X : Type -> Type -> Type where
   B : b -> X a b
   R : X a b -> X b c -> X a c
@@ -29,3 +31,13 @@ data X : Type -> Type -> Type where
   foldMap f rlr@(R l r) = do
     let r' = map @{WithFunction} f r
     concat $ assert_smaller rlr r'
+
+--- Show-related ---
+
+data Tree : Type -> Type where
+  Leaf : a -> Tree a
+  Node : a -> (left, right : Tree a) -> Tree a
+
+Show a => Show (Tree a) where
+  showPrec d (Leaf x)     = showCon d "Leaf" $ showArg x
+  showPrec d (Node x l r) = showCon d "Node" $ showArg x ++ showArg l ++ showArg r