Support explicit generalisation of assigned values with annotations
#2,143 opened on May 5, 2023
Description
When writing a local type signature, I would expect type variables mentioned in that signature to be quantified by that local type. For example, I would expect the following
let f : fn(a) -> a = fn(x) { x }
to be treated like (pretending gleam had explicit quantifiers for a second)
let f : forall a. fn(a) -> a = fn(x) { x }
But what actually happens is that gleam seems to treat type variables like skolems (unconstructable, unbindable type constants that only unify with themselves).
let f : fn(a) -> a = fn(x) { x }
let _ = f(5)
error: Type mismatch
┌─ ./src/main.gleam:5:13
│
5 │ let _ = f(5)
│ ^
Expected type:
a
Found type:
Int
Not having any way of writing polymorphic local functions seems like a pretty massive and unnecessary limitation, but even if this is the intended behavior, I cannot think of a single use case where these kinds of constants would be useful.
IMO, unbound type variables in local definitions should either be implicitly quantified or throw a type error. This would also make the error message much clearer.