Opened 2 years ago

Closed 2 years ago

#14101 closed bug (fixed)

Type synonyms can make roles too conservative

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler (Type checker) Version: 8.2.1
Keywords: roles Cc: goldfire, RyanGlScott, ethercrow
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: roles/should_compile/T14101
Blocked By: Blocking:
Related Tickets: #8234 Differential Rev(s): Phab:D3838
Wiki Page:

Description

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

type Arr# a = Array# a

then it works fine.

Change History (13)

comment:1 Changed 2 years ago by dfeuer

Keywords: roles added

comment:2 Changed 2 years ago by dfeuer

I'm guessing this may relate to the fix for #8234, but I couldn't really say.

comment:3 Changed 2 years ago by dfeuer

Type of failure: None/UnknownGHC rejects valid program

comment:4 Changed 2 years ago by RyanGlScott

Cc: goldfire RyanGlScott added

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 simply:

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:

  • compiler/typecheck/TcTyClsDecls.hs

    diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
    index 17da32f..512601f 100644
    a b checkValidRoles tc 
    29942994        ex_roles   = mkVarEnv (map (, Nominal) ex_tvs)
    29952995        role_env   = univ_roles `plusVarEnv` ex_roles
    29962996
     2997    check_ty_roles env role ty
     2998      | Just ty' <- coreView ty
     2999      = check_ty_roles env role ty'
     3000
    29973001    check_ty_roles env role (TyVarTy tv)
    29983002      = case lookupVarEnv env tv of
    29993003          Just role' -> unless (role' `ltRole` role || role' == role) $
  • compiler/typecheck/TcTyDecls.hs

    diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
    index 41482cc..6d70077 100644
    a b irDataCon datacon 
    580580irType :: VarSet -> Type -> RoleM ()
    581581irType = go
    582582  where
     583    go lcls ty                 | Just ty' <- coreView ty
     584                               = go lcls ty'
    583585    go lcls (TyVarTy tv)       = unless (tv `elemVarSet` lcls) $
    584586                                 updateRole Representational tv
    585587    go lcls (AppTy t1 t2)      = go lcls t1 >> markNominal lcls t2
  • compiler/types/Coercion.hs

    diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
    index b0b13b8..214fe2d 100644
    a b ty_co_subst lc role ty 
    15131513  = go role ty
    15141514  where
    15151515    go :: Role -> Type -> Coercion
     1516    go r ty                | Just ty' <- coreView ty
     1517                           = go r ty'
    15161518    go Phantom ty          = lift_phantom ty
    15171519    go r (TyVarTy tv)      = expectJust "ty_co_subst bad roles" $
    15181520                             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.

comment:5 Changed 2 years ago 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.

comment:6 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3838
Status: newpatch

comment:7 Changed 2 years ago 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.

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

comment:8 Changed 2 years ago 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.

comment:9 Changed 2 years ago by ethercrow

Cc: ethercrow added

comment:10 Changed 2 years ago 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 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.

comment:11 Changed 2 years ago by Ryan Scott <ryan.gl.scott@…>

In 0bb1e840/ghc:

Expand type synonyms during role inference

Summary:
During role inference, we need to expand type synonyms, since
oversaturated applications of type synonym tycons would otherwise have overly
conservative roles inferred for its arguments.

Fixes #14101.

Test Plan: ./validate

Reviewers: goldfire, austin, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie

GHC Trac Issues: #14101

Differential Revision: https://phabricator.haskell.org/D3838

comment:12 Changed 2 years ago by Ryan Scott <ryan.gl.scott@…>

In c6462ab/ghc:

Add test for #14101

I forgot to do this in
0bb1e84034a12d7f700b48fca6710c01bd08f397.

comment:13 Changed 2 years ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: roles/should_compile/T14101
Note: See TracTickets for help on using tickets.