[Agda] constructor-headed functions to Set

[Brandon Moore]

I was hoping to use the handling of "constructor-headed functions"to make it possible to write functions whose return type is
computed from implicit arguments (without always explicitly
supplying the arguments).

It seems to work if the body of a definition is just the
function with a computed return type, but
not if it's applied to any additional arguments
(which correspond to computed arrows).

In the example below I've supplied _ for explicit
arguments to make it a little clearer what is
not being inferred

module test where
open import Data.Nat

data T : Set where A : T → T ; R : T

tsem : T → Set
tsem R = ℕ
tsem (A t) = ℕ → tsem t

f : (t : T) → tsem t
f R = 0
f (A x) = λ _ → f x

test1 : ℕ → ℕ → ℕ
test1 = f _ -- inferred

test2 : ℕ
test2 = f _ 1 2 -- not inferred

{-
 Fixing the case above would be enough
 to allow the code I want to write now,
 but along the way I considered some code
 that might depend on a slightly more general
 idea of "constructor-headed function".

 When the following function is partially applied
 to anything but a function type, it seems like
 inference should also be able to solve constraints,
 but psem ℕ doesn't work as well as tsem
-}

psem : Set → T → Set
psem X R = X
psem X (A t) = ℕ → psem X t

f' : (t : T) → psem ℕ t
f' R = 0
f' (A x) = λ _ → f' x

test1' : ℕ → ℕ → ℕ
test1' = f' _ -- not inferred

Brandon