Subtyping for roles in signatures.
authorEdward Z. Yang <ezyang@cs.stanford.edu>
Fri, 10 Feb 2017 08:38:34 +0000 (00:38 -0800)
committerEdward Z. Yang <ezyang@cs.stanford.edu>
Mon, 27 Feb 2017 00:03:13 +0000 (16:03 -0800)
commit923d7ca2d90c1cb9816d14768abdd2e46adcd5dd
tree943e3c0dfff8e9674bbd6252b98101e713d47e3e
parent9603de6ac7a75ea7c620ce05e3c5f500bcaf5dd6
Subtyping for roles in signatures.

Summary:
This commit implements the plan in #13140:

* Today, roles in signature files default to representational. Let's change the
  default to nominal, as this is the most flexible implementation side. If a
  client of the signature needs to coerce with a type, the signature can be
  adjusted to have more stringent requirements.

* If a parameter is declared as nominal in a signature, it can be implemented
  by a data type which is actually representational.

* When merging abstract data declarations, we take the smallest role for every
  parameter. The roles are considered fix once we specify the structure of an
  ADT.

* Critically, abstract types are NOT injective, so we aren't allowed to
  make inferences like "if T a ~R T b, then a ~N b" based on the nominal
  role of a parameter in an abstract type (this would be unsound if the
  parameter ended up being phantom.)  This restriction is similar to the
  restriction we have on newtypes.

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

Reviewers: simonpj, bgamari, austin, goldfire

Subscribers: goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D3123
compiler/iface/TcIface.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcTyDecls.hs
compiler/types/CoAxiom.hs
docs/users_guide/separate_compilation.rst
testsuite/tests/backpack/should_compile/T13140.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_compile/T13140.stderr [new file with mode: 0644]
testsuite/tests/backpack/should_compile/all.T
testsuite/tests/backpack/should_fail/bkpfail25.stderr
testsuite/tests/backpack/should_fail/bkpfail26.stderr