diff --git a/src/as_frontend/typing.ml b/src/as_frontend/typing.ml
index b83219f4368..68127440271 100644
--- a/src/as_frontend/typing.ml
+++ b/src/as_frontend/typing.ml
@@ -549,7 +549,7 @@ and infer_exp'' env exp : T.typ =
| ArrayE (mut, exps) ->
let ts = List.map (infer_exp env) exps in
let t1 = List.fold_left T.lub T.Non ts in
- if not env.pre && t1 = T.Any && List.for_all (fun t -> T.promote t <> T.Any) ts then
+ if not env.pre && is_inconsistent t1 ts then
warn env exp.at
"this array has type %s because elements have inconsistent types"
(T.string_of_typ (T.Array t1));
@@ -665,7 +665,7 @@ and infer_exp'' env exp : T.typ =
let t2 = infer_exp env exp2 in
let t3 = infer_exp env exp3 in
let t = T.lub t2 t3 in
- if not env.pre && t = T.Any && T.promote t2 <> T.Any && T.promote t3 <> T.Any then
+ if not env.pre && is_inconsistent t [t2; t3] then
warn env exp.at
"this if has type %s because branches have inconsistent types,\ntrue produces\n %s\nfalse produces\n %s"
(T.string_of_typ t)
@@ -853,7 +853,7 @@ and infer_case env t_pat t {it = {pat; exp}; at; _} =
let ve = check_pat env t_pat pat in
let t' = recover_with T.Non (infer_exp (adjoin_vals env ve)) exp in
let t'' = T.lub t t' in
- if not env.pre && t'' = T.Any && T.promote t <> T.Any && T.promote t' <> T.Any then
+ if not env.pre && is_inconsistent t'' [t; t'] then
warn env at "the switch has type %s because branches have inconsistent types,\nthis case produces type\n %s\nthe previous produce type\n %s"
(T.string_of_typ t'')
(T.string_of_typ_expand t)
@@ -867,6 +867,9 @@ and check_case env t_pat t {it = {pat; exp}; _} =
let ve = check_pat env t_pat pat in
recover (check_exp (adjoin_vals env ve) t) exp
+and is_inconsistent lub ts =
+ lub = T.Any && List.for_all (fun t -> T.promote t <> lub) ts
+ || lub = T.Shared && List.for_all (fun t -> T.promote t <> lub) ts
(* Patterns *)
diff --git a/src/as_ir/check_ir.ml b/src/as_ir/check_ir.ml
index a213349bc6a..88858ba1820 100644
--- a/src/as_ir/check_ir.ml
+++ b/src/as_ir/check_ir.ml
@@ -128,7 +128,9 @@ let rec check_typ env typ : unit =
| T.Var (s, i) ->
error env no_region "free type variable %s, index %i" s i
| T.Con (c, typs) ->
- check env no_region (T.ConSet.mem c env.cons) "free type constructor %s" (Con.name c);
+ (*check env no_region (T.ConSet.mem c env.cons) "free type constructor %s" (Con.name c);
+ TODO(gabor): re-add above check when it is understood how to deal with mu-types
+ originating from lub/glb *)
(match Con.kind c with | T.Def (tbs, t) | T.Abs (tbs, t) ->
check_typ_bounds env tbs typs no_region
)
diff --git a/src/as_types/type.ml b/src/as_types/type.ml
index 8ca00731cb7..42864b3a472 100644
--- a/src/as_types/type.ml
+++ b/src/as_types/type.ml
@@ -288,10 +288,9 @@ let open_binds tbs =
let cs = List.map (fun {var; _} -> Con.fresh var (Abs ([], Pre))) tbs in
let ts = List.map (fun c -> Con (c, [])) cs in
let ks = List.map (fun {bound; _} -> Abs ([], open_ ts bound)) tbs in
- List.iter2 (fun c k -> set_kind c k) cs ks;
+ List.iter2 set_kind cs ks;
ts
-
(* Normalization and Classification *)
let reduce tbs t ts =
@@ -556,6 +555,12 @@ let is_concrete t =
end
in go t
+
+module M = Map.Make (struct type t = typ * typ let compare = compare end)
+(* Forward declare
+ TODO: haul string_of_typ before the lub/glb business, if possible *)
+let str = ref (fun _ -> failwith "")
+
(* Equivalence & Subtyping *)
module S = Set.Make (struct type t = typ * typ let compare = compare end)
@@ -731,63 +736,164 @@ and eq_kind k1 k2 : bool =
(* Least upper bound and greatest lower bound *)
-let rec lub t1 t2 =
+let rec lub' lubs glbs t1 t2 =
if t1 == t2 then t1 else
- (* TBR: this is just a quick hack *)
- match normalize t1, normalize t2 with
- | _, Pre
- | Pre, _ -> Pre
- | _, Any
- | Any, _ -> Any
- | _, Non -> t1
- | Non, _ -> t2
- | Prim Nat, Prim Int
- | Prim Int, Prim Nat -> Prim Int
- | Opt t1', Opt t2' -> Opt (lub t1' t2')
- | Variant t1', Variant t2' -> Variant (lub_tags t1' t2')
- | Prim Null, Opt t'
- | Opt t', Prim Null -> Opt t'
- | Array t1', (Obj _ as t2) -> lub (array_obj t1') t2
- | (Obj _ as t1), Array t2' -> lub t1 (array_obj t2')
- | t1', t2' when eq t1' t2' -> t1
- | _ -> Any
-
-and lub_tags fs1 fs2 = match fs1, fs2 with
+ match M.find_opt (t1, t2) !lubs with
+ | Some t -> t
+ | _ ->
+ match t1, t2 with
+ | _, Pre
+ | Pre, _ -> assert false
+ | _, Any
+ | Any, _ -> Any
+ | _, Non -> t1
+ | Non, _ -> t2
+ | Shared, _ when sub t2 Shared -> Shared
+ | _, Shared when sub t1 Shared -> Shared
+ | Prim Nat, (Prim Int as t)
+ | (Prim Int as t), Prim Nat -> t
+ | Opt t1', Opt t2' ->
+ Opt (lub' lubs glbs t1' t2')
+ | Prim Null, Opt t' -> t2
+ | Opt t', Prim Null -> t1
+ | Variant t1', Variant t2' ->
+ Variant (lub_tags lubs glbs t1' t2')
+ | Array t1', Obj _ -> lub' lubs glbs (array_obj t1') t2
+ | Obj _, Array t2' -> lub' lubs glbs t1 (array_obj t2')
+ | Prim Text, Obj _ -> lub' lubs glbs text_obj t2
+ | Obj _, Prim Text -> lub' lubs glbs t1 text_obj
+ | Prim Text, Array t2' -> lub' lubs glbs text_obj (array_obj t2')
+ | Array t1', Prim Text -> lub' lubs glbs (array_obj t1') text_obj
+ | Array t1', Array t2' ->
+ Array (lub' lubs glbs t1' t2')
+ | Tup ts1, Tup ts2 when List.(length ts1 = length ts2) ->
+ Tup (List.map2 (lub' lubs glbs) ts1 ts2)
+ | Obj (s1, tf1), Obj (s2, tf2) when s1 = s2 ->
+ Obj (s1, lub_fields lubs glbs tf1 tf2)
+ | Func (s1, c1, bs1, args1, res1), Func (s2, c2, bs2, args2, res2)
+ when s1 = s2 && c1 = c2 && List.(length bs1 = length bs2) &&
+ List.(length args1 = length args2 && length res1 = length res2) ->
+ combine_func_parts s1 c1 bs1 args1 res1 bs2 args2 res2 lubs glbs glb' lub'
+ | Async t1', Async t2' ->
+ Async (lub' lubs glbs t1' t2')
+ | Con _, _
+ | _, Con _ ->
+ combine_con_parts t1 t2 "lub" lubs (lub' lubs glbs)
+ | _ when eq t1 t2 -> t1
+ | _ when sub t1 Shared && sub t2 Shared -> Shared
+ | _ -> Any
+
+and lub_fields lubs glbs fs1 fs2 = match fs1, fs2 with
+ | _, [] -> []
+ | [], _ -> []
+ | f1::fs1', f2::fs2' ->
+ match compare_field f1 f2 with
+ | -1 -> lub_fields lubs glbs fs1' fs2
+ | +1 -> lub_fields lubs glbs fs1 fs2'
+ | _ -> {f1 with typ = lub' lubs glbs f1.typ f2.typ}::lub_fields lubs glbs fs1' fs2'
+
+and lub_tags lubs glbs fs1 fs2 = match fs1, fs2 with
| fs1, [] -> fs1
| [], fs2 -> fs2
| f1::fs1', f2::fs2' ->
match compare_field f1 f2 with
- | -1 -> f1 :: lub_tags fs1' fs2
- | +1 -> f2 :: lub_tags fs1 fs2'
- | _ -> {f1 with typ = lub f1.typ f2.typ} :: lub_tags fs1' fs2'
+ | -1 -> f1 :: lub_tags lubs glbs fs1' fs2
+ | +1 -> f2 :: lub_tags lubs glbs fs1 fs2'
+ | _ -> {f1 with typ = lub' lubs glbs f1.typ f2.typ} :: lub_tags lubs glbs fs1' fs2'
-let rec glb t1 t2 =
+and glb' lubs glbs t1 t2 =
if t1 == t2 then t1 else
- (* TBR: this is just a quick hack *)
- match normalize t1, normalize t2 with
- | _, Pre
- | Pre, _ -> Pre
- | _, Any -> t1
- | Any, _ -> t2
- | _, Non -> Non
- | Non, _ -> Non
- | Prim Nat, Prim Int
- | Prim Int, Prim Nat -> Prim Nat
- | Opt t1', Opt t2' -> Opt (glb t1' t2')
- | Variant t1', Variant t2' -> Variant (glb_tags t1' t2')
- | Prim Null, Opt _
- | Opt _, Prim Null -> Prim Null
- | t1', t2' when eq t1' t2' -> t1
- | _ -> Non
-
-and glb_tags fs1 fs2 = match fs1, fs2 with
+ match M.find_opt (t1, t2) !glbs with
+ | Some t -> t
+ | _ ->
+ match t1, t2 with
+ | _, Pre
+ | Pre, _ -> assert false
+ | _, Any -> t1
+ | Any, _ -> t2
+ | _, Non
+ | Non, _ -> Non
+ | Shared, _ when sub t2 Shared -> t2
+ | _, Shared when sub t1 Shared -> t1
+ | (Prim Nat as t), Prim Int
+ | Prim Int, (Prim Nat as t) -> t
+ | Opt t1', Opt t2' ->
+ Opt (glb' lubs glbs t1' t2')
+ | Variant t1', Variant t2' ->
+ Variant (glb_tags lubs glbs t1' t2')
+ | Prim Null, Opt _
+ | Opt _, Prim Null -> Prim Null
+ | Array t1', Obj _ when sub (array_obj t1') t2 -> t1 (* TODO(gabor): payload should be glb'd *)
+ | Obj _, Array t2' when sub (array_obj t2') t1 -> t2 (* TODO(gabor): payload should be glb'd *)
+ | Prim Text, Obj _ when sub text_obj t2 -> t1
+ | Obj _, Prim Text when sub text_obj t1 -> t2
+ | Tup ts1, Tup ts2 when List.(length ts1 = length ts2) ->
+ Tup (List.map2 (glb' lubs glbs) ts1 ts2)
+ | Array t1', Array t2' ->
+ Array (glb' lubs glbs t1' t2')
+ | Obj (s1, tf1), Obj (s2, tf2) when s1 = s2 ->
+ Obj (s1, glb_fields lubs glbs tf1 tf2)
+ | Func (s1, c1, bs1, args1, res1), Func (s2, c2, bs2, args2, res2)
+ when s1 = s2 && c1 = c2 && List.(length bs1 = length bs2) &&
+ List.(length args1 = length args2 && length res1 = length res2) ->
+ combine_func_parts s1 c1 bs1 args1 res1 bs2 args2 res2 lubs glbs lub' glb'
+ | Async t1', Async t2' ->
+ Async (glb' lubs glbs t1' t2')
+ | Con _, _
+ | _, Con _ ->
+ combine_con_parts t1 t2 "glb" glbs (glb' lubs glbs)
+ | _ when eq t1 t2 -> t1
+ | _ -> Non
+
+and glb_fields lubs glbs fs1 fs2 = match fs1, fs2 with
+ | fs1, [] -> fs1
+ | [], fs2 -> fs2
+ | f1::fs1', f2::fs2' ->
+ match compare_field f1 f2 with
+ | +1 -> f2::glb_fields lubs glbs fs1 fs2'
+ | -1 -> f1::glb_fields lubs glbs fs1' fs2
+ | _ -> {f1 with typ = glb' lubs glbs f1.typ f2.typ}::glb_fields lubs glbs fs1' fs2'
+
+and glb_tags lubs glbs fs1 fs2 = match fs1, fs2 with
| fs1, [] -> []
| [], fs2 -> []
| f1::fs1', f2::fs2' ->
match compare_field f1 f2 with
- | -1 -> glb_tags fs1' fs2
- | +1 -> glb_tags fs1 fs2'
- | _ -> {f1 with typ = glb f1.typ f2.typ}::glb_tags fs1' fs2'
+ | -1 -> glb_tags lubs glbs fs1' fs2
+ | +1 -> glb_tags lubs glbs fs1 fs2'
+ | _ -> {f1 with typ = glb' lubs glbs f1.typ f2.typ}::glb_tags lubs glbs fs1' fs2'
+
+and combine_func_parts s c bs1 args1 res1 bs2 args2 res2 lubs glbs contra co =
+ let open List in
+ let ts1 = open_binds bs1 in
+ let op = map (open_ ts1) in
+ let get_con = function | Con (c, []) -> c | _ -> assert false in
+ let cs = map get_con ts1 in
+ let cl = map (close cs) in
+ let combine_binds =
+ map2 (fun b1 b2 -> {b1 with bound = contra lubs glbs b1.bound b2.bound}) in
+ Func
+ (s, c, combine_binds bs1 bs2,
+ cl (map2 (contra lubs glbs) (op args1) (op args2)),
+ cl (map2 (co lubs glbs) (op res1) (op res2)))
+
+and combine_con_parts t1 t2 naming re how =
+ let s1, s2 = !str t1, !str t2 in
+ if s1 = s2 then t1 else
+ let c = Con.fresh (Printf.sprintf "@%s(%s, %s)" naming s1 s2) (Abs ([], Pre)) in
+ let t = Con (c, []) in
+ re := M.add (t2, t1) t (M.add (t1, t2) t !re);
+ let inner = how (normalize t1) (normalize t2) in
+ set_kind c (Def ([], inner));
+ (* check for short-circuiting opportunities *)
+ if eq inner t1
+ then (re := M.add (t2, t1) t1 (M.add (t1, t2) t1 !re); t1)
+ else if eq inner t2
+ then (re := M.add (t2, t1) t2 (M.add (t1, t2) t2 !re); t2)
+ else inner
+
+let lub t1 t2 = lub' (ref M.empty) (ref M.empty) t1 t2
+let glb t1 t2 = glb' (ref M.empty) (ref M.empty) t1 t2
(* Environments *)
@@ -950,6 +1056,7 @@ and string_of_kind k =
let string_of_con : con -> string = string_of_con' []
let string_of_typ : typ -> string = string_of_typ' []
+let _ = str := string_of_typ
let rec string_of_typ_expand t =
let s = string_of_typ t in
diff --git a/test/fail/ok/type-inference.tc.ok b/test/fail/ok/type-inference.tc.ok
index 26ad31a9324..6fcd921c9f0 100644
--- a/test/fail/ok/type-inference.tc.ok
+++ b/test/fail/ok/type-inference.tc.ok
@@ -1,32 +1,39 @@
-type-inference.as:10.9-10.28: warning, this if has type Any because branches have inconsistent types,
+type-inference.as:10.9-10.28: warning, this if has type Shared because branches have inconsistent types,
true produces
Bool
false produces
Nat
-type-inference.as:11.9-11.27: warning, this if has type Any because branches have inconsistent types,
+type-inference.as:11.9-11.34: warning, this if has type Any because branches have inconsistent types,
+true produces
+ Bool
+false produces
+ [var Nat]
+type-inference.as:12.9-12.27: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
Float
-type-inference.as:12.9-12.33: warning, this if has type Any because branches have inconsistent types,
+type-inference.as:13.9-13.33: warning, this if has type Any because branches have inconsistent types,
true produces
()
false produces
{}
-type-inference.as:13.9-13.53: warning, this if has type Any because branches have inconsistent types,
-true produces
- {x : Nat}
-false produces
- {x : var Nat}
-type-inference.as:17.33-17.41: warning, the switch has type Any because branches have inconsistent types,
+type-inference.as:18.33-18.41: warning, the switch has type Shared because branches have inconsistent types,
this case produces type
Bool
the previous produce type
Nat
-type-inference.as:18.43-18.56: warning, the switch has type Any because branches have inconsistent types,
+type-inference.as:19.33-19.47: warning, the switch has type Any because branches have inconsistent types,
+this case produces type
+ Bool
+the previous produce type
+ [var Nat]
+type-inference.as:20.43-20.56: warning, the switch has type Shared because branches have inconsistent types,
this case produces type
Int
the previous produce type
Text
-type-inference.as:78.13-78.16: type error, expected iterable type, but expression has type
+type-inference.as:25.9-25.18: warning, this array has type [Shared] because elements have inconsistent types
+type-inference.as:26.9-26.24: warning, this array has type [Any] because elements have inconsistent types
+type-inference.as:84.13-84.16: type error, expected iterable type, but expression has type
Non
diff --git a/test/fail/type-inference.as b/test/fail/type-inference.as
index f67c294c61e..1e34c3643be 100644
--- a/test/fail/type-inference.as
+++ b/test/fail/type-inference.as
@@ -8,6 +8,7 @@ let y = f(func x = x + 1);
// Branch warnings.
let _ = if true true else 5;
+let _ = if true true else [var 5];
let _ = if true 5 else 5.1;
let _ = if true {} else (new {});
let _ = if true (new {x = 5}) else (new {var x = 5});
@@ -15,9 +16,14 @@ let _ = if true 1 else (-1); // ok
let _ = if true true else (5 : Any); // ok
let _ = switch 0 { case 0 true; case _ 5 };
+let _ = switch 0 { case 0 true; case _ [var 5] };
let _ = switch 0 { case 0 2; case 2 (-5); case 3 "text"; case _ () };
let _ = switch 0 { case 0 true; case _ (() : Any); }; // ok
+// Array warnings.
+
+let _ = [true, 5];
+let _ = [true, [var 5]];
// Local types (not) escaping.
diff --git a/test/repl/ok/type-lub-repl.stderr.ok b/test/repl/ok/type-lub-repl.stderr.ok
new file mode 100644
index 00000000000..a32a914044d
--- /dev/null
+++ b/test/repl/ok/type-lub-repl.stderr.ok
@@ -0,0 +1,24 @@
+stdin:34.18-34.26: type error, expression of type
+ {get : Nat -> Int; keys : () -> {next : () -> ?Nat}; len : () -> Nat; vals : () -> {next : () -> ?Int}}
+cannot produce expected type
+ [Int]
+stdin:34.1-34.27: type error, expression of type
+ Nat
+cannot produce expected type
+ ()
+stdin:35.18-35.26: type error, expression of type
+ {get : Nat -> Int; keys : () -> {next : () -> ?Nat}; len : () -> Nat; vals : () -> {next : () -> ?Int}}
+cannot produce expected type
+ [Int]
+stdin:35.1-35.27: type error, expression of type
+ Nat
+cannot produce expected type
+ ()
+stdin:42.19-42.26: type error, literal of type
+ Text
+does not have expected type
+ Non
+stdin:43.19-43.44: type error, expression of type
+ [Char]
+cannot produce expected type
+ Non
diff --git a/test/repl/ok/type-lub-repl.stdout.ok b/test/repl/ok/type-lub-repl.stdout.ok
new file mode 100644
index 00000000000..a2e43e5479c
--- /dev/null
+++ b/test/repl/ok/type-lub-repl.stdout.ok
@@ -0,0 +1,43 @@
+ActorScript 0.1 interpreter
+> [null, ?42, ?-25] : [(?Int)]
+> [null, null] : [Null]
+> [{a = 42}, {b = 42}] : [{}]
+> [{a = 42}, {a = 1; b = 42}, {a = -25}] : [{a : Int}]
+> [{len = func}, [1, 2, 3]] : [{len : () -> Nat}]
+> [{len = func}, "hello"] : [{len : () -> Nat}]
+> [[1, 2, 3], "hello"] : [{len : () -> Nat}]
+> [{len = func}, [1, 2, 3], "hello"] : [{len : () -> Nat}]
+> [(12, -1), (-42, 25)] : [(Int, Int)]
+> [-1, 25] : [Int]
+> [[-42], [25]] : [[Int]]
+> [func, func] : [(Non -> Int)]
+> [func, func] : [([Nat] -> Int)]
+> 3 : Int
+> -42 : Int
+> [func, func] : [([Nat] -> Int)]
+> 3 : Int
+> -42 : Int
+> [func, func] : [([Nat] -> Int)]
+> 3 : Int
+> -42 : Int
+> [func, func] : [(([A], B) -> A)]
+> [func, func] : [(([A], B) -> A)]
+> 1 : Nat
+> 11 : Nat
+> [func, func] : [([Int] -> Nat)]
+> 13 : Nat
+> 3 : Nat
+> let combined : {get : Nat -> Int; keys : () -> {next : () -> ?Nat}; len : () -> Nat; vals : () -> {next : () -> ?Int}} = {get = func; keys = func; len = func; vals = func}
+> > 5 : Nat
+> 5 : Nat
+> [func, func] : [(Non -> Nat)]
+> > > [func, func] : [({#bar} -> ())]
+> > > [[42], [25], [77]] : [[Any]]
+> [42, 77, [1, 2, 3]] : [Shared]
+> [77, [1, 2, 3], 42] : [Shared]
+> [func, func] : [(Int -> Int)]
+> 25 : Int
+> 42 : Int
+> func : (C, D) -> [C]
+> [async ?4, async ?-42] : [(async (?Int))]
+>
diff --git a/test/repl/type-lub-repl.sh b/test/repl/type-lub-repl.sh
new file mode 100755
index 00000000000..cc4e31ca21d
--- /dev/null
+++ b/test/repl/type-lub-repl.sh
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# Tests that correct lub types are inferred when values appear in arrays
+${ASC:-$(dirname "$BASH_SOURCE")/../../src/asc} -i ../run/type-lub.as <<__END__
+opts;
+nulls;
+incompatible_objs;
+objs;
+obj_arrs;
+obj_texts;
+arr_texts;
+obj_arr_texts;
+tups;
+tup1s;
+arrs;
+incompatible_funcs;
+funcs;
+funcs[0]([1, 2, 3]);
+funcs[1]([1, 2, 3]);
+poly_funcs;
+poly_funcs[0]([1, 2, 3]);
+poly_funcs[1]([1, 2, 3]);
+poly_funcs2;
+poly_funcs2[0]([1, 2, 3]);
+poly_funcs2[1]([1, 2, 3]);
+poly_funcs3;
+poly_funcs4;
+poly_funcs4[0]([1, 2, 3], 42);
+poly_funcs4[1]([11, 22, 33], 25);
+obj_arr_funcs;
+obj_arr_funcs[0]([1, 2, 3]);
+obj_arr_funcs[1]([1, 2, 3]);
+let combined = new { len () : Nat = 42
+ ; get (i : Nat) : Int = i
+ ; keys () : {next () : ?Nat} = new { next () : ?Nat = null }
+ ; vals () : {next () : ?Int} = new { next () : ?Int = null }
+ };
+obj_arr_funcs[0](combined); // error: no object below array
+obj_arr_funcs[1](combined); // error
+
+obj_text_funcs;
+obj_text_funcs[0]("hello");
+obj_text_funcs[1]("hello");
+
+arr_text_funcs;
+arr_text_funcs[0]("hello");
+arr_text_funcs[1](['h', 'e', 'l', 'l', 'o']);
+
+variant_funcs;
+variant_funcs[0](#bar);
+variant_funcs[1](#bar);
+
+mut_arrs;
+
+shareds;
+shared2s;
+shared_funcs;
+shared_funcs[0](25);
+shared_funcs[1](25);
+
+c0;
+c1s;
+__END__
diff --git a/test/run/ok/issue442.run-ir.ok b/test/run/ok/issue442.run-ir.ok
index 136d5ad0c79..486c222891b 100644
--- a/test/run/ok/issue442.run-ir.ok
+++ b/test/run/ok/issue442.run-ir.ok
@@ -1,5 +1,5 @@
-issue442.as:1.11-1.24: warning, this array has type [Any] because elements have inconsistent types
-issue442.as:2.11-2.29: warning, this if has type Any because branches have inconsistent types,
+issue442.as:1.11-1.24: warning, this array has type [Shared] because elements have inconsistent types
+issue442.as:2.11-2.29: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
diff --git a/test/run/ok/issue442.run-low.ok b/test/run/ok/issue442.run-low.ok
index 136d5ad0c79..486c222891b 100644
--- a/test/run/ok/issue442.run-low.ok
+++ b/test/run/ok/issue442.run-low.ok
@@ -1,5 +1,5 @@
-issue442.as:1.11-1.24: warning, this array has type [Any] because elements have inconsistent types
-issue442.as:2.11-2.29: warning, this if has type Any because branches have inconsistent types,
+issue442.as:1.11-1.24: warning, this array has type [Shared] because elements have inconsistent types
+issue442.as:2.11-2.29: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
diff --git a/test/run/ok/issue442.run.ok b/test/run/ok/issue442.run.ok
index 136d5ad0c79..486c222891b 100644
--- a/test/run/ok/issue442.run.ok
+++ b/test/run/ok/issue442.run.ok
@@ -1,5 +1,5 @@
-issue442.as:1.11-1.24: warning, this array has type [Any] because elements have inconsistent types
-issue442.as:2.11-2.29: warning, this if has type Any because branches have inconsistent types,
+issue442.as:1.11-1.24: warning, this array has type [Shared] because elements have inconsistent types
+issue442.as:2.11-2.29: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
diff --git a/test/run/ok/issue442.tc.ok b/test/run/ok/issue442.tc.ok
index 136d5ad0c79..486c222891b 100644
--- a/test/run/ok/issue442.tc.ok
+++ b/test/run/ok/issue442.tc.ok
@@ -1,5 +1,5 @@
-issue442.as:1.11-1.24: warning, this array has type [Any] because elements have inconsistent types
-issue442.as:2.11-2.29: warning, this if has type Any because branches have inconsistent types,
+issue442.as:1.11-1.24: warning, this array has type [Shared] because elements have inconsistent types
+issue442.as:2.11-2.29: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
diff --git a/test/run/ok/issue442.wasm.stderr.ok b/test/run/ok/issue442.wasm.stderr.ok
index 136d5ad0c79..486c222891b 100644
--- a/test/run/ok/issue442.wasm.stderr.ok
+++ b/test/run/ok/issue442.wasm.stderr.ok
@@ -1,5 +1,5 @@
-issue442.as:1.11-1.24: warning, this array has type [Any] because elements have inconsistent types
-issue442.as:2.11-2.29: warning, this if has type Any because branches have inconsistent types,
+issue442.as:1.11-1.24: warning, this array has type [Shared] because elements have inconsistent types
+issue442.as:2.11-2.29: warning, this if has type Shared because branches have inconsistent types,
true produces
Nat
false produces
diff --git a/test/run/ok/type-lub.wasm-run.ok b/test/run/ok/type-lub.wasm-run.ok
new file mode 100644
index 00000000000..ded9968ad6a
--- /dev/null
+++ b/test/run/ok/type-lub.wasm-run.ok
@@ -0,0 +1 @@
+_out/type-lub.wasm:0x___: runtime trap: unreachable executed
diff --git a/test/run/type-lub.as b/test/run/type-lub.as
new file mode 100644
index 00000000000..783929db3d2
--- /dev/null
+++ b/test/run/type-lub.as
@@ -0,0 +1,152 @@
+let opts = [null, ?42, ?-25];
+let nulls = [null, null];
+
+let incompatible_objs = [new {a = 42}, new {b = 42}];
+let objs = [new {a = 42}, new {b = 42; a = 1}, new {a = -25}];
+let obj_arrs = [new {len() : Nat = 42}, [1, 2, 3]];
+let obj_texts = [new {len() : Nat = 42}, "hello"];
+let arr_texts = [[1, 2, 3], "hello"];
+let obj_arr_texts = [new {len() : Nat = 42}, [1, 2, 3], "hello"];
+
+let tups = [(12, -1), (-42, 25)];
+let tup1s = [(-1,), 25];
+
+let arrs = [[-42], [25]];
+
+let incompatible_funcs = [ func (a : [Int]) : Nat = a.len()
+ , func (a : ()) : Int = -42
+ ];
+
+let poly_funcs = [ func (a : [Int]) : Nat = a.len()
+ , func (a : [Nat]) : Int = -42
+ ];
+
+let poly_funcs2 = [ func (a : [Int]) : Nat = a.len()
+ , func (a : [Nat]) : Int = -42
+ ];
+
+let poly_funcs3 = [ func (as : [A], b : B) : A = as[0]
+ , func (bs : [B], a : A) : B = bs[0]
+ ];
+
+let poly_funcs4 = [ func (as : [A], b : B) : A = as[0]
+ , func (bs : [B], a : A) : B = bs[0]
+ ];
+
+let funcs = [ func (a : [Int]) : Nat = a.len()
+ , func (a : [Nat]) : Int = -42
+ ];
+
+let obj_arr_funcs = [ func (a : [Int]) : Nat { printInt (a[0]); a.len() }
+ , func (a : {len : () -> Nat}) : Nat = a.len()
+ ];
+
+let obj_text_funcs = [ func (a : Text) : Nat = a.len()
+ , func (a : {len : () -> Nat}) : Nat = a.len()
+ ];
+
+let arr_text_funcs = [ func (a : Text) : Nat = a.len()
+ , func (a : [Char]) : Nat { printChar (a[0]); a.len() }
+ ];
+
+let variant_funcs = [ func (a : {#foo; #bar}) { switch a { case (#foo) (); case (#bar) () } }
+ , func (a : {#baz; #bar}) { switch a { case (#baz) (); case (#bar) () } }
+ ];
+
+// TODO(gabor), mutable arrays
+let mut_arrs = [[var 42], [var 25], [77]]; // boring
+
+// TODO(gabor), mutable fields, see fail/type-inference.as:13
+
+let sh : Shared = 42;
+let shareds = [sh, 77, [1, 2, 3]];
+let shared2s = [77, [1, 2, 3], sh];
+
+let shared_funcs = [ func (a : Int) : Int = a
+ , func (a : Shared) : Nat = 42
+ ];
+
+type C = async(?Int);
+type D = async(?Nat);
+
+func c0(c : C, d : D) : [C] { ignore([c, d]); [c, d] };
+let c1s = [async ?4, async ?-42];
+
+
+// recursive objects
+
+// { need global types due to https://dfinity.atlassian.net/browse/AST-34
+type A = {x : A};
+type B = {x : B};
+
+func f(v : {x : {x : B}; b : B}, x : A, y : B, z : {x : B; a : A}) : [A] { ignore([v, x, y, z]); [v, x, y, z] };
+// };
+
+// {
+type A1 = {x : B1};
+type B1 = {x : A1};
+
+func f1(x : A1, y : B1) : [A1] { ignore([x, y]); [x, y] };
+// };
+
+type O = ?O;
+type P = ?P;
+
+type Q = ?R;
+type R = ?S;
+type S = ?Q;
+
+func g(o : O, p : P, q : Q, r : R) : [O] { ignore([o, p, q, r]); [o, p, q, r] };
+
+// example from https://dfinity.atlassian.net/browse/AST-83
+
+type Foo = ?(Foo);
+ignore (if true (null : Foo) else (null : Foo));
+
+
+type U = { #a : U; #b : Int };
+type V = { #a : V; #b : Nat };
+
+func v0(u : U, v : V, w : { #a : { #a : V; #b : Nat }; #b : Nat }) : [U] { ignore([u, v, w]); [u, v, w] };
+
+
+type G = (Nat, ?G);
+type H = (Int, ?H);
+
+func g0(g : G, h : H) : [H] { ignore([g, h]); [g, h] };
+
+
+type K = [K];
+type L = [L];
+
+func k0(k : K, l : L) : [L] { ignore([k, l]); [k, l] };
+
+
+type K1 = [?(Nat, K1)];
+type L1 = [?(Int, L1)];
+
+func k1(k : K1, l : L1) : [L1] { ignore([k, l]); [k, l] };
+
+
+/*
+type M = [var ?M];
+type N = [?N];
+
+func m0(m : M, n : N) : [M] { ignore([m, n]); [m, n] };
+*/
+
+type E = Int -> E;
+type F = Nat -> F;
+
+func f0(e : E, f : F) : [F] { ignore([e, f]); [e, f] };
+
+type E1 = E1 -> E1;
+type F1 = F1 -> F1;
+
+func f12(e : E1, f : F1) : [F1] { ignore([e, f]); [e, f] };
+
+type E2 = F2 -> E2;
+type F2 = E2 -> F2;
+
+func f2(e : E2, f : F2) : [F2] { ignore([e, f]); [e, f] };
+