Extend lub/glb to more types

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 *)
 

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
     )

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

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

test/fail/type-inference.as

@@ -8,16 +8,22 @@ 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});
 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.
 

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