Difference between (Coercible f g) and (forall x. Coercible (f x) (g x))
{-# LANGUAGE QuantifiedConstraints, RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}
import Data.Coerce
import Data.Functor.Identity
import Data.Functor.Compose
coeA :: Coercible f g => f x -> g x
coeA = coerce
-- This doesn't work:
-- • Couldn't match representation of type ‘Identity’
-- with that of ‘Compose Identity Identity’
-- arising from a use of ‘coeA’
--
-- exA :: Identity a -> Compose Identity Identity a
-- exA = coeA
-- This works however.
exB :: Identity a -> Compose Identity Identity a
exB = coerce
-- and also
coeC :: (forall x. Coercible (f x) (g x)) => f x -> g x
coeC = coerce
exC :: Identity a -> Compose Identity Identity a
exC = coeC
-- So this works:
forward :: Coercible f g => ((forall x. Coercible (f x) (g x)) => r) -> r
forward k = k
-- but this doesn't?
-- backwards :: (forall x. Coercible (f x) (g x)) => (Coercible f g => r) -> r
-- backwards k = k
-- but what is the difference between
--
-- Coercible f g
--
-- and
--
-- (forall x. Coercible (f x) (g x))
--
-- As far as I can tell from reading zero-cost coercions paper,
-- Co_App rule:
--
-- Γ ⊢ γ₁ : τ₁ ~ρ σ₁
-- Γ ⊢ γ₂ : τ₂ ∼N σ₂
-- Γ ⊢ τ₁ τ₂ : κ
-- Γ ⊢ σ₁ σ₂ : κ
-- --------------------------
-- Γ ⊢ γ₁ γ₂ : τ₁ τ₂ ~ρ σ₁ σ₂
--
-- Is used to show the forward direction,
-- but why the backwards, functional-extensionality -like, direction is not included?
-- What will break?
--
-- It feels that there could be some kind of Co_Abs rule, essentially doing the opposite of Co_App.
EDIT: This obviously affects ~
equality too. I don't see why f ~ g
and forall x. f x ~ g x
would not be equivalent in GHC type system.