Unbound function symbol DeepModel8.deep_model

[adpaco-aws]

I updated locally creusot after #908 and used the DeepModel derive for a recursively-defined type Expr. But when I generate the mlcfg file and load it in Why3, I get this error:

Session initialized successfully
File "../interpreter-rlib.mlcfg", line 1077, characters 37-58: unbound function symbol 'DeepModel8.deep_model'

I've put the code in the creusot-issue-910 branch. To reproduce, simply run cargo creusot using the latest version and open with creusot/ide target/debug/interpreter-rlib.mlcfg. Please let me know if those steps don't show you the error.

[xldenis]

I've confirmed locally this issue is actually caused by a mutual recursion between the deep model instance of Box and Expr I don't see an easy solution, apart from properly supporting mutually recursive definitions.

However, we should improve the mutual recursion check to handle this kind of nested inductive based recursion.

As to working around the error, I think the best possible proposal right now is to manually provide instances. You could use cargo expand to recover the currently emitted code and edit it to avoid going through the box deep model instance.