How to restrict roles on class parameters-CodePudding

The following code:

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

class C (f :: Type -> Type) where
  g :: String -> f a

class D a where
  h :: C f => a -> f a

instance C Maybe where
  g _ = Nothing

instance C (Either String) where
  g = Left 

instance D Int where
  h = g . show

newtype NewInt = NewInt Int deriving newtype D

fails to compile with the following error:

  Couldn't match representation of type: f Int
                           with that of: f NewInt
    arising from the coercion of the method ‘h’

Which I guess makes sense, if f does some weird type family stuff. But my fs do not, there just Maybe and Either, so replacing Int with it's newtype NewInt should probably work I believe.

How can I convince GHC of this (assuming I'm not wrong). I presume it's some RoleAnnotations thing required but nothing I have tried has worked.

CodePudding user response：

It's not possible to do this in GHC today. You cannot give role annotations to parameters of type variables (like your f).

Note that this is not special to type classes, you get the same problem with data types:

data E (f :: Type -> Type) a = MkE (f a)

foo :: E Maybe Int
foo = MkE Nothing

bar :: E Maybe NewInt
bar = coerce foo -- <<< error

CodePudding user response：

We can not at the moment specify roles of quantified type variables, unfortunately. The closest I was able to conjure is the following, leveraging safe coercions.

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE QuantifiedConstraints #-}

import Data.Kind
import Data.Coerce

class (forall a b . Coercible a b => Coercible (f a) (f b))
      => C (f :: Type -> Type) where
  g :: String -> f a

Note the superclass requirement, which more-or-less requires a representational role, or more precisely its analogous with coercions.

The rest is the same code as yours:

class D a where
  h :: C f => a -> f a

instance C Maybe where
  g _ = Nothing

instance C (Either String) where
  g = Left 

instance D Int where
  h = g . show

We do have to change the newtype .. deriving to a custom instance, but at least we can simply call coerce and let it do its magic.

newtype NewInt = NewInt Int
  -- No "deriving newtype D" here

-- explicit instance using "coerce"
instance D NewInt where 
  h :: forall f. C f => NewInt -> f NewInt
  h = coerce (h @Int @f)