# 8.1 Coercions

Since newtypes only differ in the type-system and not in their runtime representation, we can use a proof that types a and b have the same runtime representation to teach the type-system to convert between types a and b. These proofs are automatically generated by the compiler whenever we declare a newtype, and are not allowed to be manually written (there are other mechanisms for manually defining propositional type equality, like in Type.Reflection)

# 8.2 Roles

There are three varieties of roles, in order from strongest to weakest:

• Nominal, a ~ b
• Representational, Coercible a b
• Phantom, forall a b. Coercible (Proxy a) (Proxy b)

There are three inference rules for roles:

• All type parameters are at least phantom
• a -> b is representational in a and b (data constructors use ->)
• a ~ b is nominal in a and b, (GADTs, typefamilies use ~)

## Exercise 8.2 (i)

representational a, representational b

## Exercise 8.2 (ii)

phantom a