------------------------------------------------------------------------
-- The Agda standard library
--
-- Zero-cost coercion to cross the FFI boundary
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible #-}

module Foreign.Haskell.Coerce where

------------------------------------------------------------------------
-- Motivation

-- Problem: No COMPILE directives for common inductive types

-- In order to guarantee that the vast majority of the libary is
-- considered safe by Agda, we had to remove the COMPILE pragmas
-- associated to common inductive types.
-- These directives cannot possibly be checked by the compiler and
-- the user could define unsound mappings (e.g. swapping Bool's
-- true and false).

-- Solution: Essentially identical definitions + zero-cost coercions

-- To solve this problem, we have introduced a number of essentially
-- identical definitions in the Foreign.Haskell.* modules. However
-- converting back and forth between the FFI-friendly type and its
-- safe counterpart would take linear time.
-- This module defines zero cost coercions between these types.

------------------------------------------------------------------------
-- Definition

open import Level using (Level; _⊔_)
open import Agda.Builtin.Nat
open import Agda.Builtin.Int

import IO.Primitive.Core       as STD
import Data.List.Base          as STD
import Data.List.NonEmpty.Base as STD
import Data.Maybe.Base         as STD
import Data.Product.Base       as STD
import Data.Sum.Base           as STD

import Foreign.Haskell.Pair          as FFI
import Foreign.Haskell.Either        as FFI
import Foreign.Haskell.List.NonEmpty as FFI

private
  variable
    a b c d e f : Level
    A : Set a
    B : Set b
    C : Set c
    D : Set d

-- We define a simple indexed datatype `Coercible`. A value of
-- `Coercible A B` is a proof that `A` and `B` have the same underlying
-- runtime representation. The only possible proof is an incantation
-- from the implementer begging to be trusted.

-- We need this type to be concrete so that overlapping instances can be
-- checked for equality: we do not care what proof we get as long as we
-- get one.

-- We need for it to be a data type rather than a record type so that
-- Agda does not mistakenly build arbitrary instances by η-expansion.

data Coercible (A : Set a) (B : Set b) : Set where
  TrustMe : Coercible A B

{-# FOREIGN GHC data AgdaCoercible l1 l2 a b = TrustMe #-}
{-# COMPILE GHC Coercible = data AgdaCoercible (TrustMe) #-}

-- Once we get our hands on a proof that `Coercible A B` we postulate
-- that it is safe to convert an `A` into a `B`. This is done under the
-- hood by using `unsafeCoerce`.

postulate coerce : {{_ : Coercible A B}} → A → B

{-# FOREIGN GHC import Unsafe.Coerce #-}
{-# COMPILE GHC coerce = \ _ _ _ _ _ -> unsafeCoerce #-}

------------------------------------------------------------------------
-- Unary and binary variants for covariant type constructors

Coercible₁ : ∀ a c → (T : Set a → Set b) (U : Set c → Set d) → Set _
Coercible₁ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible (T A) (U B)

Coercible₂ : ∀ a b d e → (T : Set a → Set b → Set c) (U : Set d → Set e → Set f) → Set _
Coercible₂ _ _ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible₁ _ _ (T A) (U B)

------------------------------------------------------------------------
-- Instances

-- Nat

-- Our first instance reveals one of Agda's secrets: natural numbers are
-- represented by (arbitrary precision) integers at runtime! Note that
-- we may only coerce in one direction: arbitrary integers may actually
-- be negative and will not do as mere natural numbers.

instance

  nat-toInt : Coercible Nat Int
  nat-toInt = TrustMe

-- We then proceed to state that data types from the standard library
-- can be converted to their FFI equivalents which are bound to actual
-- Haskell types.

-- Product

  pair-toFFI : Coercible₂ a b c d STD._×_ FFI.Pair
  pair-toFFI = TrustMe

  pair-fromFFI : Coercible₂ a b c d FFI.Pair STD._×_
  pair-fromFFI = TrustMe

-- Sum

  either-toFFI : Coercible₂ a b c d STD._⊎_ FFI.Either
  either-toFFI = TrustMe

  either-fromFFI : Coercible₂ a b c d FFI.Either STD._⊎_
  either-fromFFI = TrustMe

-- NonEmpty

  nonEmpty-toFFI : Coercible₁ a b STD.List⁺ FFI.NonEmpty
  nonEmpty-toFFI = TrustMe

  nonEmpty-fromFFI : Coercible₁ a b FFI.NonEmpty STD.List⁺
  nonEmpty-fromFFI = TrustMe

-- We follow up with purely structural rules for builtin data types
-- which already have known low-level representations.

-- Maybe

  coerce-maybe : Coercible₁ a b STD.Maybe STD.Maybe
  coerce-maybe = TrustMe

-- List

  coerce-list : Coercible₁ a b STD.List STD.List
  coerce-list = TrustMe

-- IO

  coerce-IO : Coercible₁ a b STD.IO STD.IO
  coerce-IO = TrustMe

-- Function
-- Note that functions are contravariant in their domain.

  coerce-fun : {{_ : Coercible A B}} → Coercible₁ c d (λ C → B → C) (λ D → A → D)
  coerce-fun = TrustMe

-- Finally we add a reflexivity proof to discharge all the dangling
-- constraints involving type variables and concrete builtin types such
-- as `Bool`.

-- This rule overlaps with the purely structural ones: when attempting
-- to prove `Coercible (List A) (List A)`, should Agda use the proof
-- obtained by `coerce-refl` or the one obtained by `coerce-list coerce-refl`?
-- Because we are using a datatype with a single constructor these
-- distinctions do not matter: both proofs are definitionally equal.

  coerce-refl : Coercible A A
  coerce-refl = TrustMe