> What's the distinction between C-c C-space and C-c C-r?

Beats the hell out of me. Here's the docstring for agda2-give (bound to C-c C-SPC):

    Give to the goal at point the expression in it

Here's the one for agda2-refine (C-c C-r):

    Refine the goal at point.
    If the goal contains an expression e, and some "suffix" of the
    type of e unifies with the goal type, then the goal is replaced
    by e applied to a suitable number of new goals.
    
    If the goal is empty, the goal type is a data type, and there is
    exactly one constructor which unifies with this type, then the
    goal is replaced by the constructor applied to a suitable number
    of new goals.