Making instance resolution loop

InstanceLoop.agda

module InstanceLoop where

record Target (A : Set) : Set where
  constructor mkTarget
  field
    a : A

instance

  loop : {A : Set} {{tA : Target A}} → Target A
  loop {{tA}} = tA

open import Data.Nat

extract : {A : Set} {{tA : Target A}} → A
extract {{tA}} = Target.a tA

argh! : ℕ
argh! = extract