Scope the type variables

[thufschmitt]

Is your feature request related to a problem? Please describe.

Inside a (typed) polymorphic expression, it isn’t possible to annotate the type of an intermediary expression with the type variable.

For example (because the above is very weirdly phrased), I’d like to write a type annotation for y in the following expression, but it isn’t possible:

let f : forall a. a -> a = fun x => let y : ??? = x in y

Describe the solution you'd like

Something akin to GHC’s ScopedTypeVariables extension (or IIRC OCaml’s default behavior) making it so that any forall brings the newly bound type variables in scope for the whole subexpression.

Describe alternatives you've considered

Not annotate the inner expressions. But that’s not cool

[thufschmitt]

For a more compelling use-case, I was trying to implement a flatMap function on records, and got stuck because the typechecker can’t infer the type of an interemediary expression, and I can’t annotate it either:

  // Work around https://github.com/tweag/nickel/issues/375
let lists_fold = lists.fold | forall a b. (a -> b -> b) -> List a -> b -> b in
let fieldsOf = records.fieldsOf | forall a. { _ : a } -> List Str in

let
  record_flatMap : forall a b. (Str -> a -> { _ : b }) -> { _ : a } -> { _ : b } = fun f rec =>
    lists_fold
      (fun currentkey acc =>
        acc & f currentkey rec."#{currentkey}"
      )
      (records.fieldsOf rec)
      {}
in
record_flatMap

fails with

error: Incompatible types
  ┌─ /home/regnat/Repos/github.com/regnat/st_nicklaus/work/bug.ncl:8:9
  │
8 │         acc & f currentkey f."#{currentkey}"
  │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
  │
  = The type of the expression was expected to be `{_: b}`
  = The type of the expression was inferred to be `Dyn`
  = These types are not compatible

[yannham]

I don't think scoped type variables are gonna help with your example. The problem is that currently the type of merge is more or less Dyn -> Dyn -> Dyn, because it is non trivial to type in the current type system in general (to be honest, it may be feasible, but there are probably subtleties and edge cases, so we have kept it untyped until now). Unless you meant to annotate it with a contract, to circumvent the typechecker?

[thufschmitt]

I don't think scoped type variables are gonna help with your example. The problem is that currently the type of merge is more or less Dyn -> Dyn -> Dyn, because it is non trivial to type in the current type system in general (to be honest, it may be feasible, but there are probably subtleties and edge cases, so we have kept it untyped until now). Unless you meant to annotate it with a contract, to circumvent the typechecker?

That’s a good point indeed :) .But annotating it with a contract (or using a specialized version of & with a contract forall a. { _ : a } -> { _ : a } -> { _ : a }) would be good-enough in that case

[francois-caddet]

Translating the NixPkgs lib, I think I found a good example of this necesity of scoped type variable
It's in the lists.nix, the function groupBy.
The type would be forall a. (a -> Str) -> Array a -> { _: Array a}
My implementation look like follow:

= fun pred => array.foldl (fun r e =>
        let key = pred e in
          { "%{key}" = (r."%{key}" @ [e]) } & (record.remove key r)
     ) {},

In this case the typechecker will throw a type missmatch because:

{ "%{key}" = (r."%{key}" @ [e]) } & (record.remove key r)

is infered to be Dyn when we want it to be {_: Array a}

The intuitive way to fix it would have been to add a contract to it. But without scoped types vars, we get:

error: incompatible types
  ┌─ /Users/fcaddet/devel/tweag/internal/nickel/issue.ncl:6:10
  │
6 │          ({ "%{key}" = (r."%{key}" @ [e]) } & (record.remove key r)) | { _: Array a}
  │          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
  │
  = The type of the expression was expected to be `a`
  = The type of the expression was inferred to be `a`
  = These types are not compatible

So, I don't think we have any way right now to staticaly type groupBy even worst, the error is confusing.
Because this confusion is not specific to that case, I'll open an other issue to discuce how we can improve this message.