Stainless doesn't finish on polymorphic recursive data types

[pgimalac]

Hello, As discussed, on the following code using polymorphic recursive data type stainless never finishes (nor prints errors or anything).

https://github.com/jacobprudhomme/finger-tree/tree/stainless-bug

Thanks.

[mario-bucev]

Not very useful to know but seems to be related to isInductive and isWellformed definitions. Will look into it!

[vkuncak]

It is useful to know, @mario-bucev ; some things are more useful to users, some to developers. But those sets of people overlap. For now, we will need to check more carefully permitted inductive data types.

[vkuncak]

We should reject cleanly and upfront unsupported data types.

[vkuncak]

Here is a more precise link to where polymorphic recursion happens: https://github.com/jacobprudhomme/finger-tree/blob/stainless-bug/src/main/scala/fingertree/FingerTree.scala#L18