The Bove-Capretta method (http://www.cs.nott.ac.uk/~pszvc/publications/General_Recursion_MSCS_2005.pdf) is a neat trick for modelling non-structurally recursive or partial functions in languages like Agda. Terminating inputs to a function are characterised by an inductive predicate, and the function is rewritten to take the predicate as an argument.
For example, suppose we wanted to write the following definition of a base-2 logarithm in Agda (using module Data.Nat):
log2 : ℕ → ℕ
log2 0 = 0
log2 1 = 0
log2 n = suc (log2 ⌊ n /2⌋)
Unfortunately, this definition does not pass the termination checker. Following Bove-Capretta, one could define the following predicate:
data Loggable : ℕ → Set where
log-n≡0 : Loggable 0
log-n≡1 : Loggable 1
log-n≡n : ∀ {n} → Loggable ⌊ n /2⌋ → Loggable n
And then augment the original definition to take Loggable as an extra argument:
log2 : (n : ℕ) → Loggable n → ℕ
log2 0 _ = 0
log2 1 _ = 1
log2 n (log-n≡n p) = suc (log2 ⌊ n /2⌋ p)
This now successfully passes the termination checker, since the Loggable predicate serves as the structurally decreasing argument. This all works as expected.
Now, since the predicate is solely used to convince the termination checker, it would make sense to move it to the sort Prop since it should not have any computational effect. Indeed, inspecting our new definition of log2 also suggests this, since the predicate is not used to make any case splits that have not already been determined by the other argument.
This is where the problem is. Firstly, making Loggable a Prop prohibits case splitting on it when we are producing something in sort Set, which is the case in our new log2 function. The normal solution to this is to introduce an auxiliary "inversion lemma" operating in the sort Prop, which destructs the predicate and extracts the part we need. Unfortunately, this introduces a new problem - the structural termination of log2 would be broken, since Agda cannot see the result of calling the "inversion lemma" is structurally smaller than its input.
(Note that an equivalent of this problem can be written in Coq, which does not suffer from the same issue as it normalises expressions before checking for termination, and hence the proposes "inversion lemma" approach succeeds.)