F# code generation: Declared type parameters do not appear in the type being abbreviated

[DejanMilicic]

After generating F# code for Red/Black tree from a file

https://github.com/FStarLang/FStar/blob/master/examples/data_structures/RBTree.fst

generated F# code contains the following declarations

type 'At not_c_inv =
unit

type 'At lr_c_inv =
unit

type ('Ac, 'Alt, 'Aky, 'Art) pre_balance =
unit

type ('Ac, 'Alt, 'Aky, 'Art, 'Ar) post_balance =
unit

type 'At balanced_rbtree' =
unit

which are producing following compilation error

Error	FS0035	This construct is deprecated: This type abbreviation has one or more declared type parameters that do not appear in the type being abbreviated. Type abbreviations must use all declared type parameters in the type being abbreviated. Consider removing one or more type parameters, or use a concrete type definition that wraps an underlying type, such as 'type C<'a> = C of ...'.

I am using VS2019 with FSharp.Core 4.7.0

[DejanMilicic]

I found out fsharp/fslang-suggestions#597

@A-Manning Any progress on this?

[A-Manning]

@DejanMilicic Fixing this is tricky since it requires patching the F# compiler to accept these type abbreviations. I've already proposed making the changes here fsharp/fslang-suggestions#597

It's difficult for me to develop the F# compiler on linux, since many of the test suites won't run, and so it's difficult to test changes. dotnet/fsharp#7075 (comment)

If the fsharpqa test suite is ported over, then it would be more practical for me to make the required changes and then we can wait to see if it gets accepted into the next version of F#.

Nothing is going to be happening on this front for at least a few months, so for now I'd recommend targeting a different language for code generation if that's possible.

[DejanMilicic]

@A-Manning Thanks, this is valuable information. This basically means I can put FStar on hold and observe status of fsharp/fslang-suggestions#597

[nikswamy]

FYI, we are working with @mateuszbujalski to fix this in the F* compiler by adding a pass to extraction to remove unused type variables in extracted type abbreviations. cf #1087

[DejanMilicic]

@nikswamy awesome news. I went over all issues related to F# code generation and it seems like this one is the last major problem?

[mateuszbujalski]

@DejanMilicic I would say there's one more that is related to F# implementation of "unsafe_coerce". You can take a look at #2067 (comment) for an example of issue it causes. But it also prevents other things that can't be expressed directly with F# type system.

E.g. code using some_type would fail at runtime currently.

let some_type (value : du_type) : Type0 =
    match value with
    | Case1 -> case1_type
    | Case2 -> case2_type

It looks like it's not that easy to implement equivalent of Obj.magic in .net and we're discussing with @nikswamy how to best deal with it.