[GHC] #14101: Type synonyms can make roles too conservative
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler | Version: 8.2.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- {{{#!hs import GHC.Exts type Arr# = Array# data Foo a = Foo (Arr# a) type role Foo representational }}} produces {{{ error: • Role mismatch on variable a: Annotation says representational but role nominal is required • while checking a role annotation for ‘Foo’ }}} If the type synonym is instead defined {{{#!hs type Arr# a = Array# a }}} then it works fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * keywords: => roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #8234 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * related: => #8234 Comment: I'm guessing this may relate to the fix for #8234, but I couldn't really say. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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 dfeuer): * failure: None/Unknown => GHC rejects valid program -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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: | -------------------------------------+------------------------------------- Comment (by goldfire): Sorry -- I wrote a post here but somehow it got lost. (I'm sure this is my fault.) This is by design. Any non-nominal role on a type parameter must be assigned to a proper type parameter to that type. When you eta-reduce, there's no place to put the non-nominal role. Happily, Ryan's patch solves the problem and looks utterly correct to me. So, while the synonym's argument's role is still nominal, that fact becomes irrelevant during role inference. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch 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): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D3838 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch 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): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): My concern is that this might not always do the best job with closed type families. In particular, we can produce a bound on the role of an application of a closed type family even if we can't reduce it. {{{#!hs type family Foo a where Foo 'True = Maybe Foo 'False = Either Int newtype Bar a b = Bar (Foo a b) }}} We know that `Foo a` must be `Maybe`, `Either Int`, or stuck. I believe it should therefore be safe to give `b` a representational role. My guess is that the right thing is to give type signatures and closed type families role annotations with the number of components determined by the number of arrows in their kinds. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch 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): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ethercrow): I'm not sure if it belongs to this ticket. I'm trying to make a specialization for leaves in a hashmap when key type is something small, e.g. Int: {{{ data LeafInt v = LI !Int v data LeafPoly k v = LP !k v type family Leaf a where Leaf Int = LeafInt Leaf k = LeafPoly k }}} The hashmap {{{ data HashMap k v = Leaf !Hash !(Leaf k v) ... }}} itself has a type role annotation: {{{ type role HashMap nominal representational }}} I get the error {{{ • Role mismatch on variable v: Annotation says representational but role nominal is required • while checking a role annotation for ‘HashMap’ }}} I tried to express the same using data family and a class with associated type, the result is the same. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch 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): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ethercrow): * cc: ethercrow (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: patch 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): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): comment:7 and comment:8 seem out of scope for this ticket. This ticket is about type synonyms, not type families. comment:7 seems utterly out of reach. As explained in the [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1010&context=compsci_pubs paper], any type application that's not a declared parameter of a type is considered nominal. I think we'd need to overhaul the roles design to get that. comment:8, though, seems approachable, in two steps. Step 1: use data families, not type families. Step 2: #8177, which will allow non-nominal roles on data families. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14101: Type synonyms can make roles too conservative
-------------------------------------+-------------------------------------
Reporter: dfeuer | Owner: (none)
Type: bug | Status: patch
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): Phab:D3838
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#14101: Type synonyms can make roles too conservative
-------------------------------------+-------------------------------------
Reporter: dfeuer | Owner: (none)
Type: bug | Status: patch
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): Phab:D3838
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ryan Scott
#14101: Type synonyms can make roles too conservative -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: fixed | Keywords: roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | roles/should_compile/T14101 Blocked By: | Blocking: Related Tickets: #8234 | Differential Rev(s): Phab:D3838 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * testcase: => roles/should_compile/T14101 * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14101#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC