Correctly add subtype constraints to type vars

Author: ysthakur

src/snapshots/new_nu_parser__test__lexer.snap

@@ -43,8 +43,8 @@ input_file: tests/binary_ops_mismatch.nu
 16: bool
 ==== TYPE ERRORS ====
 Error (NodeId 2): Expected string, got float
-Error (NodeId 4): Expected list<top>, got string
-Error (NodeId 6): Expected list<top>, got float
+Error (NodeId 4): Expected list<bottom> <: '0 <: list<top>, got string
+Error (NodeId 6): Expected list<bottom> <: '0 <: list<top>, got float
 Error (NodeId 5): type mismatch: unsupported append between string and float
 Error (NodeId 10): Expected bool, got string
 Error (NodeId 12): Expected string, got bool

src/snapshots/new_nu_parser__test__node_output@binary_ops_mismatch.nu.snap

@@ -1,7 +1,7 @@
 ---
 source: src/test.rs
 expression: evaluate_example(path)
-input_file: tests/def_complex.nu
+input_file: tests/infer_complex.nu
 ---
 ==== COMPILER ====
 0: Name (4 to 5) "f"
@@ -196,7 +196,7 @@ input_file: tests/def_complex.nu
 86: unknown
 87: string
 88: record<a: float, b: string>
-89: record<a: number, b: top>
+89: record<a: number, b: string>
 90: ()
 91: ()
 ==== IR ====

…r__test__node_output@def_complex.nu.snap …_test__node_output@infer_complex.nu.snapsrc/snapshots/new_nu_parser__test__node_output@def_complex.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_complex.nu.snap src/snapshots/new_nu_parser__test__node_output@def_complex.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_complex.nu.snap

@@ -1,7 +1,7 @@
 ---
 source: src/test.rs
 expression: evaluate_example(path)
-input_file: tests/def_generics.nu
+input_file: tests/infer_generics.nu
 ---
 ==== COMPILER ====
 0: Name (4 to 5) "f"
@@ -30,28 +30,12 @@ input_file: tests/def_generics.nu
 23: List([NodeId(22)]) (59 to 62)
 24: Block(BlockId(0)) (39 to 65)
 25: Def { name: NodeId(0), type_params: Some(NodeId(2)), params: NodeId(7), in_out_types: Some(NodeId(16)), block: NodeId(24) } (0 to 65)
-26: Variable (71 to 73) "l1"
-27: Name (76 to 77) "f"
-28: Int (78 to 79) "1"
-29: Call { parts: [NodeId(27), NodeId(28)] } (78 to 79)
-30: Let { variable_name: NodeId(26), ty: None, initializer: NodeId(29), is_mutable: false } (67 to 79)
-31: Variable (85 to 87) "l2"
-32: Name (90 to 91) "f"
-33: Int (92 to 93) "2"
-34: Call { parts: [NodeId(32), NodeId(33)] } (92 to 93)
-35: Let { variable_name: NodeId(31), ty: None, initializer: NodeId(34), is_mutable: false } (81 to 93)
-36: Variable (98 to 100) "l3"
-37: Name (102 to 106) "list"
-38: Name (107 to 113) "number"
-39: Type { name: NodeId(38), args: None, optional: false } (107 to 113)
-40: TypeArgs([NodeId(39)]) (106 to 114)
-41: Type { name: NodeId(37), args: Some(NodeId(40)), optional: false } (102 to 106)
-42: Variable (117 to 120) "$l2"
-43: Let { variable_name: NodeId(36), ty: Some(NodeId(41)), initializer: NodeId(42), is_mutable: false } (94 to 120)
-44: Block(BlockId(1)) (0 to 121)
+26: Name (67 to 68) "f"
+27: Int (69 to 70) "1"
+28: Call { parts: [NodeId(26), NodeId(27)] } (69 to 70)
+29: Block(BlockId(1)) (0 to 71)
 ==== SCOPE ====
-0: Frame Scope, node_id: NodeId(44)
-  variables: [ l1: NodeId(26), l2: NodeId(31), l3: NodeId(36) ]
+0: Frame Scope, node_id: NodeId(29)
       decls: [ f: NodeId(0) ]
 1: Frame Scope, node_id: NodeId(24)
   variables: [ x: NodeId(3), z: NodeId(17) ]
