Modelling General Recursion in Type Theory :

An example

Assuming you have a termination proof,

qsAll :: (xs::[a]) -> Dqs xs

you can define

qs :: Ord a => [a] -> [a] qs xs = quicksort xs (qsAll xs)

with the same type as the original function.