Type synonyms can still make roles too conservative
Summary
In some cases, GHC reduces type synonyms during role checking (see #14101 (closed)). However it seemingly does not reduce all type synonyms, in particular those occurring underneath parameters. Thus if a synonym eliminates another parameter, that parameter may still be conservatively assigned nominal role when it could be phantom.
Steps to reproduce
Consider the following program:
{-# LANGUAGE RoleAnnotations #-}
type T a = Int
type role M nominal phantom
data M f a = MkM (f (T a))
type role N nominal phantom
data N f a = MkN (f Int)
Compiling this produces:
RoleTypeSynonym.hs:5:1: error:
• Role mismatch on variable a:
Annotation says phantom but role nominal is required
• while checking a role annotation for ‘M’
|
5 | type role M nominal phantom
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Note that N
is accepted, and is identical apart from reducing the type synonym. Thus it is possible to work around the problem by manually reducing type synonym applications.
Expected behavior
This program should be accepted. In the absence of the role annotation, the a
parameter of M
should be assigned phantom role.
Environment
- GHC version used: 9.0.1, 9.2.0