Removing unused parameters when extracting (Invalid F# is generated by type definitions)

[A-Manning]

F# won't accept type abbreviations that don't use all of the declared type parameters in the type being abbreviated, whereas OCaml will.

For example, OCaml will accept type ('a, 'b) t = 'a, whereas F# will result in an FS0035 error.

These types come up frequently, since F* allows this style of type definition.

In FStar.Pervasives,

let st_pre_h  (heap:Type)          = heap -> GTot Type0
let st_post_h (heap:Type) (a:Type) = a -> heap -> GTot Type0
let st_wp_h   (heap:Type) (a:Type) = st_post_h heap a -> Tot (st_pre_h heap)

is extracted to

type 'Aheap st_pre_h =
'Aheap  ->  obj
type ('Aheap, 'Aa) st_post_h =
'Aa  ->  'Aheap  ->  obj
type ('Aheap, 'Aa) st_wp_h =
Prims.unit  ->  'Aheap st_pre_h

Since 'Aa appears as a parameter of st_wp_h but not in the type abbreviation that it is defined by, the F# compiler throws FS0035.

A workaround is to use single constructor DUs when defining types like this.

[nikswamy]

This seems quite hard to solve. After erasure, in particular, we will have many cases where there are unused type variables after extraction.

@A-Manning : I don't understand your DUs remark: can you say more, please?

[A-Manning]

@nikswamy

type ('a, 'b) t = 'a // Not ok
type ('a, 'b) t = | T of 'a // Ok

I have a custom version of F# compiler services that allows for type abbreviations of this form, I can share it if that would be helpful to others who want to extract F* to F#.

[nikswamy]

Ok, that's what I was guessing you meant.

I don't think adding these additional datatypes is going to fly. It'll require special treatment to project away the constructor elsewhere which is delicate and will also be inefficient.

Also, it's very cool that you have a custom patch to F# to support this kind of stuff. But, I don't think using a custom version is really going to fly long term.

In order to solve this properly it looks like we need to remove unused parameters when extracting. This would also be useful for the OCaml and KreMLin backends. But, it's non-trivial. Renaming the issue accordingly.

[A-Manning]

@nikswamy

I don't think using a custom version is really going to fly long term.

I agree, it's a bad idea to be relying on a custom version of F# for this. I have a suggestion on fslang-suggestions regarding allowing erased types in F#.

kurtschelfthout commented on Sep 3

What about we allow this provided the unused type parameters have an attribute Erased - inspired by Measure - at the type alias declaration and are always erased in compiled form? And we give specific warnings if any erased types are used in typeof or typedefof.

dsyme commented on Sep 4

Yes. We could probably infer that without even needing any attribute, though in general having a notion of Erased type parameters (and indeed a first-class notion of erased types - rather than just the ones you get from type providers) would be useful in general.

It seems that erased types could become part of F#, which would remove the need to maintain a custom F# compiler.