@@ -83,25 +67,10 @@ input_file: tests/def_generics.nu
 23: list<T>
 24: list<T>
 25: ()
-26: list<top>
-27: unknown
-28: int
-29: list<top>
-30: ()
-31: list<number>
-32: unknown
-33: int
-34: list<number>
-35: ()
-36: list<number>
-37: unknown
-38: unknown
-39: number
-40: forbidden
-41: list<number>
-42: list<number>
-43: ()
-44: ()
+26: unknown
+27: int
+28: list<int>
+29: list<int>
 ==== IR ====
 register_count: 0
 file_count: 0

…__test__node_output@def_generics.nu.snap …test__node_output@infer_generics.nu.snapsrc/snapshots/new_nu_parser__test__node_output@def_generics.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_generics.nu.snap src/snapshots/new_nu_parser__test__node_output@def_generics.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_generics.nu.snap

@@ -1,7 +1,7 @@
 ---
 source: src/test.rs
 expression: evaluate_example(path)
-input_file: tests/def_plus.nu
+input_file: tests/infer_plus.nu
 ---
 ==== COMPILER ====
 0: Name (4 to 14) "mysterious"
@@ -21,23 +21,21 @@ input_file: tests/def_plus.nu
 14: Block(BlockId(0)) (44 to 46)
 15: Def { name: NodeId(0), type_params: Some(NodeId(2)), params: NodeId(7), in_out_types: Some(NodeId(13)), block: NodeId(14) } (0 to 46)
 16: Variable (52 to 53) "m"
-17: Name (55 to 58) "any"
-18: Type { name: NodeId(17), args: None, optional: false } (55 to 58)
-19: Name (61 to 71) "mysterious"
-20: Int (72 to 73) "0"
-21: Call { parts: [NodeId(19), NodeId(20)] } (72 to 73)
-22: Let { variable_name: NodeId(16), ty: Some(NodeId(18)), initializer: NodeId(21), is_mutable: false } (48 to 73)
-23: Variable (75 to 77) "$m"
-24: Plus (78 to 79)
-25: String (80 to 85) ""foo""
-26: BinaryOp { lhs: NodeId(23), op: NodeId(24), rhs: NodeId(25) } (75 to 85)
-27: Variable (86 to 88) "$m"
-28: Plus (89 to 90)
-29: Int (91 to 94) "123"
-30: BinaryOp { lhs: NodeId(27), op: NodeId(28), rhs: NodeId(29) } (86 to 94)
-31: Block(BlockId(1)) (0 to 95)
+17: Name (56 to 66) "mysterious"
+18: Int (67 to 68) "0"
+19: Call { parts: [NodeId(17), NodeId(18)] } (67 to 68)
+20: Let { variable_name: NodeId(16), ty: None, initializer: NodeId(19), is_mutable: false } (48 to 68)
+21: Variable (70 to 72) "$m"
+22: Plus (73 to 74)
+23: String (75 to 80) ""foo""
+24: BinaryOp { lhs: NodeId(21), op: NodeId(22), rhs: NodeId(23) } (70 to 80)
+25: Variable (81 to 83) "$m"
+26: Plus (84 to 85)
+27: Int (86 to 89) "123"
+28: BinaryOp { lhs: NodeId(25), op: NodeId(26), rhs: NodeId(27) } (81 to 89)
+29: Block(BlockId(1)) (0 to 90)
 ==== SCOPE ====
-0: Frame Scope, node_id: NodeId(31)
+0: Frame Scope, node_id: NodeId(29)
   variables: [ m: NodeId(16) ]
       decls: [ mysterious: NodeId(0) ]
 1: Frame Scope, node_id: NodeId(14)
@@ -60,22 +58,22 @@ input_file: tests/def_plus.nu
 13: unknown
 14: ()
 15: ()
-16: any
+16: bottom
 17: unknown
