Arbitrary evaluation in the type signature in agda

Question

So I have another "simple" Adga question. I wanted to have a proof that used arbitrary evaluations as premises and results. But I don't think I know the type system well enough to do that.

as a simple example take

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> (R a)
f aa rr = rr aa

which has a compilation error

Set !=< rr aa of type Set1
when checking that the expression rr aa has type rr aa

of course

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> Set
f aa rr = rr aa

compiles fine

as does

f : {S : Set} -> (a : S) 
 -> ( R : S -> Set) 
 -> (R a)
 -> (R a)
f _ _ ra = ra

What does (R a) means in context? Can it be constructed? How can it be constructed?

Answer 1

In your first example the expression rr aa has type Set, because it is the result of the application of aa of type S to the function rr of type S -> Set.

The type signature of your function demands a result type of R a though. Given the naming of your parameters the expected result type is rr aa. The type checker now tries to unify the expected type (rr aa) with the expression type (Set) and fails.

In fact a function of the type given above would be inconsistent with the type theory:

no-f : (f : {S : Set} → (a : S) → (R : S → Set) → R a) → ⊥
no-f f = f tt (λ _ → ⊥)

In other words, assuming there was a function of the type above, an element of the empty type (⊥) could be produced. So in general you cannot construct elements of type R a without additional requirements.

Imports used above:

open import Data.Empty
open import Data.Unit