CoercibleSumTypes.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE Unsafe #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
module CoercibleSumTypes (adtCoerce, ADTCoerce) where

import Data.Coerce (Coercible)
import GHC.Exts (Constraint)
import GHC.Generics
import GHC.TypeLits (ErrorMessage(..), TypeError(..))
import Unsafe.Coerce (unsafeCoerce)

adtCoerce :: (Generic a, Generic b, ADTCoerce (Rep a) (Rep b)) => a -> b
adtCoerce = unsafeCoerce

type family ADTCoerce (f :: * -> *) (g :: * -> *) :: Constraint where
  ADTCoerce V1                          V1                          = ()
  ADTCoerce U1                          U1                          = ()
  ADTCoerce (Rec0 c1)                   (Rec0 c2)                   = Coercible c1 c2
  ADTCoerce (URec a)                    (URec a)                    = ()
  ADTCoerce (f1 :+: g1)                 (f2 :+: g2)                 = (ADTCoerce f1 f2, ADTCoerce g1 g2)
  ADTCoerce (f1 :*: g1)                 (f2 :*: g2)                 = (ADTCoerce f1 f2, ADTCoerce g1 g2)
  ADTCoerce (D1 ('MetaData _ _ _ nt) f) (D1 ('MetaData _ _ _ nt) g) = ADTCoerce f g
  ADTCoerce (D1 ('MetaData _ _ _ _) _)  (D1 ('MetaData _ _ _ _) _)  = TypeError ('Text "ADTCoerce: One is a datatype, the other is a newtype")
  ADTCoerce (C1 _ f)                    (C1 _ g)                    = ADTCoerce f g
  ADTCoerce (S1 ('MetaSel _ _ _ ds) f)  (S1 ('MetaSel _ _ _ ds) g)  = ADTCoerce f g
  ADTCoerce (S1 ('MetaSel _ _ _ _) _)   (S1 ('MetaSel _ _ _ _) _)   = TypeError ('Text "ADTCoerce: Fields have different strictness properties")
  ADTCoerce _                           _                           = Impossible

class Impossible

CoercibleSumTypesExample.hs

{-# LANGUAGE DeriveGeneric #-}
module Main (main) where

import CoercibleSumTypes
import GHC.Generics

-- data Maybe a = Nothing | Just a
data Option a = None | Some a
  deriving (Eq, Ord, Read, Show, Generic)

newtype MyInt = MyInt Int
  deriving (Eq, Ord, Read, Show)

data B = F | T
  deriving (Eq, Ord, Read, Show, Generic)

main :: IO ()
main = do
  print (adtCoerce (Some 42 :: Option Int) :: Maybe MyInt)
  print (adtCoerce F :: Bool)