feat: positivity check in type constructors with stack-based error reports

fix: perform positivity check in type arguments of type constructors
test: add a simple test file for positivity checking.

Author: loutr

src/ecHiInductive.ml

@@ -23,7 +23,7 @@ type dterror =
 | DTE_TypeError       of TT.tyerror
 | DTE_DuplicatedCtor  of symbol
 | DTE_InvalidCTorType of symbol * TT.tyerror
-| DTE_NonPositive
+| DTE_NonPositive     of symbol * EI.non_positive_context
 | DTE_Empty
 
 type fxerror =
@@ -52,7 +52,7 @@ let trans_record (env : EcEnv.env) (name : ptydname) (rc : precord) =
   Msym.odup unloc (List.map fst rc) |> oiter (fun (x, y) ->
     rcerror y.pl_loc env (RCE_DuplicatedField x.pl_desc));
 
-  (* Check for emptyness *)
+  (* Check for emptiness *)
   if List.is_empty rc then
     rcerror loc env RCE_Empty;
 
@@ -106,7 +106,7 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
       dt |> List.map for1
   in
 
-  (* Check for emptyness *)
+  (* Check for emptiness *)
   begin
     let rec isempty_n (ctors : (ty list) list) =
       List.for_all isempty_1 ctors
@@ -131,21 +131,24 @@ let trans_datatype (env : EcEnv.env) (name : ptydname) (dt : pdatatype) =
 
       let tdecl = EcEnv.Ty.by_path_opt tname env0
         |> odfl (EcDecl.abs_tydecl ~params:(`Named tparams) lc) in
-      let tyinst () =
-        fun ty -> ty_instantiate tdecl.tyd_params targs ty in
+      let tyinst = ty_instantiate tdecl.tyd_params targs in
 
       match tdecl.tyd_type with
       | Abstract _ ->
-          List.exists isempty (targs)
+          List.exists isempty targs
 
       | Concrete ty ->
-          isempty_1 [tyinst () ty]
+          isempty_1 [ tyinst ty ]
 
       | Record (_, fields) ->
-          isempty_1 (List.map (tyinst () |- snd) fields)
+          isempty_1 (List.map (tyinst |- snd) fields)
 
       | Datatype dt ->
-          isempty_n (List.map (List.map (tyinst ()) |- snd) dt.tydt_ctors)
+          (* FIXME: Inspecting all constructors recursively causes
+             non-termination in some cases. One can have the same
+             limitation as is done for positivity in order to limit this
+             unfolding to well-behaved cases. *)
+          isempty_n (List.map (List.map tyinst |- snd) dt.tydt_ctors)
 
     in
 

src/ecHiInductive.mli

@@ -16,7 +16,7 @@ type dterror =
 | DTE_TypeError       of EcTyping.tyerror
 | DTE_DuplicatedCtor  of symbol
 | DTE_InvalidCTorType of symbol * EcTyping.tyerror
-| DTE_NonPositive
+| DTE_NonPositive     of symbol * non_positive_context
 | DTE_Empty
 
 type fxerror =

src/ecInductive.ml

@@ -83,10 +83,120 @@ let datatype_ind_path (mode : indmode) (p : EcPath.path) =
   EcPath.pqoname (EcPath.prefix p) name
 
 (* -------------------------------------------------------------------- *)
-exception NonPositive
-
-let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
-  let normty = odfl (identity : ty -> ty) normty in
+type non_positive_intype = Concrete | Record of symbol | Variant of symbol
+
+type non_positive_description =
+  | InType of EcIdent.ident option * non_positive_intype
+  | NonPositiveOcc of ty
+  | AbstractTypeRestriction
+  | TypePositionRestriction of ty
+
+type non_positive_context = (symbol * non_positive_description) list
+
+exception NonPositive of non_positive_context
+
+let with_context ?ident p ctx f =
+  try f () with NonPositive l -> raise (NonPositive ((EP.basename p, InType (ident, ctx)) :: l))
+
+let non_positive (p : EP.path) ctx = raise (NonPositive [(EP.basename p, ctx)])
+let non_positive' (s : EcIdent.ident) ctx = raise (NonPositive [(s.id_symb, ctx)])
+
+(** below, [fct] designates the function that takes a path to a type constructor
+    and returns the corresponding type declaration *)
+
+(** Strict positivity enforces the following, for every variant of the datatype p:
+    - for each subterm (a → b), p ∉ fv(a);
+    - inductive occurences a₁ a₂ .. aₙ p are such that ∀i. p ∉ fv(aᵢ)
+
+    Crucially, this has to be checked whenever p occurs in an instance of
+    another type constructor.
+
+    FIXME: The current implementation prohibits the use of a type which changes
+    its type arguments like e.g.
+    {v
+      type ('a, 'b) t = [
+        | Elt of 'a
+        | Swap of ('b, 'a) t
+      ].
+    v}
+    to be used in some places while defining another inductive type. *)
+
+let rec occurs ?(normty = identity) p t =
+  match (normty t).ty_node with
+  | Tconstr (p', _) when EcPath.p_equal p p' -> true
+  | _ -> EcTypes.ty_sub_exists (occurs p) t
+
+(** Tests whether the first list is a list of type variables, matching the
+    identifiers of the second list. *)
+let ty_params_compat =
+  List.for_all2 (fun ty (param_id, _) ->
+      match ty.ty_node with
+      | Tvar id -> EcIdent.id_equal id param_id
+      | _ -> false)
+
+(** Ensures all occurrences of type variable [ident] are positive in type
+    declaration [decl] (with name [p]).
+    This function provide error context in case the check fails. *)
+let rec check_positivity_in_decl fct p decl ident =
+  let check x () = check_positivity_ident fct p decl.tyd_params ident x
+  and iter l f = List.iter f l in
+
+  match decl.tyd_type with
+  | Concrete ty -> with_context ~ident p Concrete (check ty)
+  | Abstract _ -> non_positive p AbstractTypeRestriction
+  | Datatype { tydt_ctors } ->
+      iter tydt_ctors @@ fun (name, argty) ->
+      iter argty @@ fun ty ->
+      with_context ~ident p (Variant name) (check ty)
+  | Record (_, tys) ->
+      iter tys @@ fun (name, ty) ->
+      with_context ~ident p (Record name) (check ty)
+
+(** Ensures all occurrences of type variable [ident] are positive in type [ty] *)
+and check_positivity_ident fct p params ident ty =
+  match ty.ty_node with
+  | Tglob _ | Tunivar _ | Tvar _ -> ()
+  | Ttuple tys -> List.iter (check_positivity_ident fct p params ident) tys
+  | Tconstr (q, args) when EcPath.p_equal q p ->
+      if not (ty_params_compat args params) then
+        non_positive p (TypePositionRestriction ty)
+  | Tconstr (q, args) ->
+      let decl = fct q in
+      List.iter (check_positivity_ident fct p params ident) args;
+      List.combine args decl.tyd_params
+      |> List.filter_map (fun (arg, (ident', _)) ->
+             if EcTypes.var_mem ident arg then Some ident' else None)
+      |> List.iter (check_positivity_in_decl fct q decl)
+  | Tfun (from, to_) ->
+      if EcTypes.var_mem ident from then non_positive' ident (NonPositiveOcc ty);
+      check_positivity_ident fct p params ident to_
+
+(** Ensures all occurrences of path [p] are positive in type [ty] *)
+let rec check_positivity_path fct p ty =
+  match ty.ty_node with
+  | Tglob _ | Tunivar _ | Tvar _ -> ()
+  | Ttuple tys -> List.iter (check_positivity_path fct p) tys
+  | Tconstr (q, args) when EcPath.p_equal q p ->
+      if List.exists (occurs p) args then non_positive p (NonPositiveOcc ty)
+  | Tconstr (q, args) ->
+      let decl = fct q in
+      List.iter (check_positivity_path fct p) args;
+      List.combine args decl.tyd_params
+      |> List.filter_map (fun (arg, (ident, _)) ->
+             if occurs p arg then Some ident else None)
+      |> List.iter (check_positivity_in_decl fct q decl)
+  | Tfun (from, to_) ->
+      if occurs p from then non_positive p (NonPositiveOcc ty);
+      check_positivity_path fct p to_
+
+let check_positivity fct dt =
+  let check ty () = check_positivity_path fct dt.dt_path ty
+  and iter l f = List.iter f l in
+  iter dt.dt_ctors @@ fun (name, argty) ->
+  iter argty @@ fun ty ->
+  with_context dt.dt_path (Variant name) (check ty)
+
+let indsc_of_datatype ?(normty = identity) (mode : indmode) (dt : datatype) =
   let tpath  = dt.dt_path in
 
   let rec scheme1 p (pred, fac) ty =
@@ -103,13 +213,11 @@ let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
           | scs -> Some (FL.f_let (LTuple xs) fac (FL.f_ands scs))
     end
 
-    | Tconstr (p', ts)  ->
-        if List.exists (occurs p) ts then raise NonPositive;
+    | Tconstr (p', _)  ->
         if not (EcPath.p_equal p p') then None else
           Some (FL.f_app pred [fac] tbool)
 
     | Tfun (ty1, ty2) ->
-        if occurs p ty1 then raise NonPositive;
         let x = fresh_id_of_ty ty1 in
           scheme1 p (pred, FL.f_app fac [FL.f_local x ty1] ty2) ty2
             |> omap (FL.f_forall [x, GTty ty1])
@@ -152,11 +260,6 @@ let indsc_of_datatype ?normty (mode : indmode) (dt : datatype) =
     let form   = FL.f_forall [predx, GTty predty] form in
       form
 
-  and occurs p t =
-    match (normty t).ty_node with
-    | Tconstr (p', _) when EcPath.p_equal p p' -> true
-    | _ -> EcTypes.ty_sub_exists (occurs p) t
-
   in scheme mode (List.map fst dt.dt_tparams, tpath) dt.dt_ctors
 
 (* -------------------------------------------------------------------- *)

src/ecInductive.mli

@@ -43,7 +43,25 @@ val datatype_proj_name : symbol -> symbol
 val datatype_proj_path : path -> symbol -> path
 
 (* -------------------------------------------------------------------- *)
-exception NonPositive
+type non_positive_intype = Concrete | Record of symbol | Variant of symbol
+
+type non_positive_description =
+  | InType of EcIdent.ident option * non_positive_intype
+  | NonPositiveOcc of ty
+  | AbstractTypeRestriction
+  | TypePositionRestriction of ty
+
+type non_positive_context = (symbol * non_positive_description) list
+
+exception NonPositive of non_positive_context
+
+val check_positivity : (path -> tydecl) -> datatype -> unit
+(** Evaluates whether a given datatype protype satisfies the strict
+    positivity check. The first argument defines how to retrieve the
+    effective definition of a type constructor from its path.
+
+    raises the exception [NonPositive] if the check fails, otherwise
+    the function returns a unit value. *)
 
 val indsc_of_datatype : ?normty:(ty -> ty) -> [`Elim|`Case] -> datatype -> form
 

src/ecScope.ml

@@ -2246,13 +2246,16 @@ module Ty = struct
         let body   = transty tp_tydecl env ue bd in
         EcUnify.UniEnv.tparams ue, Concrete body
 
-      | PTYD_Datatype dt ->
-        let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
-        let tparams, tydt =
-          try ELI.datatype_as_ty_dtype datatype
-          with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
-        in
-        tparams, Datatype tydt
+      | PTYD_Datatype dt -> (
+          let datatype = EHI.trans_datatype env (mk_loc loc (args, name)) dt in
+          let ty_from_ctor ctor = EcEnv.Ty.by_path ctor env in
+          try
+            ELI.check_positivity ty_from_ctor datatype;
+            let tparams, tydt = ELI.datatype_as_ty_dtype datatype in
+            (tparams, Datatype tydt)
+          with ELI.NonPositive ctx ->
+            let symbol = basename datatype.dt_path in
+            EHI.dterror loc env (EHI.DTE_NonPositive (symbol, ctx)))
 
       | PTYD_Record rt ->
         let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in

src/ecTypes.ml

@@ -154,6 +154,12 @@ let rec ty_check_uni t =
   | Tunivar _ -> raise FoundUnivar
   | _ -> ty_iter ty_check_uni t
 
+let rec var_mem ?(check_glob = false) id t =
+  match t.ty_node with
+  | Tvar id' -> EcIdent.id_equal id id'
+  | Tglob id' when check_glob -> EcIdent.id_equal id id'
+  | _ -> ty_sub_exists (var_mem ~check_glob id) t
+
 (* -------------------------------------------------------------------- *)
 let symbol_of_ty (ty : ty) =
   match ty.ty_node with

src/ecTypes.mli

@@ -79,6 +79,8 @@ val ty_sub_exists : (ty -> bool) -> ty -> bool
 val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
 val ty_iter : (ty -> unit) -> ty -> unit
 
+val var_mem : ?check_glob:bool -> EcIdent.t -> ty -> bool
+
 (* -------------------------------------------------------------------- *)
 val symbol_of_ty   : ty -> string
 val fresh_id_of_ty : ty -> EcIdent.t

src/ecUserMessages.ml

@@ -573,6 +573,7 @@ module InductiveError : sig
   val pp_fxerror : env -> Format.formatter -> fxerror -> unit
 end = struct
   open EcHiInductive
+  open EcInductive
   open TypingError
 
   let pp_rcerror env fmt error =
@@ -591,8 +592,38 @@ end = struct
     | RCE_Empty ->
         msg "this record type is empty"
 
+  let format_intype fmt p (tyvar, ctx) =
+    (match ctx with
+    | Concrete -> Format.fprintf fmt "... in type %s" p
+    | Record s -> Format.fprintf fmt "... in record field %s of type %s" s p
+    | Variant s -> Format.fprintf fmt "... in variant %s of type %s" s p);
+    let subty tyvar =
+      Format.fprintf fmt " (in an instance of type variable %a)"
+        EcIdent.pp_ident tyvar
+    in
+    Option.iter subty tyvar
+
+let format_context pp fmt (p, ctx) = match ctx with
+  | InType (tyvar, ctx) -> format_intype fmt p (tyvar, ctx)
+  | NonPositiveOcc ty ->
+      Format.fprintf fmt "non-positive occurrence of %s in type %a"
+        p (EcPrinting.pp_type pp) ty
+  | AbstractTypeRestriction ->
+      Format.fprintf fmt "unauthorised abstract type constructor %s" p
+  | TypePositionRestriction ty ->
+      Format.fprintf fmt
+        "recursive occurrence %a in the definition of %s has different \
+         arguments, which is not allowed."
+        (EcPrinting.pp_type pp) ty p
+
+let format_context_list p l pp fmt =
+  Format.fprintf fmt "Could not verify strict positivity of type %s:@.@;<0 2>@[<v>" p;
+  Format.pp_print_list (format_context pp) fmt l;
+  Format.fprintf fmt "@;@]"
+
   let pp_dterror env fmt error =
     let msg x = Format.fprintf fmt x in
+    let env1  = EcPrinting.PPEnv.ofenv env in
 
     match error with
     | DTE_TypeError ee ->
@@ -605,12 +636,11 @@ end = struct
         msg "invalid constructor type: `%s`: %a'"
           name (pp_tyerror env) ee
 
-    | DTE_NonPositive ->
-        msg "the datatype does not respect the positivity condition"
-
     | DTE_Empty ->
         msg "the datatype may be empty"
 
+    | DTE_NonPositive (s, ctx) -> format_context_list s ctx env1 fmt
+
   let pp_fxerror env fmt error =
     match error with
     | FXLowError ee ->

tests/positivity_checking.ec

@@ -0,0 +1,40 @@
+(* Simple type *)
+type 'a list = [ Nil | Cons of 'a & 'a list ].
+
+type 'a tree = [
+  | Leaf
+    (* Recursive occurrence within a pre-existing type constructor *)
+  | Node of 'a tree list
+    (* Positive occurrence in a function *)
+  | Fun of (bool -> 'a tree)
+].
+
+theory Bad.
+type ('a, 'b) permlist = [
+ | N of ('a -> 'b) (* Aaaaah *)
+ | C of 'a & ('a, 'b) permlist
+ | P of ('b, 'a) permlist
+].
+
+fail type posrej = [ A | B of (bool, posrej) permlist ].
+end Bad.
+
+theory Good.
+type ('a, 'b) permlist = [
+ | N (* No problem *)
+ | C of 'a & ('a, 'b) permlist
+ | P of ('b, 'a) permlist list (* For the sake of nesting in a list *)
+].
+
+(* this type fails because of the same limitation,
+   even though it is in fact strictly positive. *)
+fail type posrej = [ A | B of (bool, posrej) permlist ].
+end Good.
+
+type ('a, 'b) arr = 'a -> 'b.
+type ('a, 'b) orr = ('a, 'b) arr.
+fail type 'a u = [ S | U of ('a u, bool) orr ].
+
+type 'a t.
+fail type tt = [ N | T of tt t ].
+fail type 'a tt = [ N | T of 'a tt tt].