title: avoid `unsafeCoerce` with some `Coercible` use case
body: <p>In the current implementation of <code>Coercible</code> can we quantify over &quot;representational preserving type constructors&quot;, to extract a safer proof in the code below</p>
  <pre class="lang-hs prettyprint-override"><code>#!/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))) =&gt; IsomorphismFromTo (Id0 a) (Id0 (ef a)) where
    isofromto (pa :: p (Id0 a)) = unsafeCoerce pa
  
  a = Id0 (7 :: Int)
  
  --- &gt;&gt;&gt; show a
  --- &gt;&gt;&gt; show (to a :: Id0 (Id0 Int))
  -- &quot;Id0 {unId0 = 7}&quot;
  -- &quot;Id0 {unId0 = Id0 {unId0 = 7}}&quot;
  -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
  main :: IO ()
  main = do
    print a
    print (to a :: Id0 (Id0 Int))
  
  -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- --
  class IsomorphismFromTo a b where
    isofromto :: forall p. p a -&gt; p b
    to :: a -&gt; b
    default to :: IsomorphismFromTo a b =&gt; a -&gt; b
    to = unId0 . isofromto . Id0
    from :: b -&gt; a
    default from :: IsomorphismFromTo a b =&gt; b -&gt; a
    from = r isofromto
      where
        r :: (forall p. p a -&gt; p b) -&gt; b -&gt; a
        r to = let (Op f) = to @(Op (-&gt;) a) (Op id) in f
  
  type Op :: (* -&gt; * -&gt; Type) -&gt; * -&gt; * -&gt; Type
  newtype Op m a b = Op (m b a)
  </code></pre>