Well-foundedness of datatypes

[Gbury]

TL;DR

The wording of the criterion for whether a datatype is well-founded is a bit unclear on certain points, and additionally that criterion may be too restrictive, particularly in situations where polymorphism is used.

The criterion

As far as I can tell, this is the criterion for well-founded datatypes from the specification:

The datatype δ must be well founded in the following inductive sense: it must have a constructor of rank τ1 · · · τmδ such that τ1 · · · τm does not contain any of the datatypes from {δ1, . . . , δn} or, if it does contain some, they are well founded

The part that I find unclear is what exactly is meant by the word "contain" in that sentence. Currently, I (and most importantly its implementation in dolmen) have interpreted it as follows: a sort/type t contain a datatype d iff d has an occurrence in t (even under any other type constructor). If that is the correct interpretation, it would be nice to clarify the wording a bit (or add a footnote).

That being said, once you have polymoprhic types, that criterion does not allow some examples that can happen easily and that most people used to deal with polymorphic types would expect to work, as shown below.

Problematic example

Consider the following example in a ML/why3-like syntax, that defines a type of rose trees (note: this example is taken from a real life problem that occurred while using why3, see Gbury/dolmen#222 for more information).

(* polymorphic lists *)
type 'a list =
  | Nil
  | Cons of 'a * 'a list

(* A type of rose tree on integers *)
type tree = {
  elem: int;
  children: list tree;
  rank: int;
  }

These type definitions have a relatively straight-forward mapping to the following SMT-LIB2 declarations:

(declare-datatypes ((list 1)) ((par (alpha) (
  (nil)
  (cons (head alpha) (tail (list alpha)))
))))

(declare-datatypes ((tree 0)) ((
  (treeqtmk (elem Int) (children (list tree)) (rank Int) )
)))

Unfortunately, the definition of tree above does not pass the well-founded criterion shown above, since the datatype itself has an occurrence in the rank/type of its only constructor, and dolmen emits an error when trying to typecheck the above declarations. That being said, in practice the type tree is indeed inhabited, and is well-founded according to at least some other criterions (e.g. the criterion used by why3 and ocaml for instance).

Conclusion

Type declarations such as the above one are quite common in polymorphic languages, so I'd expect that with polymorphism becoming fully supported in SMT-LIB3 (and SMT-LIB2.7 !), it might become more common for problems such as the above one to be generated in the context of program verification (e.g. using why3), and it'd be unfortunate if such problems could not be expressed in SMT-LIB (without modifying/encoding the original problem).

Therefore, I think it would be good to clarify the current criterion, and to investigate whether the criterion could be improved/changed to allow for the example I showed above. Unfortunately I don't have such a criterion to propose right now, but I'll try and look for one, if the maintainers agree that it's a wanted change.