Cannot infer an array type

[mtshiba]

Reproducible code:

a = [1, 2]

Error log:

compiler\erg_compiler\compile.rs:164: [DEBUG] the compiling process has started.
compiler\erg_parser\parse.rs:327: [DEBUG] the parsing process has started.
compiler\erg_parser\parse.rs:328: token stream: [Symbol a, Equal =, LSqBr [, NatLit 1, Comma ,, NatLit 2, RSqBr ], EOF ]
compiler\erg_parser\parse.rs:360: [DEBUG] entered try_reduce_module, cur: Symbol a
compiler\erg_parser\parse.rs:1248: [DEBUG] entered try_reduce_expr, cur: Symbol a
compiler\erg_parser\parse.rs:467: [DEBUG] entered try_reduce_decl, cur: Symbol a
compiler\erg_parser\parse.rs:1478: [DEBUG] entered try_reduce_name, cur: Symbol a
compiler\erg_parser\parse.rs:678: [DEBUG] entered opt_reduce_params, cur: Equal =
compiler\erg_parser\parse.rs:388: [DEBUG] entered try_reduce_block, cur: LSqBr [
compiler\erg_parser\parse.rs:1248: [DEBUG] entered try_reduce_expr, cur: LSqBr [
compiler\erg_parser\parse.rs:1391: [DEBUG] entered try_reduce_lhs, cur: LSqBr [
compiler\erg_parser\parse.rs:1465: [DEBUG] entered try_reduce_array, cur: LSqBr [
compiler\erg_parser\parse.rs:1091: [DEBUG] entered try_reduce_args, cur: NatLit 1
compiler\erg_parser\parse.rs:1189: [DEBUG] entered try_reduce_arg, cur: NatLit 1
compiler\erg_parser\parse.rs:1248: [DEBUG] entered try_reduce_expr, cur: NatLit 1
compiler\erg_parser\parse.rs:1391: [DEBUG] entered try_reduce_lhs, cur: NatLit 1
compiler\erg_parser\parse.rs:1487: [DEBUG] entered try_reduce_lit, cur: NatLit 1
compiler\erg_parser\parse.rs:1189: [DEBUG] entered try_reduce_arg, cur: NatLit 2
compiler\erg_parser\parse.rs:1248: [DEBUG] entered try_reduce_expr, cur: NatLit 2
compiler\erg_parser\parse.rs:1391: [DEBUG] entered try_reduce_lhs, cur: NatLit 2
compiler\erg_parser\parse.rs:1487: [DEBUG] entered try_reduce_lit, cur: NatLit 2
compiler\erg_parser\parse.rs:342: [DEBUG] the parsing process has completed.
compiler\erg_parser\parse.rs:343: AST:
a =
    [NatLit 1
NatLit 2]
compiler\erg_parser\parse.rs:344: [DEBUG] the desugaring process has started.
compiler\erg_parser\parse.rs:347: AST (desugared):
a =
    [NatLit 1
NatLit 2]
compiler\erg_parser\parse.rs:348: [DEBUG] the desugaring process has completed.
compiler\erg_compiler\lower.rs:381: [DEBUG] the type-checking process has started.
compiler\erg_compiler\lower.rs:356: [DEBUG] entered lower_expr
compiler\erg_compiler\lower.rs:249: [DEBUG] entered lower_def(a)
compiler\erg_compiler\context.rs:3942: grow: current namespace: <module>::a
compiler\erg_compiler\lower.rs:267: [DEBUG] entered lower_var_def(a)
compiler\erg_compiler\lower.rs:371: [DEBUG] entered lower_block
compiler\erg_compiler\lower.rs:356: [DEBUG] entered lower_expr
compiler\erg_compiler\lower.rs:88: [DEBUG] entered lower_array([NatLit 1
NatLit 2])
compiler\erg_compiler\lower.rs:356: [DEBUG] entered lower_expr
compiler\erg_compiler\lower.rs:356: [DEBUG] entered lower_expr
compiler\erg_compiler\context.rs:3961: pop: current namespace: <module>
compiler\erg_compiler\lower.rs:398: HIR (not derefed):
a (: Array(?1(: Type)[1], 0)) =
    [NatLit 1
NatLit 2]
compiler\erg_compiler\context.rs:1804: ### Array(?1(: Type)[1], 0)
compiler\erg_compiler\context.rs:1627: Type(FreeVar(Free(RcCell(RefCell { value: Unbound { id: 1, lev: 1, constraint: TypeOf(Type) } }))))
Error[#1695]: File <stdin>
?│ a = [1, 2]

CompilerSystemError: this is a bug of Erg, please report it to https://github.com/...
caused from: deref_tyvar:1695

[mtshiba]

I have tightened the type check and this is no longer passing. It seems that the type in the array is not being inferred.

[KtlTheBest]

@mtshiba Good time of the day. Seems interesting. What type system are you trying to reproduce, Hindley-Milner of ML or is it something custom? Also, is the code for typechecker in AST lowerer? I am not a Rust-person, but if you need an extra pair of eyes :eyes: ...

[mtshiba]

Erg clearly goes beyond HM type inference since it has subtyping, refinement types, and dependent types as language features.

The type checker is implemented as an ASTLowerer(and Context), which converts an untyped AST into a typed HIR.

[mtshiba]

And now that this issue has been resolved, I will close it.

If you have any questions, feel free to ask on the discord channel.