Add injectivity annotations (#9500)

Changes

@@ -3,6 +3,16 @@ Working version
 
 ### Language features:
 
+* #9500: Injectivity annotations
+  One can now mark type parameters as injective, which is useful for
+  abstract types:
+    module Vec : sig type !'a t end = struct type 'a t = 'a array end
+  On non-abstract types, this can be used to check the injectivity of
+  parameters. Since all parameters of record and sum types are by definition
+  injective, this only makes sense for type abbreviations:
+    type !'a t = 'a list
+  (Jacques Garrigue, review by Jeremy Yallop and Leo White)
+
 ### Runtime system:
 
 - #1795, #9543: modernize signal handling on Linux i386, PowerPC, and s390x,

manual/manual/refman/typedecl.etex

@@ -36,12 +36,18 @@ type-params:
         | '(' type-param { "," type-param } ')'
 ;
 type-param:
-          [variance] "'" ident
+          [ext-variance] "'" ident
+;
+ext-variance:
+          variance [injectivity]
+        | injectivity [variance]
 ;
 variance:
           '+'
         | '-'
 ;
+injectivity: '!'
+;
 record-decl:
          '{' field-decl { ';' field-decl } [';'] '}'
 ;
@@ -88,7 +94,9 @@ for type constructors with one parameter, or a list of type variables
 @"('"ident_1,\ldots,"'"ident_n")"@, for type constructors with several
 parameters. Each type parameter may be prefixed by a variance
 constraint @"+"@ (resp. @"-"@) indicating that the parameter is
-covariant (resp. contravariant).  These type parameters can appear in
+covariant (resp. contravariant), and an injectivity annotation @"!"@
+indicating that the parameter can be deduced from the whole type.
+These type parameters can appear in
 the type expressions of the right-hand side of the definition,
 optionally restricted by a variance constraint ; {\em i.e.\/} a
 covariant parameter may only appear on the right side of a functional
@@ -200,6 +208,18 @@ constraints, the variance properties of the type constructor
 are inferred from its definition, and the variance annotations are
 only checked for conformance with the definition.
 
+Injectivity annotations are only necessary for abstract types and
+private row types, since they can otherwise be deduced from the type
+declaration: all parameters are injective for record and variant type
+declarations (including extensible types); for type abbreviations a
+parameter is injective if it has an injective occurrence in its
+defining equation (be it private or not). For constrained type
+parameters in type abbreviations, they are injective if either they
+appear at an injective position in the body, or if all their type
+variables are injective; in particular, if a constrained type
+parameter contains a variable that doesn't appear in the body, it
+cannot be injective.
+
 \ikwd{constraint\@\texttt{constraint}}
 The construct @ 'constraint' "'" ident '=' typexpr @ allows the
 specification of

parsing/ast_helper.mli

@@ -204,7 +204,7 @@ module Val:
 module Type:
   sig
     val mk: ?loc:loc -> ?attrs:attrs -> ?docs:docs -> ?text:text ->
-      ?params:(core_type * variance) list ->
+      ?params:(core_type * (variance * injectivity)) list ->
       ?cstrs:(core_type * core_type * loc) list ->
       ?kind:type_kind -> ?priv:private_flag -> ?manifest:core_type -> str ->
       type_declaration
@@ -220,8 +220,8 @@ module Type:
 module Te:
   sig
     val mk: ?loc:loc -> ?attrs:attrs -> ?docs:docs ->
-      ?params:(core_type * variance) list -> ?priv:private_flag ->
-      lid -> extension_constructor list -> type_extension
+      ?params:(core_type * (variance * injectivity)) list ->
+      ?priv:private_flag -> lid -> extension_constructor list -> type_extension
 
     val mk_exception: ?loc:loc -> ?attrs:attrs -> ?docs:docs ->
       extension_constructor -> type_exception
@@ -454,7 +454,8 @@ module Cf:
 module Ci:
   sig
     val mk: ?loc:loc -> ?attrs:attrs -> ?docs:docs -> ?text:text ->
-      ?virt:virtual_flag -> ?params:(core_type * variance) list ->
+      ?virt:virtual_flag ->
+      ?params:(core_type * (variance * injectivity)) list ->
       str -> 'a -> 'a class_infos
   end
 

parsing/asttypes.mli

@@ -60,4 +60,8 @@ type 'a loc = 'a Location.loc = {
 type variance =
   | Covariant
   | Contravariant
-  | Invariant
+  | NoVariance
+
+type injectivity =
+  | Injective
+  | NoInjectivity

parsing/parser.mly

@@ -2942,9 +2942,20 @@ type_variable:
 ;
 
 type_variance:
-    /* empty */                                 { Invariant }
-  | PLUS                                        { Covariant }
-  | MINUS                                       { Contravariant }
+    /* empty */                             { NoVariance, NoInjectivity }
+  | PLUS                                    { Covariant, NoInjectivity }
+  | MINUS                                   { Contravariant, NoInjectivity }
+  | BANG                                    { NoVariance, Injective }
+  | PLUS BANG | BANG PLUS                   { Covariant, Injective }
+  | MINUS BANG | BANG MINUS                 { Contravariant, Injective }
+  | INFIXOP2
+      { if $1 = "+!" then Covariant, Injective else
+        if $1 = "-!" then Contravariant, Injective else
+        expecting $loc($1) "type_variance" }
+  | PREFIXOP
+      { if $1 = "!+" then Covariant, Injective else
+        if $1 = "!-" then Contravariant, Injective else
+        expecting $loc($1) "type_variance" }
 ;
 
 (* A sequence of constructor declarations is either a single BAR, which

parsing/parsetree.mli

@@ -429,7 +429,7 @@ and value_description =
 and type_declaration =
     {
      ptype_name: string loc;
-     ptype_params: (core_type * variance) list;
+     ptype_params: (core_type * (variance * injectivity)) list;
            (* ('a1,...'an) t; None represents  _*)
      ptype_cstrs: (core_type * core_type * Location.t) list;
            (* ... constraint T1=T1'  ... constraint Tn=Tn' *)
@@ -497,7 +497,7 @@ and constructor_arguments =
 and type_extension =
     {
      ptyext_path: Longident.t loc;
-     ptyext_params: (core_type * variance) list;
+     ptyext_params: (core_type * (variance * injectivity)) list;
      ptyext_constructors: extension_constructor list;
      ptyext_private: private_flag;
      ptyext_loc: Location.t;
@@ -598,7 +598,7 @@ and class_type_field_desc =
 and 'a class_infos =
     {
      pci_virt: virtual_flag;
-     pci_params: (core_type * variance) list;
+     pci_params: (core_type * (variance * injectivity)) list;
      pci_name: string loc;
      pci_expr: 'a;
      pci_loc: Location.t;

parsing/pprintast.ml

@@ -118,10 +118,14 @@ let override = function
 
 (* variance encoding: need to sync up with the [parser.mly] *)
 let type_variance = function
-  | Invariant -> ""
+  | NoVariance -> ""
   | Covariant -> "+"
   | Contravariant -> "-"
 
+let type_injectivity = function
+  | NoInjectivity -> ""
+  | Injective -> "!"
+
 type construct =
   [ `cons of expression list
   | `list of expression list
@@ -1434,8 +1438,8 @@ and structure_item ctxt f x =
       item_extension ctxt f e;
       item_attributes ctxt f a
 
-and type_param ctxt f (ct, a) =
-  pp f "%s%a" (type_variance a) (core_type ctxt) ct
+and type_param ctxt f (ct, (a,b)) =
+  pp f "%s%s%a" (type_variance a) (type_injectivity b) (core_type ctxt) ct
 
 and type_params ctxt f = function
   | [] -> ()

testsuite/tests/printing-types/disambiguation.ml

@@ -6,14 +6,14 @@ type 'a x = private [> `x] as 'a;;
 [%%expect {|
 Line 1:
 Error: Type declarations do not match:
-         type 'a x = private [> `x ] constraint 'a = 'a x
+         type !'a x = private [> `x ] constraint 'a = 'a x
        is not included in
          type 'a x
        Their constraints differ.
 |}, Principal{|
 Line 1:
 Error: Type declarations do not match:
-         type 'a x = private 'a constraint 'a = [> `x ]
+         type !'a x = private 'a constraint 'a = [> `x ]
        is not included in
          type 'a x
        Their constraints differ.