InstanceArguments.agda

module InstanceArguments where

postulate A₁ A₂ B : Set
          f₁ : {{a : A₁}} → B
          f₂ : {{a : A₂}} → B
          a₁ : A₁

-- resolve from signature
test₁ : B
test₁ = f₁

-- resolve from context
test₂ : {{a : A₂}} → B
test₂ = f₂

postulate F : Set → Set
          fA₁ : F A₁
          fA₂ : F A₂
          f₃ : {A : Set} → {{fA : F A}} → A → B

test₃ : B
test₃ = f₃ a₁

record Rec (t : Set) : Set₁ where
       field
         v : t

open module RecWI {t : Set} {{r : Rec t}} = Rec r

postulate testT₁ : Set 
          testV₁ : testT₁
          testT₂ : Set 
          testV₂ : testT₂

testRec₁ : Rec testT₁
testRec₁ = record { v = testV₁ }
testRec₂ : Rec testT₂
testRec₂ = record { v = testV₂ }

-- needs constraint checking in instance argument resolution
test : testT₂
test = v