fix a potential unsoundness in Twin+Explicit

kudos to François for spotting the problem

src/transform/eliminate_algebraic.ml

@@ -52,6 +52,29 @@ let rec enum_ts kn sts ts =
 
 let enum_ts kn ts = try Some (enum_ts kn Sts.empty ts) with Exit -> None
 
+let is_finite_ty enum phlist =
+  let add_ph phmap = function
+    | [MAts ts; MAint i] ->
+        let phmap, pha = try phmap, Mts.find ts phmap with
+          | Not_found ->
+              let pha = Array.make (List.length ts.ts_args) false in
+              Mts.add ts pha phmap, pha
+        in
+        Array.set pha i true;
+        phmap
+    | _ -> assert false
+  in
+  let phmap = List.fold_left add_ph Mts.empty phlist in
+  let phmap = Mts.map Array.to_list phmap in
+  let rec finite_ty ty = match ty.ty_node with
+    | Tyapp (ts,tl) when Mts.mem ts enum ->
+        let phl = try Mts.find ts phmap with Not_found ->
+          List.map Util.ffalse ts.ts_args in
+        List.for_all2 (fun ph ty -> ph || finite_ty ty) phl tl
+    | _ -> false
+  in
+  finite_ty
+
 (** Compile match patterns *)
 
 let rec rewriteT kn t = match t.t_node with

src/transform/eliminate_algebraic.mli

@@ -24,3 +24,6 @@ val compile_match : Task.task Trans.trans
 
 val meta_enum : Theory.meta (* [MTtysymbol] *)
 val meta_phantom : Theory.meta (* [MTtysymbol; MTint] *)
+
+(* tests whether a type is finite given [meta_enum] and [meta_phantom] *)
+val is_finite_ty : Ty.Sts.t -> Theory.meta_arg list list -> (Ty.ty -> bool)

src/transform/encoding_twin.ml

@@ -124,5 +124,22 @@ let decl tenv d =
 let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
   Trans.decl (decl (Mty.mapi make_pont s)) None)
 
-let () = Hashtbl.replace Encoding.ft_enco_kept "twin" (const t)
+(* Every finite protected type has a finite twin type. But
+   as we do not introduce twin types explicitly, we declare
+   a dummy type constant finite. This is enough to trigger
+   the safety in Encoding_explicit. *)
 
+let ts_dummy = Ty.create_tysymbol (id_fresh "finite_twin_type") [] None
+
+let enum =
+  Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
+  Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
+  Trans.on_meta Eliminate_algebraic.meta_phantom (fun phlist ->
+    let finite_ty = Eliminate_algebraic.is_finite_ty enum phlist in
+    if not (Sty.exists finite_ty kept) then Trans.identity else
+      Trans.add_tdecls [create_meta Eliminate_algebraic.meta_enum
+        [MAts ts_dummy]])))
+
+let twin = const (Trans.compose t enum)
+
+let () = Hashtbl.replace Encoding.ft_enco_kept "twin" twin

src/transform/protect_enumeration.ml

@@ -66,26 +66,7 @@ let protect_enumeration =
   Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
   Trans.on_tagged_ts Eliminate_algebraic.meta_enum (fun enum ->
   Trans.on_meta Eliminate_algebraic.meta_phantom (fun phlist ->
-    let add_ph phmap = function
-      | [MAts ts; MAint i] ->
-          let phmap, pha = try phmap, Mts.find ts phmap with
-            | Not_found ->
-                let pha = Array.make (List.length ts.ts_args) false in
-                Mts.add ts pha phmap, pha
-          in
-          Array.set pha i true;
-          phmap
-      | _ -> assert false
-    in
-    let phmap = List.fold_left add_ph Mts.empty phlist in
-    let phmap = Mts.map Array.to_list phmap in
-    let rec finite_ty ty = match ty.ty_node with
-      | Tyapp (ts,tl) when Mts.mem ts enum ->
-          let phl = try Mts.find ts phmap with Not_found ->
-            List.map Util.ffalse ts.ts_args in
-          List.for_all2 (fun ph ty -> ph || finite_ty ty) phl tl
-      | _ -> false
-    in
+    let finite_ty = Eliminate_algebraic.is_finite_ty enum phlist in
     let add_protect ty tenv =
       if not (finite_ty ty) then tenv else
       let ts = match ty.ty_node with Tyapp (s,_) -> s | _ -> assert false in