forbid non-well-founded algebraic types

examples/wf_types.why

+theory Test
+    type t 'a
+
+    type test 'a = Test (t (test 'a))
+end
+
+theory Main
+    type id 'a = 'a
+    type shell 'a = Shell 'a
+    type option 'a = Some 'a | None
+
+    clone Test as T1 with type t = id
+    clone Test as T2 with type t = shell
+    clone Test as T3 with type t = option
+end

src/core/decl.ml

@@ -648,8 +648,36 @@ and check_matchF kn () f = match f.f_node with
 
 let check_match kn d = decl_fold (check_matchT kn) (check_matchF kn) () d
 
+exception NonFoundedTypeDecl of tysymbol
+
+let rec check_foundness kn d =
+  let rec check_constr s ty ls =
+    let vty = of_option ls.ls_value in
+    let m = ty_match Mtv.empty vty ty in
+    let check ty = check_type s (ty_inst m ty) in
+    List.for_all check ls.ls_args
+  and check_type s ty = match ty.ty_node with
+    | Tyvar _ -> true
+    | Tyapp (ts,_) ->
+        if Sts.mem ts s then false else
+        let cl = find_constructors kn ts in
+        if cl == [] then true else
+        let s = Sts.add ts s in
+        List.exists (check_constr s ty) cl
+  in
+  match d.d_node with
+  | Dtype tdl ->
+      let check () (ts,_) =
+        let tl = List.map ty_var ts.ts_args in
+        if check_type Sts.empty (ty_app ts tl)
+        then () else raise (NonFoundedTypeDecl ts)
+      in
+      List.fold_left check () tdl
+  | _ -> ()
+
 let known_add_decl kn d =
   let kn = known_add_decl kn d in
-  ignore (check_match kn d);
+  check_foundness kn d;
+  check_match kn d;
   kn
 

src/core/decl.mli

@@ -153,6 +153,7 @@ exception KnownIdent of ident
 exception UnknownIdent of ident
 exception RedeclaredIdent of ident
 exception NonExhaustiveExpr of (pattern list * expr)
+exception NonFoundedTypeDecl of tysymbol
 
 val find_constructors : known_map -> tysymbol -> lsymbol list
 val find_inductive_cases : known_map -> lsymbol -> (prsymbol * fmla) list

src/core/pretty.ml

@@ -512,19 +512,21 @@ let () = Exn_printer.register
       fprintf fmt
         "Type symbol %a is a type alias and cannot be declared as algebraic"
         print_ts ts
+  | Decl.NonFoundedTypeDecl ts ->
+      fprintf fmt "Cannot construct a value of type %a" print_ts ts
   | Decl.NonPositiveTypeDecl (_ts, ls, ts1) ->
       fprintf fmt "Constructor %a \
           contains a non strictly positive occurrence of type symbol %a"
         print_ls ls print_ts ts1
   | Decl.InvalidIndDecl (_ls, pr) ->
-      fprintf fmt "Ill-formed clause %a in inductive predicate declaration"
+      fprintf fmt "Ill-formed inductive clause %a"
         print_pr pr
   | Decl.TooSpecificIndDecl (_ls, pr, t) ->
-      fprintf fmt "Clause %a in inductive predicate declaration \
-          has too type-specific conclusion %a"
+      fprintf fmt "Inductive clause %a has too type-specific conclusion %a"
         print_pr pr print_term t
   | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
-      fprintf fmt "Clause %a contains a negative occurrence of symbol %a"
+      fprintf fmt "Inductive clause %a contains \
+          a negative occurrence of symbol %a"
         print_pr pr print_ls ls1
   | Decl.BadLogicDecl (ls1,ls2) ->
       fprintf fmt "Ill-formed definition: symbols %a and %a are different"