The madness of implicit parameters: cured?

[Ashley Yakeley]

At 2003-08-03 14:09, Ben Rudiak-Gould wrote:

>This reduction is incorrect. Auto-lifted parameters on the RHS of an
>application get lifted out

I am interpreting this as "Auto-lifted parameters on the RHS of an 
application get lifted out before {@x=y}-style 'beta'-reduction can be 
done". I think this is ambiguous:

((\a -> ((a,?x) {@x = 2})) ?x,?x) {@x = 1}
((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1}

1.
((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1}
((\@x -> (@x,@x)) {@x = 2},\@x -> @x) {@x = 1}
((2,2),\@x -> @x) {@x = 1}
(\@x -> ((2,2),@x)) {@x = 1}
((2,2),1)

2.
(\@x -> ((\a -> ((a,\@x -> @x) {@x = 2})) @x,@x)) {@x = 1}
((\a -> ((a,\@x -> @x) {@x = 2})) 1,1)
(((1,\@x -> @x) {@x = 2}),1)
(((\@x -> (1,@x)) {@x = 2}),1)
((1,2),1)

A simpler query: what types can f have here? Which if any should the 
compiler infer?

  f a b = (a,b) {@x = 2}

And given that type, which of these are valid?

  f ?x ?x
  f ?x 1
  f 1 ?x
  f 1 1


-- 
Ashley Yakeley, Seattle WA