@@ -11,13 +11,13 @@ fun map: [A, B, E] -> List[out A] -> (A ->{E} B) ->{E} List[out B]
1111
1212
1313// * Dummy implementation
14- fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A]
14+ fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A]
1515fun mapi = s => f =>
1616 region r in
1717 map(s) of x => f(0, x)
1818//│ Type: ⊤
1919
20- fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A]
20+ fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A]
2121fun mapi = s => f =>
2222 region r in
2323 let i = r.ref 0
@@ -43,14 +43,14 @@ region r in
4343// * Should be an error. This definition would not be referentially transparent.
4444// * The error message needs improvement, though.
4545:e
46- fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{Alloc | E} List[out A]
46+ fun mapi: [A, E] -> List[out A] -> ((Int, A) ->{E} A) ->{E} List[out A]
4747fun mapi = s =>
4848 region r in
4949 let i = r.ref 0
5050 f => map(s) of x =>
5151 i := !i + 1
5252 f(!i, x)
53- //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
55_2 ) ->{<E>
56_2 } <A>
55_2 ) ->{
Alloc ∨ <E>
56_2 } List[out <A>
55_2 ]
53+ //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
54_2 ) ->{<E>
55_2 } <A>
54_2 ) ->{<E>
55_2 } List[out <A>
54_2 ]
5454//│ ║ l.49: let i = r.ref 0
5555//│ ║ ^^^^^^^
5656//│ ║ l.50: f => map(s) of x =>
@@ -59,15 +59,15 @@ fun mapi = s =>
5959//│ ║ ^^^^^^^^^^^^^^^^^
6060//│ ║ l.52: f(!i, x)
6161//│ ║ ^^^^^^^^^^^^^^
62- //│ ╟── because: cannot constrain
f71_2 ->{
E79_2 } List[out
B78_2 ] <: ((Int, <A>
55_2 ) ->{<E>
56_2 } <A>
55_2 ) ->{
Alloc ∨ <E>
56_2 } List[out <A>
55_2 ]
63- //│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
64- //│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~ <E>56_2 )
65- //│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~ <E>56_2 )
66- //│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~ <E>56_2 )
67- //│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~ <E>56_2 )
68- //│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~ <E>56_2 )
69- //│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~ <E>56_2 )
70- //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
55_2 ) ->{<E>
56_2 } <A>
55_2 ) ->{
Alloc ∨ <E>
56_2 } List[out <A>
55_2 ]
62+ //│ ╟── because: cannot constrain
f70_2 ->{
E78_2 } List[out
B77_2 ] <: ((Int, <A>
54_2 ) ->{<E>
55_2 } <A>
54_2 ) ->{<E>
55_2 } List[out <A>
54_2 ]
63+ //│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
64+ //│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2 )
65+ //│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2 )
66+ //│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2 )
67+ //│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2 )
68+ //│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2 )
69+ //│ ╙── because: cannot constrain <: ¬(~<E>55_2 )
70+ //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
54_2 ) ->{<E>
55_2 } <A>
54_2 ) ->{<E>
55_2 } List[out <A>
54_2 ]
7171//│ ║ l.49: let i = r.ref 0
7272//│ ║ ^^^^^^^
7373//│ ║ l.50: f => map(s) of x =>
@@ -76,15 +76,15 @@ fun mapi = s =>
7676//│ ║ ^^^^^^^^^^^^^^^^^
7777//│ ║ l.52: f(!i, x)
7878//│ ║ ^^^^^^^^^^^^^^
79- //│ ╟── because: cannot constrain
f71_2 ->{
E79_2 } List[out
B78_2 ] <: ((Int, <A>
55_2 ) ->{<E>
56_2 } <A>
55_2 ) ->{
Alloc ∨ <E>
56_2 } List[out <A>
55_2 ]
80- //│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
81- //│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~ <E>56_2 )
82- //│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~ <E>56_2 )
83- //│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~ <E>56_2 )
84- //│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~ <E>56_2 )
85- //│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~ <E>56_2 )
86- //│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~ <E>56_2 )
87- //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
55_2 ) ->{<E>
56_2 } <A>
55_2 ) ->{
Alloc ∨ <E>
56_2 } List[out <A>
55_2 ]
79+ //│ ╟── because: cannot constrain
f70_2 ->{
E78_2 } List[out
B77_2 ] <: ((Int, <A>
54_2 ) ->{<E>
55_2 } <A>
54_2 ) ->{<E>
55_2 } List[out <A>
54_2 ]
80+ //│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
81+ //│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2 )
82+ //│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2 )
83+ //│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2 )
84+ //│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2 )
85+ //│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2 )
86+ //│ ╙── because: cannot constrain <: ¬(~<E>55_2 )
87+ //│ ╔══[ERROR] Type error in region expression with expected type ((Int, <A>
54_2 ) ->{<E>
55_2 } <A>
54_2 ) ->{<E>
55_2 } List[out <A>
54_2 ]
8888//│ ║ l.49: let i = r.ref 0
8989//│ ║ ^^^^^^^
9090//│ ║ l.50: f => map(s) of x =>
@@ -93,28 +93,14 @@ fun mapi = s =>
9393//│ ║ ^^^^^^^^^^^^^^^^^
9494//│ ║ l.52: f(!i, x)
9595//│ ║ ^^^^^^^^^^^^^^
96- //│ ╟── because: cannot constrain f71_2 ->{E79_2} List[out B78_2] <: ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
97- //│ ╟── because: cannot constrain D( E79_2 ) <: Alloc ∨ <E>56_2
98- //│ ╟── because: cannot constrain E79_2 <: ¬(~{Alloc} && ~<E>56_2)
99- //│ ╟── because: cannot constrain ¬⊥ ∧ α80_2 <: ¬(~{Alloc} && ~<E>56_2)
100- //│ ╟── because: cannot constrain α80_2 <: ¬(~{Alloc} && ~<E>56_2)
101- //│ ╟── because: cannot constrain ¬⊥ ∧ r81_2 <: ¬(~{Alloc} && ~<E>56_2)
102- //│ ╟── because: cannot constrain r81_2 <: ¬(~{Alloc} && ~<E>56_2)
103- //│ ╙── because: cannot constrain <: ¬(~{Alloc} && ~<E>56_2)
104- //│ ╔══[ERROR] Type error in function literal with expected type (List[out <A>55_2]) ->{⊥} ((Int, <A>55_2) ->{<E>56_2} <A>55_2) ->{Alloc ∨ <E>56_2} List[out <A>55_2]
105- //│ ║ l.47: fun mapi = s =>
106- //│ ║ ^^^^
107- //│ ║ l.48: region r in
108- //│ ║ ^^^^^^^^^^^^^
109- //│ ║ l.49: let i = r.ref 0
110- //│ ║ ^^^^^^^^^^^^^^^^^^^
111- //│ ║ l.50: f => map(s) of x =>
112- //│ ║ ^^^^^^^^^^^^^^^^^^^^^^^
113- //│ ║ l.51: i := !i + 1
114- //│ ║ ^^^^^^^^^^^^^^^^^
115- //│ ║ l.52: f(!i, x)
116- //│ ║ ^^^^^^^^^^^^^^
117- //│ ╙── because: cannot constrain α70_2 ∨ Alloc <: ⊥
96+ //│ ╟── because: cannot constrain f70_2 ->{E78_2} List[out B77_2] <: ((Int, <A>54_2) ->{<E>55_2} <A>54_2) ->{<E>55_2} List[out <A>54_2]
97+ //│ ╟── because: cannot constrain D( E78_2 ) <: <E>55_2
98+ //│ ╟── because: cannot constrain E78_2 <: ¬(~<E>55_2)
99+ //│ ╟── because: cannot constrain ¬⊥ ∧ α79_2 <: ¬(~<E>55_2)
100+ //│ ╟── because: cannot constrain α79_2 <: ¬(~<E>55_2)
101+ //│ ╟── because: cannot constrain ¬⊥ ∧ r80_2 <: ¬(~<E>55_2)
102+ //│ ╟── because: cannot constrain r80_2 <: ¬(~<E>55_2)
103+ //│ ╙── because: cannot constrain <: ¬(~<E>55_2)
118104//│ Type: ⊤
119105
120106
0 commit comments