Implementing coercions through instances in Agda

CoercionsAsInstances.agda

-- An attempt to implement implicit coercions via Agda's instance
-- argument resolution.  The basic principle works, but Agda's
-- instance resolution is a bit too weak to scale it to big examples
-- because it is hard to implement chains of coercions.

-- Doesn't help: {-# OPTIONS --overlapping-instances #-}

record Coercion {a} (x y : Set a) : Set a where
  constructor ⌞_⌟
  field coe : x → y

open Coercion

-- Composition/transitivity of coercions

_⊚_ : ∀ {a} {A B C : Set a} → Coercion A B → Coercion B C → Coercion A C
_⊚_ c d = ⌞ (λ x → coe d (coe c x)) ⌟

-- A version of application that takes a coercion

_$_ : ∀ {a b} {A A′ : Set a} {B : Set b} → (A → B) →
      {{c : Coercion A′ A }} → A′ → B
_$_ f {{c}} a = f (coe c a)

postulate
  Human    : Set
  Fish     : Set
  Baracuda : Set
  Animal   : Set
  runs     : Animal → Set
  humansAreAnimals : Human    → Animal
  fishAreAnimals   : Fish     → Animal
  baracudasAreFish : Baracuda → Fish
  henry : Human
  bob   : Baracuda

-- used below

instance
  -- basic coercions
  humansAreAnimalsCoe = ⌞ humansAreAnimals ⌟
  fishAreAnimalsCoe   = ⌞ fishAreAnimals ⌟
  baracudasAreFishCoe = ⌞ baracudasAreFish ⌟

  -- Apparently this doesn't work because this instance conflicts with
  -- every other instance. (This would have workded in Scala...)
  
  --⊚-inst : ∀ {a} {A B C : Set a} →
  --         {{c : Coercion A B}} → {{d : Coercion B C}} → Coercion A C
  --⊚-inst {{c}} {{d}} = c ⊚ d

  -- OK, but we can still compose by hand

  baracudasAreAnimals = baracudasAreFishCoe ⊚ fishAreAnimalsCoe


henryRuns : Set
henryRuns = --runs henry   -- fails: Human !=< Animal
            runs $ henry   -- OK!

bobRuns : Set
bobRuns = runs $ bob