Skip to content
  • Edward Z. Yang's avatar
    Subtyping for roles in signatures. · 923d7ca2
    Edward Z. Yang authored
    
    
    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: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
    
    Test Plan: validate
    
    Reviewers: simonpj, bgamari, austin, goldfire
    
    Subscribers: goldfire, thomie
    
    Differential Revision: https://phabricator.haskell.org/D3123
    923d7ca2