This type can be coerced to ()
:
newtype Foo = Foo ()
f :: Foo -> ()
f = coerce
But the following cannot:
data Foo = Foo
f :: Foo -> ()
f = coerce -- Fails: Couldn't match representation of type ‘Foo’ with that of ‘()’
GHC says,
• 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
Is there a way to make that second Foo
coercible to ()
? They are both isomorphic after all. Failing this, what is the way to automatically create these isomorphisms? For a larger context, see this question (where the constructor's product type is coercible to the NS
's type-level list element type).
@Iceland_Jack's suggestion
Trying Jack's suggestion in comments to go via generic 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
This fails, however:
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
It doesn't look like the underlying generic representation is in fact equal?
CodePudding user response:
Applying @Iceland_Jack's suggestion (also see this answer) in the comments here's what I came up with:
{- | 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
You could eliminate the typeclass and define giso
as a top-level function, but in my case I need a constraint for use with generics-sop
's trans_NS
. https://github.com/EmaApps/ema/pull/81/commits/760fd793104ae4235055ad49c94ac014f014496e