More comments on role subtyping, unsoundness fix.
ClosedPublic

Authored by ezyang on Feb 26 2017, 10:36 PM.

Details

Summary
  • We incorrectly allowed subroling on injective data in some cases. There is now a test to check for this case, and a Note.
  • More commentary on how the subtyping with roles works.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

Test Plan

validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
ezyang created this revision.Feb 26 2017, 10:36 PM
bgamari accepted this revision.Mar 1 2017, 1:35 PM

Tricky stuff but the note describes it well.

This revision is now accepted and ready to land.Mar 1 2017, 1:35 PM
goldfire edited edge metadata.Mar 1 2017, 2:07 PM

Otherwise, looks good.

compiler/typecheck/TcRnDriver.hs
1140

Clarify that T is abstract here. If I paste this literally into a Haskell buffer, it should work!

ezyang updated this revision to Diff 11470.Mar 1 2017, 4:23 PM

Handle Richard's comment

This revision was automatically updated to reflect the committed changes.