Using Nominal Roles for Type Inference

Question

I have a newtype with a phantom type, but I'm having trouble making easy use of it.

Consider the following example:

import Data.Coerce

newtype F a b = F b

myzip :: (Num b) => F a b -> F a b
myzip = (coerce (+)) myf

myf :: F a b
myf = undefined

GHC complains that it Couldn't match representation of type ‘a0’ with that of ‘Int’. Basically, the type of coerce (+) is F a0 -> F a -> F a, rather than the type I want, which is F a -> F a -> F a.

Given a's current role of phantom, this is reasonable. I'm wondering if there's a simple way to get type inference (I don't want to have to write out signatures, that's why I'm using coerce in the first place!) by some other method. In particular, I expected that if I restricted the role of the parameter a to nominal, then GHC would be able to tell that the only possible choice for the signature was the one I wanted. No such luck: GHC gives the same error.

In the event it matters, in my real code the role of a must be at least representational, and b must be nominal.

Answer 1

Let's start by looking at a few types:

coerce (+) :: (Num n, Coercible (n -> n -> n) b) => b
myf :: F c d

The first problem is that GHC has no hope of pinning down n so it can choose an implementation of (+).

Let's see what happens if we use scoped type variables to attempt a simple solution:

myzip :: forall a b . Num b => F a b -> F a b
myzip = coerce ((+) :: b -> b -> b) myf

This is not accepted. Why? Because the type of myf is ambiguous! We can see this more clearly if we expand out myzip with another argument:

myzip x = coerce ((+) :: b -> b -> b) myf x

From the way Coercible works with type constructors (->, in this case), we can line everything up and conclude that the type of myf must be coercible with b, where x :: F a b. But the type of myf in this context is ambiguous. GHC therefore has no way to select the appropriate Coercible instance between b and a type for myf. Because coerce is really the identity function under the hood, it doesn't matter which one is chosen, but GHC simply won't choose an instance based on an ambiguous type variable. To make this work, you need something like

myzip :: forall a b . Num b => F a b -> F a b
myzip = (coerce ((+) :: b -> b -> b)) (myf :: F a b)

Type roles

Type roles cannot (at least at present) guide instance resolution in any way. All they can do is determine what Coercible instances are generated. Given

class c => X d

GHC will conclude that X d entails c. But given

instance c => X d

GHC will not conclude that X d entails c. I'm not sure of the details of why, but that has always been the case.