Improved Inference for Checking Annotations

TL;DR

This paper introduces a new type inference scheme for checking annotations in Haskell-like systems, improving completeness over existing algorithms and fully supporting Haskell 98, with implementation in the Chameleon system.

Contribution

It presents a novel inference method that enhances annotation checking, addressing incompleteness in nested annotations and improving over GHC's current implementation.

Findings

The new inference scheme is more complete than existing methods.

It achieves full completeness for Haskell 98.

Implementation in the Chameleon system demonstrates practical viability.

Abstract

We consider type inference in the Hindley/Milner system extended with type annotations and constraints with a particular focus on Haskell-style type classes. We observe that standard inference algorithms are incomplete in the presence of nested type annotations. To improve the situation we introduce a novel inference scheme for checking type annotations. Our inference scheme is also incomplete in general but improves over existing implementations as found e.g. in the Glasgow Haskell Compiler (GHC). For certain cases (e.g. Haskell 98) our inference scheme is complete. Our approach has been fully implemented as part of the Chameleon system (experimental version of Haskell).