[GHC] #14101: Type synonyms can make roles too conservative

[GHC]

#14101: Type synonyms can make roles too conservative
-------------------------------------+-------------------------------------
        Reporter:  dfeuer            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  8.2.1
  checker)                           |
      Resolution:                    |             Keywords:  roles
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #8234             |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: goldfire, RyanGlScott (added)


Comment:

 At the very least, I know why that program is currently rejected. When
 role inference occurs, GHC uses the `tyConRolesX` function to look up the
 roles of a `TyCon`. The implementation of `tyConRolesX` is
 [http://git.haskell.org/ghc.git/blob/14457cf6a50f708eecece8f286f08687791d51f7:/compiler/typecheck/TcTyDecls.hs#l636
 simply]:

 {{{#!hs
 lookupRolesX :: TyCon -> RoleM [Role]
 lookupRolesX tc
   = do { roles <- lookupRoles tc
        ; return $ roles ++ repeat Nominal }
 }}}

 In other words, if a `TyCon` is applied to more arguments than it was
 originally supplied in its definition, then the roles of these additional
 arguments will all be inferred as nominal. This is why the reported
 behavior only manifests when you define `Arr#` as `type Arr# = Array#`,
 and not `type Arr# a = Array# a`.

 Upon realizing this, my inclination to fix this bug is to simply expand
 all type synonyms during role inference. Indeed, if you apply this patch:

 {{{#!diff
 diff --git a/compiler/typecheck/TcTyClsDecls.hs
 b/compiler/typecheck/TcTyClsDecls.hs
 index 17da32f..512601f 100644
 --- a/compiler/typecheck/TcTyClsDecls.hs
 +++ b/compiler/typecheck/TcTyClsDecls.hs
 @@ -2994,6 +2994,10 @@ checkValidRoles tc
          ex_roles   = mkVarEnv (map (, Nominal) ex_tvs)
          role_env   = univ_roles `plusVarEnv` ex_roles

 +    check_ty_roles env role ty
 +      | Just ty' <- coreView ty
 +      = check_ty_roles env role ty'
 +
      check_ty_roles env role (TyVarTy tv)
        = case lookupVarEnv env tv of
            Just role' -> unless (role' `ltRole` role || role' == role) $
 diff --git a/compiler/typecheck/TcTyDecls.hs
 b/compiler/typecheck/TcTyDecls.hs
 index 41482cc..6d70077 100644
 --- a/compiler/typecheck/TcTyDecls.hs
 +++ b/compiler/typecheck/TcTyDecls.hs
 @@ -580,6 +580,8 @@ irDataCon datacon
  irType :: VarSet -> Type -> RoleM ()
  irType = go
    where
 +    go lcls ty                 | Just ty' <- coreView ty
 +                               = go lcls ty'
      go lcls (TyVarTy tv)       = unless (tv `elemVarSet` lcls) $
                                   updateRole Representational tv
      go lcls (AppTy t1 t2)      = go lcls t1 >> markNominal lcls t2
 diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
 index b0b13b8..214fe2d 100644
 --- a/compiler/types/Coercion.hs
 +++ b/compiler/types/Coercion.hs
 @@ -1513,6 +1513,8 @@ ty_co_subst lc role ty
    = go role ty
    where
      go :: Role -> Type -> Coercion
 +    go r ty                | Just ty' <- coreView ty
 +                           = go r ty'
      go Phantom ty          = lift_phantom ty
      go r (TyVarTy tv)      = expectJust "ty_co_subst bad roles" $
                               liftCoSubstTyVar lc r tv
 }}}

 Then the program reported in this ticket compiles, and all tests pass.

 The more difficult question to answer, however, is if this is the correct
 way to go about things. At one point in time, it used to be possible to
 annotate type synonyms with role annotations, which would make the idea of
 eagerly expanding all type synonyms during role inference quite unsound.
 But post-#8234, role-annotating type synonyms isn't possible, so all
 (inferred) type synonym roles are as general as possible. This leads me to
 believe that expanding type synonyms eagerly would be sound.

 In any case, it'd be helpful to hear from Richard before we proceed
 further.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14101#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler