Lots of typechecking failures with thunks

[acl-cqc]

map(X :: *, Y :: *, { X -> Y }, n :: #, Vec(X, n)) -> Vec(Y, n)
map(_, _, _, _, []) = []
map(_, _, f, _, x ,- xs) = f(x) ,- map(!, !, f, !, xs)

inc(Nat) -> Nat
inc(x) = x + 1

test_working :: Vec(Nat, 3)
test_working = map(!, !, inc, !, [4,5,6])

-- This should give the typechecker more information
-- but doesn't seem to help compared to an untyped [3,6,7,8,9]
testVec :: Vec(Nat, 5)
testVec = [3,6,7,8,9]

test_fail1 :: Vec(Nat, 5)
test_fail1 = map(!, !, {_ + 1}, !, testVec)
--Error in examples/infer.brat on line 17:
--test_fail1 = map(!, !, {_ + 1}, !, testVec)
--                        ^^^^^
--
--  Expected (NamedPort {end = In infer_check_defs_1_test_fail1_13_$rhs_check'Th_3_lambda_fake_target_4 0, portName = "a1"},VApp VPar In infer_check_defs_1_test_fail1_13_$rhs_$!_2 0 B0) but got arithmetic expression

test_fail2 :: Vec(Nat, 5)
test_fail2 = map(!, !, {x => x + 1}, !, testVec)
--Error in examples/infer.brat on line 25:
--test_fail2 = map(!, !, {x => x + 1}, !, testVec)
--                             ^^^^^
--
--  Expected (NamedPort {end = In infer_check_defs_1_test_fail2_13_$rhs_check'Th_3_lambda_fake_target_4 0, portName = "a1"},VApp VPar In infer_check_defs_1_test_fail2_13_$rhs_$!_2 0 B0) but got arithmetic expression

id(X :: *, x :: X) -> X
id(_,x) = x

test_fail3 :: Vec(Nat, 5)
test_fail3 = map(!, !, {id(!, _)}, !, testVec)
--Error in examples/infer.brat on line 36:
--test_fail3 = map(!, !, {id(!, _)}, !, testVec)
--                        ^^^^^^^^
--
--  Type error: Type dependency of VApp VPar In infer_check_defs_1_test_fail3_16_$rhs_$!_1 0 B0 (In infer_check_defs_1_test_fail3_16_$rhs_$!_1 0) had an ambiguous type.

test_fail4 :: Vec(Nat, 5)
test_fail4 = map(!, !, {_}, !, testVec)
--Error in examples/infer.brat on line 44:
--test_fail4 = map(!, !, {_}, !, testVec)
--                        ^
--
--  Type error: Type dependency of VApp VPar In infer_check_defs_1_test_fail4_16_$rhs_$!_1 0 B0 (In infer_check_defs_1_test_fail4_16_$rhs_$!_1 0) had an ambiguous type.

test_fail5 :: Vec(Nat, 5)
test_fail5 = map(!, !, {id(Nat, _)}, !, testVec)
test_fail5 :: Vec(Nat, 5)
test_fail5 = map(!, !, {id(Nat, _)}, !, testVec)
--Error in examples/infer.brat on line 52:
--test_fail5 = map(!, !, {id(Nat, _)}, !, testVec)
--                        ^^^^^^^^^^
--
--  Type error: Type dependency of VApp VPar In infer_check_defs_1_test_fail5_16_$rhs_$!_1 0 B0 (In infer_check_defs_1_test_fail5_16_$rhs_$!_1 0) had an ambiguous type.

I'm confused by the last - I thought test_fail3 and test_fail4 were failing to infer a type through a closure, but in test_fail5 the type is explicitly specified (and changing the thunk to {x => id(Nat, x)} has the same error), so...

Might this be #35 ?

The others "but got arithmetic expression" may mean we are not (correctly?) handling overloading of + / arithmetic everywhere?

[croyzor]

test_fail{1,2} appear to be scheduling problems, I've opened a fix in #110
But, once applied, we get even weirder errors! We block waiting on the values of X, Y even if I give them explicitly with

map(Nat, Nat, { x => x + 1 }, !, testVec)

in this case checkOutputs seems to be failing to unify Vec(Nat, 5) with Vec(?X, ?n) leaving us blocked on ?X.
I do see ?X := Nat, so I guess the resumption isn't being kicked off...