``可固定的''用于Uni-Constructor类型和`（）''

Question

可以将这种类型强制为（）：

newtype Foo = Foo ()
f :: Foo -> ()
f = coerce

但是以下几点不能：

data Foo = Foo
f :: Foo -> ()
f = coerce  -- Fails: Couldn't match representation of type ‘Foo’ with that of ‘()’

GHC说，

    • Couldn't match representation of type ‘Foo’ with that of ‘()’
        arising from a use of ‘coerce’
    • In the expression: coerce
      In an equation for ‘f’: f = coerce
   |
69 | f = coerce

有没有办法使第二个 foo 可牢固地（）？毕竟它们都是同构。失败，自动创建这些同构的方法是什么？对于更大的上下文，请参见这个问题（其中构造函数的产品类型可固定在 ns 的类型级列表元素类型）。

@iceland_jack的建议

尝试杰克的建议在评论中通过通用 rep ：

class (GHC.Generic a, GHC.Generic b, Coercible (GHC.Rep a ()) (GHC.Rep b ())) => HasSameRep a b where
  coerceViaRep :: I a -> I b

instance
  ( Generic a
  , Generic b
  , Coercible (GHC.Rep a ()) (GHC.Rep b ())
  ) =>
  HasSameRep a b
  where
  coerceViaRep = I . GHC.to @_ @() . coerce . GHC.from @_ @() . unI

data T = T

proof :: T -> ()
proof = unI . coerceViaRep . I

这失败了，但是：

src/Ema/Route/Generic/Sub.hs:122:15-26: error:
    • Couldn't match representation of type: GHC.U1 @Type ()
                               with that of: GHC.Rep T ()
        arising from a use of ‘coerceViaRep’
    • In the first argument of ‘(.)’, namely ‘coerceViaRep’
      In the second argument of ‘(.)’, namely ‘coerceViaRep . I’
      In the expression: unI . coerceViaRep . I
    |
122 | proof = unI . coerceViaRep . I

看起来不像基本的通用表示实际上是相同的吗？

Answer 1

应用 @iceland_jack的建议（另请参见这个答案

{- | Types `a` and `b` are isomorphic via their generic representation

  Unlike `Coercible` this constraint does not require that the two types have
  identical *runtime* representation. For example, `data Foo = Foo` is not
  coercible to `()` (they have different runtime representations), but they are
  both isomorphic via their generic representation.
-}
class (Generic a, Generic b, GHC.Rep a () `Coercible` GHC.Rep b ()) => GIsomorphic a b where
  giso :: Iso' a b

instance (Generic a, Generic b, GHC.Rep a () `Coercible` GHC.Rep b ()) => GIsomorphic a b where
  giso =
    iso
      (GHC.to @b @() . coerce . GHC.from @a @())
      (GHC.to @a @() . coerce . GHC.from @b @())

data T (s :: Symbol) = T
  deriving stock (Generic)

proof :: T "foo" -> ()
proof = view giso

）将 giso 定义为顶级功能，但是在我的情况下，我需要一个约束，以与 gensixs-sop 's trans_ns 一起使用。