| Copyright | (c) 1999 - 2004 Wolfgang Lux Martin Engelke 2011 - 2015 Björn Peemöller 2014 - 2015 Jan Tikovsky 2016 - 2017 Finn Teegen |
|---|---|
| License | BSD-3-clause |
| Maintainer | bjp@informatik.uni-kiel.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Checks.TypeCheck
Description
This module implements the type checker of the Curry compiler. The type checker is invoked after the syntactic correctness of the program has been verified and kind checking has been applied to all type expressions. Local variables have been renamed already. Thus the compiler can maintain a flat type environment. The type checker now checks the correct typing of all expressions and also verifies that the type signatures given by the user match the inferred types. The type checker uses the algorithm by Damas and Milner (1982) for inferring the types of unannotated declarations, but allows for polymorphic recursion when a type annotation is present.
The result of type checking is a (flat) top-level environment containing the types of all constructors, variables, and functions defined at the top level of a module. In addition, a type annotated source module is returned. Note that type annotations on the left hand side of a declaration hold the function or variable's generalized type with the type scheme's universal quantifier left implicit. Type annotations on the right hand side of a declaration hold the particular instance at which a polymorphic function or variable is used.