#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... 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