Fix named argument unification

lib/std/core.kk

@@ -101,7 +101,7 @@ pub fun ignore( x : a ) : ()
   ()
 
 // Return a 'constant' function that ignores its argument and always returns the same result
-pub fun const( default : a ) : total (( x : b ) -> a)
+pub fun const( default : a ) : total (( b ) -> a)
   fn(_) default
 
 // Concise way to ensure two expressions have the same type.

lib/std/core/hnd.kk

@@ -463,7 +463,7 @@ fun prompt-local-var<a,b,s,e>(loc:local-var<s,a>, res : b  ) : <div,local<s>|e>
   val v = loc
   yield-cont(fn(cont,x){ loc := v; prompt-local-var(std/core/types/@byref(loc),cont(x)) } )  // restore state early before the resume
 
-pub inline fun local-var(init:a, action: (@local-var:local-var<s,a>) -> <local<s>|e> b ) : <local<s>|e> b
+pub inline fun local-var(init:a, action: (local-var<s,a>) -> <local<s>|e> b ) : <local<s>|e> b
   pretend-no-div
     val loc : local-var<_,_> = local-new(init)
     val res = cast-ev1(action)(std/core/types/@byref(loc))
@@ -593,7 +593,7 @@ noinline fun under1x( ev : ev<h>, op : a -> e b, x : a ) : e b
   evv-set(w0)
   y
 
-pub fun clause-control-raw1( op : (x:a, r: resume-context<b,e,e0,r>) -> e r ) : clause1<a,b,h,e,r>
+pub fun clause-control-raw1( op : (a, resume-context<b,e,e0,r>) -> e r ) : clause1<a,b,h,e,r>
   Clause1(fn(m,_ev,x){ yield-to(m, fn(k){ op(x,Resume-context(k)) } ) } )
 
 fun get( ref: ref<h,a>) : <read<h>,div> a
