This is correct, but I propose this type check to be relaxed. The type checker has no information about the parametric abstract type A, so it should not refuse the type Rec. Typically, A would be a variant type whith a variant not including a vale of type Rec, so that the recursion may terminate. So it should be up to the implementor of the abstract type A to prove finiteness here. I assume that Cogent and the generated proofs would not be affected by such a relaxing. If I am wrong, please explain how it is affected, then I have a misconception about Cogent here.
BTW this is a similar argument as in my comment for issue #306 whether to allow unboxed type variables.
(Detailed Version of my proposal in the meeting today.) The code
causes the error message
This is correct, but I propose this type check to be relaxed. The type checker has no information about the parametric abstract type A, so it should not refuse the type Rec. Typically, A would be a variant type whith a variant not including a vale of type Rec, so that the recursion may terminate. So it should be up to the implementor of the abstract type A to prove finiteness here. I assume that Cogent and the generated proofs would not be affected by such a relaxing. If I am wrong, please explain how it is affected, then I have a misconception about Cogent here.
BTW this is a similar argument as in my comment for issue #306 whether to allow unboxed type variables.