Initializing a var with a value annotated with its own generic type does not typecheck

[fhackett]

I found this oddity while trying to figure out a type error in my code by annotating types I thought I knew.

Here is a minimal example:

fun test-fun(init: a): total () {
  var foo := (init: a)
  ()
}

Logically, this code should be fine. init has type a by definition, so it should be redundant but fine to annotate it with its own type.

When I try to compile it with Koka version 2.4.0, Feb 6 2022, libc x64 (gcc), it complains like this:

test.kk(3,15): error: abstract types do not match
  context      :               init: a
  term         :               init
  inferred type: $a
  expected type: forall<b> b
  because      : type cannot be instantiated to match the annotation

If I remove the annotation, it compiles fine. If I change a to a concrete type (e.g int) but keep the annotation, it also compiles fine.

Perhaps there is a missing unification rule?

[TimWhiting]

I think you have to explicitly state that you want the type parameter to be polymorphic.

See the video here for more information on the value type system (HMF): https://dl.acm.org/doi/abs/10.1145/1411204.1411245

fun test-fun(init: forall<a> a): total () {
  var foo := (init: a)
  ()
}

[fhackett]

Thank you for the response. That is interesting. I'll have a read about HMF, especially since it seems adjacent to things I should know more about.

Considering this issue as just a regular user though, it seems that "where do I put forall" is not covered at all by the manual. I noticed the keyword existed, but never saw any guidance on when, how or why I should use it. If I have time, I might try to PR a manual section in order to consolidate my understanding of HMF in practice.

[TimWhiting]

Note that you can also do this, though forall is better documentation at a function level I think:

fun test-fun(init: a): total () {
  var foo := (init: some<a> a)
  ()
}

Also, Daan also was the author of a paper on HML which was more recent. https://dl.acm.org/doi/abs/10.1145/1480881.1480891?casa_token=XzzyxRRZTIAAAAAA:uGbDUMT70JgYWj88AGzVtd-zW6GUmR7uf7m-31CHg7E6Pi1ujQvqjQbWSVdnr5no1n87FLGQS-Wg

I'm not sure exactly which type system Koka actually uses. Update: This paper says that Koka uses HMF: https://dl.acm.org/doi/pdf/10.1145/3563289