Source code on Github
{-# OPTIONS --without-K #-}
module Class.Convertible.Foreign where

open import Meta.Prelude

open import Class.Functor
open import Class.Bifunctor

open import Class.Convertible.Core
open import Class.HasHsType.Core

open import Foreign.Haskell using (Pair; Either)
open import Foreign.Haskell.Coerce using (coerce)

instance
  Convertible-Pair : Convertible₂ _×_ Pair
  Convertible-Pair = λ where
    .to    coerce  bimap to to
    .from  bimap from from  coerce

  Convertible-Either : Convertible₂ _⊎_ Either
  Convertible-Either = λ where
    .to    coerce  bimap to to
    .from  bimap from from  coerce