does this GADT actually have type role representational

Question

This data type can have type role HCons' representational representational, which allows using coerce to add or remove newtypes applied to the elements, without needing to traverse the list.

data HNil' = HNil'
data HCons' a b = HCons' a b

However the syntax for those lists is not as nice as those with the following GADT

data HList (l::[*]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)

I have a class to convert between these two representations, such that Prime (HList [a,b]) ~ HCons' a (HCons' b HNil'). Does that class make

coerceHList :: Coercible (Prime a) (Prime b) => HList a -> HList b
coerceHList = unsafeCoerce

safe?

Schram

FWIW, yes, I think so. But I don't know enough about the internals of roles to actually make a convincing argument. Your example seems to be another case where the current role system is not quite expressive enough. – Fardel

Answer 1

I don't think the existence of a conversion on its own is enough. For example, the following also lets me convert between a GADT and a coercible pair of types, but it certainly wouldn't be safe to directly coerce the GADT:

newtype Age = Age Int

data Foo a where
   I :: Bool -> Int -> Foo Int
   A :: Age -> Bool -> Foo Age

class ConvFoo a where
   toFoo :: (Bool, a) -> Foo a
   fromFoo :: Foo a -> (Bool, a)

instance ConvFoo Int where
   toFoo (b, i) = I b i
   fromFoo (I b i) = (b, i)

instance ConvFoo Age where
   toFoo (b, a) = A a b
   fromFoo (A a b) = (b, a)

I could also trivially define an UnFoo type function similar to Prime.

I think the key difference between the two examples is that in mine, Age and Int do have the same representation, whereas in yours '[] and e':l don't have the same representation.

So there's still a case for saying, as you suggest in the title, that l has type role representational, because it's kind of obvious that HList l1 and HList l2 have the same representations if l1 and l2 have the same representations.

However since in theory representations are implementation-dependent, I don't think you can ever consider this absolutely safe until GHC accepts it directly.

Delaney

I'm not so sure about "it's kind of obvious that HList l1 and HList l2 have the same representations if l1 and l2 have the same representations". We could write HCons :: (el ~ (e ': l)) => e -> HList l -> HList el. Then it is possible ghc stores something for el ~ (e ': l) that references the original e, el, l types, and not the ones that are currently in the constructor? – Schram

Even then, every HCons would still have the same surface representation as every other HCons, wouldn't it? So if e and HList l also had the same representations then the whole HCons would. – Delaney

I think the key point is that ': and '[] are concrete types that must be different, so there's no risk of confusing HCons and HNil. I'm not at all sure how to formulate the condition precisely though! – Delaney