Search code examples
haskellcoercion

`Coercible` for uni-constructor types and `()`

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?

Solution

  • 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