Add %tcinline flag to high level syntax

This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.

CHANGELOG.md

@@ -11,6 +11,10 @@ Language changes:
 * Fields of records can be accessed (and updated) using the dot syntax,
   such as `r.field1.field2` or `record { field1.field2 = 42 }`.
   For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
+* New function flag `%tcinline` which means that the function should be
+  inlined for the purposes of totality checking (but otherwise not inlined).
+  This can be used as a hint for totality checking, to make the checker look
+  inside functions that it otherwise might not.
 * %transform directive, for declaring transformation rules on runtime
   expressions. Transformation rules are automatically added for top level
   implementations of interfaces.

src/Idris/Parser.idr

@@ -1174,6 +1174,9 @@ fnDirectOpt fname
   <|> do pragma "inline"
          commit
          pure $ IFnOpt Inline
+  <|> do pragma "tcinline"
+         commit
+         pure $ IFnOpt TCInline
   <|> do pragma "extern"
          pure $ IFnOpt ExternFn
   <|> do pragma "macro"

src/TTImp/ProcessType.idr

@@ -33,6 +33,8 @@ processFnOpt : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> FnOpt -> Core ()
 processFnOpt fc ndef Inline
     = setFlag fc ndef Inline
+processFnOpt fc ndef TCInline
+    = setFlag fc ndef TCInline
 processFnOpt fc ndef (Hint d)
     = do defs <- get Ctxt
          Just ty <- lookupTyExact ndef (gamma defs)

src/TTImp/TTImp.idr

@@ -179,6 +179,7 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       TCInline : FnOpt
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
@@ -196,6 +197,7 @@ mutual
   export
   Show FnOpt where
     show Inline = "%inline"
+    show TCInline = "%tcinline"
     show (Hint t) = "%hint " ++ show t
     show (GlobalHint t) = "%globalhint " ++ show t
     show ExternFn = "%extern"
@@ -210,6 +212,7 @@ mutual
   export
   Eq FnOpt where
     Inline == Inline = True
+    TCInline == TCInline = True
     (Hint x) == (Hint y) = x == y
     (GlobalHint x) == (GlobalHint y) = x == y
     ExternFn == ExternFn = True
@@ -895,6 +898,7 @@ mutual
   export
   TTC FnOpt where
     toBuf b Inline = tag 0
+    toBuf b TCInline = tag 11
     toBuf b (Hint t) = do tag 1; toBuf b t
     toBuf b (GlobalHint t) = do tag 2; toBuf b t
     toBuf b ExternFn = tag 3
@@ -919,6 +923,7 @@ mutual
                8 => pure (Totality PartialOK)
                9 => pure Macro
                10 => do ns <- fromBuf b; pure (SpecArgs ns)
+               11 => pure TCInline
                _ => corrupt "FnOpt"
 
   export