avoid `unsafeCoerce` with some `Coercible` use case

Question

In the current implementation of Coercible can we quantify over "representational preserving type constructors", to extract a safer proof in the code below

#!/usr/bin/env stack
-- stack --resolver lts-17.10 script
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
module SOQuestionCoercibleInstances0 where

import Data.Coerce
import Data.Constraint
import Data.Kind
import Data.Type.Equality as EQ
import Data.Typeable
import Unsafe.Coerce

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
newtype Id0 a = Id0 {unId0 :: a} deriving (Show)

newtype Id ef a = Id {unId :: ef a}

instance (forall x. (Coercible x (ef x))) => IsomorphismFromTo (Id0 a) (Id0 (ef a)) where
  isofromto (pa :: p (Id0 a)) = unsafeCoerce pa

a = Id0 (7 :: Int)

--- >>> show a
--- >>> show (to a :: Id0 (Id0 Int))
-- "Id0 {unId0 = 7}"
-- "Id0 {unId0 = Id0 {unId0 = 7}}"
-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
main :: IO ()
main = do
  print a
  print (to a :: Id0 (Id0 Int))

-- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
class IsomorphismFromTo a b where
  isofromto :: forall p. p a -> p b
  to :: a -> b
  default to :: IsomorphismFromTo a b => a -> b
  to = unId0 . isofromto . Id0
  from :: b -> a
  default from :: IsomorphismFromTo a b => b -> a
  from = r isofromto
    where
      r :: (forall p. p a -> p b) -> b -> a
      r to = let (Op f) = to @(Op (->) a) (Op id) in f

type Op :: (* -> * -> Type) -> * -> * -> Type
newtype Op m a b = Op (m b a)

Answer 1

Sort of. You can use the same quantified constraint trick you used in your instance:

class IsomorphismFromTo a b where
  isofromto :: forall p. (forall a b. Coercible a b => Coercible (p a) (p b)) => p a -> p b

This sort of accidentally restricts p to those types that have a representational role in the right place. I don't think there's a direct way to write that restriction exactly. Anyway, after that change, replacing unsafeCoerce with coerce in your existing instance works fine. And just to demonstrate that this is actually callable, in ghci:

> isofromto @(Id0 Int) @(Id0 (Id0 Int)) @Id0 (Id0 (Id0 3))
Id0 {unId0 = Id0 {unId0 = Id0 {unId0 = 3}}}

For a quick refresher on type application rules: the first type argument corresponds to a, the second to b, and the third to p.