WIP: Roles for closed type families
Changes PlannedPublic

Authored by RyanGlScott on Jun 21 2017, 12:23 AM.

Details

Reviewers
goldfire
bgamari
austin
Trac Issues
#8177
Summary

An attempt at adding roles for a subet of type families (closed ones).
Not everything is working yet - see T8177_glguy for an example of a test
that feels like it should typecheck, but currently doesn't.

Test Plan

./validate

RyanGlScott created this revision.Jun 21 2017, 12:23 AM
RyanGlScott planned changes to this revision.Jun 21 2017, 12:26 AM
RyanGlScott added inline comments.
testsuite/tests/roles/should_compile/T8177_glguy.hs
15

This currently fails to typecheck with this rather inscrutable error message:

T8177_glguy.hs:14:13: error:
    • Couldn't match type ‘Op n0 b0 c0’ with ‘Op n b c’
      Expected type: Op n a c -> Op n b c
        Actual type: Op n0 a0 c0 -> Op n0 b0 c0
      NB: ‘Op’ is a type function, and may not be injective
      The type variables ‘n0’, ‘b0’, ‘c0’ are ambiguous
    • In the ambiguity check for ‘coerceOp’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        coerceOp :: Coercible a b => Op n a c -> Op n b c

Does anyone know what might be going on here?

goldfire edited edge metadata.Jun 25 2017, 8:05 AM

I suppose this is just a start, as you note. I like the general direction, but I think some more attention needs to be paid around the distinction between tyvars in the tycon and in the equations.

compiler/typecheck/TcTyClsDecls.hs
827

Maybe I'm being dense, but I'm surprised to see this. Shouldn't these roles come from a role annotation?

1192

This most certainly needs commentary. What is this doing?

2896

This line looks wrong. tyConKind tc will be closed (that is, it will quantify over all the kind variables necessary), so that the variables mentioned in the kind won't be in the role_env.

Instead, you can look for variables mentioned in the kinds of the tyConTyVars.

2900

These roles (and type variables) are different than the ones on the tycon. You want to be checking the *tycon* roles here, not the equation roles. (Well, actually, you want to check both, I suppose.)

compiler/typecheck/TcTyDecls.hs
473

I think you mean "scrutinized".

610

This statement is similarly suspicious. I don't think tyConKind is going to work for you. Instead, marking the kind variables to be nominal can happen just once at the beginning. Use tyConTyVars.

678

Need comments here.

753

The old algorithm also ignored tyvars that are used only in coercions. This new one doesn't.

compiler/types/TyCoRep.hs
1539

Ah. The comment is the function that you want during role inference, but the name of the function means something different.

RyanGlScott added inline comments.Jun 25 2017, 10:35 AM
compiler/typecheck/TcTyClsDecls.hs
827

No, this Diff only covers closed type families for now, as they are substantially easier to deal with than open ones. I can add a comment here explaining this.

1192

Yeah, I sort of avoided adding commentary here for the moment, since there's still some lingering bugs that I don't understand, and just in case this design ends up being wrong, I didn't want to devote a huge chunk of time documenting something that would be thrown out later.

But since you asked, all this is doing is computing a map from every branch tyvar to its respective inherited role. The mb_tc_roles argument describes the roles of TyCon's tyvars, not the branch's tyvars, so we have to gather the free variables (i.e., branch variables) of each type pattern to figure out what role they should inherit.

2896

This line looks wrong. tyConKind tc will be closed (that is, it will quantify over all the kind variables necessary), so that the variables mentioned in the kind won't be in the role_env.

Oops! Good catch.

Instead, you can look for variables mentioned in the kinds of the tyConTyVars.

Well, that would grab some of the kinds, but not all. For instance:

type family Any :: k where {}

In Any, k is not the kind of any TyCon tyvar. How would I grab k here (without using tyConKind)?

2900

They are different, but as I note in https://ghc.haskell.org/trac/ghc/ticket/8177#comment:39, the roles for the branch tyvars are inherited from the TyCon tyvars, so it feels quite redundant to check both.

compiler/types/TyCoRep.hs
1539

Sure. I can't think of a good name that captures both ideas without getting into Java levels of ridiculous function name lengths, though...

austin resigned from this revision.Nov 9 2017, 5:35 PM