[Ur] Question about the Sum metaprogramming example

[Adam Chlipala]

David Snider wrote:
> OK, Thanks. There are some other things I don't understand:
>
> "With sum defined, it is easy to make some sample calls. The form of the
> code for main does not make it apparent, but the compiler must "reverse
> engineer" the appropriate {Unit} from the {Type} available from the context
> at each call to sum. The compiler also infers a folder for each call,
> guessing at the desired permutations by examining the orders in which field
> names are written in the code."
>
> I understand type inference, but how does it infer the actual values of the
> parameters? How do I know which parameters need to be passed and which will
> be inferred?
>    

I believe this is addressed in the manual:
     http://www.impredicative.com/ur/manual.pdf
See Section 4.3, in a paragraph beginning "Handling of implicit...".  
This comes near the top of page 14 in the current manual.  It might also 
help to look at the "Explicitness" non-terminal "?", defined at the 
bottom of page 9 and used in a few places in the next few pages.