module InstanceArguments.08-higherOrder where

explicitize : ∀ {A : Set} {B : A → Set} → ({{x : A}} → B x) → (x : A) → B x
explicitize f x = f {{x}}

implicitize : ∀ {A : Set} {B : A → Set} → ((x : A) → B x) → {{x : A}} → B x
implicitize f {{x}} = f x

data T : Set where
  tt : T

test = explicitize (λ {{t : T}} → t)