-18: any
-19: unknown
-20: int
-21: top
-22: ()
-23: any
-24: forbidden
-25: string
-26: string
-27: any
-28: forbidden
-29: int
-30: number
-31: number
+18: int
+19: bottom
+20: ()
+21: bottom
+22: forbidden
+23: string
+24: string
+25: bottom
+26: forbidden
+27: int
+28: string
+29: string
+==== TYPE ERRORS ====
+Error (NodeId 27): Expected string, got int
 ==== IR ====
 register_count: 0
 file_count: 0

…rser__test__node_output@def_plus.nu.snap …er__test__node_output@infer_plus.nu.snapsrc/snapshots/new_nu_parser__test__node_output@def_plus.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_plus.nu.snap src/snapshots/new_nu_parser__test__node_output@def_plus.nu.snap renamed to src/snapshots/new_nu_parser__test__node_output@infer_plus.nu.snap

@@ -92,6 +92,8 @@ input_file: tests/let_mismatch.nu
 40: ()
 ==== TYPE ERRORS ====
 Error (NodeId 13): Expected string, got int
+Error (NodeId 24): Expected int, got string
+Error (NodeId 25): Expected list<int>, got list<string>
 Error (NodeId 26): Expected list<list<int>>, got list<list<string>>
 Error (NodeId 38): Expected record<a: int>, got record<a: string>
 ==== IR ====

src/snapshots/new_nu_parser__test__node_output@let_mismatch.nu.snap

