Coerce dictionaries

coerceDict.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE IncoherentInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import GHC.Types
import Data.Coerce

type role Mon representational
class Mon a where
  unit :: a
  mult :: a -> a -> a

newtype MonoidAdd = MAdd Int deriving newtype (Num) 
newtype MonoidMul = MMul Int deriving newtype (Num)

instance Mon MonoidAdd where
  unit = 0
  mult = (+)

instance Mon MonoidMul where
  unit = 1
  mult = (*)

data D c where D :: c => D c

trash :: forall ty. (Coercible ty Int, Mon ty) => D (Mon Int)
trash = coerce (D :: D (Mon ty))

test :: D (Mon Int) -> IO ()
test D = do
  print (unit @Int)
  print (mult @Int 10 20)

main :: IO ()
main = do
  test (trash @MonoidAdd)
  test (trash @MonoidMul)