@@ -620,7 +620,7 @@ fun protect-prompt( resumed : ref<global,bool>,  k : resume-result<b,r> -> e r,
     if yielding() return yield-extend( fn(_x) unsafe-reyield(yld) ) // yikes, a finally clause is itself yielding...
     unsafe-reyield(yld)
 
-fun protect( x : a, clause : (x:a, k: b -> e r) -> e r, k : resume-result<b,r> -> e r ) : e r
+fun protect( x : a, clause : (a, b -> e r) -> e r, k : resume-result<b,r> -> e r ) : e r
   val resumed = (unsafe-st{ref(False)})()
   fun kprotect(ret)
     (unsafe-st{resumed := True})()
@@ -634,7 +634,7 @@ pub fun clause-control1( clause : (x:a, k: b -> e r) -> e r ) : clause1<a,b,e,r>
 */
 
 // generic control clause
-pub fun clause-control1( clause : (x:a, k: b -> e r) -> e r ) : clause1<a,b,h,e,r>
+pub fun clause-control1( clause : (a, b -> e r) -> e r ) : clause1<a,b,h,e,r>
   Clause1(fn(m,_ev,x){ yield-to(m, fn(k) protect(x,clause,k) ) })
 
 // tail-resumptive clause: resumes exactly once at the end
@@ -713,19 +713,19 @@ fun under2( ev : ev<h>, op : (a1,a2) -> e b, x1 : a1, x2 : a2 ) : e b
   if yielding() return yield-cont( fn(cont,res) under1(ev,cont,res) )
   z
 
-fun protect2( x1 : a1, x2:a2, clause : (x:a1,x:a2, k: b -> e r) -> e r, k : resume-result<b,r> -> e r ) : e r
+fun protect2( x1 : a1, x2:a2, clause : (a1, a2, b -> e r) -> e r, k : resume-result<b,r> -> e r ) : e r
   val resumed = (unsafe-st{ref(False)})()
   fun kprotect(ret)
     (unsafe-st{ resumed := True })()
     k(Deep(ret))
   val res = clause(x1,x2,kprotect)
   protect-prompt(resumed,k,res)
 
-pub fun clause-control2( clause : (x1:a1, x2:a2, k: b -> e r) -> e r ) : clause2<a1,a2,b,h,e,r>
+pub fun clause-control2( clause : (a1, a2, b -> e r) -> e r ) : clause2<a1,a2,b,h,e,r>
   Clause2(fn(m,_ev,x1,x2){ yield-to(m, fn(k){ protect2(x1,x2,clause,k) }) })
 
 
-pub fun clause-control-raw2( op : (x1:a1, x2:a2, r: resume-context<b,e,e0,r>) -> e r ) : clause2<a1,a2,b,h,e,r>
+pub fun clause-control-raw2( op : (a1, a2, resume-context<b,e,e0,r>) -> e r ) : clause2<a1,a2,b,h,e,r>
   Clause2(fn(m,_ev,x1,x2){ yield-to(m, fn(k){ op(x1,x2,Resume-context(k)) } ) })
 
 pub fun clause-tail2<e,r,h,a1,a2,b>(op : (a1,a2) -> e b) : clause2<a1,a2,b,h,e,r>
@@ -754,10 +754,10 @@ fun xperform1( ev : ev<h>, op : (forall<e1,r> h<e1,r> -> clause1<a,b,h,e1,r>), x
     Ev(_tag,m,h,_w) -> match h.op
       Clause1(f) -> cast-clause1(f)(m,ev,x)
 
-pub fun clause-control-raw3( op : (x1:a1, x2:a2, x3:a3, r: resume-context<b,e,e0,r>) -> e r ) : clause1<(a1,a2,a3),b,h,e,r>
+pub fun clause-control-raw3( op : (a1, a2, a3, resume-context<b,e,e0,r>) -> e r ) : clause1<(a1,a2,a3),b,h,e,r>
   clause-control-raw1( fn((x1,x2,x3),r){ op(x1,x2,x3,r) } )
 
-pub fun clause-control3( op : (x1:a1, x2:a2, x3:a3, k: b -> e r) -> e r ) : clause1<(a1,a2,a3),b,h,e,r>
+pub fun clause-control3( op : (a1, a2, a3, b -> e r) -> e r ) : clause1<(a1,a2,a3),b,h,e,r>
   clause-control1( fn((x1,x2,x3),k){ op(x1,x2,x3,k) } )
 
 pub fun clause-tail3<e,r,h,a1,a2,a3,b>(op : (a1,a2,a3) -> e b) : clause1<(a1,a2,a3),b,h,e,r>
@@ -781,7 +781,7 @@ fun under3( ev : ev<h>, op : (a1,a2,a3) -> e b, x1 : a1, x2 : a2, x3 : a3 ) : e
 
 
 
-pub fun clause-control4( op : (x1:a1, x2:a2, x3:a3, x4:a4, k: b -> e r) -> e r ) : clause1<(a1,a2,a3,a4),b,h,e,r>
+pub fun clause-control4( op : (a1, a2, a3, a4, b -> e r) -> e r ) : clause1<(a1,a2,a3,a4),b,h,e,r>
   clause-control1( fn((x1,x2,x3,x4),k){ op(x1,x2,x3,x4,k) } )
 
 pub fun clause-tail4<e,r,h,a1,a2,a3,a4,b>(op : (a1,a2,a3,a4) -> e b) : clause1<(a1,a2,a3,a4),b,h,e,r>

lib/std/core/sslice.kk

@@ -234,11 +234,11 @@ pub fun slice/foreach( slice : sslice, action : (c:char) -> e ()) : e ()
 
 // Invoke a function for each character in a string.
 // If `action` returns `Just`, the function returns immediately with that result.
-pub fun string/foreach-while( s : string, action : (c:char) -> e maybe<a> ) : e maybe<a>
+pub fun string/foreach-while( s : string, action : (char) -> e maybe<a> ) : e maybe<a>
   s.slice.foreach-while(action)
 
 // Invoke a function for each character in a string
-pub fun string/foreach( s : string, action : (c:char) -> e () ) : e ()
+pub fun string/foreach( s : string, action : (char) -> e () ) : e ()
   s.slice.foreach(action)
 
 // Return the first character of a string (or `Nothing` for the empty string).

src/Common/Name.hs

@@ -31,6 +31,7 @@ module Common.Name
           , newHiddenExternalName, isHiddenExternalName
           , newHiddenName, isHiddenName, hiddenNameStartsWith
           , makeHiddenName, makeFreshHiddenName, newHiddenNameEx
+          , nameIsFixedArg
           , toUniqueName
           , newImplicitTypeVarName, isImplicitTypeVarName
           , newCreatorName, isCreatorName
@@ -468,6 +469,9 @@ nameIsNil :: Name -> Bool
 nameIsNil name
   = null (nameStem name) && null (nameModule name)
 
+nameIsFixedArg :: Name -> Bool
+nameIsFixedArg nm = nameIsNil nm || hiddenNameStartsWith nm "arg"
+
 qualify :: HasCallStack => Name -> Name -> Name
 qualify (Name m hm _ 0 _ 0) (Name _ 0 l hl n hn)     = Name m hm l hl n hn
 qualify (Name m1 _ _ 0 _ 0) name@(Name m2 _ _ _ _ _) | m1 == m2 = name

src/Syntax/Parse.hs

@@ -1044,7 +1044,7 @@ makeEffectDecl decl =
                    makeTpFun [
                     -- (newName "cfc", TpCon nameTpInt32 krng),
                     (newName "hnd", TpApp (TpCon hndName grng) (map tpVar (scopedTpVars ++ [hndEffTp,hndResTp])) grng),
-                    (newName "ret", makeTpFun [(newName "res",tpVar handleRetTp)] (tpVar hndEffTp) (tpVar hndResTp) grng),
+                    (newName "ret", makeTpFun [(nameNil,tpVar handleRetTp)] (tpVar hndEffTp) (tpVar hndResTp) grng),
                     (newName "action",
                         if (isScoped)
                           then quantify QForall tparsScoped actionTp

src/Type/Unify.hs

@@ -268,7 +268,8 @@ unify (TApp t1 ts1) (TApp u1 us2)   -- | length ts1 != length us2
 
 -- functions
 unify f1@(TFun args1 eff1 res1) f2@(TFun args2 eff2 res2) | length args1 == length args2
-  = do unifies (res1:map snd args1) (res2:map snd args2)
+  = do subunify res1 res2
+       unifiesArgs args1 args2
        withError (effErr) (unify eff1 eff2)
   where
     -- specialize to sub-part of the type for effect unification errors
@@ -325,6 +326,48 @@ unify tp1 tp2
   = -- trace ("no match: " ++  show (pretty tp1, pretty tp2)) $
     unifyError NoMatch
 
+subunify :: HasCallStack => Type -> Type -> Unify ()
+subunify tp1 tp2
+  = do stp1 <- subst tp1
+       stp2 <- subst tp2
+       unify stp1 stp2
+
+unifiesArgs :: HasCallStack => [(Name,Type)] -> [(Name,Type)] -> Unify ()
+unifiesArgs [] [] = return ()
+-- Names both nil, unify types
+unifiesArgs ((nm1, tp1):rst1) ((nm2, tp2):rst2) | nameIsFixedArg nm1 && nameIsFixedArg nm2 = do
+  subunify tp1 tp2
+  unifiesArgs rst1 rst2
+-- Names match in order
+unifiesArgs ((nm1, tp1):rst1) ((nm2, tp2):rst2) | nm1 == nm2 
+  = do subunify tp1 tp2
+       unifiesArgs rst1 rst2 
+-- Named, matches named argument elsewhere in list, or match first unnamed argument
+unifiesArgs ((nm1, tp1):rst1) ls2@((nm2, tp2):rst2) | not (nameIsFixedArg nm1)
+  = case lookup nm1 ls2 of
+      Just tp2' -> do subunify tp1 tp2'
+                      unifiesArgs rst1 (filter (\(nm,_) -> nm /= nm1) ls2)
+      Nothing  -> 
+        -- trace ("unifiesArgs: " ++ show (nm1, tp1) ++ " not found in " ++ show ls2) $
+        if nameIsFixedArg nm2 then do
+          subunify tp1 tp2 
+          unifiesArgs rst1 rst2
+        else unifyError NoMatch
+-- Named, matches named argument elsewhere in list, or match first unnamed argument
+unifiesArgs ls1@((nm1, tp1):rst1) ((nm2, tp2):rst2) | not (nameIsFixedArg nm2)
+  = case lookup nm2 ls1 of
+      Just tp1' -> do subunify tp1' tp2
+                      unifiesArgs (filter (\(nm,_) -> nm /= nm2) ls1) rst2
+      Nothing  ->
+        if nameIsFixedArg nm1 then do
+          subunify tp1 tp2 
+          unifiesArgs rst1 rst2
+        else unifyError NoMatch
+unifiesArgs [] (_:ls2) = unifyError NoMatch 
+unifiesArgs (_:ls1) [] = unifyError NoMatch
+unifiesArgs _ _ = 
+  error "Type.Unify.unifiesArgs: should not happen"
+
 
 -- | Unify a type variable with a type
 unifyTVar :: HasCallStack => TypeVar -> Type -> Unify ()

test/type/wrong/named-args.kk

@@ -0,0 +1,63 @@
+import std/num/int32
+
+val player-size = 16
+val pink = 10
+
+// take a type that has a position, and a change in position, and update the position
+fun location/update<locatable>(a: locatable, dx: int, dy: int, 
+                              ?x: locatable -> int, ?y: locatable -> int, 
+                              ?@copy: (locatable, x: int, y: int) -> locatable): locatable
+  a.@copy(x = a.x + dx, y = a.y + dy)
+
+// take a type that has a velocity, and a change in velocity, and update the velocity
+fun velocity/update<movable>(a: movable, ddx: int, ddy: int, 
+                    ?dx: movable -> int, ?dy: movable -> int, 
+                    ?@copy: (movable, dx: int, dy: int) -> movable): movable
+  a.@copy(dx = a.dx + ddx, dy = a.dy + ddy)
+
+// take a type that has a position and velocity, and apply the velocity to the position
+fun apply-velocity<movable>(a: movable, 
+                          ?x: movable -> int, ?y: movable -> int, 
+                          ?dx: movable -> int, ?dy: movable -> int, 
+  // ERROR: This copy function should not match the @copy parameter expected by `location/update`!
+                          ?@copy: (movable, dx: int, dy: int) -> movable): movable
+  a.location/update(a.dx, a.dy)
+
+// Let's make some specific types for player and enemy
+value struct player
+  x: int
+  y: int
+  dx: int
+  dy: int
+
+value struct enemy
+  x: int
+  y: int
+  dx: int
+  dy: int
+
+fun draw-rectangle(x: int32, y: int32, width: int32, height: int32, color: int)
+  // Implementation of drawing a rectangle on the screen
+  // This is a placeholder function. Replace with actual drawing logic.
+  println("Drawing rectangle at (" ++ x.show ++ ", " ++ y.show ++  ") with size (" ++ width.show ++ ", " ++ height.show ++ ") and color " ++ color.show)
+
+fun up-pressed(): bool
+  // Placeholder for checking if the up key is pressed
+  // Replace with actual input handling logic.
+  return True
+
+fun positioned/draw<locatable>(^a: locatable, ?x: locatable -> int, ?y: locatable -> int): <io> ()
+  draw-rectangle(
+    int32(a.x),
+    int32(a.y),
+    player-size.int32, player-size.int32, pink)
+
+fun main()
+  var p := Player(0, 0, 0, 0)
+  var e := Enemy(100, 100, 0, 0)
+  // ... somewhere in the update loop
+  if up-pressed() then
+    p := p.velocity/update(0, 1).apply-velocity()
+  e := e.velocity/update(0, -1).apply-velocity()
+  p.draw()
+  e.draw()

test/type/wrong/named-args.kk.out

@@ -0,0 +1,5 @@
+test/type/wrong/named-args@kk(24,19): type error: types do not match
+ context : a@location/update(a@dx, a@dy)
+ term : 
+ inferred type: ($a, dx : int, dy : int) -> _e $a
+ expected type: ($a, x : int, y : int) -> $a