wasm validation error through escaping rigid type variables

[Innf107]

Minimal Example

The follwing code throws a 'wasm validation error' in the Roc REPL. It should arguably not compile at all since the (rigid) local type variable a escapes its scope by being unified with the type of x in the expression h x.

f = \x ->
    g : (a -> {}) -> {}
    g = \h -> h x
    g
f 5

Error Message

JsValue(CompileError: wasm validation error: at offset 5077: unused values not explicitly dropped by end of block)

[ayazhafiz]

This is a bug, and the program should compile. That “a” leaks into the outer scope is not a problem as long as the inner function g is not generalized.

---

From: Prophet @.> Sent: Wednesday, April 19, 2023 6:48:06 AM To: roc-lang/roc @.> Cc: Subscribed @.***> Subject: [roc-lang/roc] wasm validation error through escaping rigid type variables (Issue #5306)

Minimal Example

The follwing code throws a 'wasm validation error' in the Roc REPL. It should arguably not compile at all since the (rigid) local type variable a escapes its scope by being unified with the type of x in the expression h x.

f = \x -> g : (a -> {}) -> {} g = \h -> h x g f 5

Error Message

JsValue(CompileError: wasm validation error: at offset 5077: unused values not explicitly dropped by end of block)

— Reply to this email directly, view it on GitHubhttps://github.com/roc-lang/roc/issues/5306, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AE6GL6XVYYSZK7H7YHVPXFLXB7GHNANCNFSM6AAAAAAXD6KJ2Q. You are receiving this because you are subscribed to this thread.Message ID: @.***>

[Innf107]

Is g not generalized even though it has a type signature? If it's not, then my understanding of type variables in Roc seems to be wrong.

What does a type variable like a in the example above mean?

I assumed it meant the same as it would in Haskell, which would be equivalent to

g : forall a. (a -> {}) -> {}

And it certainly doesn't mean the same as 'a in OCaml (i.e. just introducing a unification variable), since then

g : a
g = 5

would have to compile.

[ayazhafiz]

It’s a great question. A type variable “a” does introduce a generalized variable, but the scope of the generalization is not guaranteed - concretely, in this case we want “g” and “f” respectively to be generalized on the same level, that is, both should be generalized on the top level. However, “g” should not be generalized relative to “f”, because Roc does not support higher ranks. So, the type of “f” would be “a->((a->{})->{})” where a is the same as it is on g.

---

From: Prophet @.> Sent: Wednesday, April 19, 2023 8:37:36 AM To: roc-lang/roc @.> Cc: Ayaz @.>; Comment @.> Subject: Re: [roc-lang/roc] wasm validation error through escaping rigid type variables (Issue #5306)

Is g not generalized even though it has a type signature? If it's not, then my understanding of type variables in Roc seems to be wrong.

What does a type variable like a in the example above mean?

I assumed it meant the same as it would in Haskell, which would be equivalent to

g : forall a. (a -> {}) -> {}

And it certainly doesn't mean the same as 'a in OCaml (i.e. just introducing a unification variable), since then

g : a g = 5

would have to compile.

— Reply to this email directly, view it on GitHubhttps://github.com/roc-lang/roc/issues/5306#issuecomment-1514752797, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AE6GL6XUIYXWLHXVZEAD7R3XB7TCBANCNFSM6AAAAAAXD6KJ2Q. You are receiving this because you commented.Message ID: @.***>

[Innf107]

That makes sense. Thanks!