Strange expected type of a match expression

[osa1]

fun loop(num: i32): <console, div>()
  val i: i32 = match parse-int("asdf")
    Nothing ->
      println("That's not an int!")
      return loop(num)
    Just(i) ->
      i.i32

  ()

Error:

...(18,16): type error: types do not match
  context      :       i
  term         :                match parse-int("asdf")
                 ...
                       i.i32
  inferred type: int32
  expected type: forall<a> a
  because      : type cannot be instantiated to match the annotation

Failed to compile guess-the-number.kk

How can the expected type of this match expression be forall<a> a?

~ $ koka --version
Koka 3.1.2, 17:56:43 May 30 2024 (ghc release version)

[chtenb]

The two arms of the match expression do not have the same return type. The first has (), while the second has int32. What do you want it to do?

[osa1]

What do you want it to do?

See how Rust does it: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0078ed289e1549309ab48b492e6e7e49

In general, early return statements don't need to have the type expected by the surrounding expression as they return from the function, do not generate a value for the surrounding expression.

[chtenb]

Interesting, I didn't know that was allowed in Koka, but it seems to be. That's cool.

[osa1]

The real issue here seems to be that i32 isn't a type but I'm still able to use it as a type (I don't get a "type i32 is not defined" error as usual) and it causes a seemingly unrelated error. If I correct it as int32 then my code type checks.

[osa1]

import std/num/int32

pub fun main()
  ()

fun loop(num: i32): <console, div>()
  val i: i32 = match parse-int("asdf")
    Nothing ->
      println("That's not an int!")
      return loop(num)
    Just(i) ->
      i.i32

  ()

Replace i32s with int32s to fix.

Edit: I noticed that you also have to remove the type annotation on val i: ... to fix. No idea why that's also needed.

[TimWhiting]

Update: I figured out the issue

Type variables in koka are any name in type position that start with a single letter and are followed by any number of numbers.

So the compiler treats your program like this.

fun loop<a>(num: a): <console, div>()
  val i: b = match parse-int("asdf")
    Nothing ->
      println("That's not an int!")
      return loop(num)
    Just(i) ->
      i.i32
  ()

The error messages make so much more sense now. I do believe the error message could be improved though. Any suggestions?

[osa1]

Ahh, good catch.

Type variables in koka are any name in type position that start with a single letter and are followed by any number of numbers.

This is only for implicitly quantified variables, right? When I explicitly list the quantified variables I can use any id.

This makes me think that maybe having a syntax for type variables (like 'a in OCaml) makes sense.

[TimWhiting]

Yes it seems like you can explicitly quantify them and use any name, that is something I hadn't known before. Yeah, I hadn't realized why OCaml chose to use a syntax like that until now.

[osa1]

This makes me think that maybe having a syntax for type variables (like 'a in OCaml) makes sense.

Or we could make type constructors and constants uppercase (e.g. Int32) and variables lowercase (e.g. int32), like in Haskell.