@@ -215,10 +215,17 @@ impl<'a> Typechecker<'a> {
             let last_node_id = NodeId(last);
             self.typecheck_node(last_node_id);
 
+            for i in 0..self.type_vars.len() {
+                let var = &self.type_vars[i];
+                let bound = var.lower_bound;
+                let cleaned = self.eliminate_type_vars(bound, TypeVarId(0), true);
+                self.types[bound.0] = self.types[cleaned.0];
+            }
+
             for i in 0..self.types.len() {
-                let res = self.eliminate_type_vars(TypeId(i), TypeVarId(0), false);
-                if res.0 != i {
-                    self.types[i] = self.types[res.0];
+                if let Type::Var(var_id) = &self.types[i] {
+                    let bound = self.type_vars[var_id.0].lower_bound;
+                    self.types[i] = self.types[bound.0];
                 }
             }
         }
@@ -389,9 +396,10 @@ impl<'a> Typechecker<'a> {
             AstNode::True | AstNode::False => BOOL_TYPE,
             AstNode::String => STRING_TYPE,
             AstNode::List(ref items) => {
-                // TODO inspect the expected type and infer a union type instead
+                // TODO infer a union type instead
                 if let Some(first_id) = items.first() {
-                    self.typecheck_expr(*first_id, TOP_TYPE);
+                    let expected_elem = self.extract_elem_type(expected);
+                    self.typecheck_expr(*first_id, expected_elem.unwrap_or(TOP_TYPE));
                     let first_type = self.type_of(*first_id);
 
                     let mut all_numbers = self.is_type_compatible(first_type, Type::Number);
@@ -709,25 +717,22 @@ impl<'a> Typechecker<'a> {
                 }
             }
             AstNode::Append => {
-                // TODO cache this type
-                let list_ty = self.push_type(Type::List(TOP_TYPE));
-                let lhs_type = self.typecheck_expr(lhs, list_ty);
-                let rhs_type = self.typecheck_expr(rhs, list_ty);
-
-                //todo account for any
-                match (self.types[lhs_type.0], self.types[rhs_type.0]) {
-                    (Type::List(lhs_item), Type::List(rhs_item)) => {
-                        let mut types = HashSet::new();
-                        types.insert(lhs_item);
-                        types.insert(rhs_item);
-                        let common_type = self.create_oneof(types);
-                        self.push_type(Type::List(common_type))
-                    }
-                    (_, Type::Any | Type::Bottom) | (Type::Any | Type::Bottom, _) => ANY_TYPE,
-                    _ => {
-                        self.binary_op_err("append", lhs, op, rhs);
-                        ERROR_TYPE
-                    }
+                // TODO cache these two types
+                let top_list = self.push_type(Type::List(TOP_TYPE));
+                let bottom_list = self.push_type(Type::List(BOTTOM_TYPE));
+
+                let res_var = self.new_typevar(bottom_list, top_list);
+                let res_type = self.push_type(Type::Var(res_var));
+                let lhs_type = self.typecheck_expr(lhs, res_type);
+                let rhs_type = self.typecheck_expr(rhs, res_type);
+
+                if self.is_subtype(lhs_type, LIST_ANY_TYPE)
+                    && self.is_subtype(rhs_type, LIST_ANY_TYPE)
+                {
+                    res_type
+                } else {
+                    self.binary_op_err("append", lhs, op, rhs);
+                    ERROR_TYPE
                 }
             }
             AstNode::Assignment
@@ -1162,6 +1167,18 @@ impl<'a> Typechecker<'a> {
         }
     }
 
+    /// Given the type for a list, extract the type of its elements
+    fn extract_elem_type(&mut self, list_ty: TypeId) -> Option<TypeId> {
+        match self.types[list_ty.0] {
+            Type::List(elem) => Some(elem),
+            Type::Top => Some(TOP_TYPE),
+            Type::Bottom => Some(BOTTOM_TYPE),
+            Type::Any => Some(ANY_TYPE),
+            Type::Unknown => Some(UNKNOWN_TYPE),
+            _ => None,
+        }
+    }
+
     fn set_node_type_id(&mut self, node_id: NodeId, type_id: TypeId) {
         self.node_types[node_id.0] = type_id;
     }
@@ -1223,7 +1240,10 @@ impl<'a> Typechecker<'a> {
             (Type::Var(var_id), _) => {
                 let lb = self.type_vars[var_id.0].lower_bound;
                 let ub = self.type_vars[var_id.0].upper_bound;
-                let new_ub = self.create_intersection(ub, supe_id);
+                let mut types = HashSet::new();
+                types.insert(ub);
+                types.insert(supe_id);
+                let new_ub = self.create_allof(types);
                 // Prevent forward references/cycles
                 let new_ub = self.eliminate_type_vars(new_ub, var_id, true);
 
@@ -1241,7 +1261,10 @@ impl<'a> Typechecker<'a> {
             (_, Type::Var(var_id)) => {
                 let lb = self.type_vars[var_id.0].lower_bound;
                 let ub = self.type_vars[var_id.0].upper_bound;
-                let new_lb = self.create_intersection(lb, sub_id);
+                let mut types = HashSet::new();
+                types.insert(lb);
+                types.insert(sub_id);
+                let new_lb = self.create_oneof(types);
                 // Prevent forward references/cycles
                 let new_lb = self.eliminate_type_vars(new_lb, var_id, false);
 
@@ -1598,6 +1621,8 @@ impl<'a> Typechecker<'a> {
         let mut flattened = HashSet::new();
         for ty_id in types {
             match self.types[ty_id.0] {
+                Type::Top | Type::Any | Type::Unknown => return ty_id,
+                Type::Bottom => {}
                 Type::OneOf(id) => {
                     flattened.extend(&self.oneof_types[id.0]);
                 }
@@ -1846,11 +1871,4 @@ impl<'a> Typechecker<'a> {
 
         self.create_oneof(inters)
     }
-
-    fn create_intersection(&mut self, lhs_id: TypeId, rhs_id: TypeId) -> TypeId {
-        let mut types = HashSet::new();
-        types.insert(lhs_id);
-        types.insert(rhs_id);
-        self.create_allof(types)
-    }
 }

src/typechecker.rs

@@ -3,7 +3,4 @@ def f<T> [ x: T ] : nothing -> list<T> {
   [$z]
 }
 
-let l1 = f 1
-
-let l2 = f 2
-let l3: list<number> = $l2
+f 1

tests/def_complex.nu tests/infer_complex.nutests/def_complex.nu renamed to tests/infer_complex.nu

@@ -1,6 +1,6 @@
 def mysterious<T> [ x: int ] : nothing -> T {}
 
-let m: any = mysterious 0
+let m = mysterious 0
 
 $m + "foo"
 $m + 123