Cyclic Type Dependency through Abstract Type

[gteege]

(Detailed Version of my proposal in the meeting today.) The code

type A a
type Rec = {x: U32, y:(A Rec)}
f: Rec -> Rec
f r = r

causes the error message

Parsing...
Resolving dependencies...
cyclic dependency
   - Rec ("CycTypeAbstract.cogent" (line 2, column 1))
Compilation failed!

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.