Partially applied type aliases?

[SchrodingerZhu]

alias mylist<a> = list<a>

alias mykind<s, a> = list<s<a>>

fun foo(): mykind<mylist, int> {
    [[1]]
}

// the following compiles
// fun foo(): mykind<list, int> {
//     [[1]]
// }

This gives me an error like:

error: types do not match
  context      : fun foo(): mykind<mylist, int> {
                     [[1]]
                 }
  term         :                                {
                     [[1]]
                 }
  inferred type: list<list<int>>
  expected type: mykind<mylist,int>
  because      : function returns values of different types

[SchrodingerZhu]

Or is this a feature? xD

[daanx]

Ha, interesting example. I first thought it was a bug in Koka but now I remember that aliases always must be fully applied and cannot be partially applied (so, indeed, a "feature" :-) ). The reason is quite fundamental, during type inference we may have to determine an equality like m a ~ b; normally, this must mean that b is unified to m a; but if I allow partially applied aliases, we may have an alias like alias id<a> = a and we get a constraint id a ~ b and now we could also have a = b instead ...

This is a fundamentally hard problem (and dependent type systems have this as there the m can be a function and thus these systems need much more complex machinery).

Actually, Haskell has the same restriction but GHC has the liberalized type synonyms extension that delays kind checking until after full alias expansion but Koka does not do that (yet?)