Unexpected termination failure with %tcinline and assert_total

[gallais]

The idea here is to have a way to express domain-specific knowledge by declaring that some primitives are considered guarding.

I figured I could introduce a newtype wrapper that users cannot build themselves (unexported constructor) and give some primitives a blessing by making them return a guarded result. This guarded result will morally only arrive after something productive has happened and can therefore be used to guard a co-recursive call.

By marking callGuarded with %tcinline, and making its body be a big assert_total I was hoping it'd have the right behaviour however the main I include is currently rejected by the compiler with the error

Guarded.idr line 24 col 0:
     main is not total, possibly not terminating due to recursive path Main.main

while the (commented-out) alternative definition is accepted just fine.

%default total

namespace Guard

  -- Do NOT export the constructor
  export
  data Guarded : Type -> Type where
    MkGuarded : (1 _ : a) -> Guarded a

  runGuarded : (1 _ : Guarded a) -> a
  runGuarded (MkGuarded v) = v

  export %tcinline
  callGuarded : Guarded a -> (a -> b) -> b
  callGuarded x f = assert_total (f (runGuarded x))

  export
  -- getLine is declared guarding
  getLine : IO (Guarded String)
  getLine = do
    str <- Prelude.getLine
    pure (MkGuarded str)

main : IO ()
main = do
  putStrLn "What is your name?"
  gstr <- getLine
  callGuarded gstr $ \ name => do
    putStrLn "Hello \{name}"
    main

{-
  name <- Prelude.getLine
  assert_total $ do
    putStrLn "Hello \{name}"
    main
-}

[gallais]

It does work if I make callGuarded public export.

That may very well be the intended behaviour although I would expect to be able to distinguish exporting the definition to allow the machine to inline it during termination checking vs. users being able to look at the internals themselves.