A new bottom-up type-checker needed

[ameeratgithub]

We've seen many problems in type-checker and many of them are scattered across different issues. If possible, it would be great if we can write those snippets at one place.

For those who aren't familiar with the details, I'm just going to explain one problem for now. Consider the following snippet

(list none none)

It returns OptionalType(NoType) and it does make sense, because it has no context. Now consider the following snippet

(define-private (foo (el (optional int))) (is-eq el none)) (filter foo (list none none))

List shouldn't have type OptionalType(NoType) in this context because we're using this list with foo which accepts OptionalType(Int). (list none none) is compatible with OptionalType(Int) so we should update OptionalType(NoType) to OptionalType(Int).

There are many issues like this and having a bottom-up type checker can solve this problem effectively. With the bottom-up type checker, issues would be easier to solve because

• The type checker would first determine the type of individual elements (in this case none)
• Then it would infer the type of the list based on its elements.
• Finally, it would reconcile the inferred types with the expected types as the type information propagates upwards (it will consider foo to determine the type of (list none none)).

How long should it take? I had 1-1.5 weeks in my mind but may be I'm wrong here. Please feel free to correct me if I'm wrong or missing something.

[ameeratgithub]

One approach is to have type checker that generates WASM types and is only compatible with the compiler. Another approach is to have similar structure of type checker to that of the interpreter but corrected. These types will be converted to WASM types as we're doing right now. The latter approach looks easier to implement and seems like it will take a lot less time than the former.

[ameeratgithub]

@obycode it would be great if you could give us your valuable input, particularly how much time it should take.

[obycode]

We cannot use Wasm types for the type-checker, as we lose a lot of information when converting Clarity types to Wasm types. I think the main problem with the current implementation is that there is not a pass to propagate the type inferencing through to all expressions. I think it would be reasonable to have an initial implementation of this done in a week, but then I would allow 4 weeks for completion. Thankfully, we already have lots of testing in place to validate these changes.

When implementing this type-checker, we should have two goals:

1. Ensure all expressions are properly typed
   • Remove the need for all of the workarounds that are currently in place in clarity-wasm
   • Resolve the open issues in stacks-core where the type-checker is currently known to fail
2. Provide better error messages (esp. in developer mode)
   • This includes clear errors and ensuring that the proper location information is used when reporting the error

[ameeratgithub]

Thanks for your suggestions @obycode . I'll keep these in mind and will let you know if I need any help.