Make user-specified type vars to be skolem

[Heimdell]

Make user-specified type vars to be skolem

TL;DR: code like

let cast : 'a -> 'b = fun x -> x

becomes an error, not a warning.

---

I propose we make universally quantified type variables to be rigid ones.

The existing way of approaching this problem in F# is better explained by compiling this, rather dumb and obvious, example:

// example.fs
module Example

let cast : 'a -> 'b = fun x -> x
let str : string = cast 1

The cast type means "for all types 'a and 'b, convert 'a to 'b".

dotnet fsi example.fs produces

/tmp/example.fs(4,23): warning FS0064: This construct causes code to be less generic than indicated by the type annotations. The type variable 'b has been constrained to be type ''a'.

/tmp/example.fs(6,25): error FS0001: This expression was expected to have type
    'string'    
but here has type
    'int'

If you comment out str definition, the dotnet fsi will tell you, that cast has type 'a -> 'a, which is not what user meant initially.

As you see, despite using different type variables, the compiler merges them into one. This happens because the variables are not skolem (or rigid) ones.

The negative consequence of current state of arts is that instead of getting an error right in cast, we get only warning. And if user calls cast somewhere, compiler will silently replace its type with narrower one, producing type errors - elsewhere. If there are no type annotations and the stars align, the type error might not even be where cast is used (in sufficiently polymorphic code), making path back to cast to be long.

When I have errors, I try to fix them first - and only then go to warnings. But this behavior leads to warning on the cause of the problem and type errors on the consequences, which is a priority inversion.

Pros and Cons

The advantages of making this adjustment to F# are

1. Functions like cast stop typechecking, and do not cause further confusion.

The disadvantages of making this adjustment to F# are

1. Code that compiles with warning FS0064 stops compiling.

Extra information

Estimated cost (XS, S, M, L, XL, XXL): S-M.

Related suggestions:

• Honor type annotations in let-declarations more. #839

Affidavit (please submit!)

Please tick this by placing a cross in the box:

• This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
• I have searched both open and closed suggestions on this site and believe this is not a duplicate
• This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

• This is not a breaking change to the F# language design
• I would be willing to help implement and/or test this

For Readers

If you would like to see this issue implemented, please click the 👍 emoji on this issue. These counts are used to generally order the suggestions by engagement.

[abelbraaksma]

It's a warning, because it is just as likely that the user meant to write let f: 'a -> 'a = fun x -> x, esp considering that there is no way that this can be two different types. So if the user got the implementation correct, the type system protects him and tells him "are you sure?". Hence the warning.

The easy way to do what you suggest is to just add FS0064 to the warnings-as-error flag, which you can set per project. That'll give precisely the behavior you want.

If we were to change this design it would be a breaking change, as existing, valid code where that warning is ignored will stop to compile.

An alternative suggestion would be to allow negative generic constraints, something like let f: a' -> 'b when 'a: not 'b = fun x -> x, which would lead to a checkable inconsistency, as 'a must not be 'b, but the type system might be able to check that this is never gonna happen and raise an error.

(edit: I see the other suggestion you made is basically the same thing, where I suggested the same thing, as you can already do what you want. Perhaps merge both issues into one, they seem the same)

[charlesroddie]

I think the current behaviour is right:

// You are telling the compiler that cast has the form 'a -> 'b,
// and it does, so this compiles:
let cast : 'a -> 'b = fun x -> x

// You are telling the compiler that for any 'a,'b, cast is defined as follows,
// which is incorrect, so this gives an error:
let cast<'a,'b> : 'a -> 'b = fun x -> x

[dsyme]

Thank you for the suggestion but I don't think this is something we'll pursue, per replies above