Roles and higher-kinded types

RoleTest.hs

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE ViewPatterns    #-}

{-# OPTIONS_GHC -Wall #-}

module RoleTest where

import GHC.Exts
import Unsafe.Coerce

{-------------------------------------------------------------------------------
  Simple example of a higher-kinded type
-------------------------------------------------------------------------------}

data App f a = UnsafeApp (f Any)

-- Declaring a to be representational is problematic, see below
type role App representational representational

fromApp :: App f a -> f a
fromApp (UnsafeApp x) = unsafeCoerce x

pattern App :: f a -> App f a
pattern App x <- (fromApp -> x)
  where
    App x = UnsafeApp (unsafeCoerce x)

{-# COMPLETE App #-}

hmap :: (f a -> g a) -> App f a -> App g a
hmap f (App x) = App (f x)

{-------------------------------------------------------------------------------
  First argument representational

  This means that if @Coercible f g@, then @Coercible (App f a) (App g a)@,
  where @Coercible f g@ implies, for all @x@, @Coercible (f x) (g x)@
  (see "Safe Zero-cost Coercions for Haskell", Section 2.8,
  "Supporting higher order polymorphism").

  NOTE: The example below does not work if we define

  > newtype Id2 a = Id2 a

  because the above implication is in one direction only.
-------------------------------------------------------------------------------}

coerceF :: Coercible f g => App f a -> App g a
coerceF = coerce

newtype Id1 a = Id1 a
newtype Id2 a = Id2 (Id1 a)

changeId :: App Id1 a -> App Id2 a
changeId = coerceF

{-------------------------------------------------------------------------------
  Second argument representational

  This is problematic, because we do not know what the @f@ parameter does.
-------------------------------------------------------------------------------}

newtype Age = MkAge Int -- the age-old counter-example that motivated roles

type family F a where
  F Int = Int
  F Age = Bool

newtype WrapF a = WrapF { unwrapF :: F a }

trouble :: App f Int -> App f Age
trouble = coerce

oops :: Int -> Bool
oops =
      unwrapF
    . fromApp
    . (trouble :: App WrapF Int -> App WrapF Age)
    . App
    . (WrapF :: Int -> WrapF Int)

-- We kind of what to be able to say that @App@ is representational in its
-- argument /if and only/ @f@ is; that is, @App@ /preserves/ this property of
-- @f@. But we cannot currently express that in Haskell's role language.