Fix problems in pull derivation

[DeSevilla]

The "pull" builtin, which derives its semantics from the type it's applied to, has some problems in the derivation for arbitrary type constructors, which cause execution errors (incomplete pattern match) as noted in #278 and #316 . This PR fixes those issues and adds more thorough tests for pull. I'm marking it as a draft because I'm uncertain about a few semantic aspects and would like feedback on my code structure.

The problems are:

1. Unnecessary use of box patterns when matching on non-boxed arguments of type constructors. This is fixed in lines 455-462 of the modified Deriving.hs by changing the function to only use box patterns for arguments with coeffects.
2. Failure to apply boxes to the output. Since pull always returns a type with a coeffect, I believe the output should have a coeffect and be boxed regardless of whether any of its arguments do. However, I'm a little hazy on the intended semantics of pull when applied to types without coeffect-bearing parameters, so there may be some situation where this is wrong. My fix is on line 473 of the modified Deriving.hs and just unconditionally boxes the output.
3. When recursively applying pull to subterms, since pull returns a coeffected term, conflicts can arise between the type of the constructor's parameter and the type that it's pulled to. The only way I've found to solve this is to unbox the result with a let-binding. The fix here is more complex than the other two and appears on lines 252-283 of the modified Deriving.hs -- it duplicates mkConstructorApplication, puts it in the Checker monad (to get a free variable for the let), and reverses the order in which it processes the arguments so that it can properly match the types. I'm pretty sure it's correct, but it might be possible to structure better.