.

* Mark only included files as potentially unused

* Update CHANGELOG

* Add test

.circleci/config.yml

@@ -3,7 +3,7 @@ version: 2.1
 executors:
   aebuilder:
     docker:
-      - image: aeternity/builder:xenial-otp21
+      - image: aeternity/builder:bionic-otp24
         user: builder
     working_directory: ~/aesophia
 

.github/workflows/docs-develop.yml

@@ -13,10 +13,6 @@ jobs:
       - uses: actions/setup-python@v2
         with:
           python-version: 3.8
-      - uses: actions/cache@v2
-        with:
-          path: ~/.cache/pip3
-          key: ${{ runner.os }}-pip-${{ hashFiles('.github/workflows/requirements.txt') }}
       - run: pip3 install -r .github/workflows/requirements.txt -U
       - run: git config --global user.email "github-action@users.noreply.github.com"
       - run: git config --global user.name "GitHub Action"

.github/workflows/docs-release.yml

@@ -13,10 +13,6 @@ jobs:
       - uses: actions/setup-python@v2
         with:
           python-version: 3.8
-      - uses: actions/cache@v2
-        with:
-          path: ~/.cache/pip3
-          key: ${{ runner.os }}-pip-${{ hashFiles('.github/workflows/requirements.txt') }}
       - run: pip3 install -r .github/workflows/requirements.txt -U
       - run: git config --global user.email "github-action@users.noreply.github.com"
       - run: git config --global user.name "GitHub Action"

.github/workflows/requirements.txt

@@ -1,5 +1,5 @@
-mkdocs==1.2.4
-mkdocs-simple-hooks==0.1.3
-mkdocs-material==7.1.9
-mike==1.0.1
-pygments==2.11.2
+mkdocs==1.4.2
+mkdocs-simple-hooks==0.1.5
+mkdocs-material==9.0.9
+mike==1.1.2
+pygments==2.14.0

CHANGELOG.md

@@ -1,12 +1,53 @@
 # Changelog
-All notable changes to this project will be documented in this file.
+All notable changes to this project shall be documented in this file.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
-and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
+and this project adheres to [Semantic
+Versioning](https://semver.org/spec/v2.0.0.html). One deviation from _Keep a
+Changelog_ is that "Unreleased" may suggest a specific version bump in case of
+breaking changes.
 
-## [Unreleased]
+## [Unreleased] [8.x.x]
 ### Added
-- Compiler warnings for the follwing: shadowing, negative spends, division by zero, unused functions, unused includes, unused stateful annotations, unused variables, unused parameters, unused user-defined type, dead return value.
+### Changed
+- `pp_assembler` option to `pp_fate` as it is more specific.
+### Removed
+- `pp_sophia_code` option as it was a duplicate of `pp_ast`.
+- `aeso_ast` module as it was unused.
+### Fixed
+- Warning about unused include when there is no include.
+
+## [7.1.0]
+### Added
+- Options to enable/disable certain optimizations.
+- The ability to call a different instance of the current contract
+  ```
+  contract Main =
+    entrypoint spend(x : int) : int = x
+    entrypoint f(c : Main) : int = c.spend(10)
+  ```
+- Return a mapping from variables to FATE registers in the compilation output.
+- Hole expression.
+### Changed
+- Type definitions serialised to ACI as `typedefs` field instead of `type_defs` to increase compatibility.
+- Check contracts and entrypoints modifiers when implementing interfaces.
+- Contracts can no longer be used as namespaces.
+- Do not show unused stateful warning for functions that call other contracts with a non-zero value argument.
+### Fixed
+- Typechecker crashes if Chain.create or Chain.clone are used without arguments.
+
+## [7.0.1]
+### Added
+- Add CONTRIBUTING.md file.
+### Changed
+- Update Sophia syntax docs to include missing information about existing syntax.
+### Fixed
+- [404](https://github.com/aeternity/aesophia/issues/404) Contract polymorphism crashes on non-obvious child contract typing.
+
+## [7.0.0]
+### Added
+- Added support for `EXIT` opcode via `exit : (string) => 'a` function (behaves same as `ABORT`, but consumes all gas).
+- Compiler warnings for the following: shadowing, negative spends, division by zero, unused functions, unused includes, unused stateful annotations, unused variables, unused parameters, unused user-defined type, dead return value.
 - The pipe operator |>
   ```
   [1, 2, 3] |> List.first |> Option.is_some  // Option.is_some(List.first([1, 2, 3]))
@@ -16,14 +57,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   function sum(l : list(int)) : int = foldl((+), 0, l)
   function logical_and(x, y) = (&&)(x, y)
   ```
-- Add comparable typevar constraints (`ord` and `eq`)
-  ```
-  lt : 'a is ord ; ('a, 'a) => bool
-  lt(x, y) = x < y
-
-  is_eq : 'a is eq ; ('a, 'a) => bool
-  is_eq(x, y) = x == y
-  ```
+- Contract interfaces polymorphism
 ### Changed
 - Error messages have been restructured (less newlines) to provide more unified errors. Also `pp_oneline/1` has been added.
 - Ban empty record definitions (e.g. `record r = {}` would give an error).
@@ -353,7 +387,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Simplify calldata creation - instead of passing a compiled contract, simply
   pass a (stubbed) contract string.
 
-[Unreleased]: https://github.com/aeternity/aesophia/compare/v6.1.0...HEAD
+[Unreleased]: https://github.com/aeternity/aesophia/compare/v7.1.0...HEAD
+[7.1.0]: https://github.com/aeternity/aesophia/compare/v7.0.1...v7.1.0
+[7.0.1]: https://github.com/aeternity/aesophia/compare/v7.0.0...v7.0.1
+[7.0.0]: https://github.com/aeternity/aesophia/compare/v6.1.0...v7.0.0
 [6.1.0]: https://github.com/aeternity/aesophia/compare/v6.0.2...v6.1.0
 [6.0.2]: https://github.com/aeternity/aesophia/compare/v6.0.1...v6.0.2
 [6.0.1]: https://github.com/aeternity/aesophia/compare/v6.0.0...v6.0.1

CONTRIBUTING.md

@@ -0,0 +1,40 @@
+# Contributing to Sophia
+
+## Checklist For Creating New Pull Requests
+
+The following points should be considered before creating a new PR to the Sophia compiler.
+
+### Documentation
+
+- The [Changelog](CHANGELOG.md) file should be updated for all PRs.
+- If a PR introduces a new feature that is relevant to the users of the language, the [Sophia Features Documentation](docs/sophia_features.md) should be updated to describe the new feature.
+- If a PR introduces new syntax (e.g. changes in [aeso_syntax.erl](src/aeso_syntax.erl), [aeso_scan.erl](src/aeso_scan.erl), or [aeso_parser.erl](src/aeso_parser.erl)), the [Sophia Syntax Documentation](docs/sophia_syntax.md) should be updated to include the new syntax.
+- If a PR introduces a new library, the public interface of the new library should be fully documented in the [Sophia Standard Library Documentation](docs/sophia_stdlib.md).
+- If a PR introduces a new compiler option, the new option should be documented in the file
+[aeso_compiler.md](docs/aeso_compiler.md).
+
+### Tests
+
+- If a PR introduces new syntax (e.g. changes in [aeso_syntax.erl](src/aeso_syntax.erl), [aeso_scan.erl](src/aeso_scan.erl), or [aeso_parser.erl](src/aeso_parser.erl)), the contract [all_syntax.aes](test/contracts/all_syntax.aes) should be updated to include the new syntax.
+- If a PR fixes a bug, the code that replicates the bug should be added as a new passing test contract.
+- If a PR introduces a new feature, add tests for both successful and failing usage of that feature. In order to run the entire compilation pipeline and to avoid erroring during intermediate steps, failing tests should not be mixed with the successful ones.
+
+### Source Code
+
+- If a PR introduces new syntax (e.g. changes in [aeso_syntax.erl](src/aeso_syntax.erl), [aeso_scan.erl](src/aeso_scan.erl), or [aeso_parser.erl](src/aeso_parser.erl)), the following code should be updated to handle the new syntax:
+    - The function `aeso_syntax_utils:fold/4` in the file [aeso_syntax_utils.erl](src/aeso_syntax_utils.erl).
+    - Any related pretty printing function in the file [aeso_pretty.erl](src/aeso_pretty.erl), depending on the type of the newly added syntax.
+
+## Checklist For Creating a Release
+
+- Update the version in the file [aesophia.app.src](src/aesophia.app.src).
+- Update the version in the file [rebar.config](rebar.config).
+- In the [Changelog](CHANGELOG.md):
+    - Update the `Unreleased` changes to be under the new version.
+    - Update the version at the bottom of the file.
+- Commit and the changes and create a new PR (check the commit of [v6.1.0](https://github.com/aeternity/aesophia/commit/5ad5270e381f6e810d7b8b5cdc168d283e7a90bb) for reference).
+- Create a release after merging the new PR to `master` branch.
+- After releasing `aesophia`, refer to each of the following repositories and create new releases as well, using the new `aesophia` release:
+    - [aesophia_cli](https://github.com/aeternity/aesophia_cli)
+    - [aesophia_http](https://github.com/aeternity/aesophia_http)
+    - [aerepl](https://github.com/aeternity/aerepl)

README.md

@@ -14,6 +14,7 @@ The compiler is currently being used three places
 * [Features](docs/sophia_features.md)
 * [Standard library](docs/sophia_stdlib.md)
 * [Contract examples](docs/sophia_examples.md)
+* [Contributing](CONTRIBUTING.md)
 
 Additionally you can check out the [contracts section](https://github.com/aeternity/protocol/blob/master/contracts/contracts.md) of the æternity blockchain specification.
 

docs/aeso_aci.md

@@ -67,7 +67,7 @@ generates the following JSON structure representing the contract interface:
         }
       ]
     },
-    "type_defs": [
+    "typedefs": [
       {
         "name": "answers",
         "typedef": {
@@ -138,7 +138,7 @@ be included inside another contract.
              state =>
                  #{record =>
                        [#{name => <<"a">>,type => <<"Answers.answers">>}]},
-             type_defs =>
+             typedefs =>
                  [#{name => <<"answers">>,
                     typedef => #{<<"map">> => [<<"string">>,<<"int">>]},
                     vars => []}]}}]}

docs/aeso_compiler.md

@@ -51,6 +51,36 @@ The **pp_** options all print to standard output the following:
 
 `pp_assembler` - print the generated assembler code
 
+The option `include_child_contract_symbols` includes the symbols of child contracts functions in the generated fate code. It is turned off by default to avoid making contracts bigger on chain.
+
+The option `debug_info` includes information related to debugging in the compiler output. Currently this option only includes the mapping from variables to registers.
+
+#### Options to control which compiler optimizations should run:
+
+By default all optimizations are turned on, to disable an optimization, it should be
+explicitly set to false and passed as a compiler option.
+
+List of optimizations:
+
+- optimize_inliner
+- optimize_inline_local_functions
+- optimize_bind_subexpressions
+- optimize_let_floating
+- optimize_simplifier
+- optimize_drop_unused_lets
+- optimize_push_consume
+- optimize_one_shot_var
+- optimize_write_to_dead_var
+- optimize_inline_switch_target
+- optimize_swap_push
+- optimize_swap_pop
+- optimize_swap_write
+- optimize_constant_propagation
+- optimize_prune_impossible_branches
+- optimize_single_successful_branch
+- optimize_inline_store
+- optimize_float_switch_bod
+
 #### check_call(ContractString, Options) -> CheckRet
 
 Types

docs/sophia_features.md

@@ -134,6 +134,166 @@ main contract IntHolderFactory =
 In case of a presence of child contracts (`IntHolder` in this case), the main
 contract must be pointed out with the `main` keyword as shown in the example.
 
+### Contract interfaces and polymorphism
+
+Contracts can implement one or multiple interfaces, the contract has to define
+every entrypoint from the implemented interface and the entrypoints in both
+the contract and implemented interface should have compatible types.
+
+```
+contract interface Animal =
+  entrypoint sound : () => string
+
+ contract Cat : Animal =
+  entrypoint sound() = "Cat sound"
+```
+
+Contract interfaces can extend other interfaces. An extended interface has to
+declare all entrypoints from every parent interface. All the declarations in the extended
+interface must have types compatible with the declarations from the parent
+interface.
+
+```
+contract interface II =
+  entrypoint f : () => unit
+
+contract interface I : II =
+  entrypoint f : () => unit
+  entrypoint g : () => unit
+
+contract C : I =
+  entrypoint f() = ()
+  entrypoint g() = ()
+```
+
+It is only possible to implement (or extend) an interface that has been already
+defined earlier in the file (or in an included file). Therefore recursive
+interface implementation is not allowed in Sophia.
+
+```
+// The following code would show an error
+
+contract interface X : Z =
+     entrypoint x : () => int
+
+ contract interface Y : X =
+     entrypoint x : () => int
+     entrypoint y : () => int
+
+ contract interface Z : Y =
+     entrypoint x : () => int
+     entrypoint y : () => int
+     entrypoint z : () => int
+
+ contract C : Z =
+     entrypoint x() = 1
+     entrypoint y() = 1
+     entrypoint z() = 1
+```
+
+#### Adding or removing modifiers
+
+When a `contract` or a `contract interface` implements another `contract interface`, the `payable` and `stateful` modifiers can be kept or changed, both in the contract and in the entrypoints, according to the following rules:
+
+1. A `payable` contract or interface can implement a `payable` interface or a non-`payable` interface.
+2. A non-`payable` contract or interface can only implement a non-`payable` interface, and cannot implement a `payable` interface.
+3. A `payable` entrypoint can implement a `payable` entrypoint or a non-`payable` entrypoint.
+4. A non-`payable` entrypoint can only implement a non-`payable` entrypoint, and cannot implement a `payable` entrypoint.
+5. A non-`stateful` entrypoint can implement a `stateful` entrypoint or a non-`stateful` entrypoint.
+6. A `stateful` entrypoint can only implement a `stateful` entrypoint, and cannot implement a non-`stateful` entrypoint.
+
+#### Subtyping and variance
+
+Subtyping in Sophia follows common rules that take type variance into account. As described by [Wikipedia](https://en.wikipedia.org/wiki/Covariance_and_contravariance_(computer_science)), 
+
+>Variance refers to how subtyping between more complex types relates to subtyping between their components.
+
+This concept plays an important role in complex types such as tuples, `datatype`s and functions. Depending on the context, it can apply to positions in the structure of a type, or type parameters of generic types. There are four kinds of variances:
+
+- covariant
+- contravariant
+- invariant
+- bivariant
+
+A type is said to be on a "covariant" position when it describes output or a result of some computation. Analogously, position is "contravariant" when it is an input, or a parameter. Intuitively, when a part of the type is produced by values of it, it is covariant. When it is consumed, it is contravariant. When a type appears to be simultaneously input and output, it is described as invariant. If a type is neither of those (that is, it's unused) it's bivariant. Furthermore, whenever a complex type appears on a contravariant position, all its covariant components become contravariant and vice versa.
+
+Variance influences how subtyping is applied. Types on covariant positions are subtyped normally, while contravariant the opposite way. Invariant types have to be exactly the same in order for subtyping to work. Bivariant types are always compatible.
+
+A good example of where it matters can be pictured by subtyping of function types. Let us assume there is a contract interface `Animal` and two contracts that implement it: `Dog` and `Cat`.
+
+```sophia
+contract interface Animal =
+  entrypoint age : () => int
+  
+contract Dog : Animal =
+  entrypoint age() = // ...
+  entrypoint woof() = "woof"
+  
+contract Cat : Animal =
+  entrypoint age() = // ...
+  entrypoint meow() = "meow"
+```
+
+The assumption of this exercise is that cats do not bark (because `Cat` does not define the `woof` entrypoint). If subtyping rules were applied naively, that is if we let `Dog => Dog` be a subtype of `Animal => Animal`, the following code would break:
+
+```sophia
+let f : (Dog) => string  = d => d.woof()
+let g : (Animal) => string  = f
+let c : Cat = Chain.create()
+g(c)  // Cat barking!
+```
+
+That is because arguments of functions are contravariant, as opposed to return the type which is covariant. Because of that, the assignment of `f` to `g` is invalid - while `Dog` is a subtype of `Animal`, `Dog => string` is **not** a subtype of `Animal => string`. However, `Animal => string` **is** a subtype of `Dog => string`. More than that, `(Dog => Animal) => Dog` is a subtype of `(Animal => Dog) => Animal`.
+
+This has consequences on how user-defined generic types work. A type variable gains its variance from its role in the type definition as shown in the example:
+
+```sophia
+datatype co('a) = Co('a) // co is covariant on 'a
+datatype ct('a) = Ct('a => unit) // ct is contravariant on 'a
+datatype in('a) = In('a => 'a) // in is invariant on 'a
+datatype bi('a) = Bi // bi is bivariant on 'a
+```
+
+The following facts apply here:
+
+- `co('a)` is a subtype of `co('b)` when `'a` is a subtype of `'b`
+- `ct('a)` is a subtype of `ct('b)` when `'b` is a subtype of `'a`
+- `in('a)` is a subtype of `in('b)` when `'a` is equal to `'b`
+- `bi('a)` is a subtype of `bi('b)` always
+
+That altogether induce the following rules of subtyping in Sophia:
+
+- A function type `(Args1) => Ret1` is a subtype of `(Args2) => Ret2` when `Ret1`
+is a subtype of `Ret2` and each argument type from `Args2` is a subtype of its
+counterpart in `Args1`.
+
+- A list type `list(A)` is a subtype of `list(B)` if `A` is a subtype of `B`.
+
+- An option type `option(A)` is a subtype of `option(B)` if `A` is a subtype of `B`.
+
+- A map type `map(A1, A2)` is a subtype of `map(B1, B2)` if `A1` is a subtype
+of `B1`, and `A2` is a subtype of `B2`.
+
+- An oracle type `oracle(A1, A2)` is a subtype of `oracle(B1, B2)` if `B1` is
+a subtype of `A1`, and `A2` is a subtype of `B2`.
+
+- An oracle_query type `oracle_query(A1, A2)` is a subtype of `oracle_query(B1, B2)`
+if `A1` is a subtype of `B1`, and `A2` is a subtype of `B2`.
+
+- A user-defined datatype `t(Args1)` is a subtype of `t(Args2)`
+
+- When a user-defined type `t('a)` is covariant in `'a`, then `t(A)` is a
+subtype of `t(B)` when `A` is a subtype of `B`.
+
+- When a user-defined type `t('a)` is contravariant in `'a`, then `t(A)` is a
+subtype of `t(B)` when `B` is a subtype of `A`.
+
+- When a user-defined type `t('a)` is binvariant in `'a`, then `t(A)` is a
+subtype of `t(B)` when either `A` is a subtype of `B` or when `B` is a subtype
+of `A`.
+
+- When a user-defined type `t('a)` is invariant in `'a`, then `t(A)` can never be
+a subtype of `t(B)`.
 
 ## Mutable state
 
@@ -354,29 +514,28 @@ namespace C =
 ## Types
 Sophia has the following types:
 
-| Type                 | Description                                                                                 | Example                                                                       |
-|----------------------|---------------------------------------------------------------------------------------------|-------------------------------------------------------------------------------|
-| int                  | A 2-complement integer                                                                      | ```-1```                                                                      |
-| char                 | A single character                                                                          | ```'c'```                                                                     |
-| address              | æternity address, 32 bytes                                                                  | ```Call.origin``` ```ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt``` |
-| bool                 | A Boolean                                                                                   | ```true```                                                                    |
-| bits                 | A bit field                                                                                 | ```Bits.none```                                                               |
-| bytes(n)             | A byte array with `n` bytes                                                                 | ```#fedcba9876543210```                                                       |
-| string               | An array of bytes                                                                           | ```"Foo"```                                                                   |
-| list                 | A homogeneous immutable singly linked list.                                                 | ```[1, 2, 3]```                                                               |
-| ('a, 'b) => 'c       | A function. Parentheses can be skipped if there is only one argument                        | ```(x : int, y : int) => x + y```                                             |
-| tuple                | An ordered heterogeneous array                                                              | ```(42, "Foo", true)```                                                       |
-| record               | An immutable key value store with fixed key names and typed values                          | ``` record balance = { owner: address, value: int } ```                       |
-| map                  | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)```                                    |
-| option('a)           | An optional value either None or Some('a)                                                   | ```Some(42)```                                                                |
-| state                | A user defined type holding the contract state                                              | ```record state = { owner: address, magic_key: bytes(4) }```                  |
-| event                | An append only list of blockchain events (or log entries)                                   | ```datatype event = EventX(indexed int, string)```                            |
-| hash                 | A 32-byte hash - equivalent to `bytes(32)`                                                  |                                                                               |
-| signature            | A signature - equivalent to `bytes(64)`                                                     |                                                                               |
-| Chain.ttl            | Time-to-live (fixed height or relative to current block)                                    | ```FixedTTL(1050)``` ```RelativeTTL(50)```                                    |
-| oracle('a, 'b)       | And oracle answering questions of type 'a with answers of type 'b                           | ```Oracle.register(acct, qfee, ttl)```                                        |
-| oracle_query('a, 'b) | A specific oracle query                                                                     | ```Oracle.query(o, q, qfee, qttl, rttl)```                                    |
-| contract             | A user defined, typed, contract address                                                     | ```function call_remote(r : RemoteContract) = r.fun()```                      |
+| Type                 | Description                                                                                 | Example                                                      |
+|----------------------|---------------------------------------------------------------------------------------------|--------------------------------------------------------------|
+| int                  | A 2-complement integer                                                                      | ```-1```                                                     |
+| address              | æternity address, 32 bytes                                                                 | ```Call.origin```                                            |
+| bool                 | A Boolean                                                                                   | ```true```                                                   |
+| bits                 | A bit field                                                                                 | ```Bits.none```                                              |
+| bytes(n)             | A byte array with `n` bytes                                                                 | ```#fedcba9876543210```                                      |
+| string               | An array of bytes                                                                           | ```"Foo"```                                                  |
+| list                 | A homogeneous immutable singly linked list.                                                 | ```[1, 2, 3]```                                              |
+| ('a, 'b) => 'c       | A function. Parentheses can be skipped if there is only one argument                        | ```(x : int, y : int) => x + y```                            |
+| tuple                | An ordered heterogeneous array                                                              | ```(42, "Foo", true)```                                      |
+| record               | An immutable key value store with fixed key names and typed values                          | ``` record balance = { owner: address, value: int } ```      |
+| map                  | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)```                   |
+| option('a)           | An optional value either None or Some('a)                                                   | ```Some(42)```                                               |
+| state                | A user defined type holding the contract state                                              | ```record state = { owner: address, magic_key: bytes(4) }``` |
+| event                | An append only list of blockchain events (or log entries)                                   | ```datatype event = EventX(indexed int, string)```           |
+| hash                 | A 32-byte hash - equivalent to `bytes(32)`                                                  |                                                              |
+| signature            | A signature - equivalent to `bytes(64)`                                                     |                                                              |
+| Chain.ttl            | Time-to-live (fixed height or relative to current block)                                    | ```FixedTTL(1050)``` ```RelativeTTL(50)```                   |
+| oracle('a, 'b)       | And oracle answering questions of type 'a with answers of type 'b                           | ```Oracle.register(acct, qfee, ttl)```                       |
+| oracle_query('a, 'b) | A specific oracle query                                                                     | ```Oracle.query(o, q, qfee, qttl, rttl)```                   |
+| contract             | A user defined, typed, contract address                                                     | ```function call_remote(r : RemoteContract) = r.fun()```     |
 
 ## Literals
 | Type                 | Constant/Literal example(s)                                                                                                         |
@@ -401,6 +560,19 @@ Sophia has the following types:
 | oracle_query('a, 'b) | `oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY`                                                                             |
 | contract             | `ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ`                                                                              |
 
+## Hole expression
+
+Hole expressions, written as `???`, are expressions that are used as a placeholder. During compilation, the compiler will generate a type error indication the type of the hole expression.
+
+```
+include "List.aes"
+contract C =
+    entrypoint f() =
+        List.sum(List.map(???, [1,2,3]))
+```
+
+A hole expression found in the example above will generate the error `` Found a hole of type `(int) => int` ``. This says that the compiler expects a function from `int` to `int` in place of the `???` placeholder.
+
 ## Arithmetic
 
 Sophia integers (`int`) are represented by arbitrary-sized signed words and support the following
@@ -502,59 +674,6 @@ function
 
 Guards cannot be stateful even when used inside a stateful function.
 
-## Comparable types
-
-Only certain types are allowed to be compared by equality (`==`, `!=`) and
-inequality (`<`, `>`, `=<`, `>=`). For instance, while it is legal to compare
-integers, comparing functions would lead to an error:
-
-```
-function f() = 
-  f == f  // type error
-```
-
-The rules apply as follows:
-
-- All types that are comparable by inequality are also comparable by equality.
-- The builtin types `bool`, `int`, `char`, `bits`, `bytes`, `string`, `unit`,
-  `hash`, `address` and `signature` are comparable by inequality (and thus by
-  equality).
-- The composite types `list`, `option`, and tuples are comparable by
-  equality/inequality if their type parameters are comparable by
-  equality/inequality.
-- The composite types `map`, `oracle`, and `oracle_query` are comparable by
-  equality if their type parameters are comparable by equality.
-- User-defined records and datatypes are comparable by equality if their type
-  parameters are comparable by equality.
-- Smart contracts are comparable by equality.
-- User-declared type variables are comparable according to the [type
-  constraints](#type-constraints) given in the function signature.
-
-In all other cases the types are not comparable.
-
-### Type constraints
-
-Polymorphic types are not declared as comparable by default. If the user
-specifies the type signature for a function, they need to manually declare type
-constraints in order to allow the variables to be compared. This can only be
-done if the type declaration is separated from the function definition. The
-constraints have to be prepended to the type declaration and separated with a
-semicolon:
-
-```
-
-function eq(x : 'a, y : 'a) = x == y  // Type error, 'a is not comparable
-
-function
-  eq : 'a is eq ; ('a, 'a) => bool
-  eq(x, y) = x == y                   // Compiles
-
-function eq(x, y) = x == y            // Compiles as the constraints are inferred
-```
-
-Currently only two constraints are allowed: `eq` for equality and `ord` for
-inequality. Declaring a type as `ord` automatically implies `eq`.
-
 ## Lists
 
 A Sophia list is a dynamically sized, homogenous, immutable, singly
@@ -916,6 +1035,16 @@ function require(b : bool, err : string) =
     if(!b) abort(err)
 ```
 
+Aside from that, there is an almost equivalent function `exit`
+
+```sophia
+exit(reason : string) : 'a
+```
+
+Just like `abort`, it breaks the execution with the given reason. The difference
+however is in the gas consumption — while `abort` returns unused gas, a call to
+`exit` burns it all.
+
 ## Delegation signature
 
 Some chain operations (`Oracle.<operation>` and `AENS.<operation>`) have an

docs/sophia_stdlib.md

@@ -483,7 +483,7 @@ The address of the account that mined the current block.
 Chain.timestamp : int
 ```
 
-The timestamp of the current block.
+The timestamp of the current block (unix time, milliseconds).
 
 
 ##### difficulty
@@ -812,8 +812,8 @@ Registers new oracle answering questions of type `'a` with answers of type `'b`.
   private key of the account, proving you have the private key of the oracle to be. If the
   address is the same as the contract `sign` is ignored and can be left out entirely.
 * The `qfee` is the minimum query fee to be paid by a user when asking a question of the oracle.
-* The `ttl` is the Time To Live for the oracle, either relative to the current
-  height (`RelativeTTL(delta)`) or a fixed height (`FixedTTL(height)`).
+* The `ttl` is the Time To Live for the oracle in key blocks, either relative to the current
+  key block height (`RelativeTTL(delta)`) or a fixed key block height (`FixedTTL(height)`).
 * The type `'a` is the type of the question to ask.
 * The type `'b` is the type of the oracle answers.
 

docs/sophia_syntax.md

@@ -10,8 +10,9 @@ and `*/` and can be nested.
 ### Keywords
 
 ```
-contract elif else entrypoint false function if import include let mod namespace
-private payable stateful switch true type record datatype main interface
+contract include let switch type record datatype if elif else function
+stateful payable true false mod public entrypoint private indexed namespace
+interface main using as for hiding
 ```
 
 ### Tokens
@@ -91,18 +92,30 @@ A Sophia file consists of a sequence of *declarations* in a layout block.
 ```c
 File ::= Block(TopDecl)
 
-TopDecl ::= ['payable'] 'contract' Con '=' Block(Decl)
-       | 'namespace' Con '=' Block(Decl)
-       | '@compiler' PragmaOp Version
-       | 'include' String
+TopDecl ::= ['payable'] ['main'] 'contract' Con [Implement] '=' Block(Decl)
+          | 'contract' 'interface' Con [Implement] '=' Block(Decl)
+          | 'namespace' Con '=' Block(Decl)
+          | '@compiler' PragmaOp Version
+          | 'include' String
+          | Using
+
+Implement ::= ':' Sep1(Con, ',')
 
 Decl ::= 'type'     Id ['(' TVar* ')'] '=' TypeAlias
        | 'record'   Id ['(' TVar* ')'] '=' RecordType
        | 'datatype' Id ['(' TVar* ')'] '=' DataType
        | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl)
+       | Using
 
 FunDecl ::= Id ':' Type                             // Type signature
           | Id Args [':' Type] '=' Block(Stmt)      // Definition
+          | Id Args [':' Type] Block(GuardedDef)    // Guarded definitions
+
+GuardedDef ::= '|' Sep1(Expr, ',') '=' Block(Stmt)
+
+Using ::= 'using' Con ['as' Con] [UsingParts]
+UsingParts ::= 'for' '[' Sep1(Id, ',') ']'
+             | 'hiding' '[' Sep1(Id, ',') ']'
 
 PragmaOp ::= '<' | '=<' | '==' | '>=' | '>'
 Version  ::= Sep1(Int, '.')
@@ -172,12 +185,17 @@ Stmt ::= 'switch' '(' Expr ')' Block(Case)
        | 'elif' '(' Expr ')' Block(Stmt)
        | 'else' Block(Stmt)
        | 'let' LetDef
+       | Using
        | Expr
 
 LetDef ::= Id Args [':' Type] '=' Block(Stmt)   // Function definition
          | Pattern '=' Block(Stmt)              // Value definition
 
 Case    ::= Pattern '=>' Block(Stmt)
+          | Pattern Block(GuardedCase)
+
+GuardedCase ::= '|' Sep1(Expr, ',') '=>' Block(Stmt)
+
 Pattern ::= Expr
 ```
 
@@ -215,10 +233,12 @@ Expr ::= '(' LamArgs ')' '=>' Block(Stmt)   // Anonymous function    (x) => x +
        | '[' Expr '..' Expr ']'             // List range            [1..n]
        | '{' Sep(FieldUpdate, ',') '}'      // Record or map value   {x = 0, y = 1}, {[key] = val}
        | '(' Expr ')'                       // Parens                (1 + 2) * 3
+       | '(' Expr '=' Expr ')'              // Assign pattern        (y = x::_)
        | Id | Con | QId | QCon              // Identifiers           x, None, Map.member, AELib.Token
        | Int | Bytes | String | Char        // Literals              123, 0xff, #00abc123, "foo", '%'
        | AccountAddress | ContractAddress   // Chain identifiers
        | OracleAddress | OracleQueryId      // Chain identifiers
+       | '???'                              // Hole expression       1 + ???
 
 Generator ::= Pattern '<-' Expr   // Generator
             | 'if' '(' Expr ')'   // Guard
@@ -244,12 +264,12 @@ UnOp  ::= '-' | '!'
 | Operators | Type
 | --- | ---
 | `-` `+` `*` `/` `mod` `^` | arithmetic operators
-| `!` `&&` `\|\|` | logical operators
+| `!` `&&` `||` | logical operators
 | `==` `!=` `<` `>` `=<` `>=` | comparison operators
 | `::` `++` | list operators
-| `\|>` | functional operators
+| `|>` | functional operators
 
-## Operator precendences
+## Operator precedence
 
 In order of highest to lowest precedence.
 
@@ -263,5 +283,5 @@ In order of highest to lowest precedence.
 | `::` `++` | right
 | `<` `>` `=<` `>=` `==` `!=` | none
 | `&&` | right
-| `\|\|` | right
-| `\|>` | left
+| `||` | right
+| `|>` | left

priv/stdlib/List.aes

@@ -29,11 +29,9 @@ namespace List =
     []   => abort("drop_last_unsafe: list empty")
 
 
-  function
-    contains : 'a is eq; ('a, list('a)) => bool
-    contains(e, l) = switch(l)
-      []   => false
-      h::t => h == e || contains(e, t)
+  function contains(e : 'a, l : list('a)) = switch(l)
+    []   => false
+    h::t => h == e || contains(e, t)
 
 /** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
  * if no such element exists.

priv/stdlib/Option.aes

@@ -30,9 +30,7 @@ namespace Option =
     None    => abort(err)
     Some(x) => x
 
-  function
-    contains : 'a is eq; ('a, option('a)) => bool
-    contains(e, o) = o == Some(e)
+  function contains(e : 'a, o : option('a)) = o == Some(e)
 
   function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)
 

priv/stdlib/String.aes

@@ -90,7 +90,6 @@ namespace String =
           Some(ix)
 
   private function
-    is_prefix : (list(char), list(char)) => option(list(char))
     is_prefix([], ys) = Some(ys)
     is_prefix(_, [])  = None
     is_prefix(x :: xs, y :: ys) =
@@ -99,10 +98,10 @@ namespace String =
 
   private function
     to_int_([], _, x, _) = Some(x)
-    to_int_(i :: ints, value, x, b) =
+    to_int_(i :: is, value, x, b) =
       switch(value(i))
         None => None
-        Some(i) => to_int_(ints, value, x * b + i, b)
+        Some(n) => to_int_(is, value, x * b + n, b)
 
   private function ch_to_int_10(ch) =
     let c = Char.to_int(ch)

rebar.config

@@ -2,11 +2,10 @@
 
 {erl_opts, [debug_info]}.
 
-{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"0699f35"}}}
+{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {tag, "v3.2.0"}}}
        , {getopt, "1.0.1"}
        , {eblake2, "1.0.0"}
-       , {jsx, {git, "https://github.com/talentdeficit/jsx.git",
-                     {tag, "2.8.0"}}}
+       , {jsx, {git, "https://github.com/talentdeficit/jsx.git", {tag, "2.8.0"}}}
        ]}.
 
 {dialyzer, [
@@ -15,7 +14,7 @@
             {base_plt_apps, [erts, kernel, stdlib, crypto, mnesia]}
            ]}.
 
-{relx, [{release, {aesophia, "6.1.0"},
+{relx, [{release, {aesophia, "7.1.0"},
          [aesophia, aebytecode, getopt]},
 
         {dev_mode, true},

rebar.lock

@@ -1,11 +1,11 @@
-{"1.1.0",
+{"1.2.0",
 [{<<"aebytecode">>,
   {git,"https://github.com/aeternity/aebytecode.git",
-       {ref,"0699f35b0398bac6cd4468da654d608375bd853d"}},
+       {ref,"2a0a397afad6b45da52572170f718194018bf33c"}},
   0},
  {<<"aeserialization">>,
   {git,"https://github.com/aeternity/aeserialization.git",
-       {ref,"47aaa8f5434b365c50a35bfd1490340b19241991"}},
+       {ref,"eb68fe331bd476910394966b7f5ede7a74d37e35"}},
   1},
  {<<"base58">>,
   {git,"https://github.com/aeternity/erl-base58.git",
@@ -14,7 +14,7 @@
  {<<"eblake2">>,{pkg,<<"eblake2">>,<<"1.0.0">>},0},
  {<<"enacl">>,
   {git,"https://github.com/aeternity/enacl.git",
-       {ref,"26180f42c0b3a450905d2efd8bc7fd5fd9cece75"}},
+       {ref,"793ddb502f7fe081302e1c42227dca70b09f8e17"}},
   2},
  {<<"getopt">>,{pkg,<<"getopt">>,<<"1.0.1">>},0},
  {<<"jsx">>,
@@ -24,5 +24,8 @@
 [
 {pkg_hash,[
  {<<"eblake2">>, <<"EC8AD20E438AAB3F2E8D5D118C366A0754219195F8A0F536587440F8F9BCF2EF">>},
- {<<"getopt">>, <<"C73A9FA687B217F2FF79F68A3B637711BB1936E712B521D8CE466B29CBF7808A">>}]}
+ {<<"getopt">>, <<"C73A9FA687B217F2FF79F68A3B637711BB1936E712B521D8CE466B29CBF7808A">>}]},
+{pkg_hash_ext,[
+ {<<"eblake2">>, <<"3C4D300A91845B25D501929A26AC2E6F7157480846FAB2347A4C11AE52E08A99">>},
+ {<<"getopt">>, <<"53E1AB83B9CEB65C9672D3E7A35B8092E9BDC9B3EE80721471A161C10C59959C">>}]}
 ].

src/aeso_aci.erl

@@ -83,7 +83,7 @@ from_typed_ast(Type, TypedAst) ->
         string -> do_render_aci_json(JArray)
     end.
 
-encode_contract(Contract = {Head, _, {con, _, Name}, _}) when ?IS_CONTRACT_HEAD(Head) ->
+encode_contract(Contract = {Head, _, {con, _, Name}, _, _}) when ?IS_CONTRACT_HEAD(Head) ->
     C0 = #{name => encode_name(Name)},
 
     Tdefs0 = [ encode_typedef(T) || T <- sort_decls(contract_types(Contract)) ],
@@ -91,7 +91,7 @@ encode_contract(Contract = {Head, _, {con, _, Name}, _}) when ?IS_CONTRACT_HEAD(
     {Es, Tdefs1} = lists:partition(FilterT(<<"event">>), Tdefs0),
     {Ss, Tdefs}  = lists:partition(FilterT(<<"state">>), Tdefs1),
 
-    C1 = C0#{type_defs => Tdefs},
+    C1 = C0#{typedefs => Tdefs},
 
     C2 = case Es of
              []                 -> C1;
@@ -111,7 +111,7 @@ encode_contract(Contract = {Head, _, {con, _, Name}, _}) when ?IS_CONTRACT_HEAD(
 encode_contract(Namespace = {namespace, _, {con, _, Name}, _}) ->
     Tdefs = [ encode_typedef(T) || T <- sort_decls(contract_types(Namespace)) ],
     #{namespace => #{name => encode_name(Name),
-                     type_defs => Tdefs}}.
+                     typedefs => Tdefs}}.
 
 %%  Encode a function definition. Currently we are only interested in
 %%  the interface and type.
@@ -234,7 +234,7 @@ do_render_aci_json(Json) ->
 decode_contract(#{contract := #{name := Name,
                                 kind := Kind,
                                 payable := Payable,
-                                type_defs := Ts0,
+                                typedefs := Ts0,
                                 functions := Fs} = C}) ->
     MkTDef = fun(N, T) -> #{name => N, vars => [], typedef => T} end,
     Ts = [ MkTDef(<<"state">>, maps:get(state, C)) || maps:is_key(state, C) ] ++
@@ -246,7 +246,7 @@ decode_contract(#{contract := #{name := Name,
                        end,
      io_lib:format("~s", [Name])," =\n",
      decode_tdefs(Ts), decode_funcs(Fs)];
-decode_contract(#{namespace := #{name := Name, type_defs := Ts}}) when Ts /= [] ->
+decode_contract(#{namespace := #{name := Name, typedefs := Ts}}) when Ts /= [] ->
     ["namespace ", io_lib:format("~s", [Name])," =\n",
      decode_tdefs(Ts)];
 decode_contract(_) -> [].
@@ -341,10 +341,12 @@ stateful(false) -> "".
 
 %% #contract{Ann, Con, [Declarations]}.
 
-contract_funcs({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
+contract_funcs({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
     [ D || D <- Decls, is_fun(D)].
 
-contract_types({C, _, _, Decls}) when ?IS_CONTRACT_HEAD(C); C == namespace ->
+contract_types({namespace, _, _, Decls}) ->
+    [ D || D <- Decls, is_type(D) ];
+contract_types({C, _, _, _, Decls}) when ?IS_CONTRACT_HEAD(C) ->
     [ D || D <- Decls, is_type(D) ].
 
 is_fun({letfun, _, _, _, _, _}) -> true;

src/aeso_ast.erl

@@ -1,27 +0,0 @@
--module(aeso_ast).
-
--export([int/2,
-         line/1,
-         pp/1,
-         pp_typed/1,
-         symbol/2,
-         symbol_name/1
-        ]).
-
-
-symbol(Line, Chars) -> {symbol, Line, Chars}.
-int(Line, Int) -> {'Int', Line, Int}.
-
-line({symbol, Line, _}) -> Line.
-
-symbol_name({symbol, _, Name}) -> Name.
-
-pp(Ast) ->
-    String = prettypr:format(aeso_pretty:decls(Ast, [])),
-    io:format("Ast:\n~s\n", [String]).
-
-pp_typed(TypedAst) ->
-    %% io:format("Typed tree:\n~p\n",[TypedAst]),
-    String = prettypr:format(aeso_pretty:decls(TypedAst, [show_generated])),
-    io:format("Type ast:\n~s\n",[String]).
-

src/aeso_ast_code_analysis.erl

@@ -0,0 +1,154 @@
+-module(aeso_ast_code_analysis).
+
+
+all_warnings() ->
+    [ warn_unused_includes
+    , warn_unused_stateful
+    , warn_unused_variables
+    , warn_unused_typedefs
+    , warn_unused_return_value
+    , warn_unused_functions
+    , warn_shadowing
+    , warn_division_by_zero
+    , warn_negative_spend ].
+
+
+when_warning(Warn, Do) ->
+    case lists:member(Warn, all_warnings()) of
+        false ->
+            create_type_errors(),
+            type_error({unknown_warning, Warn}),
+            destroy_and_report_type_errors(global_env());
+        true ->
+            case ets_tab_exists(warnings) of
+                true ->
+                    IsEnabled = get_option(Warn, false),
+                    IsAll = get_option(warn_all, false) andalso lists:member(Warn, all_warnings()),
+                    if
+                        IsEnabled orelse IsAll -> Do();
+                        true -> ok
+                    end;
+                false ->
+                    ok
+            end
+    end.
+
+%% Warnings (Unused includes)
+
+potential_unused_include(Ann, SrcFile) ->
+    IsIncluded = aeso_syntax:get_ann(include_type, Ann, none) =/= none,
+    case IsIncluded of
+        false -> ok;
+        true  ->
+            case aeso_syntax:get_ann(file, Ann, no_file) of
+                no_file -> ok;
+                File    -> ets_insert(warnings, {unused_include, File, SrcFile})
+            end
+    end.
+
+used_include(Ann) ->
+    case aeso_syntax:get_ann(file, Ann, no_file) of
+        no_file -> ok;
+        File    -> ets_match_delete(warnings, {unused_include, File, '_'})
+    end.
+
+%% Warnings (Unused stateful)
+
+potential_unused_stateful(Ann, Fun) ->
+    case aeso_syntax:get_ann(stateful, Ann, false) of
+        false -> ok;
+        true  -> ets_insert(warnings, {unused_stateful, Ann, Fun})
+    end.
+
+used_stateful(Fun) ->
+    ets_match_delete(warnings, {unused_stateful, '_', Fun}).
+
+%% Warnings (Unused type defs)
+
+potential_unused_typedefs(Namespace, TypeDefs) ->
+    lists:map(fun({type_def, Ann, Id, Args, _}) ->
+        ets_insert(warnings, {unused_typedef, Ann, Namespace ++ qname(Id), length(Args)}) end, TypeDefs).
+
+used_typedef(TypeAliasId, Arity) ->
+    ets_match_delete(warnings, {unused_typedef, '_', qname(TypeAliasId), Arity}).
+
+%% Warnings (Unused variables)
+
+potential_unused_variables(Namespace, Fun, Vars0) ->
+    Vars = [ Var || Var = {id, _, VarName} <- Vars0, VarName /= "_" ],
+    lists:map(fun({id, Ann, VarName}) ->
+        ets_insert(warnings, {unused_variable, Ann, Namespace, Fun, VarName}) end, Vars).
+
+used_variable(Namespace, Fun, [VarName]) ->
+    ets_match_delete(warnings, {unused_variable, '_', Namespace, Fun, VarName});
+used_variable(_, _, _) -> ok.
+
+%% Warnings (Unused return value)
+
+potential_unused_return_value({typed, Ann, {app, _, {typed, _, _, {fun_t, _, _, _, {id, _, Type}}}, _}, _}) when Type /= "unit" ->
+    ets_insert(warnings, {unused_return_value, Ann});
+potential_unused_return_value(_) -> ok.
+
+%% Warnings (Unused functions)
+
+create_unused_functions() ->
+    ets_new(function_calls, [bag]),
+    ets_new(all_functions, [set]).
+
+register_function_call(Caller, Callee) ->
+    ets_insert(function_calls, {Caller, Callee}).
+
+potential_unused_function(#env{ what = namespace }, Ann, FunQName, FunId) ->
+    ets_insert(all_functions, {Ann, FunQName, FunId, not aeso_syntax:get_ann(private, Ann, false)});
+potential_unused_function(_Env, Ann, FunQName, FunId) ->
+    ets_insert(all_functions, {Ann, FunQName, FunId, aeso_syntax:get_ann(entrypoint, Ann, false)}).
+
+remove_used_funs(All) ->
+    {Used, Unused} = lists:partition(fun({_, _, _, IsUsed}) -> IsUsed end, All),
+    CallsByUsed = lists:flatmap(fun({_, F, _, _}) -> ets_lookup(function_calls, F) end, Used),
+    CalledFuns = sets:from_list(lists:map(fun({_, Callee}) -> Callee end, CallsByUsed)),
+    MarkUsedFun = fun(Fun, Acc) ->
+                      case lists:keyfind(Fun, 2, Acc) of
+                          false -> Acc;
+                          T     -> lists:keyreplace(Fun, 2, Acc, setelement(4, T, true))
+                      end
+                  end,
+    NewUnused = sets:fold(MarkUsedFun, Unused, CalledFuns),
+    case lists:keyfind(true, 4, NewUnused) of
+        false -> NewUnused;
+        _     -> remove_used_funs(NewUnused)
+    end.
+
+destroy_and_report_unused_functions() ->
+    AllFuns = ets_tab2list(all_functions),
+    lists:map(fun({Ann, _, FunId, _}) -> ets_insert(warnings, {unused_function, Ann, name(FunId)}) end,
+              remove_used_funs(AllFuns)),
+    ets_delete(all_functions),
+    ets_delete(function_calls).
+
+%% Warnings (Shadowing)
+
+warn_potential_shadowing(_, "_", _) -> ok;
+warn_potential_shadowing(Ann, Name, Vars) ->
+    case proplists:get_value(Name, Vars, false) of
+        false -> ok;
+        {AnnOld, _} -> ets_insert(warnings, {shadowing, Ann, Name, AnnOld})
+    end.
+
+%% Warnings (Division by zero)
+
+warn_potential_division_by_zero(Ann, Op, Args) ->
+    case {Op, Args} of
+        {{'/', _}, [_, {int, _, 0}]} -> ets_insert(warnings, {division_by_zero, Ann});
+        _ -> ok
+    end.
+
+%% Warnings (Negative spends)
+
+warn_potential_negative_spend(Ann, Fun, Args) ->
+    case {Fun, Args} of
+        { {typed, _, {qid, _, ["Chain", "spend"]}, _}
+        , [_, {typed, _, {app, _, {'-', _}, [{typed, _, {int, _, X}, _}]}, _}]} when X > 0 ->
+            ets_insert(warnings, {negative_spend, Ann});
+        _ -> ok
+    end.

src/aeso_ast_to_fcode.erl

@@ -149,17 +149,18 @@
 
 -type state_layout() :: {tuple, [state_layout()]} | {reg, state_reg()}.
 
--type env() :: #{ type_env      := type_env(),
-                  fun_env       := fun_env(),
-                  con_env       := con_env(),
-                  child_con_env := child_con_env(),
-                  event_type    => aeso_syntax:typedef(),
-                  builtins      := builtins(),
-                  options       := [option()],
-                  state_layout  => state_layout(),
-                  context       => context(),
-                  vars          => [var_name()],
-                  functions     := #{ fun_name() => fun_def() }
+-type env() :: #{ type_env          := type_env(),
+                  fun_env           := fun_env(),
+                  con_env           := con_env(),
+                  child_con_env     := child_con_env(),
+                  event_type        => aeso_syntax:typedef(),
+                  builtins          := builtins(),
+                  options           := [option()],
+                  state_layout      => state_layout(),
+                  context           => context(),
+                  vars              => [var_name()],
+                  functions         := #{ fun_name() => fun_def() },
+                  saved_fresh_names => #{ var_name() => var_name() }
                }.
 
 -define(HASH_BYTES, 32).
@@ -170,7 +171,7 @@
 %% and produces Fate intermediate code.
 -spec ast_to_fcode(aeso_syntax:ast(), [option()]) -> {env(), fcode()}.
 ast_to_fcode(Code, Options) ->
-    init_fresh_names(),
+    init_fresh_names(Options),
     {Env1, FCode1} = to_fcode(init_env(Options), Code),
     FCode2 = optimize(FCode1, Options),
     Env2 = Env1#{ child_con_env :=
@@ -178,13 +179,18 @@ ast_to_fcode(Code, Options) ->
                         fun (_, FC) -> optimize(FC, Options) end,
                         maps:get(child_con_env, Env1)
                        )},
-    clear_fresh_names(),
-    {Env2, FCode2}.
+    Env3 =
+        case proplists:get_value(debug_info, Options, false) of
+            true  -> Env2#{ saved_fresh_names => get(saved_fresh_names) };
+            false -> Env2
+        end,
+    clear_fresh_names(Options),
+    {Env3, FCode2}.
 
 optimize(FCode1, Options) ->
     Verbose = lists:member(pp_fcode, Options),
     [io:format("-- Before lambda lifting --\n~s\n\n", [format_fcode(FCode1)]) || Verbose],
-    FCode2 = optimize_fcode(FCode1),
+    FCode2 = optimize_fcode(FCode1, Options),
     [ io:format("-- After optimization --\n~s\n\n", [format_fcode(FCode2)]) || Verbose, FCode2 /= FCode1 ],
     FCode3 = lambda_lift(FCode2),
     [ io:format("-- After lambda lifting --\n~s\n\n", [format_fcode(FCode3)]) || Verbose, FCode3 /= FCode2 ],
@@ -242,7 +248,7 @@ builtins() ->
     MkName = fun(NS, Fun) ->
                 list_to_atom(string:to_lower(string:join(NS ++ [Fun], "_")))
              end,
-    Scopes = [{[],           [{"abort", 1}, {"require", 2}]},
+    Scopes = [{[],           [{"abort", 1}, {"require", 2}, {"exit", 1}]},
               {["Chain"],    [{"spend", 2}, {"balance", 1}, {"block_hash", 1}, {"coinbase", none},
                               {"timestamp", none}, {"block_height", none}, {"difficulty", none},
                               {"gas_limit", none}, {"bytecode_hash", 1}, {"create", variable}, {"clone", variable}]},
@@ -326,7 +332,7 @@ get_option(Opt, Env, Default) ->
 %% -- Compilation ------------------------------------------------------------
 
 -spec to_fcode(env(), aeso_syntax:ast()) -> {env(), fcode()}.
-to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, Decls}|Rest])
+to_fcode(Env, [{Contract, Attrs, {con, _, Name}, _Impls, Decls}|Rest])
   when ?IS_CONTRACT_HEAD(Contract) ->
     case Contract =:= contract_interface of
         false ->
@@ -349,7 +355,7 @@ to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, Decls}|Rest])
                           event_type    => EventType,
                           payable       => Payable,
                           functions     => add_init_function(
-                                             Env1, Con, StateType,
+                                             Env1,
                                              add_event_function(Env1, EventType, Funs)) },
             case Contract of
                 contract_main -> [] = Rest, {Env1, ConFcode};
@@ -362,8 +368,6 @@ to_fcode(Env, [{Contract, Attrs, Con = {con, _, Name}, Decls}|Rest])
             Env1 = decls_to_fcode(Env#{ context => {abstract_contract, Name} }, Decls),
             to_fcode(Env1, Rest)
     end;
-to_fcode(_Env, [NotMain = {NotMainHead, _ ,_ , _}]) when NotMainHead =/= contract_def ->
-    fcode_error({last_declaration_must_be_main_contract, NotMain});
 to_fcode(Env, [{namespace, _, {con, _, Con}, Decls} | Code]) ->
     Env1 = decls_to_fcode(Env#{ context => {namespace, Con} }, Decls),
     to_fcode(Env1, Code).
@@ -377,22 +381,15 @@ decls_to_fcode(Env, Decls) ->
                 end, Env1, Decls).
 
 -spec decl_to_fcode(env(), aeso_syntax:decl()) -> env().
-decl_to_fcode(Env = #{context := {contract_def, _}}, {fun_decl, _, Id, _}) ->
-    case is_no_code(Env) of
-        false -> fcode_error({missing_definition, Id});
-        true  -> Env
-    end;
 decl_to_fcode(Env, {fun_decl, _, _, _})  -> Env;
 decl_to_fcode(Env, {type_def, _Ann, Name, Args, Def}) ->
     typedef_to_fcode(Env, Name, Args, Def);
-decl_to_fcode(Env = #{ functions := Funs }, {letfun, Ann, Id = {id, _, Name}, Args, Ret, [{guarded, _, [], Body}]}) ->
+decl_to_fcode(Env = #{ functions := Funs }, {letfun, Ann, {id, _, Name}, Args, Ret, [{guarded, _, [], Body}]}) ->
     Attrs = get_attributes(Ann),
     FName = lookup_fun(Env, qname(Env, Name)),
     FArgs = args_to_fcode(Env, Args),
     FRet  = type_to_fcode(Env, Ret),
     FBody = expr_to_fcode(Env#{ vars => [X || {X, _} <- FArgs] }, Body),
-    [ ensure_first_order_entrypoint(Ann, Id, Args, Ret, FArgs, FRet)
-      || aeso_syntax:get_ann(entrypoint, Ann, false) ],
     Def   = #{ attrs  => Attrs,
                args   => FArgs,
                return => FRet,
@@ -401,8 +398,7 @@ decl_to_fcode(Env = #{ functions := Funs }, {letfun, Ann, Id = {id, _, Name}, Ar
     Env#{ functions := NewFuns }.
 
 -spec typedef_to_fcode(env(), aeso_syntax:id(), [aeso_syntax:tvar()], aeso_syntax:typedef()) -> env().
-typedef_to_fcode(Env, Id = {id, _, Name}, Xs, Def) ->
-    check_state_and_event_types(Env, Id, Xs),
+typedef_to_fcode(Env, {id, _, Name}, Xs, Def) ->
     Q = qname(Env, Name),
     FDef = fun(Args) when length(Args) == length(Xs) ->
                 Sub = maps:from_list(lists:zip([X || {tvar, _, X} <- Xs], Args)),
@@ -466,14 +462,6 @@ compute_state_layout(R, [H | T]) ->
 compute_state_layout(R, _) ->
     {R + 1, {reg, R}}.
 
-check_state_and_event_types(#{ context := {contract_def, _} }, Id, [_ | _]) ->
-    case Id of
-        {id, _, "state"} -> fcode_error({parameterized_state, Id});
-        {id, _, "event"} -> fcode_error({parameterized_event, Id});
-        _                -> ok
-    end;
-check_state_and_event_types(_, _, _) -> ok.
-
 -spec type_to_fcode(env(), aeso_syntax:type()) -> ftype().
 type_to_fcode(Env, Type) ->
     type_to_fcode(Env, #{}, Type).
@@ -491,12 +479,8 @@ type_to_fcode(Env, Sub, {record_t, Fields}) ->
     type_to_fcode(Env, Sub, {tuple_t, [], lists:map(FieldType, Fields)});
 type_to_fcode(_Env, _Sub, {bytes_t, _, N}) ->
     {bytes, N};
-type_to_fcode(_Env, _Sub, {tvar, Ann, "void"}) ->
-    fcode_error({found_void, Ann});
 type_to_fcode(_Env, Sub, {tvar, _, X}) ->
     maps:get(X, Sub, {tvar, X});
-type_to_fcode(Env, Sub, {constrained_t, _, _, TVar = {tvar, _, _}}) ->
-    type_to_fcode(Env, Sub, TVar);
 type_to_fcode(_Env, _Sub, {fun_t, Ann, _, var_args, _}) ->
     fcode_error({var_args_not_set, {id, Ann, "a very suspicious function"}});
 type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
@@ -556,7 +540,7 @@ expr_to_fcode(_Env, _Type, {bytes,           _, B}) -> {lit, {bytes, B}};
 
 %% Variables
 expr_to_fcode(Env, _Type, {id, _, X})  -> resolve_var(Env, [X]);
-expr_to_fcode(Env, Type, {qid, Ann, X}) ->
+expr_to_fcode(Env, Type, {qid, _, X}) ->
     case resolve_var(Env, X) of
         {builtin_u, B, Ar} when B =:= oracle_query;
                                 B =:= oracle_get_question;
@@ -567,13 +551,11 @@ expr_to_fcode(Env, Type, {qid, Ann, X}) ->
                                 B =:= oracle_check_query ->
             OType = get_oracle_type(B, Type),
             {oracle, QType, RType} = type_to_fcode(Env, OType),
-            validate_oracle_type(Ann, OType, QType, RType),
             TypeArgs = [{lit, {typerep, QType}}, {lit, {typerep, RType}}],
             {builtin_u, B, Ar, TypeArgs};
         {builtin_u, B = aens_resolve, Ar} ->
             {fun_t, _, _, _, ResType} = Type,
             AensType = type_to_fcode(Env, ResType),
-            validate_aens_resolve_type(Ann, ResType, AensType),
             TypeArgs = [{lit, {typerep, AensType}}],
             {builtin_u, B, Ar, TypeArgs};
         {builtin_u, B = bytes_split, Ar} ->
@@ -717,7 +699,7 @@ expr_to_fcode(Env, _Type, {app, _Ann, {Op, _}, [A]}) when is_atom(Op) ->
     end;
 
 %% Function calls
-expr_to_fcode(Env, Type, {app, _, Fun = {typed, _, FunE, {fun_t, _, NamedArgsT, ArgsT, _}}, Args}) ->
+expr_to_fcode(Env, _, {app, _, Fun = {typed, _, FunE, {fun_t, _, NamedArgsT, ArgsT, Type}}, Args}) ->
     Args1 = get_named_args(NamedArgsT, Args),
     FArgs = [expr_to_fcode(Env, Arg) || Arg <- Args1],
     case expr_to_fcode(Env, Fun) of
@@ -826,53 +808,6 @@ get_oracle_type(oracle_check,        {fun_t, _, _, [OType | _], _}) -> OType;
 get_oracle_type(oracle_check_query,  {fun_t, _, _, [OType | _], _}) -> OType;
 get_oracle_type(oracle_respond,      {fun_t, _, _, [OType | _], _}) -> OType.
 
-validate_oracle_type(Ann, Type, QType, RType) ->
-    ensure_monomorphic(QType, {invalid_oracle_type, polymorphic,  query,    Ann, Type}),
-    ensure_monomorphic(RType, {invalid_oracle_type, polymorphic,  response, Ann, Type}),
-    ensure_first_order(QType, {invalid_oracle_type, higher_order, query,    Ann, Type}),
-    ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}),
-    ok.
-
-validate_aens_resolve_type(Ann, {app_t, _, _, [Type]}, {variant, [[], [FType]]}) ->
-    case FType of
-        string         -> ok;
-        address        -> ok;
-        contract       -> ok;
-        {oracle, _, _} -> ok;
-        oracle_query   -> ok;
-        _              -> fcode_error({invalid_aens_resolve_type, Ann, Type})
-    end.
-
-ensure_first_order_entrypoint(Ann, Id = {id, _, Name}, Args, Ret, FArgs, FRet) ->
-    [ ensure_first_order(FT, {invalid_entrypoint, higher_order, Ann1, Id, {argument, X, T}})
-      || {{typed, Ann1, X, T}, {_, FT}} <- lists:zip(Args, FArgs) ],
-    [ ensure_first_order(FRet, {invalid_entrypoint, higher_order, Ann, Id, {result, Ret}})
-      || Name /= "init" ],  %% init can return higher-order values, since they're written to the store
-                            %% rather than being returned.
-    ok.
-
-ensure_monomorphic(Type, Err) ->
-    case is_monomorphic(Type) of
-        true  -> ok;
-        false -> fcode_error(Err)
-    end.
-
-ensure_first_order(Type, Err) ->
-    case is_first_order(Type) of
-        true  -> ok;
-        false -> fcode_error(Err)
-    end.
-
-is_monomorphic({tvar, _})              -> false;
-is_monomorphic(Ts) when is_list(Ts)    -> lists:all(fun is_monomorphic/1, Ts);
-is_monomorphic(Tup) when is_tuple(Tup) -> is_monomorphic(tuple_to_list(Tup));
-is_monomorphic(_)                      -> true.
-
-is_first_order({function, _, _})       -> false;
-is_first_order(Ts) when is_list(Ts)    -> lists:all(fun is_first_order/1, Ts);
-is_first_order(Tup) when is_tuple(Tup) -> is_first_order(tuple_to_list(Tup));
-is_first_order(_)                      -> true.
-
 %% -- Pattern matching --
 
 -spec alts_to_fcode(env(), ftype(), var_name(), [aeso_syntax:alt()], aeso_syntax:expr()) -> fsplit().
@@ -1205,11 +1140,11 @@ builtin_to_fcode(_Layout, Builtin, Args) ->
 
 %% -- Init function --
 
-add_init_function(Env, Main, StateType, Funs0) ->
+add_init_function(Env, Funs0) ->
     case is_no_code(Env) of
         true  -> Funs0;
         false ->
-            Funs     = add_default_init_function(Env, Main, StateType, Funs0),
+            Funs     = add_default_init_function(Env, Funs0),
             InitName = {entrypoint, <<"init">>},
             InitFun  = #{ body := InitBody} = maps:get(InitName, Funs),
             Funs1 = Funs#{ InitName => InitFun#{ return => {tuple, []},
@@ -1217,16 +1152,14 @@ add_init_function(Env, Main, StateType, Funs0) ->
             Funs1
     end.
 
-add_default_init_function(_Env, Main, StateType, Funs) ->
+add_default_init_function(_Env, Funs) ->
     InitName = {entrypoint, <<"init">>},
     case maps:get(InitName, Funs, none) of
-        %% Only add default init function if state is unit.
-        none when StateType == {tuple, []} ->
+        none ->
             Funs#{ InitName => #{attrs  => [],
                                  args   => [],
                                  return => {tuple, []},
                                  body   => {tuple, []}} };
-        none -> fcode_error({missing_init_function, Main});
         _    -> Funs
     end.
 
@@ -1360,20 +1293,28 @@ lambda_lift_exprs(Layout, As) -> [lambda_lift_expr(Layout, A) || A <- As].
 %% - Constant propagation
 %% - Inlining
 
--spec optimize_fcode(fcode()) -> fcode().
-optimize_fcode(Code = #{ functions := Funs }) ->
-    Code1 = Code#{ functions := maps:map(fun(Name, Def) -> optimize_fun(Code, Name, Def) end, Funs) },
+-spec optimize_fcode(fcode(), [option()]) -> fcode().
+optimize_fcode(Code = #{ functions := Funs }, Options) ->
+    Code1 = Code#{ functions := maps:map(fun(Name, Def) -> optimize_fun(Code, Name, Def, Options) end, Funs) },
     eliminate_dead_code(Code1).
 
--spec optimize_fun(fcode(), fun_name(), fun_def()) -> fun_def().
-optimize_fun(Fcode, Fun, Def = #{ body := Body }) ->
-    %% io:format("Optimizing ~p =\n~s\n", [_Fun, prettypr:format(pp_fexpr(_Body))]),
-    Def#{ body := drop_unused_lets(
-                  simplifier(
-                  let_floating(
-                  bind_subexpressions(
-                  inline_local_functions(
-                  inliner(Fcode, Fun, Body)))))) }.
+-spec optimize_fun(fcode(), fun_name(), fun_def(), [option()]) -> fun_def().
+optimize_fun(Fcode, Fun, Def = #{ body := Body0 }, Options) ->
+    Inliner              = proplists:get_value(optimize_inliner,                Options, true),
+    InlineLocalFunctions = proplists:get_value(optimize_inline_local_functions, Options, true),
+    BindSubexpressions   = proplists:get_value(optimize_bind_subexpressions,    Options, true),
+    LetFloating          = proplists:get_value(optimize_let_floating,           Options, true),
+    Simplifier           = proplists:get_value(optimize_simplifier,             Options, true),
+    DropUnusedLets       = proplists:get_value(optimize_drop_unused_lets,       Options, true),
+
+    Body1 = if Inliner              -> inliner   (Fcode, Fun, Body0); true -> Body0 end,
+    Body2 = if InlineLocalFunctions -> inline_local_functions(Body1); true -> Body1 end,
+    Body3 = if BindSubexpressions   -> bind_subexpressions   (Body2); true -> Body2 end,
+    Body4 = if LetFloating          -> let_floating          (Body3); true -> Body3 end,
+    Body5 = if Simplifier           -> simplifier            (Body4); true -> Body4 end,
+    Body6 = if DropUnusedLets       -> drop_unused_lets      (Body5); true -> Body5 end,
+
+    Def#{ body := Body6 }.
 
 %% --- Inlining ---
 
@@ -1793,12 +1734,29 @@ resolve_fun(#{ fun_env := Funs, builtins := Builtin } = Env, Q) ->
         {{Fun, Ar}, _}         -> {def_u, Fun, Ar}
     end.
 
-init_fresh_names() ->
+init_fresh_names(Options) ->
+    proplists:get_value(debug_info, Options, false) andalso init_saved_fresh_names(),
     put('%fresh', 0).
 
-clear_fresh_names() ->
+clear_fresh_names(Options) ->
+    proplists:get_value(debug_info, Options, false) andalso clear_saved_fresh_names(),
     erase('%fresh').
 
+init_saved_fresh_names() ->
+    put(saved_fresh_names, #{}).
+
+clear_saved_fresh_names() ->
+    erase(saved_fresh_names).
+
+-spec fresh_name_save(string()) -> var_name().
+fresh_name_save(Name) ->
+    Fresh = fresh_name(),
+    case get(saved_fresh_names) of
+        undefined -> ok;
+        Old       -> put(saved_fresh_names, Old#{Fresh => Name})
+    end,
+    Fresh.
+
 -spec fresh_name() -> var_name().
 fresh_name() -> fresh_name("%").
 
@@ -1927,7 +1885,7 @@ bottom_up(F, Env, Expr) ->
                                (_)            -> true end,
             case ShouldFreshen(X) of
                 true ->
-                    Z = fresh_name(),
+                    Z = fresh_name_save(X),
                     Env1 = Env#{ Z => E1 },
                     {'let', Z, E1, bottom_up(F, Env1, rename([{X, Z}], Body))};
                 false ->
@@ -2092,7 +2050,9 @@ setnth(I, X, Xs) ->
 -dialyzer({nowarn_function, [fcode_error/1, internal_error/1]}).
 
 fcode_error(Error) ->
-    aeso_errors:throw(aeso_code_errors:format(Error)).
+    Pos = aeso_errors:pos(0, 0),
+    Msg = lists:flatten(io_lib:format("Unknown error: ~p\n", [Error])),
+    aeso_errors:throw(aeso_errors:new(code_error, Pos, Msg)).
 
 internal_error(Error) ->
     Msg = lists:flatten(io_lib:format("~p\n", [Error])),

src/aeso_ast_types_errors.erl

@@ -0,0 +1,721 @@
+-module(aeso_ast_types_errors).
+
+
+cannot_unify(A, B, Cxt, When) ->
+    type_error({cannot_unify, A, B, Cxt, When}).
+
+
+type_error(Err) ->
+    ets_insert(type_errors, Err).
+
+
+mk_t_err(Pos, Msg) ->
+    aeso_errors:new(type_error, Pos, lists:flatten(Msg)).
+mk_t_err(Pos, Msg, Ctxt) ->
+    aeso_errors:new(type_error, Pos, lists:flatten(Msg), lists:flatten(Ctxt)).
+
+mk_t_err_from_warn(Warn) ->
+    aeso_warnings:warn_to_err(type_error, Warn).
+
+mk_error({no_decls, File}) ->
+    Pos = aeso_errors:pos(File, 0, 0),
+    mk_t_err(Pos, "Empty contract");
+mk_error({mismatched_decl_in_funblock, Name, Decl}) ->
+    Msg = io_lib:format("Mismatch in the function block. Expected implementation/type declaration of ~s function", [Name]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({higher_kinded_typevar, T}) ->
+    Msg = io_lib:format("Type `~s` is a higher kinded type variable "
+                        "(takes another type as an argument)", [pp(instantiate(T))]
+                       ),
+    mk_t_err(pos(T), Msg);
+mk_error({wrong_type_arguments, X, ArityGiven, ArityReal}) ->
+    Msg = io_lib:format("Arity for ~s doesn't match. Expected ~p, got ~p"
+                       , [pp(instantiate(X)), ArityReal, ArityGiven]
+                       ),
+    mk_t_err(pos(X), Msg);
+mk_error({unnamed_map_update_with_default, Upd}) ->
+    Msg = "Invalid map update with default",
+    mk_t_err(pos(Upd), Msg);
+mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
+    Msg = io_lib:format("`~s` was declared with an invalid type `~s`. "
+                       "Entrypoints and functions must have functional types"
+                       , [pp(Id), pp(instantiate(Type))]),
+    mk_t_err(pos(Id), Msg);
+mk_error({cannot_unify, A, B, Cxt, When}) ->
+    VarianceContext = case Cxt of
+                          none -> "";
+                          _    -> io_lib:format(" in a ~p context", [Cxt])
+                      end,
+    Msg = io_lib:format("Cannot unify `~s` and `~s`" ++ VarianceContext,
+                        [pp(instantiate(A)), pp(instantiate(B))]),
+    {Pos, Ctxt} = pp_when(When),
+    mk_t_err(Pos, Msg, Ctxt);
+mk_error({hole_found, Ann, Type}) ->
+    Msg = io_lib:format("Found a hole of type `~s`", [pp(instantiate(Type))]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({unbound_variable, Id}) ->
+    Msg = io_lib:format("Unbound variable `~s`", [pp(Id)]),
+    case Id of
+        {qid, _, ["Chain", "event"]} ->
+            Cxt = "Did you forget to define the event type?",
+            mk_t_err(pos(Id), Msg, Cxt);
+        _ -> mk_t_err(pos(Id), Msg)
+    end;
+mk_error({undefined_field, Id}) ->
+    Msg = io_lib:format("Unbound field ~s", [pp(Id)]),
+    mk_t_err(pos(Id), Msg);
+mk_error({not_a_record_type, Type, Why}) ->
+    Msg = io_lib:format("Not a record type: `~s`", [pp_type(Type)]),
+    {Pos, Ctxt} = pp_why_record(Why),
+    mk_t_err(Pos, Msg, Ctxt);
+mk_error({not_a_contract_type, Type, Cxt}) ->
+    Msg =
+        case Type of
+            {tvar, _, _} ->
+                "Unresolved contract type";
+            _ ->
+                io_lib:format("The type `~s` is not a contract type", [pp_type(Type)])
+        end,
+    {Pos, Cxt1} =
+        case Cxt of
+            {var_args, Ann, Fun} ->
+                {pos(Ann),
+                 io_lib:format("when calling variadic function `~s`", [pp_expr(Fun)])};
+            {contract_literal, Lit} ->
+                {pos(Lit),
+                 io_lib:format("when checking that the contract literal `~s` has the type `~s`",
+                               [pp_expr(Lit), pp_type(Type)])};
+            {address_to_contract, Ann} ->
+                {pos(Ann),
+                 io_lib:format("when checking that the call to `Address.to_contract` has the type `~s`",
+                               [pp_type(Type)])}
+        end,
+    mk_t_err(Pos, Msg, Cxt1);
+mk_error({non_linear_pattern, Pattern, Nonlinear}) ->
+    Msg = io_lib:format("Repeated name~s ~s in the pattern `~s`",
+                        [plural("", "s", Nonlinear),
+                         string:join(lists:map(fun(F) -> "`" ++ F ++ "`" end, Nonlinear), ", "),
+                         pp_expr(Pattern)]),
+    mk_t_err(pos(Pattern), Msg);
+mk_error({ambiguous_record, Fields = [{_, First} | _], Candidates}) ->
+    Msg = io_lib:format("Ambiguous record type with field~s ~s could be one of~s",
+                        [plural("", "s", Fields),
+                         string:join([ "`" ++ pp(F) ++ "`" || {_, F} <- Fields ], ", "),
+                         [ ["\n  - ", "`" ++ pp(C) ++ "`", " (at ", pp_loc(C), ")"] || C <- Candidates ]]),
+    mk_t_err(pos(First), Msg);
+mk_error({missing_field, Field, Rec}) ->
+    Msg = io_lib:format("Record type `~s` does not have field `~s`",
+                        [pp(Rec), pp(Field)]),
+    mk_t_err(pos(Field), Msg);
+mk_error({missing_fields, Ann, RecType, Fields}) ->
+    Msg = io_lib:format("The field~s ~s ~s missing when constructing an element of type `~s`",
+                        [plural("", "s", Fields),
+                         string:join(lists:map(fun(F) -> "`" ++ F ++ "`" end, Fields), ", "),
+                         plural("is", "are", Fields), pp(RecType)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({no_records_with_all_fields, Fields = [{_, First} | _]}) ->
+    Msg = io_lib:format("No record type with field~s ~s",
+                        [plural("", "s", Fields),
+                         string:join([ "`" ++ pp(F) ++ "`" || {_, F} <- Fields ], ", ")]),
+    mk_t_err(pos(First), Msg);
+mk_error({recursive_types_not_implemented, Types}) ->
+    S = plural(" is", "s are mutually", Types),
+    Msg = io_lib:format("The following type~s recursive, which is not yet supported:~s",
+                        [S, [io_lib:format("\n  - `~s` (at ~s)", [pp(T), pp_loc(T)]) || T <- Types]]),
+    mk_t_err(pos(hd(Types)), Msg);
+mk_error({event_must_be_variant_type, Where}) ->
+    Msg = io_lib:format("The event type must be a variant type", []),
+    mk_t_err(pos(Where), Msg);
+mk_error({indexed_type_must_be_word, Type, Type}) ->
+    Msg = io_lib:format("The indexed type `~s` is not a word type",
+                        [pp_type(Type)]),
+    mk_t_err(pos(Type), Msg);
+mk_error({indexed_type_must_be_word, Type, Type1}) ->
+    Msg = io_lib:format("The indexed type `~s` equals `~s` which is not a word type",
+                        [pp_type(Type), pp_type(Type1)]),
+    mk_t_err(pos(Type), Msg);
+mk_error({event_0_to_3_indexed_values, Constr}) ->
+    Msg = io_lib:format("The event constructor `~s` has too many indexed values (max 3)",
+                        [name(Constr)]),
+    mk_t_err(pos(Constr), Msg);
+mk_error({event_0_to_1_string_values, Constr}) ->
+    Msg = io_lib:format("The event constructor `~s` has too many non-indexed values (max 1)",
+                        [name(Constr)]),
+    mk_t_err(pos(Constr), Msg);
+mk_error({repeated_constructor, Cs}) ->
+    Msg = io_lib:format("Variant types must have distinct constructor names~s",
+                        [[ io_lib:format("\n`~s`  (at ~s)", [pp_typed("  - ", C, T), pp_loc(C)]) || {C, T} <- Cs ]]),
+    mk_t_err(pos(element(1, hd(Cs))), Msg);
+mk_error({bad_named_argument, [], Name}) ->
+    Msg = io_lib:format("Named argument ~s supplied to function expecting no named arguments.",
+                        [pp(Name)]),
+    mk_t_err(pos(Name), Msg);
+mk_error({bad_named_argument, Args, Name}) ->
+    Msg = io_lib:format("Named argument `~s` is not one of the expected named arguments~s",
+                        [pp(Name),
+                        [ io_lib:format("\n  - `~s`", [pp_typed("", Arg, Type)])
+                          || {named_arg_t, _, Arg, Type, _} <- Args ]]),
+    mk_t_err(pos(Name), Msg);
+mk_error({unsolved_named_argument_constraint, #named_argument_constraint{name = Name, type = Type}}) ->
+    Msg = io_lib:format("Named argument ~s supplied to function with unknown named arguments.",
+                        [pp_typed("", Name, Type)]),
+    mk_t_err(pos(Name), Msg);
+mk_error({reserved_entrypoint, Name, Def}) ->
+    Msg = io_lib:format("The name '~s' is reserved and cannot be used for a "
+                        "top-level contract function.", [Name]),
+    mk_t_err(pos(Def), Msg);
+mk_error({duplicate_definition, Name, Locs}) ->
+    Msg = io_lib:format("Duplicate definitions of `~s` at~s",
+                        [Name, [ ["\n  - ", pp_loc(L)] || L <- Locs ]]),
+    mk_t_err(pos(lists:last(Locs)), Msg);
+mk_error({duplicate_scope, Kind, Name, OtherKind, L}) ->
+    Msg = io_lib:format("The ~p `~s` has the same name as a ~p at ~s",
+                        [Kind, pp(Name), OtherKind, pp_loc(L)]),
+    mk_t_err(pos(Name), Msg);
+mk_error({include, _, {string, Pos, Name}}) ->
+    Msg = io_lib:format("Include of `~s` is not allowed, include only allowed at top level.",
+                        [binary_to_list(Name)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Nested namespaces are not allowed. Namespace `~s` is not defined at top level.",
+                        [Name]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({Contract, _Pos, {con, Pos, Name}, _Impls, _Def}) when ?IS_CONTRACT_HEAD(Contract) ->
+    Msg = io_lib:format("Nested contracts are not allowed. Contract `~s` is not defined at top level.",
+                        [Name]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({type_decl, _, {id, Pos, Name}, _}) ->
+    Msg = io_lib:format("Empty type declarations are not supported. Type `~s` lacks a definition",
+                        [Name]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({letval, _Pos, {id, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Toplevel \"let\" definitions are not supported. Value `~s` could be replaced by 0-argument function.",
+                        [Name]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({stateful_not_allowed, Id, Fun}) ->
+    Msg = io_lib:format("Cannot reference stateful function `~s` in the definition of non-stateful function `~s`.",
+                        [pp(Id), pp(Fun)]),
+    mk_t_err(pos(Id), Msg);
+mk_error({stateful_not_allowed_in_guards, Id}) ->
+    Msg = io_lib:format("Cannot reference stateful function `~s` in a pattern guard.",
+                        [pp(Id)]),
+    mk_t_err(pos(Id), Msg);
+mk_error({value_arg_not_allowed, Value, Fun}) ->
+    Msg = io_lib:format("Cannot pass non-zero value argument `~s` in the definition of non-stateful function `~s`.",
+                        [pp_expr(Value), pp(Fun)]),
+    mk_t_err(pos(Value), Msg);
+mk_error({init_depends_on_state, Which, [_Init | Chain]}) ->
+    WhichCalls = fun("put") -> ""; ("state") -> ""; (_) -> ", which calls" end,
+    Msg = io_lib:format("The `init` function should return the initial state as its result and cannot ~s the state, but it calls~s",
+                        [if Which == put -> "write"; true -> "read" end,
+                         [ io_lib:format("\n  - `~s` (at ~s)~s", [Fun, pp_loc(Ann), WhichCalls(Fun)])
+                           || {[_, Fun], Ann} <- Chain]]),
+    mk_t_err(pos(element(2, hd(Chain))), Msg);
+mk_error({missing_body_for_let, Ann}) ->
+    Msg = io_lib:format("Let binding must be followed by an expression.", []),
+    mk_t_err(pos(Ann), Msg);
+mk_error({public_modifier_in_contract, Decl}) ->
+    Decl1 = mk_entrypoint(Decl),
+    Msg = io_lib:format("Use `entrypoint` instead of `function` for public function `~s`: `~s`",
+                        [pp_expr(element(3, Decl)),
+                         prettypr:format(aeso_pretty:decl(Decl1))]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({init_must_be_an_entrypoint, Decl}) ->
+    Decl1 = mk_entrypoint(Decl),
+    Msg = io_lib:format("The init function must be an entrypoint: ~s",
+                        [prettypr:format(prettypr:nest(2, aeso_pretty:decl(Decl1)))]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({init_must_not_be_payable, Decl}) ->
+    Msg = io_lib:format("The init function cannot be payable. "
+                        "You don't need the 'payable' annotation to be able to attach "
+                        "funds to the create contract transaction.",
+                        []),
+    mk_t_err(pos(Decl), Msg);
+mk_error({proto_must_be_entrypoint, Decl}) ->
+    Decl1 = mk_entrypoint(Decl),
+    Msg = io_lib:format("Use `entrypoint` for declaration of `~s`: `~s`",
+                        [pp_expr(element(3, Decl)),
+                         prettypr:format(aeso_pretty:decl(Decl1))]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({proto_in_namespace, Decl}) ->
+    Msg = io_lib:format("Namespaces cannot contain function prototypes.", []),
+    mk_t_err(pos(Decl), Msg);
+mk_error({entrypoint_in_namespace, Decl}) ->
+    Msg = io_lib:format("Namespaces cannot contain entrypoints. Use `function` instead.", []),
+    mk_t_err(pos(Decl), Msg);
+mk_error({private_entrypoint, Decl}) ->
+    Msg = io_lib:format("The entrypoint `~s` cannot be private. Use `function` instead.",
+                        [pp_expr(element(3, Decl))]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({private_and_public, Decl}) ->
+    Msg = io_lib:format("The function `~s` cannot be both public and private.",
+                        [pp_expr(element(3, Decl))]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({contract_has_no_entrypoints, Con}) ->
+    Msg = io_lib:format("The contract `~s` has no entrypoints. Since Sophia version 3.2, public "
+                        "contract functions must be declared with the `entrypoint` keyword instead of "
+                        "`function`.", [pp_expr(Con)]),
+    mk_t_err(pos(Con), Msg);
+mk_error({definition_in_contract_interface, Ann, {id, _, Id}}) ->
+    Msg = "Contract interfaces cannot contain defined functions or entrypoints.",
+    Cxt = io_lib:format("Fix: replace the definition of `~s` by a type signature.", [Id]),
+    mk_t_err(pos(Ann), Msg, Cxt);
+mk_error({unbound_type, Type}) ->
+    Msg = io_lib:format("Unbound type ~s.", [pp_type(Type)]),
+    mk_t_err(pos(Type), Msg);
+mk_error({new_tuple_syntax, Ann, Ts}) ->
+    Msg = io_lib:format("Invalid type `~s`. The syntax of tuple types changed in Sophia version 4.0. Did you mean `~s`",
+                        [pp_type({args_t, Ann, Ts}), pp_type({tuple_t, Ann, Ts})]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({map_in_map_key, Ann, KeyType}) ->
+    Msg = io_lib:format("Invalid key type `~s`", [pp_type(KeyType)]),
+    Cxt = "Map keys cannot contain other maps.",
+    mk_t_err(pos(Ann), Msg, Cxt);
+mk_error({cannot_call_init_function, Ann}) ->
+    Msg = "The 'init' function is called exclusively by the create contract transaction "
+          "and cannot be called from the contract code.",
+    mk_t_err(pos(Ann), Msg);
+mk_error({contract_treated_as_namespace, Ann, [Con, Fun] = QName}) ->
+    Msg = io_lib:format("Invalid call to contract entrypoint `~s`.", [string:join(QName, ".")]),
+    Cxt = io_lib:format("It must be called as `c.~s` for some `c : ~s`.", [Fun, Con]),
+    mk_t_err(pos(Ann), Msg, Cxt);
+mk_error({bad_top_level_decl, Decl}) ->
+    What = case element(1, Decl) of
+               letval -> "function or entrypoint";
+               _      -> "contract or namespace"
+           end,
+    Id = element(3, Decl),
+    Msg = io_lib:format("The definition of '~s' must appear inside a ~s.",
+                        [pp_expr(Id), What]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({unknown_byte_length, Type}) ->
+    Msg = io_lib:format("Cannot resolve length of byte array.", []),
+    mk_t_err(pos(Type), Msg);
+mk_error({unsolved_bytes_constraint, Ann, concat, A, B, C}) ->
+    Msg = io_lib:format("Failed to resolve byte array lengths in call to Bytes.concat with arguments of type\n"
+                        "~s  (at ~s)\n~s  (at ~s)\nand result type\n~s  (at ~s)",
+                        [pp_type("  - ", A), pp_loc(A), pp_type("  - ", B),
+                         pp_loc(B), pp_type("  - ", C), pp_loc(C)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({unsolved_bytes_constraint, Ann, split, A, B, C}) ->
+    Msg = io_lib:format("Failed to resolve byte array lengths in call to Bytes.split with argument of type\n"
+                        "~s  (at ~s)\nand result types\n~s  (at ~s)\n~s  (at ~s)",
+                        [ pp_type("  - ", C), pp_loc(C), pp_type("  - ", A), pp_loc(A),
+                          pp_type("  - ", B), pp_loc(B)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({failed_to_get_compiler_version, Err}) ->
+    Msg = io_lib:format("Failed to get compiler version. Error: ~p", [Err]),
+    mk_t_err(pos(0, 0), Msg);
+mk_error({compiler_version_mismatch, Ann, Version, Op, Bound}) ->
+    PrintV = fun(V) -> string:join([integer_to_list(N) || N <- V], ".") end,
+    Msg = io_lib:format("Cannot compile with this version of the compiler, "
+                        "because it does not satisfy the constraint"
+                        " ~s ~s ~s", [PrintV(Version), Op, PrintV(Bound)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({empty_record_or_map_update, Expr}) ->
+    Msg = io_lib:format("Empty record/map update `~s`", [pp_expr(Expr)]),
+    mk_t_err(pos(Expr), Msg);
+mk_error({mixed_record_and_map, Expr}) ->
+    Msg = io_lib:format("Mixed record fields and map keys in `~s`", [pp_expr(Expr)]),
+    mk_t_err(pos(Expr), Msg);
+mk_error({named_argument_must_be_literal_bool, Name, Arg}) ->
+    Msg = io_lib:format("Invalid `~s` argument `~s`. "
+                        "It must be either `true` or `false`.",
+                        [Name, pp_expr(instantiate(Arg))]),
+    mk_t_err(pos(Arg), Msg);
+mk_error({conflicting_updates_for_field, Upd, Key}) ->
+    Msg = io_lib:format("Conflicting updates for field '~s'", [Key]),
+    mk_t_err(pos(Upd), Msg);
+mk_error({ambiguous_main_contract, Ann}) ->
+    Msg = "Could not deduce the main contract. You can point it out manually with the `main` keyword.",
+    mk_t_err(pos(Ann), Msg);
+mk_error({main_contract_undefined, Ann}) ->
+    Msg = "No contract defined.",
+    mk_t_err(pos(Ann), Msg);
+mk_error({multiple_main_contracts, Ann}) ->
+    Msg = "Only one main contract can be defined.",
+    mk_t_err(pos(Ann), Msg);
+mk_error({unify_varargs, When}) ->
+    Msg = "Cannot infer types for variable argument list.",
+    {Pos, Ctxt} = pp_when(When),
+    mk_t_err(Pos, Msg, Ctxt);
+mk_error({clone_no_contract, Ann}) ->
+    Msg = "Chain.clone requires `ref` named argument of contract type.",
+    mk_t_err(pos(Ann), Msg);
+mk_error({contract_lacks_definition, Type, When}) ->
+    Msg = io_lib:format(
+            "~s is not implemented.",
+            [pp_type(Type)]
+           ),
+    {Pos, Ctxt} = pp_when(When),
+    mk_t_err(Pos, Msg, Ctxt);
+mk_error({ambiguous_name, Name, QIds}) ->
+    Msg = io_lib:format("Ambiguous name `~s` could be one of~s",
+                        [pp(Name),
+                         [io_lib:format("\n  - `~s` (at ~s)", [pp(QId), pp_loc(QId)]) || QId <- QIds]]),
+    mk_t_err(pos(Name), Msg);
+mk_error({using_undefined_namespace, Ann, Namespace}) ->
+    Msg = io_lib:format("Cannot use undefined namespace ~s", [Namespace]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({using_undefined_namespace_parts, Ann, Namespace, Parts}) ->
+    PartsStr = lists:concat(lists:join(", ", Parts)),
+    Msg = io_lib:format("The namespace ~s does not define the following names: ~s", [Namespace, PartsStr]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({unknown_warning, Warning}) ->
+    Msg = io_lib:format("Trying to report unknown warning: ~p", [Warning]),
+    mk_t_err(pos(0, 0), Msg);
+mk_error({empty_record_definition, Ann, Name}) ->
+    Msg = io_lib:format("Empty record definitions are not allowed. Cannot define the record `~s`", [Name]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({unimplemented_interface_function, ConId, InterfaceName, FunName}) ->
+    Msg = io_lib:format("Unimplemented entrypoint `~s` from the interface `~s` in the contract `~s`", [FunName, InterfaceName, pp(ConId)]),
+    mk_t_err(pos(ConId), Msg);
+mk_error({referencing_undefined_interface, InterfaceId}) ->
+    Msg = io_lib:format("Trying to implement or extend an undefined interface `~s`", [pp(InterfaceId)]),
+    mk_t_err(pos(InterfaceId), Msg);
+mk_error({missing_definition, Id}) ->
+    Msg = io_lib:format("Missing definition of function `~s`", [name(Id)]),
+    mk_t_err(pos(Id), Msg);
+mk_error({parameterized_state, Ann}) ->
+    Msg = "The state type cannot be parameterized",
+    mk_t_err(pos(Ann), Msg);
+mk_error({parameterized_event, Ann}) ->
+    Msg = "The event type cannot be parameterized",
+    mk_t_err(pos(Ann), Msg);
+mk_error({missing_init_function, Con}) ->
+    Msg = io_lib:format("Missing `init` function for the contract `~s`.", [name(Con)]),
+    Cxt = "The `init` function can only be omitted if the state type is `unit`",
+    mk_t_err(pos(Con), Msg, Cxt);
+mk_error({higher_order_entrypoint, Ann, {id, _, Name}, Thing}) ->
+    What = "higher-order (contains function types)",
+    ThingS = case Thing of
+                 {argument, X, T} -> io_lib:format("argument\n~s`\n", [pp_typed("  `", X, T)]);
+                 {result, T}      -> io_lib:format("return type\n~s`\n", [pp_type("  `", T)])
+             end,
+    Bad = case Thing of
+              {argument, _, _} -> io_lib:format("has a ~s type", [What]);
+              {result, _}      -> io_lib:format("is ~s", [What])
+          end,
+    Msg = io_lib:format("The ~sof entrypoint `~s` ~s",
+                        [ThingS, Name, Bad]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({invalid_aens_resolve_type, Ann, T}) ->
+    Msg = io_lib:format("Invalid return type of `AENS.resolve`:\n"
+                        "~s`\n"
+                        "It must be a `string` or a pubkey type (`address`, `oracle`, etc)",
+                        [pp_type("  `", T)]),
+    mk_t_err(pos(Ann), Msg);
+mk_error({invalid_oracle_type, Why, What, Ann, Type}) ->
+    WhyS = case Why of higher_order -> "higher-order (contain function types)";
+                       polymorphic  -> "polymorphic (contain type variables)" end,
+    Msg = io_lib:format("Invalid oracle type\n~s`", [pp_type("  `", Type)]),
+    Cxt = io_lib:format("The ~s type must not be ~s", [What, WhyS]),
+    mk_t_err(pos(Ann), Msg, Cxt);
+mk_error({interface_implementation_conflict, Contract, I1, I2, Fun}) ->
+    Msg = io_lib:format("Both interfaces `~s` and `~s` implemented by "
+                        "the contract `~s` have a function called `~s`",
+                        [name(I1), name(I2), name(Contract), name(Fun)]),
+    mk_t_err(pos(Contract), Msg);
+mk_error({function_should_be_entrypoint, Impl, Base, Interface}) ->
+    Msg = io_lib:format("`~s` must be declared as an entrypoint instead of a function "
+                        "in order to implement the entrypoint `~s` from the interface `~s`",
+                        [name(Impl), name(Base), name(Interface)]),
+    mk_t_err(pos(Impl), Msg);
+mk_error({entrypoint_cannot_be_stateful, Impl, Base, Interface}) ->
+    Msg = io_lib:format("`~s` cannot be stateful because the entrypoint `~s` in the "
+                        "interface `~s` is not stateful",
+                        [name(Impl), name(Base), name(Interface)]),
+    mk_t_err(pos(Impl), Msg);
+mk_error({entrypoint_must_be_payable, Impl, Base, Interface}) ->
+    Msg = io_lib:format("`~s` must be payable because the entrypoint `~s` in the "
+                        "interface `~s` is payable",
+                        [name(Impl), name(Base), name(Interface)]),
+    mk_t_err(pos(Impl), Msg);
+mk_error({unpreserved_payablity, Kind, ContractCon, InterfaceCon}) ->
+    KindStr = case Kind of
+                  contract -> "contract";
+                  contract_interface -> "interface"
+              end,
+    Msg = io_lib:format("Non-payable ~s `~s` cannot implement payable interface `~s`",
+                        [KindStr, name(ContractCon), name(InterfaceCon)]),
+    mk_t_err(pos(ContractCon), Msg);
+mk_error(Err) ->
+    Msg = io_lib:format("Unknown error: ~p", [Err]),
+    mk_t_err(pos(0, 0), Msg).
+
+mk_warning({unused_include, FileName, SrcFile}) ->
+    Msg = io_lib:format("The file `~s` is included but not used.", [FileName]),
+    aeso_warnings:new(aeso_errors:pos(SrcFile, 0, 0), Msg);
+mk_warning({unused_stateful, Ann, FunName}) ->
+    Msg = io_lib:format("The function `~s` is unnecessarily marked as stateful.", [name(FunName)]),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({unused_variable, Ann, _Namespace, _Fun, VarName}) ->
+    Msg = io_lib:format("The variable `~s` is defined but never used.", [VarName]),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({unused_typedef, Ann, QName, _Arity}) ->
+    Msg = io_lib:format("The type `~s` is defined but never used.", [lists:last(QName)]),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({unused_return_value, Ann}) ->
+    Msg = io_lib:format("Unused return value.", []),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({unused_function, Ann, FunName}) ->
+    Msg = io_lib:format("The function `~s` is defined but never used.", [FunName]),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({shadowing, Ann, VarName, AnnOld}) ->
+    Msg = io_lib:format("The definition of `~s` shadows an older definition at ~s.", [VarName, pp_loc(AnnOld)]),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({division_by_zero, Ann}) ->
+    Msg = io_lib:format("Division by zero.", []),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning({negative_spend, Ann}) ->
+    Msg = io_lib:format("Negative spend.", []),
+    aeso_warnings:new(pos(Ann), Msg);
+mk_warning(Warn) ->
+    Msg = io_lib:format("Unknown warning: ~p", [Warn]),
+    aeso_warnings:new(Msg).
+
+mk_entrypoint(Decl) ->
+    Ann   = [entrypoint | lists:keydelete(public, 1,
+                          lists:keydelete(private, 1,
+                            aeso_syntax:get_ann(Decl))) -- [public, private]],
+    aeso_syntax:set_ann(Ann, Decl).
+
+pp_when({todo, What}) -> {pos(0, 0), io_lib:format("[TODO] ~p", [What])};
+pp_when({at, Ann}) -> {pos(Ann), io_lib:format("at ~s", [pp_loc(Ann)])};
+pp_when({check_typesig, Name, Inferred, Given}) ->
+    {pos(Given),
+     io_lib:format("when checking the definition of `~s`\n"
+                   "  inferred type: `~s`\n"
+                   "  given type:    `~s`",
+         [Name, pp(instantiate(Inferred)), pp(instantiate(Given))])};
+pp_when({infer_app, Fun, NamedArgs, Args, Inferred0, ArgTypes0}) ->
+    Inferred = instantiate(Inferred0),
+    ArgTypes = instantiate(ArgTypes0),
+    {pos(Fun),
+     io_lib:format("when checking the application of\n"
+                   "  `~s`\n"
+                   "to arguments~s",
+                   [pp_typed("", Fun, Inferred),
+                    [ ["\n  ", "`" ++ pp_expr(NamedArg) ++ "`"] || NamedArg <- NamedArgs ] ++
+                    [ ["\n  ", "`" ++ pp_typed("", Arg, ArgT) ++ "`"]
+                       || {Arg, ArgT} <- lists:zip(Args, ArgTypes) ] ])};
+pp_when({field_constraint, FieldType0, InferredType0, Fld}) ->
+    FieldType    = instantiate(FieldType0),
+    InferredType = instantiate(InferredType0),
+    {pos(Fld),
+     case Fld of
+         {var_args, _Ann, _Fun} ->
+             io_lib:format("when checking contract construction of type\n~s (at ~s)\nagainst the expected type\n~s\n",
+                          [pp_type("  ", FieldType),
+                           pp_loc(Fld),
+                           pp_type("  ", InferredType)
+                          ]);
+         {field, _Ann, LV, Id, E} ->
+             io_lib:format("when checking the assignment of the field `~s` to the old value `~s` and the new value `~s`",
+                 [pp_typed("", {lvalue, [], LV}, FieldType),
+                  pp(Id),
+                  pp_typed("", E, InferredType)]);
+         {field, _Ann, LV, E} ->
+             io_lib:format("when checking the assignment of the field `~s` to the value `~s`",
+                 [pp_typed("", {lvalue, [], LV}, FieldType),
+                  pp_typed("", E, InferredType)]);
+         {proj, _Ann, _Rec, _Fld} ->
+             io_lib:format("when checking the record projection `~s` against the expected type `~s`",
+                 [pp_typed("  ", Fld, FieldType),
+                  pp_type("  ", InferredType)])
+     end};
+pp_when({record_constraint, RecType0, InferredType0, Fld}) ->
+    RecType      = instantiate(RecType0),
+    InferredType = instantiate(InferredType0),
+    {Pos, WhyRec} = pp_why_record(Fld),
+    case Fld of
+        {var_args, _Ann, _Fun} ->
+            {Pos,
+             io_lib:format("when checking that contract construction of type\n~s\n~s\n"
+                           "matches the expected type\n~s",
+                           [pp_type("  ", RecType), WhyRec, pp_type("  ", InferredType)]
+                          )
+            };
+        {field, _Ann, _LV, _Id, _E} ->
+            {Pos,
+             io_lib:format("when checking that the record type\n~s\n~s\n"
+                           "matches the expected type\n~s",
+                 [pp_type("  ", RecType), WhyRec, pp_type("  ", InferredType)])};
+        {field, _Ann, _LV, _E} ->
+            {Pos,
+             io_lib:format("when checking that the record type\n~s\n~s\n"
+                           "matches the expected type\n~s",
+                 [pp_type("  ", RecType), WhyRec, pp_type("  ", InferredType)])};
+        {proj, _Ann, Rec, _FldName} ->
+            {pos(Rec),
+             io_lib:format("when checking that the expression\n~s (at ~s)\nhas type\n~s\n~s",
+                 [pp_typed("  ", Rec, InferredType), pp_loc(Rec),
+                  pp_type("  ", RecType), WhyRec])}
+    end;
+pp_when({if_branches, Then, ThenType0, Else, ElseType0}) ->
+    {ThenType, ElseType} = instantiate({ThenType0, ElseType0}),
+    Branches = [ {Then, ThenType} | [ {B, ElseType} || B <- if_branches(Else) ] ],
+    {pos(element(1, hd(Branches))),
+     io_lib:format("when comparing the types of the if-branches\n"
+                   "~s", [ [ io_lib:format("~s (at ~s)\n", [pp_typed("  - ", B, BType), pp_loc(B)])
+                           || {B, BType} <- Branches ] ])};
+pp_when({case_pat, Pat, PatType0, ExprType0}) ->
+    {PatType, ExprType} = instantiate({PatType0, ExprType0}),
+    {pos(Pat),
+     io_lib:format("when checking the type of the pattern `~s` against the expected type `~s`",
+                   [pp_typed("", Pat, PatType),
+                    pp_type(ExprType)])};
+pp_when({check_expr, Expr, Inferred0, Expected0}) ->
+    {Inferred, Expected} = instantiate({Inferred0, Expected0}),
+    {pos(Expr),
+     io_lib:format("when checking the type of the expression `~s` against the expected type `~s`",
+                   [pp_typed("", Expr, Inferred), pp_type(Expected)])};
+pp_when({checking_init_type, Ann}) ->
+    {pos(Ann),
+     io_lib:format("when checking that `init` returns a value of type `state`", [])};
+pp_when({list_comp, BindExpr, Inferred0, Expected0}) ->
+    {Inferred, Expected} = instantiate({Inferred0, Expected0}),
+    {pos(BindExpr),
+     io_lib:format("when checking rvalue of list comprehension binding `~s` against type `~s`",
+                   [pp_typed("", BindExpr, Inferred), pp_type(Expected)])};
+pp_when({check_named_arg_constraint, C}) ->
+    {id, _, Name} = Arg = C#named_argument_constraint.name,
+    [Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- C#named_argument_constraint.args, Name1 == Name ],
+    Err = io_lib:format("when checking named argument `~s` against inferred type `~s`",
+                        [pp_typed("", Arg, Type), pp_type(C#named_argument_constraint.type)]),
+    {pos(Arg), Err};
+pp_when({checking_init_args, Ann, Con0, ArgTypes0}) ->
+    Con = instantiate(Con0),
+    ArgTypes = instantiate(ArgTypes0),
+    {pos(Ann),
+     io_lib:format("when checking arguments of `~s`'s init entrypoint to match\n(~s)",
+                   [pp_type(Con), string:join([pp_type(A) || A <- ArgTypes], ", ")])
+    };
+pp_when({return_contract, App, Con0}) ->
+    Con = instantiate(Con0),
+    {pos(App)
+    , io_lib:format("when checking that expression returns contract of type `~s`", [pp_type(Con)])
+    };
+pp_when({arg_name, Id1, Id2, When}) ->
+    {Pos, Ctx} = pp_when(When),
+    {Pos
+    , io_lib:format("when unifying names of named arguments: `~s` and `~s`\n~s", [pp_expr(Id1), pp_expr(Id2), Ctx])
+    };
+pp_when({var_args, Ann, Fun}) ->
+    {pos(Ann)
+    , io_lib:format("when resolving arguments of variadic function `~s`", [pp_expr(Fun)])
+    };
+pp_when(unknown) -> {pos(0,0), ""}.
+
+-spec pp_why_record(why_record()) -> {pos(), iolist()}.
+pp_why_record({var_args, Ann, Fun}) ->
+    {pos(Ann),
+     io_lib:format("arising from resolution of variadic function `~s`",
+                   [pp_expr(Fun)])};
+pp_why_record(Fld = {field, _Ann, LV, _E}) ->
+    {pos(Fld),
+     io_lib:format("arising from an assignment of the field `~s`",
+                   [pp_expr({lvalue, [], LV})])};
+pp_why_record(Fld = {field, _Ann, LV, _Alias, _E}) ->
+    {pos(Fld),
+     io_lib:format("arising from an assignment of the field `~s`",
+                   [pp_expr({lvalue, [], LV})])};
+pp_why_record({proj, _Ann, Rec, FldName}) ->
+    {pos(Rec),
+     io_lib:format("arising from the projection of the field `~s`",
+         [pp(FldName)])}.
+
+
+if_branches(If = {'if', Ann, _, Then, Else}) ->
+    case proplists:get_value(format, Ann) of
+        elif -> [Then | if_branches(Else)];
+        _    -> [If]
+    end;
+if_branches(E) -> [E].
+
+pp_typed(Label, E, T = {type_sig, _, _, _, _, _}) -> pp_typed(Label, E, typesig_to_fun_t(T));
+pp_typed(Label, {typed, _, Expr, _}, Type) ->
+    pp_typed(Label, Expr, Type);
+pp_typed(Label, Expr, Type) ->
+    pp_expr(Label, {typed, [], Expr, Type}).
+
+pp_expr(Expr) ->
+    pp_expr("", Expr).
+pp_expr(Label, Expr) ->
+    prettypr:format(prettypr:beside(prettypr:text(Label), aeso_pretty:expr(Expr, [show_generated])), 80, 80).
+
+pp_type(Type) ->
+    pp_type("", Type).
+pp_type(Label, Type) ->
+    prettypr:format(prettypr:beside(prettypr:text(Label), aeso_pretty:type(Type, [show_generated])), 80, 80).
+
+src_file(T)      -> aeso_syntax:get_ann(file, T, no_file).
+include_type(T)  -> aeso_syntax:get_ann(include_type, T, none).
+line_number(T)   -> aeso_syntax:get_ann(line, T, 0).
+column_number(T) -> aeso_syntax:get_ann(col, T, 0).
+
+pos(T)    -> aeso_errors:pos(src_file(T), line_number(T), column_number(T)).
+pos(L, C) -> aeso_errors:pos(L, C).
+
+loc(T) ->
+    {src_file(T), include_type(T), line_number(T), column_number(T)}.
+
+pp_loc(T) ->
+    {File, IncludeType, Line, Col} = loc(T),
+    case {Line, Col} of
+        {0, 0} -> "(builtin location)";
+        _      -> case IncludeType of
+                      none -> io_lib:format("line ~p, column ~p", [Line, Col]);
+                      _    -> io_lib:format("line ~p, column ~p in ~s", [Line, Col, File])
+                  end
+    end.
+
+plural(No, _Yes, [_]) -> No;
+plural(_No, Yes, _)   -> Yes.
+
+pp(T = {type_sig, _, _, _, _, _}) ->
+    pp(typesig_to_fun_t(T));
+pp([]) ->
+    "";
+pp([T]) ->
+    pp(T);
+pp([T|Ts]) ->
+    [pp(T), ", "|pp(Ts)];
+pp({id, _, Name}) ->
+    Name;
+pp({qid, _, Name}) ->
+    string:join(Name, ".");
+pp({con, _, Name}) ->
+    Name;
+pp({qcon, _, Name}) ->
+    string:join(Name, ".");
+pp({uvar, _, Ref}) ->
+    %% Show some unique representation
+    ["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
+pp({tvar, _, Name}) ->
+    Name;
+pp({if_t, _, Id, Then, Else}) ->
+    ["if(", pp([Id, Then, Else]), ")"];
+pp({tuple_t, _, []}) ->
+    "unit";
+pp({tuple_t, _, Cpts}) ->
+    ["(", string:join(lists:map(fun pp/1, Cpts), " * "), ")"];
+pp({bytes_t, _, any}) -> "bytes(_)";
+pp({bytes_t, _, Len}) ->
+    ["bytes(", integer_to_list(Len), ")"];
+pp({app_t, _, T, []}) ->
+    pp(T);
+pp({app_t, _, Type, Args}) ->
+    [pp(Type), "(", pp(Args), ")"];
+pp({named_arg_t, _, Name, Type, _Default}) ->
+    [pp(Name), " : ", pp(Type)];
+pp({fun_t, _, Named = {uvar, _, _}, As, B}) ->
+    ["(", pp(Named), " | ", pp(As), ") => ", pp(B)];
+pp({fun_t, _, Named, As, B}) when is_list(Named) ->
+    ["(", pp(Named ++ As), ") => ", pp(B)];
+pp(Other) ->
+    io_lib:format("~p", [Other]).
+
+
+plural(No, _Yes, [_]) -> No;
+plural(_No, Yes, _)   -> Yes.

src/aeso_ast_types_solve.erl

@@ -0,0 +1,344 @@
+-module(aeso_ast_types_solve).
+
+
+
+-spec solve_constraints(env()) -> ok.
+solve_constraints(Env) ->
+    %% First look for record fields that appear in only one type definition
+    IsAmbiguous =
+        fun(#field_constraint{
+               record_t = RecordType,
+               field    = Field={id, _Attrs, FieldName},
+               field_t  = FieldType,
+               kind     = Kind,
+               context  = When }) ->
+                Arity = fun_arity(dereference_deep(FieldType)),
+                FieldInfos = case Arity of
+                                 none -> lookup_record_field(Env, FieldName, Kind);
+                                 _    -> lookup_record_field_arity(Env, FieldName, Arity, Kind)
+                             end,
+                case FieldInfos of
+                    [] ->
+                        type_error({undefined_field, Field}),
+                        false;
+                    [#field_info{field_t = FldType, record_t = RecType}] ->
+                        create_freshen_tvars(),
+                        FreshFldType = freshen(FldType),
+                        FreshRecType = freshen(RecType),
+                        destroy_freshen_tvars(),
+                        unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
+                        unify(Env, FreshRecType, RecordType, {record_constraint, FreshRecType, RecordType, When}),
+                        false;
+                    _ ->
+                        %% ambiguity--need cleverer strategy
+                        true
+                end;
+           (_) -> true
+        end,
+    AmbiguousConstraints = lists:filter(IsAmbiguous, get_constraints()),
+
+    % The two passes on AmbiguousConstraints are needed
+    solve_ambiguous_constraints(Env, AmbiguousConstraints ++ AmbiguousConstraints).
+
+-spec solve_ambiguous_constraints(env(), [constraint()]) -> ok.
+solve_ambiguous_constraints(Env, Constraints) ->
+    Unknown = solve_known_record_types(Env, Constraints),
+    if Unknown == [] -> ok;
+       length(Unknown) < length(Constraints) ->
+            %% progress! Keep trying.
+            solve_ambiguous_constraints(Env, Unknown);
+       true ->
+            case solve_unknown_record_types(Env, Unknown) of
+                true -> %% Progress!
+                    solve_ambiguous_constraints(Env, Unknown);
+                _ -> ok %% No progress. Report errors later.
+            end
+    end.
+
+solve_then_destroy_and_report_unsolved_constraints(Env) ->
+    solve_constraints(Env),
+    destroy_and_report_unsolved_constraints(Env).
+
+destroy_and_report_unsolved_constraints(Env) ->
+    {FieldCs, OtherCs} =
+        lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
+                        get_constraints()),
+    {CreateCs, OtherCs1} =
+        lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
+                        OtherCs),
+    {ContractCs, OtherCs2} =
+        lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
+    {NamedArgCs, OtherCs3} =
+        lists:partition(fun(#dependent_type_constraint{}) -> true;
+                           (#named_argument_constraint{}) -> true;
+                           (_)                            -> false
+                        end, OtherCs2),
+    {BytesCs, OtherCs4} =
+        lists:partition(fun({is_bytes, _})              -> true;
+                           ({add_bytes, _, _, _, _, _}) -> true;
+                           (_)                          -> false
+                        end, OtherCs3),
+    {AensResolveCs, OtherCs5} =
+        lists:partition(fun({aens_resolve_type, _}) -> true;
+                           (_)                      -> false
+                        end, OtherCs4),
+    {OracleTypeCs, []} =
+        lists:partition(fun({oracle_type, _, _}) -> true;
+                           (_)                   -> false
+                        end, OtherCs5),
+
+    Unsolved = [ S || S <- [ solve_constraint(Env, dereference_deep(C)) || C <- NamedArgCs ],
+                      S == unsolved ],
+    [ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
+
+    Unknown = solve_known_record_types(Env, FieldCs),
+    if Unknown == [] -> ok;
+       true ->
+            case solve_unknown_record_types(Env, Unknown) of
+                true   -> ok;
+                Errors -> [ type_error(Err) || Err <- Errors ]
+            end
+    end,
+
+    check_record_create_constraints(Env, CreateCs),
+    check_is_contract_constraints(Env, ContractCs),
+    check_bytes_constraints(Env, BytesCs),
+    check_aens_resolve_constraints(Env, AensResolveCs),
+    check_oracle_type_constraints(Env, OracleTypeCs),
+
+    destroy_constraints().
+
+%% If false, a type error has been emitted, so it's safe to drop the constraint.
+-spec check_named_argument_constraint(env(), named_argument_constraint()) -> true | false | unsolved.
+check_named_argument_constraint(_Env, #named_argument_constraint{ args = {uvar, _, _} }) ->
+    unsolved;
+check_named_argument_constraint(Env,
+        C = #named_argument_constraint{ args = Args,
+                                        name = Id = {id, _, Name},
+                                        type = Type }) ->
+    case [ T || {named_arg_t, _, {id, _, Name1}, T, _} <- Args, Name1 == Name ] of
+        []  ->
+            type_error({bad_named_argument, Args, Id}),
+            false;
+        [T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true
+    end;
+check_named_argument_constraint(Env,
+        #dependent_type_constraint{ named_args_t = NamedArgsT0,
+                                    named_args = NamedArgs,
+                                    general_type = GenType,
+                                    specialized_type = SpecType,
+                                    context = {check_return, App} }) ->
+    NamedArgsT = dereference(NamedArgsT0),
+    case dereference(NamedArgsT0) of
+        [_ | _] = NamedArgsT ->
+            GetVal = fun(Name, Default) ->
+                        hd([ Val || {named_arg, _, {id, _, N}, Val} <- NamedArgs, N == Name] ++
+                           [ Default ])
+                     end,
+            ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)}
+                                      || {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]),
+            GenType1 = specialize_dependent_type(ArgEnv, GenType),
+            unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}),
+            true;
+        _ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true
+    end.
+
+solve_constraint(_Env, #field_constraint{record_t = {uvar, _, _}}) ->
+    not_solved;
+solve_constraint(Env, C = #field_constraint{record_t = RecType,
+                                            field    = FieldName,
+                                            field_t  = FieldType,
+                                            context  = When}) ->
+    RecId = record_type_name(RecType),
+    Attrs = aeso_syntax:get_ann(RecId),
+    case lookup_type(Env, RecId) of
+        {_, {_Ann, {Formals, {What, Fields}}}} when What =:= record_t; What =:= contract_t ->
+            FieldTypes = [{Name, Type} || {field_t, _, {id, _, Name}, Type} <- Fields],
+            {id, _, FieldString} = FieldName,
+            case proplists:get_value(FieldString, FieldTypes) of
+                undefined ->
+                    type_error({missing_field, FieldName, RecId}),
+                    not_solved;
+                FldType ->
+                    create_freshen_tvars(),
+                    FreshFldType = freshen(FldType),
+                    FreshRecType = freshen(app_t(Attrs, RecId, Formals)),
+                    destroy_freshen_tvars(),
+                    unify(Env, FreshFldType, FieldType, {field_constraint, FreshFldType, FieldType, When}),
+                    unify(Env, FreshRecType, RecType, {record_constraint, FreshRecType, RecType, When}),
+                    C
+            end;
+        _ ->
+            type_error({not_a_record_type, instantiate(RecType), When}),
+            not_solved
+    end;
+solve_constraint(Env, C = #dependent_type_constraint{}) ->
+    check_named_argument_constraint(Env, C);
+solve_constraint(Env, C = #named_argument_constraint{}) ->
+    check_named_argument_constraint(Env, C);
+solve_constraint(_Env, {is_bytes, _}) -> ok;
+solve_constraint(Env, {add_bytes, Ann, _, A0, B0, C0}) ->
+    A = unfold_types_in_type(Env, dereference(A0)),
+    B = unfold_types_in_type(Env, dereference(B0)),
+    C = unfold_types_in_type(Env, dereference(C0)),
+    case {A, B, C} of
+        {{bytes_t, _, M}, {bytes_t, _, N}, _} -> unify(Env, {bytes_t, Ann, M + N}, C, {at, Ann});
+        {{bytes_t, _, M}, _, {bytes_t, _, R}} when R >= M -> unify(Env, {bytes_t, Ann, R - M}, B, {at, Ann});
+        {_, {bytes_t, _, N}, {bytes_t, _, R}} when R >= N -> unify(Env, {bytes_t, Ann, R - N}, A, {at, Ann});
+        _ -> ok
+    end;
+solve_constraint(_, _) -> ok.
+
+check_bytes_constraints(Env, Constraints) ->
+    InAddConstraint = [ T || {add_bytes, _, _, A, B, C} <- Constraints,
+                             T <- [A, B, C],
+                             element(1, T) /= bytes_t ],
+    %% Skip is_bytes constraints for types that occur in add_bytes constraints
+    %% (no need to generate error messages for both is_bytes and add_bytes).
+    Skip = fun({is_bytes, T}) -> lists:member(T, InAddConstraint);
+              (_) -> false end,
+    [ check_bytes_constraint(Env, C) || C <- Constraints, not Skip(C) ].
+
+check_bytes_constraint(Env, {is_bytes, Type}) ->
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    case Type1 of
+        {bytes_t, _, _} -> ok;
+        _               ->
+            type_error({unknown_byte_length, Type})
+    end;
+check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->
+    A = unfold_types_in_type(Env, instantiate(A0)),
+    B = unfold_types_in_type(Env, instantiate(B0)),
+    C = unfold_types_in_type(Env, instantiate(C0)),
+    case {A, B, C} of
+        {{bytes_t, _, _M}, {bytes_t, _, _N}, {bytes_t, _, _R}} ->
+            ok; %% If all are solved we checked M + N == R in solve_constraint.
+        _ -> type_error({unsolved_bytes_constraint, Ann, Fun, A, B, C})
+    end.
+
+check_aens_resolve_constraints(_Env, []) ->
+    ok;
+check_aens_resolve_constraints(Env, [{aens_resolve_type, Type} | Rest]) ->
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    {app_t, _, {id, _, "option"}, [Type2]} = Type1,
+    case Type2 of
+        {id, _, "string"} -> ok;
+        {id, _, "address"} -> ok;
+        {con, _, _} -> ok;
+        {app_t, _, {id, _, "oracle"}, [_, _]} -> ok;
+        {app_t, _, {id, _, "oracle_query"}, [_, _]} -> ok;
+        _ -> type_error({invalid_aens_resolve_type, aeso_syntax:get_ann(Type), Type2})
+    end,
+    check_aens_resolve_constraints(Env, Rest).
+
+check_oracle_type_constraints(_Env, []) ->
+    ok;
+check_oracle_type_constraints(Env, [{oracle_type, Ann, OType} | Rest]) ->
+    Type = unfold_types_in_type(Env, instantiate(OType)),
+    {app_t, _, {id, _, "oracle"}, [QType, RType]} = Type,
+    ensure_monomorphic(QType, {invalid_oracle_type, polymorphic,  query,    Ann, Type}),
+    ensure_monomorphic(RType, {invalid_oracle_type, polymorphic,  response, Ann, Type}),
+    ensure_first_order(QType, {invalid_oracle_type, higher_order, query,    Ann, Type}),
+    ensure_first_order(RType, {invalid_oracle_type, higher_order, response, Ann, Type}),
+    check_oracle_type_constraints(Env, Rest).
+
+%% -- Field constraints --
+
+check_record_create_constraints(_, []) -> ok;
+check_record_create_constraints(Env, [C | Cs]) ->
+    #record_create_constraint{
+        record_t = Type,
+        fields   = Fields,
+        context  = When } = C,
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    try lookup_type(Env, record_type_name(Type1)) of
+        {_QId, {_Ann, {_Args, {record_t, RecFields}}}} ->
+            ActualNames = [ Fld || {field_t, _, {id, _, Fld}, _} <- RecFields ],
+            GivenNames  = [ Fld || {id, _, Fld} <- Fields ],
+            case ActualNames -- GivenNames of   %% We know already that we don't have too many fields
+                []      -> ok;
+                Missing -> type_error({missing_fields, When, Type1, Missing})
+            end;
+        _ -> %% We can get here if there are other type errors.
+            ok
+    catch _:_ ->    %% Might be unsolved, we get a different error in that case
+        ok
+    end,
+    check_record_create_constraints(Env, Cs).
+
+check_is_contract_constraints(_Env, []) -> ok;
+check_is_contract_constraints(Env, [C | Cs]) ->
+    #is_contract_constraint{ contract_t = Type, context = Cxt, force_def = ForceDef } = C,
+    Type1 = unfold_types_in_type(Env, instantiate(Type)),
+    TypeName = record_type_name(Type1),
+    case lookup_type(Env, TypeName) of
+        {_, {_Ann, {[], {contract_t, _}}}} ->
+            case not ForceDef orelse is_contract_defined(TypeName) of
+                true -> ok;
+                false -> type_error({contract_lacks_definition, Type1, Cxt})
+                end;
+        _ -> type_error({not_a_contract_type, Type1, Cxt})
+    end,
+    check_is_contract_constraints(Env, Cs).
+
+-spec solve_unknown_record_types(env(), [field_constraint()]) -> true | [tuple()].
+solve_unknown_record_types(Env, Unknown) ->
+    UVars = lists:usort([UVar || #field_constraint{record_t = UVar = {uvar, _, _}} <- Unknown]),
+    Solutions = [solve_for_uvar(Env, UVar, [{Kind, When, Field}
+                                            || #field_constraint{record_t = U, field = Field, kind = Kind, context = When} <- Unknown,
+                                               U == UVar])
+                 || UVar <- UVars],
+    case lists:member(true, Solutions) of
+        true  -> true;
+        false -> Solutions
+    end.
+
+%% This will solve all kinds of constraints but will only return the
+%% unsolved field constraints
+-spec solve_known_record_types(env(), [constraint()]) -> [field_constraint()].
+solve_known_record_types(Env, Constraints) ->
+    DerefConstraints = lists:map(fun(C = #field_constraint{record_t = RecordType}) ->
+                                        C#field_constraint{record_t = dereference(RecordType)};
+                                    (C) -> dereference_deep(C)
+                                 end, Constraints),
+    SolvedConstraints = lists:map(fun(C) -> solve_constraint(Env, dereference_deep(C)) end, DerefConstraints),
+    Unsolved = DerefConstraints--SolvedConstraints,
+    lists:filter(fun(#field_constraint{}) -> true; (_) -> false end, Unsolved).
+
+solve_for_uvar(Env, UVar = {uvar, Attrs, _}, Fields0) ->
+    Fields = [{Kind, Fld} || {Kind, _, Fld} <- Fields0],
+    [{_, When, _} | _] = Fields0,    %% Get the location from the first field
+    %% If we have 'create' constraints they must be complete.
+    Covering = lists:usort([ Name || {create, {id, _, Name}} <- Fields ]),
+    %% Does this set of fields uniquely identify a record type?
+    FieldNames = [ Name || {_Kind, {id, _, Name}} <- Fields ],
+    UniqueFields = lists:usort(FieldNames),
+    Candidates = [RecType || #field_info{record_t = RecType} <- lookup_record_field(Env, hd(FieldNames))],
+    TypesAndFields = [case lookup_type(Env, record_type_name(RecType)) of
+                        {_, {_, {_, {record_t, RecFields}}}} ->
+                            {RecType, [Field || {field_t, _, {id, _, Field}, _} <- RecFields]};
+                        {_, {_, {_, {contract_t, ConFields}}}} ->
+                            %% TODO: is this right?
+                            {RecType, [Field || {field_t, _, {id, _, Field}, _} <- ConFields]};
+                        false -> %% impossible?
+                            error({no_definition_for, record_type_name(RecType), in, Env})
+                      end
+                      || RecType <- Candidates],
+    PartialSolutions =
+        lists:sort([{RecType, if Covering == [] -> []; true -> RecFields -- Covering end}
+                    || {RecType, RecFields} <- TypesAndFields,
+                       UniqueFields -- RecFields == []]),
+    Solutions = [RecName || {RecName, []} <- PartialSolutions],
+
+
+apply_typesig_constraint(_Ann, none, _FunT) -> ok;
+apply_typesig_constraint(Ann, address_to_contract, {fun_t, _, [], [_], Type}) ->
+    add_constraint([#is_contract_constraint{ contract_t = Type,
+                                        context    = {address_to_contract, Ann}}]);
+apply_typesig_constraint(Ann, bytes_concat, {fun_t, _, [], [A, B], C}) ->
+    add_constraint({add_bytes, Ann, concat, A, B, C});
+apply_typesig_constraint(Ann, bytes_split, {fun_t, _, [], [C], {tuple_t, _, [A, B]}}) ->
+    add_constraint({add_bytes, Ann, split, A, B, C});
+apply_typesig_constraint(Ann, bytecode_hash, {fun_t, _, _, [Con], _}) ->
+    add_constraint([#is_contract_constraint{ contract_t = Con,
+                                        context    = {bytecode_hash, Ann} }]).

src/aeso_code_errors.erl

@@ -1,94 +0,0 @@
-%%%-------------------------------------------------------------------
-%%% @author Ulf Norell
-%%% @copyright (C) 2019, Aeternity Anstalt
-%%% @doc
-%%%     Formatting of code generation errors.
-%%% @end
-%%%
-%%%-------------------------------------------------------------------
--module(aeso_code_errors).
-
--export([format/1, pos/1]).
-
-format({last_declaration_must_be_main_contract, Decl = {Kind, _, {con, _, C}, _}}) ->
-    Msg = io_lib:format("Expected a main contract as the last declaration instead of the ~p '~s'",
-                        [Kind, C]),
-    mk_err(pos(Decl), Msg);
-format({missing_init_function, Con}) ->
-    Msg = io_lib:format("Missing init function for the contract '~s'.", [pp_expr(Con)]),
-    Cxt = "The 'init' function can only be omitted if the state type is 'unit'.",
-    mk_err(pos(Con), Msg, Cxt);
-format({missing_definition, Id}) ->
-    Msg = io_lib:format("Missing definition of function '~s'.", [pp_expr(Id)]),
-    mk_err(pos(Id), Msg);
-format({parameterized_state, Decl}) ->
-    Msg = "The state type cannot be parameterized.",
-    mk_err(pos(Decl), Msg);
-format({parameterized_event, Decl}) ->
-    Msg = "The event type cannot be parameterized.",
-    mk_err(pos(Decl), Msg);
-format({invalid_entrypoint, Why, Ann, {id, _, Name}, Thing}) ->
-    What = case Why of higher_order -> "higher-order (contains function types)";
-                       polymorphic  -> "polymorphic (contains type variables)" end,
-    ThingS = case Thing of
-                 {argument, X, T} -> io_lib:format("argument\n~s\n", [pp_typed(X, T)]);
-                 {result, T}      -> io_lib:format("return type\n~s\n", [pp_type(2, T)])
-             end,
-    Bad = case Thing of
-              {argument, _, _} -> io_lib:format("has a ~s type", [What]);
-              {result, _}      -> io_lib:format("is ~s", [What])
-          end,
-    Msg = io_lib:format("The ~sof entrypoint '~s' ~s.",
-                        [ThingS, Name, Bad]),
-    case Why of
-        higher_order -> mk_err(pos(Ann), Msg)
-    end;
-format({invalid_aens_resolve_type, Ann, T}) ->
-    Msg = io_lib:format("Invalid return type of AENS.resolve:\n"
-                        "~s\n"
-                        "It must be a string or a pubkey type (address, oracle, etc).",
-                        [pp_type(2, T)]),
-    mk_err(pos(Ann), Msg);
-format({invalid_oracle_type, Why, What, Ann, Type}) ->
-    WhyS = case Why of higher_order -> "higher-order (contain function types)";
-                       polymorphic  -> "polymorphic (contain type variables)" end,
-    Msg = io_lib:format("Invalid oracle type\n~s", [pp_type(2, Type)]),
-    Cxt = io_lib:format("The ~s type must not be ~s.", [What, WhyS]),
-    mk_err(pos(Ann), Msg, Cxt);
-format({var_args_not_set, Expr}) ->
-    mk_err( pos(Expr), "Could not deduce type of variable arguments list"
-          , "When compiling " ++ pp_expr(Expr)
-          );
-format({found_void, Ann}) ->
-    mk_err(pos(Ann), "Found a void-typed value.", "`void` is a restricted, uninhabited type. Did you mean `unit`?");
-
-format(Err) ->
-    mk_err(aeso_errors:pos(0, 0), io_lib:format("Unknown error: ~p\n", [Err])).
-
-pos(Ann) ->
-    File = aeso_syntax:get_ann(file, Ann, no_file),
-    Line = aeso_syntax:get_ann(line, Ann, 0),
-    Col  = aeso_syntax:get_ann(col, Ann, 0),
-    aeso_errors:pos(File, Line, Col).
-
-pp_typed(E, T) ->
-    prettypr:format(prettypr:nest(2,
-    lists:foldr(fun prettypr:beside/2, prettypr:empty(),
-                [aeso_pretty:expr(E), prettypr:text(" : "),
-                 aeso_pretty:type(T)]))).
-
-pp_expr(E) ->
-    pp_expr(0, E).
-
-pp_expr(N, E) ->
-    prettypr:format(prettypr:nest(N, aeso_pretty:expr(E))).
-
-pp_type(N, T) ->
-    prettypr:format(prettypr:nest(N, aeso_pretty:type(T))).
-
-mk_err(Pos, Msg) ->
-    aeso_errors:new(code_error, Pos, lists:flatten(Msg)).
-
-mk_err(Pos, Msg, Cxt) ->
-    aeso_errors:new(code_error, Pos, lists:flatten(Msg), lists:flatten(Cxt)).
-

src/aeso_compiler.erl

@@ -29,11 +29,10 @@
 -include("aeso_utils.hrl").
 
 
--type option() :: pp_sophia_code
-                | pp_ast
+-type option() :: pp_ast
                 | pp_types
                 | pp_typed_ast
-                | pp_assembler
+                | pp_fate
                 | no_code
                 | keep_included
                 | debug_mode
@@ -112,11 +111,13 @@ from_string(ContractString, Options) ->
 
 from_string1(ContractString, Options) ->
     #{ fcode := FCode
-     , fcode_env := #{child_con_env := ChildContracts}
+     , fcode_env := FCodeEnv
      , folded_typed_ast := FoldedTypedAst
      , warnings := Warnings } = string_to_code(ContractString, Options),
-    FateCode = aeso_fcode_to_fate:compile(ChildContracts, FCode, Options),
-    pp_assembler(FateCode, Options),
+    #{ child_con_env := ChildContracts } = FCodeEnv,
+    SavedFreshNames = maps:get(saved_fresh_names, FCodeEnv, #{}),
+    {FateCode, VarsRegs} = aeso_fcode_to_fate:compile(ChildContracts, FCode, SavedFreshNames, Options),
+    pp_fate(FateCode, Options),
     ByteCode = aeb_fate_code:serialize(FateCode, []),
     {ok, Version} = version(),
     Res = #{byte_code => ByteCode,
@@ -128,7 +129,13 @@ from_string1(ContractString, Options) ->
             payable => maps:get(payable, FCode),
             warnings => Warnings
            },
-    {ok, maybe_generate_aci(Res, FoldedTypedAst, Options)}.
+    ResDbg = Res#{variables_registers => VarsRegs},
+    FinalRes =
+        case proplists:get_value(debug_info, Options, false) of
+            true  -> ResDbg;
+            false -> Res
+        end,
+    {ok, maybe_generate_aci(FinalRes, FoldedTypedAst, Options)}.
 
 maybe_generate_aci(Result, FoldedTypedAst, Options) ->
     case proplists:get_value(aci, Options) of
@@ -142,7 +149,6 @@ maybe_generate_aci(Result, FoldedTypedAst, Options) ->
 -spec string_to_code(string(), options()) -> map().
 string_to_code(ContractString, Options) ->
     Ast = parse(ContractString, Options),
-    pp_sophia_code(Ast, Options),
     pp_ast(Ast, Options),
     {TypeEnv, FoldedTypedAst, UnfoldedTypedAst, Warnings} = aeso_ast_infer_types:infer(Ast, [return_env | Options]),
     pp_typed_ast(UnfoldedTypedAst, Options),
@@ -185,7 +191,7 @@ check_call1(ContractString0, FunName, Args, Options) ->
         #{fcode := OrgFcode
         , fcode_env := #{child_con_env := ChildContracts}
         , ast := Ast} = string_to_code(ContractString0, Options),
-        FateCode = aeso_fcode_to_fate:compile(ChildContracts, OrgFcode, []),
+        {FateCode, _} = aeso_fcode_to_fate:compile(ChildContracts, OrgFcode, #{}, []),
         %% collect all hashes and compute the first name without hash collision to
         SymbolHashes = maps:keys(aeb_fate_code:symbols(FateCode)),
         CallName = first_none_match(?CALL_NAME, SymbolHashes,
@@ -238,8 +244,8 @@ insert_init_function(Code, Options) ->
 
 last_contract_indent(Decls) ->
     case lists:last(Decls) of
-        {_, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
-        _                     -> 0
+        {_, _, _, _, [Decl | _]} -> aeso_syntax:get_ann(col, Decl, 1) - 1;
+        _                        -> 0
     end.
 
 -spec to_sophia_value(string(), string(), ok | error | revert, binary()) ->
@@ -338,7 +344,7 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
     end.
 
 -dialyzer({nowarn_function, get_decode_type/2}).
-get_decode_type(FunName, [{Contract, Ann, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
+get_decode_type(FunName, [{Contract, Ann, _, _, Defs}]) when ?IS_CONTRACT_HEAD(Contract) ->
     GetType = fun({letfun, _, {id, _, Name}, Args, Ret, _})               when Name == FunName -> [{Args, Ret}];
                  ({fun_decl, _, {id, _, Name}, {fun_t, _, _, Args, Ret}}) when Name == FunName -> [{Args, Ret}];
                  (_) -> [] end,
@@ -349,7 +355,7 @@ get_decode_type(FunName, [{Contract, Ann, _, Defs}]) when ?IS_CONTRACT_HEAD(Cont
                 "init" -> {ok, [], {tuple_t, [], []}};
                  _ ->
                     Msg = io_lib:format("Function '~s' is missing in contract", [FunName]),
-                    Pos = aeso_code_errors:pos(Ann),
+                    Pos = aeso_errors:pos(Ann),
                     aeso_errors:throw(aeso_errors:new(data_error, Pos, Msg))
             end
     end;
@@ -357,21 +363,22 @@ get_decode_type(FunName, [_ | Contracts]) ->
     %% The __decode should be in the final contract
     get_decode_type(FunName, Contracts).
 
-pp_sophia_code(C, Opts)->  pp(C, Opts, pp_sophia_code, fun(Code) ->
-                                io:format("~s\n", [prettypr:format(aeso_pretty:decls(Code))])
-                            end).
-pp_ast(C, Opts)      ->  pp(C, Opts, pp_ast, fun aeso_ast:pp/1).
-pp_typed_ast(C, Opts)->  pp(C, Opts, pp_typed_ast, fun aeso_ast:pp_typed/1).
+pp_ast(C, Opts) ->
+    [ io:format("AST:\n~s\n",
+                [prettypr:format(aeso_pretty:decls(Ast, []))])
+      || true <- proplists:get_value(pp_ast, Opts)
+    ].
 
-pp_assembler(C, Opts) ->  pp(C, Opts, pp_assembler, fun(Asm) -> io:format("~s", [aeb_fate_asm:pp(Asm)]) end).
+pp_typed_ast(C, Opts) ->
+    [ io:format("Typed AST:\n~s\n",
+                [prettypr:format(aeso_pretty:decls(Ast, [show_generated]))])
+      || true <- proplists:get_value(pp_typed_ast, Opts)
+    ].
 
-pp(Code, Options, Option, PPFun) ->
-    case proplists:lookup(Option, Options) of
-        {Option1, true} when Option1 =:= Option ->
-            PPFun(Code);
-        none ->
-            ok
-    end.
+pp_fate(C, Opts) ->
+    [ io:format("FATE:\n~s\n", [aeb_fate_asm:pp(Asm)])
+      || true <- proplists:get_value(pp_fate, Opts)
+    ].
 
 %% -- Byte code validation ---------------------------------------------------
 

src/aeso_errors.erl

@@ -34,6 +34,7 @@
         , new/2
         , new/3
         , new/4
+        , pos/1
         , pos/2
         , pos/3
         , pp/1
@@ -53,6 +54,12 @@ new(Type, Pos, Msg) ->
 new(Type, Pos, Msg, Ctxt) ->
     #err{ type = Type, pos = Pos, message = Msg, context = Ctxt }.
 
+pos(Ann) ->
+    File = aeso_syntax:get_ann(file, Ann, no_file),
+    Line = aeso_syntax:get_ann(line, Ann, 0),
+    Col  = aeso_syntax:get_ann(col, Ann, 0),
+    pos(File, Line, Col).
+
 pos(Line, Col) ->
     #pos{ line = Line, col = Col }.
 

src/aeso_fcode_to_fate.erl

@@ -9,7 +9,7 @@
 %%%-------------------------------------------------------------------
 -module(aeso_fcode_to_fate).
 
--export([compile/2, compile/3, term_to_fate/1, term_to_fate/2]).
+-export([compile/3, compile/4, term_to_fate/1, term_to_fate/2]).
 
 -ifdef(TEST).
 -export([optimize_fun/4, to_basic_blocks/1]).
@@ -45,7 +45,14 @@
 -define(s(N), {store, N}).
 -define(void, {var, 9999}).
 
--record(env, { contract, vars = [], locals = [], current_function, tailpos = true, child_contracts = #{}, options = []}).
+-record(env, { contract,
+               vars              = [],
+               locals            = [],
+               current_function,
+               tailpos           = true,
+               child_contracts   = #{},
+               saved_fresh_names = #{},
+               options           = [] }).
 
 %% -- Debugging --------------------------------------------------------------
 
@@ -64,21 +71,34 @@ debug(Tag, Options, Fun) ->
 
 -dialyzer({nowarn_function, [code_error/1]}).
 code_error(Err) ->
-    aeso_errors:throw(aeso_code_errors:format(Err)).
+    Pos = aeso_errors:pos(0, 0),
+    Msg = lists:flatten(io_lib:format("Unknown error: ~p\n", [Err])),
+    aeso_errors:throw(aeso_errors:new(code_error, Pos, Msg)).
 
 %% -- Main -------------------------------------------------------------------
 
 %% @doc Main entry point.
-compile(FCode, Options) ->
-    compile(#{}, FCode, Options).
-compile(ChildContracts, FCode, Options) ->
+compile(FCode, SavedFreshNames, Options) ->
+    compile(#{}, FCode, SavedFreshNames, Options).
+compile(ChildContracts, FCode, SavedFreshNames, Options) ->
+    try
+        compile1(ChildContracts, FCode, SavedFreshNames, Options)
+    after
+        put(variables_registers, undefined)
+    end.
+
+compile1(ChildContracts, FCode, SavedFreshNames, Options) ->
     #{ contract_name := ContractName,
        functions     := Functions } = FCode,
-    SFuns  = functions_to_scode(ChildContracts, ContractName, Functions, Options),
+    SFuns  = functions_to_scode(ChildContracts, ContractName, Functions, SavedFreshNames, Options),
     SFuns1 = optimize_scode(SFuns, Options),
     FateCode = to_basic_blocks(SFuns1),
     ?debug(compile, Options, "~s\n", [aeb_fate_asm:pp(FateCode)]),
-    FateCode.
+    FateCode1 = case proplists:get_value(include_child_contract_symbols, Options, false) of
+                    false -> FateCode;
+                    true -> add_child_symbols(ChildContracts, FateCode)
+                end,
+    {FateCode1, get_variables_registers()}.
 
 make_function_id(X) ->
     aeb_fate_code:symbol_identifier(make_function_name(X)).
@@ -87,22 +107,48 @@ make_function_name(event)              -> <<"Chain.event">>;
 make_function_name({entrypoint, Name}) -> Name;
 make_function_name({local_fun, Xs})    -> list_to_binary("." ++ string:join(Xs, ".")).
 
-functions_to_scode(ChildContracts, ContractName, Functions, Options) ->
+add_child_symbols(ChildContracts, FateCode) ->
+    Funs = lists:flatten([ maps:keys(ChildFuns) || {_, #{functions := ChildFuns}} <- maps:to_list(ChildContracts) ]),
+    Symbols = maps:from_list([ {make_function_id(FName), make_function_name(FName)} || FName <- Funs ]),
+    aeb_fate_code:update_symbols(FateCode, Symbols).
+
+functions_to_scode(ChildContracts, ContractName, Functions, SavedFreshNames, Options) ->
     FunNames = maps:keys(Functions),
     maps:from_list(
-        [ {make_function_name(Name), function_to_scode(ChildContracts, ContractName, FunNames, Name, Attrs, Args, Body, Type, Options)}
+        [ {make_function_name(Name), function_to_scode(ChildContracts, ContractName, FunNames, Name, Attrs, Args, Body, Type, SavedFreshNames, Options)}
         || {Name, #{args   := Args,
                     body   := Body,
                     attrs  := Attrs,
                     return := Type}} <- maps:to_list(Functions)]).
 
-function_to_scode(ChildContracts, ContractName, Functions, Name, Attrs0, Args, Body, ResType, Options) ->
+function_to_scode(ChildContracts, ContractName, Functions, Name, Attrs0, Args, Body, ResType, SavedFreshNames, Options) ->
     {ArgTypes, ResType1} = typesig_to_scode(Args, ResType),
     Attrs = Attrs0 -- [stateful], %% Only track private and payable from here.
-    Env = init_env(ChildContracts, ContractName, Functions, Name, Args, Options),
+    Env = init_env(ChildContracts, ContractName, Functions, Name, Args, SavedFreshNames, Options),
+    [ add_variables_register(Env, Arg, Register) ||
+        proplists:get_value(debug_info, Options, false),
+        {Arg, Register} <- Env#env.vars ],
     SCode = to_scode(Env, Body),
     {Attrs, {ArgTypes, ResType1}, SCode}.
 
+get_variables_registers() ->
+    case get(variables_registers) of
+        undefined -> #{};
+        Vs        -> Vs
+    end.
+
+add_variables_register(Env = #env{saved_fresh_names = SavedFreshNames}, Name, Register) ->
+    Olds = get_variables_registers(),
+    RealName = maps:get(Name, SavedFreshNames, Name),
+    FunName =
+        case Env#env.current_function of
+            event -> "Chain.event";
+            {entrypoint, BinName} -> binary_to_list(BinName);
+            {local_fun, QualName} -> lists:last(QualName)
+        end,
+    New = {Env#env.contract, FunName, RealName},
+    put(variables_registers, Olds#{New => Register}).
+
 -define(tvars, '$tvars').
 
 typesig_to_scode(Args, Res) ->
@@ -147,19 +193,21 @@ types_to_scode(Ts) -> lists:map(fun type_to_scode/1, Ts).
 
 %% -- Environment functions --
 
-init_env(ChildContracts, ContractName, FunNames, Name, Args, Options) ->
+init_env(ChildContracts, ContractName, FunNames, Name, Args, SavedFreshNames, Options) ->
     #env{ vars      = [ {X, {arg, I}} || {I, {X, _}} <- with_ixs(Args) ],
           contract  = ContractName,
           child_contracts = ChildContracts,
           locals    = FunNames,
           current_function = Name,
           options = Options,
-          tailpos   = true }.
+          tailpos   = true,
+          saved_fresh_names = SavedFreshNames }.
 
 next_var(#env{ vars = Vars }) ->
     1 + lists:max([-1 | [J || {_, {var, J}} <- Vars]]).
 
 bind_var(Name, Var, Env = #env{ vars = Vars }) ->
+    proplists:get_value(debug_info, Env#env.options, false) andalso add_variables_register(Env, Name, Var),
     Env#env{ vars = [{Name, Var} | Vars] }.
 
 bind_local(Name, Env) ->
@@ -183,9 +231,10 @@ serialize_contract_code(Env, C) ->
             end,
     case maps:get(C, Cache, none) of
         none ->
-            Options  = Env#env.options,
-            FCode    = maps:get(C, Env#env.child_contracts),
-            FateCode = compile(Env#env.child_contracts, FCode, Options),
+            Options = Env#env.options,
+            SavedFreshNames = Env#env.saved_fresh_names,
+            FCode = maps:get(C, Env#env.child_contracts),
+            {FateCode, _} = compile1(Env#env.child_contracts, FCode, SavedFreshNames, Options),
             ByteCode = aeb_fate_code:serialize(FateCode, []),
             {ok, Version} = aeso_compiler:version(),
             OriginalSourceCode = proplists:get_value(original_src, Options, ""),
@@ -507,6 +556,8 @@ builtin_to_scode(Env, bytes_split, [_, _] = Args) ->
     call_to_scode(Env, aeb_fate_ops:bytes_split(?a, ?a, ?a), Args);
 builtin_to_scode(Env, abort, [_] = Args) ->
     call_to_scode(Env, aeb_fate_ops:abort(?a), Args);
+builtin_to_scode(Env, exit, [_] = Args) ->
+    call_to_scode(Env, aeb_fate_ops:exit(?a), Args);
 builtin_to_scode(Env, chain_spend, [_, _] = Args) ->
     call_to_scode(Env, [aeb_fate_ops:spend(?a, ?a),
                         tuple(0)], Args);
@@ -705,7 +756,7 @@ tuple(N) -> aeb_fate_ops:tuple(?a, N).
 
 optimize_scode(Funs, Options) ->
     maps:map(fun(Name, Def) -> optimize_fun(Funs, Name, Def, Options) end,
-             Funs).
+            Funs).
 
 flatten(missing) -> missing;
 flatten(Code)    -> lists:map(fun flatten_s/1, lists:flatten(Code)).
@@ -1088,7 +1139,8 @@ simpl_top(I, Code, Options) ->
 simpl_top(0, I, Code, _Options) ->
     code_error({optimizer_out_of_fuel, I, Code});
 simpl_top(Fuel, I, Code, Options) ->
-    apply_rules(Fuel, rules(), I, Code, Options).
+    Rules = [R || R = {Rule, _} <- rules(), proplists:get_value(Rule, Options, true)],
+    apply_rules(Fuel, Rules, I, Code, Options).
 
 apply_rules(Fuel, Rules, I, Code, Options) ->
     Cons = fun(X, Xs) -> simpl_top(Fuel - 1, X, Xs, Options) end,
@@ -1115,29 +1167,29 @@ apply_rules_once([{RName, Rule} | Rules], I, Code) ->
 -define(RULE(Name), {Name, fun Name/2}).
 
 merge_rules() ->
-    [?RULE(r_push_consume),
-     ?RULE(r_one_shot_var),
-     ?RULE(r_write_to_dead_var),
-     ?RULE(r_inline_switch_target)
+    [?RULE(optimize_push_consume),
+     ?RULE(optimize_one_shot_var),
+     ?RULE(optimize_write_to_dead_var),
+     ?RULE(optimize_inline_switch_target)
     ].
 
 rules() ->
     merge_rules() ++
-    [?RULE(r_swap_push),
-     ?RULE(r_swap_pop),
-     ?RULE(r_swap_write),
-     ?RULE(r_constant_propagation),
-     ?RULE(r_prune_impossible_branches),
-     ?RULE(r_single_successful_branch),
-     ?RULE(r_inline_store),
-     ?RULE(r_float_switch_body)
+    [?RULE(optimize_swap_push),
+     ?RULE(optimize_swap_pop),
+     ?RULE(optimize_swap_write),
+     ?RULE(optimize_constant_propagation),
+     ?RULE(optimize_prune_impossible_branches),
+     ?RULE(optimize_single_successful_branch),
+     ?RULE(optimize_inline_store),
+     ?RULE(optimize_float_switch_body)
     ].
 
 %% Removing pushes that are immediately consumed.
-r_push_consume({i, Ann1, {'STORE', ?a, A}}, Code) ->
+optimize_push_consume({i, Ann1, {'STORE', ?a, A}}, Code) ->
     inline_push(Ann1, A, 0, Code, []);
 %% Writing directly to memory instead of going through the accumulator.
-r_push_consume({i, Ann1, I}, [{i, Ann2, {'STORE', R, ?a}} | Code]) ->
+optimize_push_consume({i, Ann1, I}, [{i, Ann2, {'STORE', R, ?a}} | Code]) ->
     IsPush =
         case op_view(I) of
             {_, ?a, _} -> true;
@@ -1149,7 +1201,7 @@ r_push_consume({i, Ann1, I}, [{i, Ann2, {'STORE', R, ?a}} | Code]) ->
         end,
     if IsPush -> {[{i, merge_ann(Ann1, Ann2), setelement(2, I, R)}], Code};
        true   -> false end;
-r_push_consume(_, _) -> false.
+optimize_push_consume(_, _) -> false.
 
 inline_push(Ann, Arg, Stack, [{i, _, switch_body} = AI | Code], Acc) ->
     {AI1, {i, Ann1, _}} = swap_instrs({i, Ann, {'STORE', ?a, Arg}}, AI),
@@ -1182,7 +1234,7 @@ split_stack_arg(N, [A | As], Acc) ->
     split_stack_arg(N1, As, [A | Acc]).
 
 %% Move PUSHes past non-stack instructions.
-r_swap_push(Push = {i, _, PushI}, [I | Code]) ->
+optimize_swap_push(Push = {i, _, PushI}, [I | Code]) ->
     case op_view(PushI) of
         {_, ?a, _} ->
             case independent(Push, I) of
@@ -1193,10 +1245,10 @@ r_swap_push(Push = {i, _, PushI}, [I | Code]) ->
             end;
         _ -> false
     end;
-r_swap_push(_, _) -> false.
+optimize_swap_push(_, _) -> false.
 
 %% Move non-stack instruction past POPs.
-r_swap_pop(IA = {i, _, I}, [JA = {i, _, J} | Code]) ->
+optimize_swap_pop(IA = {i, _, I}, [JA = {i, _, J} | Code]) ->
     case independent(IA, JA) of
         true ->
             case {op_view(I), op_view(J)} of
@@ -1204,7 +1256,7 @@ r_swap_pop(IA = {i, _, I}, [JA = {i, _, J} | Code]) ->
                 {_, false} -> false;
                 {{_, IR, IAs}, {_, RJ, JAs}} ->
                     NonStackI = not lists:member(?a, [IR | IAs]),
-                    %% RJ /= ?a to not conflict with r_swap_push
+                    %% RJ /= ?a to not conflict with optimize_swap_push
                     PopJ      = RJ /= ?a andalso lists:member(?a, JAs),
                     case NonStackI andalso PopJ of
                         false -> false;
@@ -1215,22 +1267,22 @@ r_swap_pop(IA = {i, _, I}, [JA = {i, _, J} | Code]) ->
             end;
         false -> false
     end;
-r_swap_pop(_, _) -> false.
+optimize_swap_pop(_, _) -> false.
 
 %% Match up writes to variables with instructions further down.
-r_swap_write(I = {i, _, _}, [J | Code]) ->
+optimize_swap_write(I = {i, _, _}, [J | Code]) ->
     case {var_writes(I), independent(I, J)} of
         {[_], true} ->
             {J1, I1} = swap_instrs(I, J),
-            r_swap_write([J1], I1, Code);
+            optimize_swap_write([J1], I1, Code);
         _ -> false
     end;
-r_swap_write(_, _) -> false.
+optimize_swap_write(_, _) -> false.
 
-r_swap_write(Pre, I, [{i, _, switch_body} = J | Code]) ->
+optimize_swap_write(Pre, I, [{i, _, switch_body} = J | Code]) ->
     {J1, I1} = swap_instrs(I, J),
-    r_swap_write([J1 | Pre], I1, Code);
-r_swap_write(Pre, I, Code0 = [J | Code]) ->
+    optimize_swap_write([J1 | Pre], I1, Code);
+optimize_swap_write(Pre, I, Code0 = [J | Code]) ->
     case apply_rules_once(merge_rules(), I, Code0) of
         {_Rule, New, Rest} ->
             {lists:reverse(Pre) ++ New, Rest};
@@ -1239,27 +1291,27 @@ r_swap_write(Pre, I, Code0 = [J | Code]) ->
                 false -> false;
                 true  ->
                     {J1, I1} = swap_instrs(I, J),
-                    r_swap_write([J1 | Pre], I1, Code)
+                    optimize_swap_write([J1 | Pre], I1, Code)
             end
     end;
-r_swap_write(_, _, _) -> false.
+optimize_swap_write(_, _, _) -> false.
 
 %% Precompute instructions with known values
-r_constant_propagation(Cons = {i, Ann1, {'CONS', R, X, Xs}}, [{i, Ann, {'IS_NIL', S, R}} | Code]) ->
+optimize_constant_propagation(Cons = {i, Ann1, {'CONS', R, X, Xs}}, [{i, Ann, {'IS_NIL', S, R}} | Code]) ->
     Store = {i, Ann, {'STORE', S, ?i(false)}},
     Cons1 = case R of
                 ?a -> {i, Ann1, {'CONS', ?void, X, Xs}};
                 _  -> Cons
             end,
     {[Cons1, Store], Code};
-r_constant_propagation(Nil = {i, Ann1, {'NIL', R}}, [{i, Ann, {'IS_NIL', S, R}} | Code]) ->
+optimize_constant_propagation(Nil = {i, Ann1, {'NIL', R}}, [{i, Ann, {'IS_NIL', S, R}} | Code]) ->
     Store = {i, Ann, {'STORE', S, ?i(true)}},
     Nil1 = case R of
                ?a -> {i, Ann1, {'NIL', ?void}};
                _  -> Nil
            end,
     {[Nil1, Store], Code};
-r_constant_propagation({i, Ann, I}, Code) ->
+optimize_constant_propagation({i, Ann, I}, Code) ->
     case op_view(I) of
         false -> false;
         {Op, R, As} ->
@@ -1273,7 +1325,7 @@ r_constant_propagation({i, Ann, I}, Code) ->
                     end
             end
     end;
-r_constant_propagation(_, _) -> false.
+optimize_constant_propagation(_, _) -> false.
 
 eval_op('ADD', [X, Y]) when is_integer(X), is_integer(Y) -> X + Y;
 eval_op('SUB', [X, Y]) when is_integer(X), is_integer(Y) -> X - Y;
@@ -1292,12 +1344,12 @@ eval_op('NOT', [false]) -> true;
 eval_op(_, _)           -> no_eval.   %% TODO: bits?
 
 %% Prune impossible branches from switches
-r_prune_impossible_branches({switch, ?i(V), Type, Alts, missing}, Code) ->
+optimize_prune_impossible_branches({switch, ?i(V), Type, Alts, missing}, Code) ->
     case pick_branch(Type, V, Alts) of
         false -> false;
         Alt   -> {Alt, Code}
     end;
-r_prune_impossible_branches({switch, ?i(V), boolean, [False, True] = Alts, Def}, Code) when V == true; V == false ->
+optimize_prune_impossible_branches({switch, ?i(V), boolean, [False, True] = Alts, Def}, Code) when V == true; V == false ->
     Alts1 = [if V -> missing; true -> False   end,
              if V -> True;    true -> missing end],
     case Alts == Alts1 of
@@ -1308,7 +1360,7 @@ r_prune_impossible_branches({switch, ?i(V), boolean, [False, True] = Alts, Def},
                 _                  -> {[{switch, ?i(V), boolean, Alts1, Def}], Code}
             end
     end;
-r_prune_impossible_branches(Variant = {i, _, {'VARIANT', R, ?i(_), ?i(Tag), ?i(_)}},
+optimize_prune_impossible_branches(Variant = {i, _, {'VARIANT', R, ?i(_), ?i(Tag), ?i(_)}},
                             [{switch, R, Type = {variant, _}, Alts, missing} | Code]) when is_integer(Tag) ->
     case {R, lists:nth(Tag + 1, Alts)} of
         {_, missing} ->
@@ -1324,7 +1376,7 @@ r_prune_impossible_branches(Variant = {i, _, {'VARIANT', R, ?i(_), ?i(Tag), ?i(_
                 false -> {Alt, Code}
             end
     end;
-r_prune_impossible_branches(_, _) -> false.
+optimize_prune_impossible_branches(_, _) -> false.
 
 pick_branch(boolean, V, [False, True]) when V == true; V == false ->
     Alt = if V -> True; true -> False end,
@@ -1337,7 +1389,7 @@ pick_branch(_Type, _V, _Alts) ->
 
 %% If there's a single branch that doesn't abort we can push the code for that
 %% out of the switch.
-r_single_successful_branch({switch, R, Type, Alts, Def}, Code) ->
+optimize_single_successful_branch({switch, R, Type, Alts, Def}, Code) ->
     case push_code_out_of_switch([Def | Alts]) of
         {_, none} -> false;
         {_, many} -> false;
@@ -1345,7 +1397,7 @@ r_single_successful_branch({switch, R, Type, Alts, Def}, Code) ->
         {[Def1 | Alts1], PushedOut} ->
             {[{switch, R, Type, Alts1, Def1} | PushedOut], Code}
     end;
-r_single_successful_branch(_, _) -> false.
+optimize_single_successful_branch(_, _) -> false.
 
 push_code_out_of_switch([]) -> {[], none};
 push_code_out_of_switch([Alt | Alts]) ->
@@ -1381,7 +1433,7 @@ does_abort({switch, _, _, Alts, Def}) ->
 does_abort(_) -> false.
 
 %% STORE R A, SWITCH R --> SWITCH A
-r_inline_switch_target({i, Ann, {'STORE', R, A}}, [{switch, R, Type, Alts, Def} | Code]) ->
+optimize_inline_switch_target({i, Ann, {'STORE', R, A}}, [{switch, R, Type, Alts, Def} | Code]) ->
     Ann1   =
         case is_reg(A) of
             true  -> Ann#{ live_out := ordsets:add_element(A, maps:get(live_out, Ann)) };
@@ -1400,18 +1452,18 @@ r_inline_switch_target({i, Ann, {'STORE', R, A}}, [{switch, R, Type, Alts, Def}
             end;
         _        -> false %% impossible
     end;
-r_inline_switch_target(_, _) -> false.
+optimize_inline_switch_target(_, _) -> false.
 
 %% Float switch-body to closest switch
-r_float_switch_body(I = {i, _, _}, [J = {i, _, switch_body} | Code]) ->
+optimize_float_switch_body(I = {i, _, _}, [J = {i, _, switch_body} | Code]) ->
     {J1, I1} = swap_instrs(I, J),
     {[], [J1, I1 | Code]};
-r_float_switch_body(_, _) -> false.
+optimize_float_switch_body(_, _) -> false.
 
 %% Inline stores
-r_inline_store({i, _, {'STORE', R, R}}, Code) ->
+optimize_inline_store({i, _, {'STORE', R, R}}, Code) ->
     {[], Code};
-r_inline_store(I = {i, _, {'STORE', R = {var, _}, A}}, Code) ->
+optimize_inline_store(I = {i, _, {'STORE', R = {var, _}, A}}, Code) ->
     %% Not when A is var unless updating the annotations properly.
     Inline = case A of
                  {arg, _}   -> true;
@@ -1419,13 +1471,13 @@ r_inline_store(I = {i, _, {'STORE', R = {var, _}, A}}, Code) ->
                  {store, _} -> true;
                  _          -> false
              end,
-    if Inline -> r_inline_store([I], false, R, A, Code);
+    if Inline -> optimize_inline_store([I], false, R, A, Code);
        true   -> false end;
-r_inline_store(_, _) -> false.
+optimize_inline_store(_, _) -> false.
 
-r_inline_store(Acc, Progress, R, A, [I = {i, _, switch_body} | Code]) ->
-    r_inline_store([I | Acc], Progress, R, A, Code);
-r_inline_store(Acc, Progress, R, A, [{i, Ann, I} | Code]) ->
+optimize_inline_store(Acc, Progress, R, A, [I = {i, _, switch_body} | Code]) ->
+    optimize_inline_store([I | Acc], Progress, R, A, Code);
+optimize_inline_store(Acc, Progress, R, A, [{i, Ann, I} | Code]) ->
     #{ write := W } = attributes(I),
     Inl = fun(X) when X == R -> A; (X) -> X end,
     case live_in(R, Ann) of
@@ -1445,14 +1497,14 @@ r_inline_store(Acc, Progress, R, A, [{i, Ann, I} | Code]) ->
             case lists:member(W, [R, A]) of
                 true when Progress1 -> {lists:reverse(Acc1), Code};
                 true                -> false;
-                false               -> r_inline_store(Acc1, Progress1, R, A, Code)
+                false               -> optimize_inline_store(Acc1, Progress1, R, A, Code)
             end
     end;
-r_inline_store(Acc, true, _, _, Code) -> {lists:reverse(Acc), Code};
-r_inline_store(_, false, _, _, _) -> false.
+optimize_inline_store(Acc, true, _, _, Code) -> {lists:reverse(Acc), Code};
+optimize_inline_store(_, false, _, _, _) -> false.
 
 %% Shortcut write followed by final read
-r_one_shot_var({i, Ann1, I}, [{i, Ann2, J} | Code]) ->
+optimize_one_shot_var({i, Ann1, I}, [{i, Ann2, J} | Code]) ->
     case op_view(I) of
         {Op, R = {var, _}, As} ->
             Copy = case J of
@@ -1466,11 +1518,11 @@ r_one_shot_var({i, Ann1, I}, [{i, Ann2, J} | Code]) ->
             end;
         _ -> false
     end;
-r_one_shot_var(_, _) -> false.
+optimize_one_shot_var(_, _) -> false.
 
 %% Remove writes to dead variables
-r_write_to_dead_var({i, _, {'STORE', ?void, ?a}}, _) -> false; %% Avoid looping
-r_write_to_dead_var({i, Ann, I}, Code) ->
+optimize_write_to_dead_var({i, _, {'STORE', ?void, ?a}}, _) -> false; %% Avoid looping
+optimize_write_to_dead_var({i, Ann, I}, Code) ->
     #{ pure := Pure } = attributes(I),
     case op_view(I) of
         {_Op, R, As} when R /= ?a, Pure ->
@@ -1483,9 +1535,10 @@ r_write_to_dead_var({i, Ann, I}, Code) ->
             end;
         _ -> false
     end;
-r_write_to_dead_var(_, _) -> false.
+optimize_write_to_dead_var(_, _) -> false.
 
 op_view({'ABORT', R}) -> {'ABORT', none, [R]};
+op_view({'EXIT', R}) -> {'EXIT', none, [R]};
 op_view(T) when is_tuple(T) ->
     [Op, R | As] = tuple_to_list(T),
     CheckReads = fun(Rs, X) -> case [] == Rs -- [dst, src] of true -> X; false -> false end end,

src/aeso_parser.erl

@@ -8,22 +8,17 @@
 -export([string/1,
          string/2,
          string/3,
-         auto_imports/1,
-         hash_include/2,
          decl/0,
          type/0,
          body/0,
          maybe_block/1,
-         run_parser/2,
-         run_parser/3]).
+         run_parser/2]).
 
 -include("aeso_parse_lib.hrl").
 -import(aeso_parse_lib, [current_file/0, set_current_file/1,
                          current_include_type/0, set_current_include_type/1]).
 
--type parse_result() :: aeso_syntax:ast() | {aeso_syntax:ast(), sets:set(include_hash())} | none().
-
--type include_hash() :: {string(), binary()}.
+-type parse_result() :: aeso_syntax:ast() | none().
 
 
 escape_errors({ok, Ok}) ->
@@ -31,32 +26,21 @@ escape_errors({ok, Ok}) ->
 escape_errors({error, Err}) ->
     parse_error(Err).
 
--spec string(string()) -> parse_result().
-string(String) ->
-    string(String, sets:new(), []).
+-spec module(string()) -> parse_result().
+module(String) ->
+    module(String, []).
 
--spec string(string(), aeso_compiler:options()) -> parse_result().
-string(String, Opts) ->
-    case lists:keyfind(src_file, 1, Opts) of
-        {src_file, File} -> string(String, sets:add_element(File, sets:new()), Opts);
-        false -> string(String, sets:new(), Opts)
-    end.
-
--spec string(string(), sets:set(include_hash()), aeso_compiler:options()) -> parse_result().
-string(String, Included, Opts) ->
+-spec module(string(), aeso_compiler:options()) -> parse_result().
+module(String, Opts) ->
     AST = run_parser(file(), String, Opts),
-    case expand_includes(AST, Included, Opts) of
-        {ok, AST1}   -> AST1;
-        {error, Err} -> parse_error(Err)
-    end.
-
+    add_auto_imports(AST).
 
 run_parser(P, Inp) ->
-    escape_errors(parse_and_scan(P, Inp, [])).
+    escape_errors(scan_and_parse(P, Inp, [])).
 run_parser(P, Inp, Opts) ->
-    escape_errors(parse_and_scan(P, Inp, Opts)).
+    escape_errors(scan_and_parse(P, Inp, Opts)).
 
-parse_and_scan(P, S, Opts) ->
+scan_and_parse(P, S, Opts) ->
     set_current_file(proplists:get_value(src_file, Opts, no_file)),
     set_current_include_type(proplists:get_value(include_type, Opts, none)),
     case aeso_scan:scan(S) of
@@ -96,17 +80,29 @@ decl() ->
     choice(
       %% Contract declaration
     [ ?RULE(token(main), keyword(contract),
-            con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5})
+            con(), tok('='), maybe_block(decl()), {contract_main, _2, _3, [], _5})
+    , ?RULE(token(main), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_main, _2, _3, _5, _7})
     , ?RULE(keyword(contract),
-            con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4})
+            con(), tok('='), maybe_block(decl()), {contract_child, _1, _2, [], _4})
+    , ?RULE(keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_child, _1, _2, _4, _6})
     , ?RULE(keyword(contract), token(interface),
-            con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5})
+            con(), tok('='), maybe_block(decl()), {contract_interface, _1, _3, [], _5})
+    , ?RULE(keyword(contract), token(interface),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), {contract_interface, _1, _3, _5, _7})
     , ?RULE(token(payable), token(main), keyword(contract),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, [], _6}))
+    , ?RULE(token(payable), token(main), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_main, _3, _4, _6, _8}))
     , ?RULE(token(payable), keyword(contract),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, [], _5}))
+    , ?RULE(token(payable), keyword(contract),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_child, _2, _3, _5, _7}))
     , ?RULE(token(payable), keyword(contract), token(interface),
-            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6}))
+            con(), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, [], _6}))
+    , ?RULE(token(payable), keyword(contract), token(interface),
+            con(), tok(':'), comma_sep(con()), tok('='), maybe_block(decl()), add_modifiers([_1], {contract_interface, _2, _4, _6, _8}))
 
 
     , ?RULE(keyword(namespace), con(), tok('='), maybe_block(decl()), {namespace, _1, _2, _4})
@@ -134,19 +130,9 @@ fun_block(Mods, Kind, [Decl]) ->
 fun_block(Mods, Kind, Decls) ->
     {block, get_ann(Kind), [ add_modifiers(Mods, Kind, Decl) || Decl <- Decls ]}.
 
-typevar_constraint() ->
-    ?RULE(tvar(), keyword(is), id(), {constraint, get_ann(_1), _1, _3}).
-
-typevars_constraints() ->
-    ?RULE(comma_sep1(typevar_constraint()), tok(';'), _1).
-
-fundecl() ->
-    choice([?RULE(id(), tok(':'), typevars_constraints(), type(),
-                  {fun_decl, get_ann(_1), _1, {constrained_t, get_ann(_1), _3, _4}}),
-            ?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3})]).
-
 fundef_or_decl() ->
-    choice([fundecl(), fundef()]).
+    choice([?RULE(id(), tok(':'), type(), {fun_decl, get_ann(_1), _1, _3}),
+            fundef()]).
 
 using() ->
     Alias = {keyword(as), con()},
@@ -357,9 +343,12 @@ exprAtom() ->
         , ?RULE(tok('['), Expr, binop('..'), Expr, tok(']'), _3(_2, _4))
         , ?RULE(keyword('('), comma_sep(Expr), tok(')'), tuple_e(_1, _2))
         , letpat()
+        , hole()
         ])
     end).
 
+hole() -> ?RULE(token('???'), {id, get_ann(_1), "???"}).
+
 comprehension_exp() ->
     ?LAZY_P(choice(
       [ comprehension_bind()
@@ -537,7 +526,6 @@ parens(P)   -> between(tok('('), P, tok(')')).
 braces(P)   -> between(tok('{'), P, tok('}')).
 brackets(P) -> between(tok('['), P, tok(']')).
 comma_sep(P) -> sep(P, tok(',')).
-comma_sep1(P) -> sep1(P, tok(',')).
 
 paren_list(P)   -> parens(comma_sep(P)).
 brace_list(P)   -> braces(comma_sep(P)).
@@ -556,6 +544,9 @@ pos_ann(Line, Col) ->
     , {line, Line}
     , {col, Col} ].
 
+top_ann() ->
+    pos_ann(0, 0).
+
 ann_pos(Ann) ->
     {proplists:get_value(file, Ann),
      proplists:get_value(line, Ann),
@@ -677,107 +668,13 @@ bad_expr_err(Reason, E) ->
 
 %% -- Helper functions -------------------------------------------------------
 
-expand_includes(AST, Included, Opts) ->
+add_auto_imports(AST) ->
     Ann  = [{origin, system}],
-    AST1 = [ {include, Ann, {string, Ann, File}}
-             || File <- lists:usort(auto_imports(AST)) ] ++ AST,
-    expand_includes(AST1, Included, [], Opts).
+    [ {using, Ann, {con, Ann, Import}}
+      || Import <- lists:usort(auto_imports(AST)) ] ++ AST.
 
-expand_includes([], Included, Acc, Opts) ->
-    case lists:member(keep_included, Opts) of
-        false ->
-            {ok, lists:reverse(Acc)};
-        true ->
-            {ok, {lists:reverse(Acc), Included}}
-    end;
-expand_includes([{include, Ann, {string, _SAnn, File}} | AST], Included, Acc, Opts) ->
-    case get_include_code(File, Ann, Opts) of
-        {ok, Code} ->
-            Hashed = hash_include(File, Code),
-            case sets:is_element(Hashed, Included) of
-                false ->
-                    SrcFile = proplists:get_value(src_file, Opts, no_file),
-                    IncludeType = case proplists:get_value(file, Ann) of
-                                      SrcFile -> direct;
-                                      _       -> indirect
-                                  end,
-                    Opts1 = lists:keystore(src_file, 1, Opts, {src_file, File}),
-                    Opts2 = lists:keystore(include_type, 1, Opts1, {include_type, IncludeType}),
-                    Included1 = sets:add_element(Hashed, Included),
-                    case parse_and_scan(file(), Code, Opts2) of
-                        {ok, AST1} ->
-                            expand_includes(AST1 ++ AST, Included1, Acc, Opts);
-                        Err = {error, _} ->
-                            Err
-                    end;
-                true ->
-                    expand_includes(AST, Included, Acc, Opts)
-            end;
-        Err = {error, _} ->
-            Err
-    end;
-expand_includes([E | AST], Included, Acc, Opts) ->
-    expand_includes(AST, Included, [E | Acc], Opts).
-
-read_file(File, Opts) ->
-    case proplists:get_value(include, Opts, {explicit_files, #{}}) of
-        {file_system, Paths} ->
-            CandidateNames = [ filename:join(Dir, File) || Dir <- Paths ],
-            lists:foldr(fun(F, {error, _}) -> file:read_file(F);
-                           (_F, OK) -> OK end, {error, not_found}, CandidateNames);
-        {explicit_files, Files} ->
-            case maps:get(binary_to_list(File), Files, not_found) of
-                not_found -> {error, not_found};
-                Src       -> {ok, Src}
-            end;
-        escript ->
-            try
-                Escript        = escript:script_name(),
-                {ok, Sections} = escript:extract(Escript, []),
-                Archive        = proplists:get_value(archive, Sections),
-                FileName       = binary_to_list(filename:join([aesophia, priv, stdlib, File])),
-                case zip:extract(Archive, [{file_list, [FileName]}, memory]) of
-                    {ok, [{_, Src}]} -> {ok, Src};
-                    _                -> {error, not_found}
-                end
-            catch _:_ ->
-                {error, not_found}
-            end
-    end.
-
-stdlib_options() ->
-    StdLibDir = aeso_stdlib:stdlib_include_path(),
-    case filelib:is_dir(StdLibDir) of
-        true  -> [{include, {file_system, [StdLibDir]}}];
-        false -> [{include, escript}]
-    end.
-
-get_include_code(File, Ann, Opts) ->
-    case {read_file(File, Opts), read_file(File, stdlib_options())} of
-        {{ok, Bin}, {ok, _}} ->
-            case filename:basename(File) == File of
-                true -> { error
-                        , fail( ann_pos(Ann)
-                              , "Illegal redefinition of standard library " ++ binary_to_list(File))};
-                %% If a path is provided then the stdlib takes lower priority
-                false -> {ok, binary_to_list(Bin)}
-            end;
-        {_, {ok, Bin}} ->
-            {ok, binary_to_list(Bin)};
-        {{ok, Bin}, _} ->
-            {ok, binary_to_list(Bin)};
-        {_, _} ->
-            {error, {ann_pos(Ann), include_error, File}}
-    end.
-
--spec hash_include(string() | binary(), string()) -> include_hash().
-hash_include(File, Code) when is_binary(File) ->
-    hash_include(binary_to_list(File), Code);
-hash_include(File, Code) when is_list(File) ->
-    {filename:basename(File), crypto:hash(sha256, Code)}.
-
-auto_imports({comprehension_bind, _, _}) -> [<<"ListInternal.aes">>];
-auto_imports({'..', _})                  -> [<<"ListInternal.aes">>];
+auto_imports({comprehension_bind, _, _}) -> ["ListInternal"];
+auto_imports({'..', _})                  -> ["ListInternal"];
 auto_imports(L) when is_list(L) ->
     lists:flatmap(fun auto_imports/1, L);
 auto_imports(T) when is_tuple(T) ->

src/aeso_pretty.erl

@@ -151,12 +151,16 @@ decl(D, Options) ->
     with_options(Options, fun() -> decl(D) end).
 
 -spec decl(aeso_syntax:decl()) -> doc().
-decl({Con, Attrs, C, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
+decl({Con, Attrs, C, Is, Ds}) when ?IS_CONTRACT_HEAD(Con) ->
     Mod = fun({Mod, true}) when Mod == payable ->
                   text(atom_to_list(Mod));
              (_) -> empty() end,
+    ImplsList = case Is of
+                    [] -> [empty()];
+                    _  -> [text(":"), par(punctuate(text(","), lists:map(fun name/1, Is)), 0)]
+                end,
     block(follow( hsep(lists:map(Mod, Attrs) ++ [contract_head(Con)])
-                , hsep(name(C), text("="))), decls(Ds));
+                , hsep([name(C)] ++ ImplsList ++ [text("=")])), decls(Ds));
 decl({namespace, _, C, Ds}) ->
     block(follow(text("namespace"), hsep(name(C), text("="))), decls(Ds));
 decl({pragma, _, Pragma}) -> pragma(Pragma);
@@ -257,6 +261,8 @@ type(Type, Options) ->
     with_options(Options, fun() -> type(Type) end).
 
 -spec type(aeso_syntax:type()) -> doc().
+type(F = {fun_t, _, _, var_args, _}) ->
+    type(setelement(4, F, [var_args]));
 type({fun_t, _, Named, Args, Ret}) ->
     follow(hsep(args_type(Named ++ Args), text("=>")), type(Ret));
 type({type_sig, _, Named, Args, Ret}) ->
@@ -285,8 +291,8 @@ type(T = {qid, _, _})  -> name(T);
 type(T = {con, _, _})  -> name(T);
 type(T = {qcon, _, _}) -> name(T);
 type(T = {tvar, _, _}) -> name(T);
-type({constrained_t, _, Cs, T}) ->
-    beside([name(T), text(" is "), tuple(lists:map(fun expr/1, Cs))]).
+
+type(var_args) -> text("var_args").
 
 -spec args_type([aeso_syntax:type()]) -> doc().
 args_type(Args) ->
@@ -428,6 +434,7 @@ lc_bind(Let) ->
 bin_prec('..')   -> {  0,   0,   0};  %% Always printed inside '[ ]'
 bin_prec('=')    -> {  0,   0,   0};  %% Always printed inside '[ ]'
 bin_prec('@')    -> {  0,   0,   0};  %% Only in error messages
+bin_prec('|>')   -> {150, 150, 200};
 bin_prec('||')   -> {200, 300, 200};
 bin_prec('&&')   -> {300, 400, 300};
 bin_prec('<')    -> {400, 500, 500};
@@ -519,4 +526,3 @@ get_elifs(If = {'if', Ann, Cond, Then, Else}, Elifs) ->
         _    -> {lists:reverse(Elifs), If}
     end;
 get_elifs(Else, Elifs) -> {lists:reverse(Elifs), {else, Else}}.
-

src/aeso_scan.erl

@@ -45,7 +45,7 @@ lexer() ->
 
     Keywords = ["contract", "include", "let", "switch", "type", "record", "datatype", "if", "elif", "else", "function",
                 "stateful", "payable", "true", "false", "mod", "public", "entrypoint", "private", "indexed", "namespace",
-                "interface", "main", "using", "as", "for", "hiding", "is"
+                "interface", "main", "using", "as", "for", "hiding"
                ],
     KW = string:join(Keywords, "|"),
 

src/aeso_syntax.erl

@@ -13,20 +13,21 @@
 -export_type([ann_line/0, ann_col/0, ann_origin/0, ann_format/0, ann/0]).
 -export_type([name/0, id/0, con/0, qid/0, qcon/0, tvar/0, op/0]).
 -export_type([bin_op/0, un_op/0]).
--export_type([decl/0, letbind/0, typedef/0, pragma/0]).
+-export_type([top_decl/0, decl/0, letbind/0, typedef/0, pragma/0, fundecl/0]).
 -export_type([arg/0, field_t/0, constructor_t/0, named_arg_t/0]).
 -export_type([type/0, constant/0, expr/0, arg_expr/0, field/1, stmt/0, alt/0, lvalue/0, elim/0, pat/0]).
 -export_type([ast/0]).
 
--type ast() :: [decl()].
+-type ast() :: [top_decl()].
 
 -type ann_line()   :: integer().
 -type ann_col()    :: integer().
 -type ann_origin() :: system | user.
 -type ann_format() :: '?:' | hex | infix | prefix | elif.
 
--type ann() :: [ {line, ann_line()} | {col, ann_col()} | {format, ann_format()} | {origin, ann_origin()}
-               | stateful | private | payable | main | interface].
+-type ann() :: [ {line, ann_line()} | {col, ann_col()} | {file, ann_file()}
+               | {format, ann_format()} | {origin, ann_origin()}
+               | stateful | private | payable | main | interface | entrypoint].
 
 -type name() :: string().
 -type id()   :: {id,   ann(), name()}.
@@ -38,19 +39,31 @@
 -type namespace_alias() :: none | con().
 -type namespace_parts() :: none | {for, [id()]} | {hiding, [id()]}.
 
--type decl() :: {contract_main, ann(), con(), [decl()]}
-              | {contract_child, ann(), con(), [decl()]}
-              | {contract_interface, ann(), con(), [decl()]}
-              | {namespace, ann(), con(), [decl()]}
-              | {pragma, ann(), pragma()}
-              | {type_decl, ann(), id(), [tvar()]} % Only for error msgs
-              | {type_def, ann(), id(), [tvar()], typedef()}
-              | {fun_clauses, ann(), id(), type(), [letfun() | fundecl()]}
-              | {block, ann(), [decl()]}
-              | {using, ann(), con(), namespace_alias(), namespace_parts()}
-              | fundecl()
-              | letfun()
-              | letval(). % Only for error msgs
+% Can't be toplevel
+-type scoped_decl()
+ :: {contract_decl, ann(), con()}
+  | {namespace_decl, ann(), con()}
+  | {type_decl, ann(), id(), [tvar()]} % Only for error msgs
+  | {type_def, ann(), id(), [tvar()], typedef()}
+  | {fun_clauses, ann(), id(), type(), [letfun() | fundecl()]}
+  | {block, ann(), [scoped_decl()]}
+  | fundecl()
+  | letfun()
+  | letval() % Only for error msgs
+  | decl().
+
+% Toplevel, can be nested
+-type decl()
+:: {contract_main, ann(), con(), [con()], [scoped_decl()]}
+ | {contract_child, ann(), con(), [con()], [scoped_decl()]}
+ | {contract_interface, ann(), con(), [con()], [scoped_decl()]}
+ | {namespace, ann(), con(), [scoped_decl()]}
+ | {using, ann(), con(), namespace_alias(), namespace_parts()}.
+
+% Toplevel only
+-type top_decl()
+ :: {pragma, ann(), pragma()}
+  | decl().
 
 -type compiler_version() :: [non_neg_integer()].
 
@@ -79,14 +92,11 @@
 
 -type constructor_t() :: {constr_t, ann(), con(), [type()]}.
 
--type tvar_constraint() :: {constraint, ann(), tvar(), id()}.
-
 -type type() :: {fun_t, ann(), [named_arg_t()], [type()], type()}
               | {app_t, ann(), type(), [type()]}
               | {tuple_t, ann(), [type()]}
               | {args_t, ann(), [type()]}   %% old tuple syntax, old for error messages
               | {bytes_t, ann(), integer() | any}
-              | {constrained_t, ann(), [tvar_constraint()], type()}
               | id()  | qid()
               | con() | qcon()  %% contracts
               | tvar().
@@ -108,7 +118,7 @@
 
 -type bin_op() :: '+' | '-' | '*' | '/' | mod | '^'
                 | '++' | '::' | '<' | '>' | '=<' | '>=' | '==' | '!='
-                | '||' | '&&' | '..'.
+                | '||' | '&&' | '..' | '|>'.
 -type un_op() :: '-' | '!'.
 
 -type expr()

src/aeso_syntax_utils.erl

@@ -61,7 +61,6 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) ->
             {fun_t, _, Named, Args, Ret} -> Type([Named, Args, Ret]);
             {app_t, _, T, Ts}            -> Type([T | Ts]);
             {tuple_t, _, Ts}             -> Type(Ts);
-            {constrained_t, _, _, T}     -> Type(T);
             %% named_arg_t()
             {named_arg_t, _, _, T, E} -> Plus(Type(T), Expr(E));
             %% expr()

src/aesophia.app.src

@@ -1,6 +1,6 @@
 {application, aesophia,
  [{description, "Compiler for Aeternity Sophia language"},
-  {vsn, "6.1.0"},
+  {vsn, "7.1.0"},
   {registered, []},
   {applications,
    [kernel,

test/aeso_aci_tests.erl

@@ -21,7 +21,7 @@ test_cases(1) ->
 		 "  payable stateful entrypoint a(i : int) = i+1\n">>,
     MapACI = #{contract =>
 		   #{name => <<"C">>,
-		     type_defs => [],
+		     typedefs => [],
          payable => true,
          kind => contract_main,
 		     functions =>
@@ -43,7 +43,7 @@ test_cases(2) ->
     MapACI = #{contract =>
                    #{name => <<"C">>, payable => false,
                      kind => contract_main,
-                     type_defs =>
+                     typedefs =>
                          [#{name => <<"allan">>,
                             typedef => <<"int">>,
                             vars => []}],
@@ -76,7 +76,7 @@ test_cases(3) ->
 		     name => <<"C">>, payable => false, kind => contract_main,
          event => #{variant => [#{<<"SingleEventDefined">> => []}]},
          state => <<"unit">>,
-		     type_defs =>
+		     typedefs =>
              [#{name => <<"bert">>,
                 typedef =>
                     #{variant =>
@@ -127,7 +127,7 @@ check_stub(Stub, Options) ->
         Ast ->
             try
                 %% io:format("AST: ~120p\n", [Ast]),
-                aeso_ast_infer_types:infer(Ast, [])
+                aeso_ast_infer_types:infer(Ast, [no_code])
             catch throw:{type_errors, TE} ->
                 io:format("Type error:\n~s\n", [TE]),
                 error(TE);

test/aeso_calldata_tests.erl

@@ -29,7 +29,7 @@ calldata_aci_test_() ->
      [ {"Testing " ++ ContractName ++ " contract calling " ++ Fun,
         fun() ->
            ContractString       = aeso_test_utils:read_contract(ContractName),
-           {ok, ContractACIBin} = aeso_aci:contract_interface(string, ContractString),
+           {ok, ContractACIBin} = aeso_aci:contract_interface(string, ContractString, [no_code]),
            ContractACI = binary_to_list(ContractACIBin),
            io:format("ACI:\n~s\n", [ContractACIBin]),
            FateExprs = ast_exprs(ContractACI, Fun, Args),
@@ -39,7 +39,7 @@ calldata_aci_test_() ->
         end} || {ContractName, Fun, Args} <- compilable_contracts()].
 
 parse_args(Fun, Args) ->
-    [{contract_main, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
+    [{contract_main, _, _, _, [{letfun, _, _, _, _, [{guarded, _, [], {app, _, _, AST}}]}]}] =
         aeso_parser:string("main contract Temp = function foo() = " ++ Fun ++ "(" ++ string:join(Args, ", ") ++ ")"),
     strip_ann(AST).
 

test/aeso_compiler_tests.erl

@@ -45,12 +45,6 @@ simple_compile_test_() ->
            check_errors(ExpectedErrors, Errors)
        end} ||
            {ContractName, ExpectedErrors} <- failing_contracts() ] ++
-    [ {"Testing code generation error messages of " ++ ContractName,
-       fun() ->
-               Errors = compile(ContractName),
-               check_errors([ExpectedError], Errors)
-       end} ||
-           {ContractName, ExpectedError} <- failing_code_gen_contracts()] ++
     [ {"Testing include with explicit files",
        fun() ->
            FileSystem = maps:from_list(
@@ -75,6 +69,7 @@ simple_compile_test_() ->
     [ {"Testing warning messages",
        fun() ->
            #{ warnings := Warnings } = compile("warnings", [warn_all]),
+           #{ warnings := [] } = compile("warning_unused_include_no_include", [warn_all]),
            check_warnings(warnings(), Warnings)
        end} ] ++
     [].
@@ -202,6 +197,31 @@ compilable_contracts() ->
      "assign_patterns",
      "patterns_guards",
      "pipe_operator",
+     "polymorphism_contract_implements_interface",
+     "polymorphism_contract_multi_interface",
+     "polymorphism_contract_interface_extends_interface",
+     "polymorphism_contract_interface_extensions",
+     "polymorphism_contract_interface_same_decl_multi_interface",
+     "polymorphism_contract_interface_same_name_same_type",
+     "polymorphism_variance_switching_chain_create",
+     "polymorphism_variance_switching_void_supertype",
+     "polymorphism_variance_switching_unify_with_interface_decls",
+     "polymorphism_preserve_or_add_payable_contract",
+     "polymorphism_preserve_or_add_payable_entrypoint",
+     "polymorphism_preserve_or_remove_stateful_entrypoint",
+     "missing_init_fun_state_unit",
+     "complex_compare_leq",
+     "complex_compare",
+     "higher_order_compare",
+     "higher_order_map_keys",
+     "higher_order_state",
+     "polymorphic_compare",
+     "polymorphic_entrypoint",
+     "polymorphic_entrypoint_return",
+     "polymorphic_map_keys",
+     "unapplied_contract_call",
+     "unapplied_named_arg_builtin",
+     "resolve_field_constraint_by_arity",
      "test" % Custom general-purpose test file. Keep it last on the list.
     ].
 
@@ -265,9 +285,7 @@ warnings() ->
         "The function `called_unused_function2` is defined but never used.">>,
       <<?PosW(48, 5)
         "Unused return value.">>,
-      <<?PosW(53, 44)
-        "The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
-      <<?PosW(65, 5)
+      <<?PosW(60, 5)
         "The function `dec` is defined but never used.">>
      ]).
 
@@ -285,34 +303,26 @@ failing_contracts() ->
 
     %% Type errors
     , ?TYPE_ERROR(name_clash,
-       [<<?Pos(14, 3)
+       [<<?Pos(4, 3)
+          "Duplicate definitions of `double_def` at\n"
+          "  - line 3, column 3\n"
+          "  - line 4, column 3">>,
+        <<?Pos(7, 3)
           "Duplicate definitions of `abort` at\n"
           "  - (builtin location)\n"
-          "  - line 14, column 3">>,
-        <<?Pos(15, 3)
+          "  - line 7, column 3">>,
+        <<?Pos(8, 3)
           "Duplicate definitions of `require` at\n"
           "  - (builtin location)\n"
-          "  - line 15, column 3">>,
-        <<?Pos(11, 3)
-          "Duplicate definitions of `double_def` at\n"
-          "  - line 10, column 3\n"
-          "  - line 11, column 3">>,
-        <<?Pos(5, 3)
-          "Duplicate definitions of `double_proto` at\n"
-          "  - line 4, column 3\n"
-          "  - line 5, column 3">>,
-        <<?Pos(8, 3)
-          "Duplicate definitions of `proto_and_def` at\n"
-          "  - line 7, column 3\n"
           "  - line 8, column 3">>,
-        <<?Pos(16, 3)
+        <<?Pos(9, 3)
           "Duplicate definitions of `put` at\n"
           "  - (builtin location)\n"
-          "  - line 16, column 3">>,
-        <<?Pos(17, 3)
+          "  - line 9, column 3">>,
+        <<?Pos(10, 3)
           "Duplicate definitions of `state` at\n"
           "  - (builtin location)\n"
-          "  - line 17, column 3">>])
+          "  - line 10, column 3">>])
     , ?TYPE_ERROR(type_errors,
        [<<?Pos(17, 23)
           "Unbound variable `zz`">>,
@@ -566,7 +576,7 @@ failing_contracts() ->
       ])
     , ?TYPE_ERROR(list_comp_bad_shadow,
       [<<?Pos(2, 53)
-         "Cannot unify `int` and `string`\n"
+         "Cannot unify `string` and `int`\n"
          "when checking the type of the pattern `x : int` against the expected type `string`">>
       ])
     , ?TYPE_ERROR(map_as_map_key,
@@ -728,10 +738,22 @@ failing_contracts() ->
                      "Conflicting updates for field 'foo'">>])
     , ?TYPE_ERROR(factories_type_errors,
                   [<<?Pos(10,18)
-                    "Chain.clone requires `ref` named argument of contract type.">>,
+                     "Chain.clone requires `ref` named argument of contract type.">>,
                    <<?Pos(11,18)
-                     "Cannot unify `(gas : int, value : int, protected : bool) => if(protected, option(void), void)` and `(gas : int, value : int, protected : bool, int, bool) => 'b`\n"
-                     "when checking contract construction of type\n  (gas : int, value : int, protected : bool) =>\n    if(protected, option(void), void) (at line 11, column 18)\nagainst the expected type\n  (gas : int, value : int, protected : bool, int, bool) => 'b">>,
+                     "Cannot unify `(gas : int, value : int, protected : bool) => if(protected, option(void), void)` and `(gas : int, value : int, protected : bool, int, bool) => if(protected, option(void), void)`\n"
+                     "when checking contract construction of type\n"
+                     "  (gas : int, value : int, protected : bool) =>\n"
+                     "    if(protected, option(void), void) (at line 11, column 18)\n"
+                     "against the expected type\n"
+                     "  (gas : int, value : int, protected : bool, int, bool) =>\n"
+                     "    if(protected, option(void), void)">>,
+                   <<?Pos(11,18)
+                     "Cannot unify `Bakoom` and `Kaboom`\n"
+                     "when checking that contract construction of type\n"
+                     "  Bakoom\n"
+                     "arising from resolution of variadic function `Chain.clone`\n"
+                     "matches the expected type\n"
+                     "  Kaboom">>,
                    <<?Pos(12,37)
                      "Cannot unify `int` and `bool`\n"
                      "when checking named argument `gas : int` against inferred type `bool`">>,
@@ -807,88 +829,6 @@ failing_contracts() ->
                      "to arguments\n"
                      "  `1 : int`">>
                   ])
-    , ?TYPE_ERROR(comparable_typevar_constraints,
-                  [<<?Pos(21,30)
-                     "Values of type `'a` are not comparable by equality">>,
-                   <<?Pos(25,38)
-                     "The type variable `'b` is constrained but never used">>,
-                   <<?Pos(29,41)
-                     "Unknown constraint `foo` used on the type variable `'a`">>,
-                   <<?Pos(63,58)
-                     "Values of type `Chain.ttl` are not comparable by inequality">>,
-                   <<?Pos(66,45)
-                     "Values of type `A` are not comparable by inequality">>,
-                   <<?Pos(73,47)
-                     "Values of type `(int, char) => bool` are not comparable by inequality">>,
-                   <<?Pos(74,47)
-                     "Values of type `(int, char) => bool` are not comparable by equality">>,
-                   <<?Pos(89,59)
-                     "Values of type `list(A)` are not comparable by inequality">>,
-                   <<?Pos(92,65)
-                     "Values of type `option(A)` are not comparable by inequality">>,
-                   <<?Pos(95,64)
-                     "Values of type `(A * int)` are not comparable by inequality">>,
-                   <<?Pos(96,64)
-                     "Values of type `(A * int)` are not comparable by equality">>,
-                   <<?Pos(100,68)
-                     "Values of type `list((int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(101,68)
-                     "Values of type `list((int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(103,74)
-                     "Values of type `option((int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(104,74)
-                     "Values of type `option((int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(106,73)
-                     "Values of type `((int, char) => bool * int)` are not comparable by inequality">>,
-                   <<?Pos(107,73)
-                     "Values of type `((int, char) => bool * int)` are not comparable by equality">>,
-                   <<?Pos(111,71)
-                     "Values of type `map(int, int)` are not comparable by inequality">>,
-                   <<?Pos(114,80)
-                     "Values of type `oracle(int, int)` are not comparable by inequality">>,
-                   <<?Pos(117,98)
-                     "Values of type `oracle_query(int, int)` are not comparable by inequality">>,
-                   <<?Pos(120,90)
-                     "Values of type `custom_datatype(int)` are not comparable by inequality">>,
-                   <<?Pos(123,84)
-                     "Values of type `custom_record(int)` are not comparable by inequality">>,
-                   <<?Pos(128,62)
-                     "Values of type `map(A, A)` are not comparable by inequality">>,
-                   <<?Pos(131,71)
-                     "Values of type `oracle(A, A)` are not comparable by inequality">>,
-                   <<?Pos(134,89)
-                     "Values of type `oracle_query(A, A)` are not comparable by inequality">>,
-                   <<?Pos(137,85)
-                     "Values of type `custom_datatype(A)` are not comparable by inequality">>,
-                   <<?Pos(140,79)
-                     "Values of type `custom_record(A)` are not comparable by inequality">>,
-                   <<?Pos(145,75)
-                     "Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(146,75)
-                     "Values of type `map((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(148,84)
-                     "Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(149,84)
-                     "Values of type `oracle((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(151,102)
-                     "Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(152,102)
-                     "Values of type `oracle_query((int, char) => bool, (int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(154,94)
-                     "Values of type `custom_datatype((int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(155,94)
-                     "Values of type `custom_datatype((int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(157,88)
-                     "Values of type `custom_record((int, char) => bool)` are not comparable by inequality">>,
-                   <<?Pos(158,88)
-                     "Values of type `custom_record((int, char) => bool)` are not comparable by equality">>,
-                   <<?Pos(162,35)
-                     "Values of type `map(int, int)` are not comparable by inequality">>,
-                   <<?Pos(163,35)
-                     "Values of type `('a) => 'a` are not comparable by inequality">>,
-                   <<?Pos(167,34)
-                     "Values of type `('b) => 'b` are not comparable by equality">>
-                  ])
     , ?TYPE_ERROR(warnings,
                   [<<?Pos(0, 0)
                       "The file `Triple.aes` is included but not used.">>,
@@ -918,62 +858,341 @@ failing_contracts() ->
                      "The function `called_unused_function2` is defined but never used.">>,
                    <<?Pos(48, 5)
                      "Unused return value.">>,
-                   <<?Pos(53, 44)
-                     "The constraint on the type variable `'a` is a duplication of the constraint at line 53, column 34">>,
-                   <<?Pos(65, 5)
+                   <<?Pos(60, 5)
                      "The function `dec` is defined but never used.">>
                   ])
-    ].
-
--define(Path(File), "code_errors/" ??File).
--define(Msg(File, Line, Col, Err), <<?Pos("Code generation", ?Path(File), Line, Col) Err>>).
-
--define(FATE_ERR(File, Line, Col, Err), {?Path(File), ?Msg(File, Line, Col, Err)}).
-
-failing_code_gen_contracts() ->
-    [ ?FATE_ERR(missing_definition, 2, 14,
-            "Missing definition of function 'foo'.")
-    , ?FATE_ERR(higher_order_entrypoint, 2, 20,
-            "The argument\n"
-            "  f : (int) => int\n"
-            "of entrypoint 'apply' has a higher-order (contains function types) type.")
-    , ?FATE_ERR(higher_order_entrypoint_return, 2, 3,
-            "The return type\n"
-            "  (int) => int\n"
-            "of entrypoint 'add' is higher-order (contains function types).")
-    , ?FATE_ERR(missing_init_function, 1, 10,
-            "Missing init function for the contract 'MissingInitFunction'.\n"
-            "The 'init' function can only be omitted if the state type is 'unit'.")
-    , ?FATE_ERR(parameterised_state, 3, 8,
-            "The state type cannot be parameterized.")
-    , ?FATE_ERR(parameterised_event, 3, 12,
-            "The event type cannot be parameterized.")
-    , ?FATE_ERR(polymorphic_aens_resolve, 4, 5,
-            "Invalid return type of AENS.resolve:\n"
-            "  'a\n"
-            "It must be a string or a pubkey type (address, oracle, etc).")
-    , ?FATE_ERR(bad_aens_resolve, 6, 5,
-            "Invalid return type of AENS.resolve:\n"
-            "  list(int)\n"
-            "It must be a string or a pubkey type (address, oracle, etc).")
-    , ?FATE_ERR(polymorphic_query_type, 3, 5,
-            "Invalid oracle type\n"
-            "  oracle('a, 'b)\n"
-            "The query type must not be polymorphic (contain type variables).")
-    , ?FATE_ERR(polymorphic_response_type, 3, 5,
-            "Invalid oracle type\n"
-            "  oracle(string, 'r)\n"
-            "The response type must not be polymorphic (contain type variables).")
-    , ?FATE_ERR(higher_order_query_type, 3, 5,
-            "Invalid oracle type\n"
-            "  oracle((int) => int, string)\n"
-            "The query type must not be higher-order (contain function types).")
-    , ?FATE_ERR(higher_order_response_type, 3, 5,
-            "Invalid oracle type\n"
-            "  oracle(string, (int) => int)\n"
-            "The response type must not be higher-order (contain function types).")
-    , ?FATE_ERR(child_with_decls, 2, 14,
-            "Missing definition of function 'f'.")
+    , ?TYPE_ERROR(polymorphism_contract_interface_recursive,
+                  [<<?Pos(1,24)
+                     "Trying to implement or extend an undefined interface `Z`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_interface_same_name_different_type,
+                  [<<?Pos(9,5)
+                     "Duplicate definitions of `f` at\n"
+                     "  - line 8, column 5\n"
+                     "  - line 9, column 5">>])
+    , ?TYPE_ERROR(polymorphism_contract_missing_implementation,
+                  [<<?Pos(4,20)
+                     "Unimplemented entrypoint `f` from the interface `I1` in the contract `I2`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_same_decl_multi_interface,
+                  [<<?Pos(7,10)
+                     "Both interfaces `I` and `J` implemented by the contract `C` have a function called `f`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_undefined_interface,
+                  [<<?Pos(1,14)
+                     "Trying to implement or extend an undefined interface `I`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_same_name_different_type_multi_interface,
+                  [<<?Pos(7,10)
+                     "Both interfaces `I` and `J` implemented by the contract `C` have a function called `f`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_contract_interface_undefined_interface,
+                  [<<?Pos(1,24)
+                     "Trying to implement or extend an undefined interface `H`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_variance_switching,
+                  [<<?Pos(36,49)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the application of\n"
+                     "  `g2 : (Cat) => Cat`\n"
+                     "to arguments\n"
+                     "  `x : Animal`">>,
+                   <<?Pos(39,43)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `g3(x) : Animal` against the expected type `Cat`">>,
+                   <<?Pos(48,55)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the application of\n"
+                     "  `g5 : ((Animal) => Animal) => Cat`\n"
+                     "to arguments\n"
+                     "  `x : (Cat) => Cat`">>,
+                   <<?Pos(52,44)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `f6() : option(Animal)` against the expected type `option(Cat)`">>,
+                   <<?Pos(73,43)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `some_animal : Animal` against the expected type `Cat`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_variance_switching_custom_types,
+                  [<<?Pos(56,39)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_CONTRA(f_c_to_u) : dt_contra(Cat)` against the expected type `dt_contra(Animal)`">>,
+                   <<?Pos(62,35)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `DT_CO(f_u_to_a) : dt_co(Animal)` against the expected type `dt_co(Cat)`">>,
+                   <<?Pos(67,36)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the application of\n  `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n  `f_c_to_a : (Cat) => Animal`">>,
+                   <<?Pos(68,36)
+                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV(f_c_to_c) : dt_inv(Cat)` against the expected type `dt_inv(Animal)`">>,
+                   <<?Pos(69,36)
+                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV(f_a_to_a) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
+                   <<?Pos(70,36)
+                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV(f_a_to_c) : dt_inv(Animal)` against the expected type `dt_inv(Cat)`">>,
+                   <<?Pos(71,36)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the application of\n  `DT_INV : ((Cat) => Cat) => dt_inv(Cat)`\nto arguments\n  `f_c_to_a : (Cat) => Animal`">>,
+                   <<?Pos(80,40)
+                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV_SEP_A(f_c_to_u) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
+                   <<?Pos(82,40)
+                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV_SEP_B(f_u_to_c) : dt_inv_sep(Cat)` against the expected type `dt_inv_sep(Animal)`">>,
+                   <<?Pos(83,40)
+                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV_SEP_A(f_a_to_u) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
+                   <<?Pos(85,40)
+                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
+                     "when checking the type of the expression `DT_INV_SEP_B(f_u_to_a) : dt_inv_sep(Animal)` against the expected type `dt_inv_sep(Cat)`">>,
+                   <<?Pos(90,42)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `DT_CO_NEST_A(f_dt_contra_a_to_u) : dt_co_nest_a(Animal)` against the expected type `dt_co_nest_a(Cat)`">>,
+                   <<?Pos(94,46)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_CONTRA_NEST_A(f_dt_co_c_to_u) : dt_contra_nest_a(Cat)` against the expected type `dt_contra_nest_a(Animal)`">>,
+                   <<?Pos(99,46)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_CONTRA_NEST_B(f_u_to_dt_contra_c) : dt_contra_nest_b(Cat)` against the expected type `dt_contra_nest_b(Animal)`">>,
+                   <<?Pos(105,42)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the expression `DT_CO_NEST_B(f_u_to_dt_co_a) : dt_co_nest_b(Animal)` against the expected type `dt_co_nest_b(Cat)`">>,
+                   <<?Pos(110,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `vj3 : dt_co_twice(Cat)` against the expected type `dt_co_twice(Animal)`">>,
+                   <<?Pos(114,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
+                   <<?Pos(115,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
+                   <<?Pos(116,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Animal)`">>,
+                   <<?Pos(119,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u) : dt_a_contra_b_contra(Cat, Animal)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
+                   <<?Pos(120,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Animal, Cat)`">>,
+                   <<?Pos(122,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u) : dt_a_contra_b_contra(Animal, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
+                   <<?Pos(124,59)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the expression `DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u) : dt_a_contra_b_contra(Cat, Cat)` against the expected type `dt_a_contra_b_contra(Cat, Animal)`">>,
+                   <<?Pos(131,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `vl2 : dt_contra_twice(Animal)` against the expected type `dt_contra_twice(Cat)`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_variance_switching_records,
+                  [<<?Pos(27,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `r03 : rec_co(Cat)` against the expected type `Main.rec_co(Animal)`">>,
+                   <<?Pos(33,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `r06 : rec_contra(Animal)` against the expected type `Main.rec_contra(Cat)`">>,
+                   <<?Pos(40,13)
+                     "Cannot unify `Cat` and `Animal` in a invariant context\n"
+                     "when checking the type of the pattern `r10 : rec_inv(Animal)` against the expected type `Main.rec_inv(Cat)`">>,
+                   <<?Pos(41,13)
+                     "Cannot unify `Animal` and `Cat` in a invariant context\n"
+                     "when checking the type of the pattern `r11 : rec_inv(Cat)` against the expected type `Main.rec_inv(Animal)`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_variance_switching_oracles,
+                  [<<?Pos(15,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `o03 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(16,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `o04 : oracle(Animal, Animal)` against the expected type `oracle(Cat, Cat)`">>,
+                   <<?Pos(17,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `o05 : oracle(Animal, Cat)` against the expected type `oracle(Animal, Animal)`">>,
+                   <<?Pos(19,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `o07 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(20,13)
+                     "Cannot unify `Cat` and `Animal` in a contravariant context\n"
+                     "when checking the type of the pattern `o08 : oracle(Animal, Cat)` against the expected type `oracle(Cat, Cat)`">>,
+                   <<?Pos(25,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `o13 : oracle(Cat, Cat)` against the expected type `oracle(Animal, Animal)`">>,
+                   <<?Pos(27,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `o15 : oracle(Cat, Cat)` against the expected type `oracle(Cat, Animal)`">>,
+                   <<?Pos(34,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q05 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
+                   <<?Pos(36,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q07 : oracle_query(Animal, Cat)` against the expected type `oracle_query(Cat, Animal)`">>,
+                   <<?Pos(38,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q09 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Animal)`">>,
+                   <<?Pos(39,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q10 : oracle_query(Cat, Animal)` against the expected type `oracle_query(Animal, Cat)`">>,
+                   <<?Pos(42,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q13 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Animal)`">>,
+                   <<?Pos(43,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q14 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Animal, Cat)`">>,
+                   <<?Pos(44,13)
+                     "Cannot unify `Animal` and `Cat` in a covariant context\n"
+                     "when checking the type of the pattern `q15 : oracle_query(Cat, Cat)` against the expected type `oracle_query(Cat, Animal)`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_variance_switching_chain_create_fail,
+                  [<<?Pos(9,22)
+                     "I is not implemented.\n"
+                     "when resolving arguments of variadic function `Chain.create`">>,
+                   <<?Pos(10,13)
+                     "Cannot unify `I` and `C` in a covariant context\n"
+                     "when checking the type of the pattern `c2 : C` against the expected type `I`">>,
+                   <<?Pos(10,22)
+                     "I is not implemented.\n"
+                     "when resolving arguments of variadic function `Chain.create`">>,
+                   <<?Pos(11,22)
+                     "I is not implemented.\n"
+                     "when resolving arguments of variadic function `Chain.create`">>
+                  ])
+    , ?TYPE_ERROR(missing_definition,
+                  [<<?Pos(2,14)
+                     "Missing definition of function `foo`">>
+                  ])
+    , ?TYPE_ERROR(child_with_decls,
+                  [<<?Pos(2,14)
+                     "Missing definition of function `f`">>
+                  ])
+    , ?TYPE_ERROR(parameterised_state,
+                  [<<?Pos(3,8)
+                     "The state type cannot be parameterized">>
+                  ])
+    , ?TYPE_ERROR(parameterised_event,
+                  [<<?Pos(3,12)
+                     "The event type cannot be parameterized">>
+                  ])
+    , ?TYPE_ERROR(missing_init_fun_alias_to_type,
+                  [<<?Pos(1,10)
+                     "Missing `init` function for the contract `AliasToType`.\n"
+                     "The `init` function can only be omitted if the state type is `unit`">>
+                  ])
+    , ?TYPE_ERROR(missing_init_fun_alias_to_alias_to_type,
+                  [<<?Pos(1,10)
+                     "Missing `init` function for the contract `AliasToAliasToType`.\n"
+                     "The `init` function can only be omitted if the state type is `unit`">>
+                  ])
+    , ?TYPE_ERROR(higher_order_entrypoint,
+                  [<<?Pos(2,20)
+                     "The argument\n"
+                     "  `f : (int) => int`\n"
+                     "of entrypoint `apply` has a higher-order (contains function types) type">>
+                  ])
+    , ?TYPE_ERROR(higher_order_entrypoint_return,
+                  [<<?Pos(2,3)
+                     "The return type\n"
+                     "  `(int) => int`\n"
+                     "of entrypoint `add` is higher-order (contains function types)">>
+                  ])
+    , ?TYPE_ERROR(polymorphic_aens_resolve,
+                  [<<?Pos(4,5)
+                     "Invalid return type of `AENS.resolve`:\n"
+                     "  `'a`\n"
+                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
+                  ])
+    , ?TYPE_ERROR(bad_aens_resolve,
+                  [<<?Pos(6,5)
+                     "Invalid return type of `AENS.resolve`:\n"
+                     "  `list(int)`\n"
+                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
+                  ])
+    , ?TYPE_ERROR(bad_aens_resolve_using,
+                  [<<?Pos(7,5)
+                     "Invalid return type of `AENS.resolve`:\n"
+                     "  `list(int)`\n"
+                     "It must be a `string` or a pubkey type (`address`, `oracle`, etc)">>
+                  ])
+    , ?TYPE_ERROR(polymorphic_query_type,
+                  [<<?Pos(3,5)
+                     "Invalid oracle type\n"
+                     "  `oracle('a, 'b)`\n"
+                     "The query type must not be polymorphic (contain type variables)">>,
+                   <<?Pos(3,5)
+                     "Invalid oracle type\n"
+                     "  `oracle('a, 'b)`\n"
+                     "The response type must not be polymorphic (contain type variables)">>
+                  ])
+    , ?TYPE_ERROR(polymorphic_response_type,
+                  [<<?Pos(3,5)
+                     "Invalid oracle type\n"
+                     "  `oracle(string, 'r)`\n"
+                     "The response type must not be polymorphic (contain type variables)">>
+                  ])
+    , ?TYPE_ERROR(higher_order_query_type,
+                  [<<?Pos(3,5)
+                     "Invalid oracle type\n"
+                     "  `oracle((int) => int, string)`\n"
+                     "The query type must not be higher-order (contain function types)">>
+                  ])
+    , ?TYPE_ERROR(higher_order_response_type,
+                  [<<?Pos(3,5)
+                     "Invalid oracle type\n"
+                     "  `oracle(string, (int) => int)`\n"
+                     "The response type must not be higher-order (contain function types)">>
+                  ])
+    , ?TYPE_ERROR(var_args_unify_let,
+                  [<<?Pos(3,9)
+                     "Cannot infer types for variable argument list.\n"
+                     "when checking the type of the pattern `x : 'a` against the expected type `(gas : int, value : int, protected : bool, ref : 'b, var_args) => 'b`">>
+                  ])
+    , ?TYPE_ERROR(var_args_unify_fun_call,
+                  [<<?Pos(6,5)
+                     "Cannot infer types for variable argument list.\n"
+                     "when checking the application of\n"
+                     "  `g : (() => 'b) => 'b`\n"
+                     "to arguments\n"
+                     "  `Chain.create : (value : int, var_args) => 'c`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_add_stateful_entrypoint,
+                  [<<?Pos(5,25)
+                     "`f` cannot be stateful because the entrypoint `f` in the interface `I` is not stateful">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_change_entrypoint_to_function,
+                  [<<?Pos(6,14)
+                     "`f` must be declared as an entrypoint instead of a function in order to implement the entrypoint `f` from the interface `I`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_non_payable_contract_implement_payable,
+                  [<<?Pos(4,10)
+                     "Non-payable contract `C` cannot implement payable interface `I`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_non_payable_interface_implement_payable,
+                  [<<?Pos(4,20)
+                     "Non-payable interface `H` cannot implement payable interface `I`">>
+                  ])
+    , ?TYPE_ERROR(polymorphism_remove_payable_entrypoint,
+                  [<<?Pos(5,16)
+                     "`f` must be payable because the entrypoint `f` in the interface `I` is payable">>
+                  ])
+    , ?TYPE_ERROR(calling_child_contract_entrypoint,
+                  [<<?Pos(5,20)
+                     "Invalid call to contract entrypoint `F.g`.\n"
+                     "It must be called as `c.g` for some `c : F`.">>])
+    , ?TYPE_ERROR(using_contract_as_namespace,
+                  [<<?Pos(5,3)
+                     "Cannot use undefined namespace F">>])
+    , ?TYPE_ERROR(hole_expression,
+                  [<<?Pos(5,13)
+                     "Found a hole of type `bool`">>,
+                   <<?Pos(6,17)
+                     "Found a hole of type `string`">>,
+                   <<?Pos(9,37)
+                     "Found a hole of type `(int) => int`">>,
+                   <<?Pos(13,20)
+                     "Found a hole of type `'a`">>
+                  ])
     ].
 
 validation_test_() ->

test/aeso_parser_tests.erl

@@ -15,7 +15,7 @@ simple_contracts_test_() ->
             Text = "main contract Identity =\n"
                    "  function id(x) = x\n",
             ?assertMatch(
-                [{contract_main, _, {con, _, "Identity"},
+                [{contract_main, _, {con, _, "Identity"}, _,
                     [{letfun, _, {id, _, "id"}, [{id, _, "x"}], {id, _, "_"},
                         [{guarded, _, [], {id, _, "x"}}]}]}], parse_string(Text)),
             ok

test/contracts/aens.aes

@@ -1,5 +1,7 @@
+contract C = entrypoint init() = ()
+
 // AENS tests
-contract AENSTest =
+main contract AENSTest =
 
   // Name resolution
 
@@ -9,10 +11,19 @@ contract AENSTest =
   stateful entrypoint resolve_string(name : string, key : string) : option(string) =
     AENS.resolve(name, key)
 
+  stateful entrypoint resolve_contract(name : string, key : string) : option(C) =
+    AENS.resolve(name, key)
+
+  stateful entrypoint resolve_oracle(name : string, key : string) : option(oracle(int, int)) =
+    AENS.resolve(name, key)
+
+  stateful entrypoint resolve_oracle_query(name : string, key : string) : option(oracle_query(int, int)) =
+    AENS.resolve(name, key)
+
   // Transactions
 
   stateful entrypoint preclaim(addr  : address,     // Claim on behalf of this account (can be Contract.address)
-                             chash : hash) : unit = // Commitment hash
+                               chash : hash) : unit = // Commitment hash
     AENS.preclaim(addr, chash)
 
   stateful entrypoint signedPreclaim(addr  : address, // Claim on behalf of this account (can be Contract.address)

test/contracts/all_syntax.aes

@@ -80,3 +80,4 @@ contract AllSyntax =
      let sh : shakespeare(shakespeare(int)) =
        {wolfgang = state}
      sh{wolfgang.wolfgang = sh.wolfgang} // comment
+     exit("hope you had fun reading this")

test/contracts/bad_aens_resolve_using.aes

@@ -0,0 +1,9 @@
+contract BadAENSresolve =
+  using AENS
+
+  type t('a) = option(list('a))
+
+  function fail() : t(int) =
+    resolve("foo.aet", "whatever")
+
+  entrypoint main_fun() = ()

test/contracts/calling_child_contract_entrypoint.aes

@@ -0,0 +1,5 @@
+contract F =
+  entrypoint g() = 1
+
+main contract C =
+  entrypoint f() = F.g()

test/contracts/code_errors/missing_init_function.aes

@@ -1,3 +0,0 @@
-contract MissingInitFunction =
-  type state = int * int
-

test/contracts/comparable_typevar_constraints.aes

@@ -1,169 +0,0 @@
-contract A = entrypoint init() = ()
-
-main contract C =
-    datatype custom_datatype('a) = CD('a)
-
-    record custom_record('a) = { f : 'a }
-
-    // pass
-    function
-        passing_ord : 'a is ord ; ('a, 'a) => bool
-        passing_ord(x, y) = x >= y
-
-    // pass
-    function
-        passing_eq : 'a is eq ; ('a, 'a) => bool
-        passing_eq(x, y) = x == y
-
-    // fail because eq is not specified for 'a
-    function
-        fail_no_eq : ('a, 'a) => bool
-        fail_no_eq(x, y) = x == y
-
-    // fail because 'b is not used
-    function
-        fail_unused_tvar : 'a is eq, 'b is eq ; ('a, 'a) => bool
-        fail_unused_tvar(x, y) = x == y
-
-    function
-        fail_unknown_constraint : 'a is foo ; ('a) => 'a
-        fail_unknown_constraint(x) = x
-
-    // Ord types
-
-    function bool_ord(x : bool, y : bool) = x >= y  // pass
-    function bool_eq (x : bool, y : bool) = x == y  // pass
-
-    function int_ord(x : int, y : int) = x >= y  // pass
-    function int_eq (x : int, y : int) = x == y  // pass
-
-    function char_ord(x : char, y : char) = x >= y  // pass
-    function char_eq (x : char, y : char) = x == y  // pass
-
-    function bits_ord(x : bits, y : bits) = x >= y  // pass
-    function bits_eq (x : bits, y : bits) = x == y  // pass
-
-    function bytes_ord(x : bytes(16), y : bytes(16)) = x >= y  // pass
-    function bytes_eq (x : bytes(16), y : bytes(16)) = x == y  // pass
-
-    function string_ord(x : string, y : string) = x >= y  // pass
-    function string_eq (x : string, y : string) = x == y  // pass
-
-    function hash_ord(x : hash, y : hash) = x >= y  // pass
-    function hash_eq (x : hash, y : hash) = x == y  // pass
-
-    function signature_ord(x : signature, y : signature) = x >= y  // pass
-    function signature_eq (x : signature, y : signature) = x == y  // pass
-
-    function address_ord(x : address, y : address) = x >= y  // pass
-    function address_eq (x : address, y : address) = x == y  // pass
-
-    // Eq types
-
-    function event_ord(x : Chain.ttl, y : Chain.ttl) = x >= y  // fail
-    function event_eq (x : Chain.ttl, y : Chain.ttl) = x == y  // pass
-
-    function contract_ord(x : A, y : A) = x >= y  // fail
-    function contract_eq (x : A, y : A) = x == y  // pass
-
-    // Noncomparable types
-
-    type lam = (int, char) => bool
-
-    function lambda_ord(x : lam, y : lam) = x >= y  // fail
-    function lambda_eq (x : lam, y : lam) = x == y  // fail
-
-    // Ord composite types of ord
-
-    function list_of_ord_ord(x : list(int), y : list(int)) = x >= y  // pass
-    function list_of_ord_eq (x : list(int), y : list(int)) = x == y  // pass
-
-    function option_of_ord_ord(x : option(int), y : option(int)) = x >= y  // pass
-    function option_of_ord_eq (x : option(int), y : option(int)) = x == y  // pass
-
-    function tuple_of_ord_ord(x : (int * bool), y : (int * bool)) = x >= y  // pass
-    function tuple_of_ord_eq (x : (int * bool), y : (int * bool)) = x == y  // pass
-
-    // Ord composite types of eq
-
-    function list_of_eq_ord(x : list(A), y : list(A)) = x >= y  // fail
-    function list_of_eq_eq (x : list(A), y : list(A)) = x == y  // pass
-
-    function option_of_eq_ord(x : option(A), y : option(A)) = x >= y  // fail
-    function option_of_eq_eq (x : option(A), y : option(A)) = x == y  // pass
-
-    function tuple_of_eq_ord(x : (A * int), y : (A * int)) = x >= y  // fail
-    function tuple_of_eq_eq (x : (A * int), y : (A * int)) = x == y  // pass
-
-    // Ord composite types of nomcomparable
-
-    function list_of_noncomp_ord(x : list(lam), y : list(lam)) = x >= y  // fail
-    function list_of_noncomp_eq (x : list(lam), y : list(lam)) = x == y  // fail
-
-    function option_of_noncomp_ord(x : option(lam), y : option(lam)) = x >= y  // fail
-    function option_of_noncomp_eq (x : option(lam), y : option(lam)) = x == y  // fail
-
-    function tuple_of_noncomp_ord(x : (lam * int), y : (lam * int)) = x >= y  // fail
-    function tuple_of_noncomp_eq (x : (lam * int), y : (lam * int)) = x == y  // fail
-
-    // Eq composite types of ord
-
-    function map_of_ord_ord(x : map(int, int), y : map(int, int)) = x >= y  // fail
-    function map_of_ord_eq (x : map(int, int), y : map(int, int)) = x == y  // pass
-
-    function oracle_of_ord_ord(x : oracle(int, int), y : oracle(int, int)) = x >= y  // fail
-    function oracle_of_ord_eq (x : oracle(int, int), y : oracle(int, int)) = x == y  // pass
-
-    function oracle_query_of_ord_ord(x : oracle_query(int, int), y : oracle_query(int, int)) = x >= y  // fail
-    function oracle_query_of_ord_eq (x : oracle_query(int, int), y : oracle_query(int, int)) = x == y  // pass
-
-    function datatype_of_ord_ord(x : custom_datatype(int), y : custom_datatype(int)) = x >= y  // fail
-    function datatype_of_ord_eq (x : custom_datatype(int), y : custom_datatype(int)) = x == y  // pass
-
-    function record_of_ord_ord(x : custom_record(int), y : custom_record(int)) = x >= y  // fail
-    function record_of_ord_eq (x : custom_record(int), y : custom_record(int)) = x == y  // pass
-
-    // Eq composite types of eq
-
-    function map_of_eq_ord(x : map(A, A), y : map(A, A)) = x >= y  // fail
-    function map_of_eq_eq (x : map(A, A), y : map(A, A)) = x == y  // pass
-
-    function oracle_of_eq_ord(x : oracle(A, A), y : oracle(A, A)) = x >= y  // fail
-    function oracle_of_eq_eq (x : oracle(A, A), y : oracle(A, A)) = x == y  // pass
-
-    function oracle_query_of_eq_ord(x : oracle_query(A, A), y : oracle_query(A, A)) = x >= y  // fail
-    function oracle_query_of_eq_eq (x : oracle_query(A, A), y : oracle_query(A, A)) = x == y  // pass
-
-    function datatype_of_eq_ord(x : custom_datatype(A), y : custom_datatype(A)) = x >= y  // fail
-    function datatype_of_eq_eq (x : custom_datatype(A), y : custom_datatype(A)) = x == y  // pass
-
-    function record_of_eq_ord(x : custom_record(A), y : custom_record(A)) = x >= y  // fail
-    function record_of_eq_eq (x : custom_record(A), y : custom_record(A)) = x == y  // pass
-
-    // Eq composite types of nomcomparable
-
-    function map_of_noncomp_ord(x : map(lam, lam), y : map(lam, lam)) = x >= y  // fail
-    function map_of_noncomp_eq (x : map(lam, lam), y : map(lam, lam)) = x == y  // fail
-
-    function oracle_of_noncomp_ord(x : oracle(lam, lam), y : oracle(lam, lam)) = x >= y  // fail
-    function oracle_of_noncomp_eq (x : oracle(lam, lam), y : oracle(lam, lam)) = x == y  // fail
-
-    function oracle_query_of_noncomp_ord(x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x >= y  // fail
-    function oracle_query_of_noncomp_eq (x : oracle_query(lam, lam), y : oracle_query(lam, lam)) = x == y  // fail
-
-    function datatype_of_noncomp_ord(x : custom_datatype(lam), y : custom_datatype(lam)) = x >= y  // fail
-    function datatype_of_noncomp_eq (x : custom_datatype(lam), y : custom_datatype(lam)) = x == y  // pass
-
-    function record_of_nomcomp_ord(x : custom_record(lam), y : custom_record(lam)) = x >= y  // fail
-    function record_of_nomcomp_eq (x : custom_record(lam), y : custom_record(lam)) = x == y  // pass
-
-    entrypoint init() =
-        let passing_ord_ord     = passing_ord([1], [2])              // pass
-        let passing_ord_eq      = passing_ord({[1] = 2}, {[2] = 3})  // fail
-        let passing_ord_noncomp = passing_ord((x) => x, (x) => x)    // fail
-
-        let passing_eq_ord     = passing_eq([1], [2])              // pass
-        let passing_eq_eq      = passing_eq({[1] = 2}, {[2] = 3})  // pass
-        let passing_eq_noncomp = passing_eq((x) => x, (x) => x)    // fail
-
-        ()

test/contracts/complex_types.aes

@@ -1,16 +1,7 @@
 
-contract interface Remote =
-  entrypoint up_to       : (int)               => list(int)
-  entrypoint sum         : (list(int))         => int
-  entrypoint some_string : ()                  => string
-  entrypoint pair        : (int, string)       => int * string
-  entrypoint squares     : (int)               => list(int * int)
-  entrypoint filter_some : (list(option(int))) => list(int)
-  entrypoint all_some    : (list(option(int))) => option(list(int))
-
 contract ComplexTypes =
 
-  record state = { worker : Remote }
+  record state = { worker : ComplexTypes }
 
   entrypoint init(worker) = {worker = worker}
 

test/contracts/environment.aes

@@ -1,14 +1,9 @@
 
 // Testing primitives for accessing the block chain environment
-contract interface Interface =
-  entrypoint contract_address : () => address
-  entrypoint call_origin      : () => address
-  entrypoint call_caller      : () => address
-  entrypoint call_value       : () => int
 
 contract Environment =
 
-  record state = {remote : Interface}
+  record state = {remote : Environment}
 
   entrypoint init(remote) = {remote = remote}
 

test/contracts/hole_expression.aes

@@ -0,0 +1,13 @@
+include "List.aes"
+
+contract C =
+    entrypoint f() =
+        let ??? = true
+        let v = ???
+        let q = v == "str"
+        let xs = [1, 2, 3, 4]
+        switch (List.first(List.map(???, xs)))
+            Some(x) => x + 1
+            None    => 0
+
+    function g() = ???

test/contracts/missing_init_fun_alias_to_alias_to_type.aes

@@ -0,0 +1,3 @@
+contract AliasToAliasToType =
+  type alias = int * int
+  type state = alias

test/contracts/missing_init_fun_alias_to_type.aes

@@ -0,0 +1,2 @@
+contract AliasToType =
+  type state = int * int

test/contracts/missing_init_fun_state_unit.aes

@@ -0,0 +1,9 @@
+contract AliasToAliasToUnit =
+  type alias = unit
+  type state = alias
+
+contract AliasToUnit =
+  type state = unit
+
+main contract ImplicitState =
+    type sometype = int

test/contracts/name_clash.aes

@@ -1,12 +1,5 @@
-
 contract NameClash =
 
-  entrypoint double_proto : () => int
-  entrypoint double_proto : () => int
-
-  entrypoint proto_and_def : int => int
-  entrypoint proto_and_def(n) = n + 1
-
   entrypoint double_def(x) = x
   entrypoint double_def(y) = 0
 
@@ -14,4 +7,4 @@ contract NameClash =
   entrypoint abort() : int = 0
   entrypoint require(b, err) = if(b) abort(err)
   entrypoint put(x) = x
-  entrypoint state(x, y) = x + y
+  entrypoint state(x, y) = x + y

test/contracts/polymorphism_add_stateful_entrypoint.aes

@@ -0,0 +1,5 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract C : I =
+    stateful entrypoint f() = 1

test/contracts/polymorphism_change_entrypoint_to_function.aes

@@ -0,0 +1,6 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract C : I =
+    entrypoint init() = ()
+    function f() = 1

test/contracts/polymorphism_contract_implements_interface.aes

@@ -0,0 +1,5 @@
+contract interface Strokable =
+  entrypoint stroke : () => string
+
+contract Cat : Strokable =
+  entrypoint stroke() = "Cat stroke"

test/contracts/polymorphism_contract_interface_extends_interface.aes

@@ -0,0 +1,10 @@
+contract interface II =
+    entrypoint f : () => unit
+
+contract interface I : II =
+    entrypoint f : () => unit
+    entrypoint g : () => unit
+
+contract C : I =
+    entrypoint f() = ()
+    entrypoint g() = ()

test/contracts/polymorphism_contract_interface_extensions.aes

@@ -0,0 +1,9 @@
+contract interface I0 =
+  entrypoint f : () => int
+
+contract interface I1 : I0 =
+  entrypoint f : () => int
+  entrypoint something_else : () => int
+
+main contract C =
+  entrypoint f(x : I1) = x.f() // Here we should know that x has f

test/contracts/polymorphism_contract_interface_recursive.aes

@@ -0,0 +1,13 @@
+contract interface X : Z =
+    entrypoint x : () => int
+
+contract interface Y : X =
+    entrypoint y : () => int
+
+contract interface Z : Y =
+    entrypoint z : () => int
+
+contract C : Z =
+    entrypoint x() = 1
+    entrypoint y() = 1
+    entrypoint z() = 1

test/contracts/polymorphism_contract_interface_same_decl_multi_interface.aes

@@ -0,0 +1,8 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface II : I =
+    entrypoint f : () => int
+
+contract C : II =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_interface_same_name_different_type.aes

@@ -0,0 +1,9 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint f : () => char
+
+contract C : I2 =
+    entrypoint f() = 1
+    entrypoint f() = 'c'

test/contracts/polymorphism_contract_interface_same_name_same_type.aes

@@ -0,0 +1,8 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint f : () => int
+
+contract C : I2 =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_interface_undefined_interface.aes

@@ -0,0 +1,5 @@
+contract interface I : H =
+    entrypoint f : () => unit
+
+contract C =
+    entrypoint g() = ()

test/contracts/polymorphism_contract_missing_implementation.aes

@@ -0,0 +1,8 @@
+contract interface I1 =
+    entrypoint f : () => int
+
+contract interface I2 : I1 =
+    entrypoint g : () => int
+
+contract C : I2 =
+    entrypoint g() = 1

test/contracts/polymorphism_contract_multi_interface.aes

@@ -0,0 +1,9 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint g : () => char
+
+contract C : I, J =
+    entrypoint f() = 1
+    entrypoint g() = 'c'

test/contracts/polymorphism_contract_same_decl_multi_interface.aes

@@ -0,0 +1,8 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint f : () => int
+
+contract C : I, J =
+    entrypoint f() = 1

test/contracts/polymorphism_contract_same_name_different_type_multi_interface.aes

@@ -0,0 +1,9 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract interface J =
+    entrypoint f : () => char
+
+contract C : I, J =
+    entrypoint f() = 1
+    entrypoint f() = 'c'

test/contracts/polymorphism_contract_undefined_interface.aes

@@ -0,0 +1,2 @@
+contract C : I =
+    entrypoint f() = ()

test/contracts/polymorphism_non_payable_contract_implement_payable.aes

@@ -0,0 +1,5 @@
+payable contract interface I =
+    payable entrypoint f : () => int
+
+contract C : I =
+    entrypoint f() = 123

test/contracts/polymorphism_non_payable_interface_implement_payable.aes

@@ -0,0 +1,8 @@
+payable contract interface I =
+    payable entrypoint f : () => int
+
+contract interface H : I =
+    payable entrypoint f : () => int
+
+payable contract C : H =
+    entrypoint f() = 123

test/contracts/polymorphism_preserve_or_add_payable_contract.aes

@@ -0,0 +1,14 @@
+contract interface F =
+    entrypoint f : () => int
+
+payable contract interface G : F =
+    payable entrypoint f : () => int
+    entrypoint g : () => int
+
+payable contract interface H =
+    payable entrypoint h : () => int
+
+payable contract C : G, H =
+    payable entrypoint f() = 1
+    payable entrypoint g() = 2
+    payable entrypoint h() = 3

test/contracts/polymorphism_preserve_or_add_payable_entrypoint.aes

@@ -0,0 +1,7 @@
+contract interface I =
+    payable entrypoint f : () => int
+    entrypoint g : () => int
+
+contract C : I =
+    payable entrypoint f() = 1
+    payable entrypoint g() = 2

test/contracts/polymorphism_preserve_or_remove_stateful_entrypoint.aes

@@ -0,0 +1,7 @@
+contract interface I =
+    stateful entrypoint f : () => int
+    stateful entrypoint g : () => int
+
+contract C : I =
+    stateful entrypoint f() = 1
+    entrypoint g() = 2

test/contracts/polymorphism_remove_payable_entrypoint.aes

@@ -0,0 +1,5 @@
+contract interface I =
+    payable entrypoint f : () => int
+
+contract C : I =
+    entrypoint f() = 1

test/contracts/polymorphism_variance_switching.aes

@@ -0,0 +1,75 @@
+contract interface Creature =
+    entrypoint is_alive : () => bool
+
+contract interface Animal : Creature =
+    entrypoint is_alive : () => bool
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+    entrypoint is_alive() = true
+
+main contract Main =
+    entrypoint init() = ()
+
+    stateful function g0(_ : Creature) : Cat = Chain.create()
+    stateful function f0(x : Cat) : Creature = g0(x)
+    stateful function h0() =
+        let a : Animal = (Chain.create() : Cat)
+        let c : Creature = (Chain.create() : Cat)
+        let c1 : Creature = a
+        ()
+
+    stateful function g1(x : Animal) : Cat = Chain.create()
+    stateful function f1(x : Cat) : Animal = g1(x)
+
+    stateful function g11(x : list(Animal)) : list(Cat) = [Chain.create()]
+    stateful function f11(x : list(Cat)) : list(Animal) = g11(x)
+
+    stateful function g12(x : Animal * Animal) : Cat * Cat = (Chain.create(), Chain.create())
+    stateful function f12(x : Cat * Cat) : Animal * Animal = g12(x)
+
+    stateful function g13() : map(Cat, Cat) = { [Chain.create()] = Chain.create() }
+    stateful function f13() : map(Animal, Animal) = g13()
+
+    stateful function g2(x : Cat) : Cat = Chain.create()
+    stateful function f2(x : Animal) : Animal = g2(x)  // fail
+
+    stateful function g3(x : Cat) : Animal = f1(x)
+    stateful function f3(x : Cat) : Cat = g3(x)  // fail
+
+    stateful function g4(x : (Cat => Animal)) : Cat = Chain.create()
+    stateful function f4(x : (Animal => Cat)) : Animal = g4(x)
+
+    stateful function g44(x : list(list(Cat) => list(Animal))) : Cat = Chain.create()
+    stateful function f44(x : list(list(Animal) => list(Cat))) : Animal = g44(x)
+
+    stateful function g5(x : (Animal => Animal)) : Cat = Chain.create()
+    stateful function f5(x : (Cat => Cat)) : Animal = g5(x)  // fail
+
+    stateful function g6() : option(Cat) = Some(Chain.create())
+    stateful function f6() : option(Animal) = g6()
+    stateful function h6() : option(Cat) = f6()  // fail
+
+    type cat_type = Cat
+    type animal_type = Animal
+    type cat_cat_map = map(cat_type, cat_type)
+    type animal_animal_map = map(animal_type, animal_type)
+
+    stateful function g71(x : animal_type) : cat_type = Chain.create()
+    stateful function f71(x : cat_type) : animal_type = g1(x)
+
+    stateful function g72() : cat_cat_map = { [Chain.create()] = Chain.create() }
+    stateful function f72() : animal_animal_map = g13()
+
+    stateful function g73() =
+        let some_cat : Cat = Chain.create()
+        let some_animal : Animal = some_cat
+
+        let some_cat_cat_map : map(Cat, Cat) = g13()
+        let some_animal_animal_map : map(Animal, Animal) = some_cat_cat_map
+
+        let x : Animal = some_animal_animal_map[some_cat]  // success
+        let y : Cat    = some_cat_cat_map[some_animal]     // fail
+
+        ()

test/contracts/polymorphism_variance_switching_chain_create.aes

@@ -0,0 +1,29 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract C1 : I =
+    entrypoint f() = 123
+
+contract C2 : I =
+    entrypoint f() = 888
+
+namespace Make =
+    stateful function new1() : I = Chain.create() : C1
+    stateful function new2() : I = Chain.create() : C2
+
+    stateful function new(c : I) : int = c.f()
+
+main contract Main =
+    stateful entrypoint test1() =
+        let c = Make.new1()
+        Make.new(c)
+
+    stateful entrypoint test2() =
+        let c = Make.new2()
+        Make.new(c)
+
+    stateful entrypoint test3() =
+        let c1      = Chain.create() : C1  // succeeds
+        let c2 : I  = Chain.create() : C1  // succeeds
+        let c3 : C1 = Chain.create()       // succeeds
+        ()

test/contracts/polymorphism_variance_switching_chain_create_fail.aes

@@ -0,0 +1,12 @@
+contract interface I =
+    entrypoint f : () => int
+
+contract C : I =
+    entrypoint f() = 123
+
+main contract Main =
+    stateful entrypoint test() =
+        let c1 : I = Chain.create()       // fails
+        let c2 : C = Chain.create() : I   // fails
+        let c3     = Chain.create() : I   // fails
+        ()

test/contracts/polymorphism_variance_switching_custom_types.aes

@@ -0,0 +1,135 @@
+contract interface Animal =
+    entrypoint sound : () => string
+
+contract Cat : Animal =
+    entrypoint sound() = "meow"
+
+main contract Main =
+    datatype dt_contra('a) = DT_CONTRA('a => unit)
+    datatype dt_co('a) = DT_CO(unit => 'a)
+    datatype dt_inv('a) = DT_INV('a => 'a)
+    datatype dt_biv('a) = DT_BIV(unit => unit)
+    datatype dt_inv_sep('a) = DT_INV_SEP_A('a => unit) | DT_INV_SEP_B(unit => 'a)
+    datatype dt_co_nest_a('a) = DT_CO_NEST_A(dt_contra('a) => unit)
+    datatype dt_contra_nest_a('a) = DT_CONTRA_NEST_A(dt_co('a) => unit)
+    datatype dt_contra_nest_b('a) = DT_CONTRA_NEST_B(unit => dt_contra('a))
+    datatype dt_co_nest_b('a) = DT_CO_NEST_B(unit => dt_co('a))
+    datatype dt_co_twice('a) = DT_CO_TWICE(('a => unit) => 'a)
+    datatype dt_contra_twice('a) = DT_CONTRA_TWICE('a => 'a => unit)
+    datatype dt_a_contra_b_contra('a, 'b) = DT_A_CONTRA_B_CONTRA('a => 'b => unit)
+
+    function f_a_to_a_to_u(_ : Animal) : (Animal => unit) = f_a_to_u
+    function f_a_to_c_to_u(_ : Animal) : (Cat => unit) = f_c_to_u
+    function f_c_to_a_to_u(_ : Cat) : (Animal => unit) = f_a_to_u
+    function f_c_to_c_to_u(_ : Cat) : (Cat => unit) = f_c_to_u
+
+    function f_u_to_u(_ : unit) : unit = ()
+    function f_a_to_u(_ : Animal) : unit = ()
+    function f_c_to_u(_ : Cat) : unit = ()
+
+    function f_dt_contra_a_to_u(_ : dt_contra(Animal)) : unit = ()
+    function f_dt_contra_c_to_u(_ : dt_contra(Cat)) : unit = ()
+    function f_dt_co_a_to_u(_ : dt_co(Animal)) : unit = ()
+    function f_dt_co_c_to_u(_ : dt_co(Cat)) : unit = ()
+    function f_u_to_dt_contra_a(_ : unit) : dt_contra(Animal) = DT_CONTRA(f_a_to_u)
+    function f_u_to_dt_contra_c(_ : unit) : dt_contra(Cat) = DT_CONTRA(f_c_to_u)
+
+    stateful function f_c() : Cat = Chain.create()
+    stateful function f_a() : Animal = f_c()
+
+    stateful function f_u_to_a(_ : unit) : Animal = f_a()
+    stateful function f_u_to_c(_ : unit) : Cat = f_c()
+    stateful function f_a_to_a(_ : Animal) : Animal = f_a()
+    stateful function f_a_to_c(_ : Animal) : Cat = f_c()
+    stateful function f_c_to_a(_ : Cat) : Animal = f_a()
+    stateful function f_c_to_c(_ : Cat) : Cat = f_c()
+
+    stateful function f_a_to_u_to_c(_ : (Animal => unit)) : Cat = f_c()
+    stateful function f_c_to_u_to_a(_ : (Cat => unit)) : Animal = f_a()
+    stateful function f_c_to_u_to_c(_ : (Cat => unit)) : Cat = f_c()
+
+    stateful function f_u_to_dt_co_a(_ : unit) : dt_co(Animal) = DT_CO(f_u_to_a)
+    stateful function f_u_to_dt_co_c(_ : unit) : dt_co(Cat) = DT_CO(f_u_to_c)
+
+    stateful entrypoint init() =
+        let va1 : dt_contra(Animal) = DT_CONTRA(f_a_to_u)  // success
+        let va2 : dt_contra(Animal) = DT_CONTRA(f_c_to_u)  // fail
+        let va3 : dt_contra(Cat)    = DT_CONTRA(f_a_to_u)  // success
+        let va4 : dt_contra(Cat)    = DT_CONTRA(f_c_to_u)  // success
+
+        let vb1 : dt_co(Animal) = DT_CO(f_u_to_a)  // success
+        let vb2 : dt_co(Animal) = DT_CO(f_u_to_c)  // success
+        let vb3 : dt_co(Cat)    = DT_CO(f_u_to_a)  // fail
+        let vb4 : dt_co(Cat)    = DT_CO(f_u_to_c)  // success
+
+        let vc1 : dt_inv(Animal) = DT_INV(f_a_to_a)  // success
+        let vc2 : dt_inv(Animal) = DT_INV(f_a_to_c)  // success
+        let vc3 : dt_inv(Animal) = DT_INV(f_c_to_a)  // fail
+        let vc4 : dt_inv(Animal) = DT_INV(f_c_to_c)  // fail
+        let vc5 : dt_inv(Cat)    = DT_INV(f_a_to_a)  // fail
+        let vc6 : dt_inv(Cat)    = DT_INV(f_a_to_c)  // fail
+        let vc7 : dt_inv(Cat)    = DT_INV(f_c_to_a)  // fail
+        let vc8 : dt_inv(Cat)    = DT_INV(f_c_to_c)  // success
+
+        let vd1 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
+        let vd2 : dt_biv(Animal) = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success
+        let vd3 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Animal)  // success
+        let vd4 : dt_biv(Cat)    = DT_BIV(f_u_to_u) : dt_biv(Cat)     // success
+
+        let ve1 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_a_to_u)  // success
+        let ve2 : dt_inv_sep(Animal) = DT_INV_SEP_A(f_c_to_u)  // fail
+        let ve3 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_a)  // success
+        let ve4 : dt_inv_sep(Animal) = DT_INV_SEP_B(f_u_to_c)  // fail
+        let ve5 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_a_to_u)  // fail
+        let ve6 : dt_inv_sep(Cat)    = DT_INV_SEP_A(f_c_to_u)  // success
+        let ve7 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_a)  // fail
+        let ve8 : dt_inv_sep(Cat)    = DT_INV_SEP_B(f_u_to_c)  // success
+
+        let vf1 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_a_to_u)  // success
+        let vf2 : dt_co_nest_a(Animal) = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success
+        let vf3 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_a_to_u)  // fail
+        let vf4 : dt_co_nest_a(Cat)    = DT_CO_NEST_A(f_dt_contra_c_to_u)  // success
+
+        let vg1 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
+        let vg2 : dt_contra_nest_a(Animal) = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // fail
+        let vg3 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_a_to_u)  // success
+        let vg4 : dt_contra_nest_a(Cat)    = DT_CONTRA_NEST_A(f_dt_co_c_to_u)  // success
+
+        let vh1 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
+        let vh2 : dt_contra_nest_b(Animal) = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // fail
+        let vh3 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_a)  // success
+        let vh4 : dt_contra_nest_b(Cat)    = DT_CONTRA_NEST_B(f_u_to_dt_contra_c)  // success
+
+        let vi1 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_a)  // success
+        let vi2 : dt_co_nest_b(Animal) = DT_CO_NEST_B(f_u_to_dt_co_c)  // success
+        let vi3 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_a)  // fail
+        let vi4 : dt_co_nest_b(Cat)    = DT_CO_NEST_B(f_u_to_dt_co_c)  // success
+
+        let vj1 : dt_co_twice(Animal) = DT_CO_TWICE(f_a_to_u_to_c : (Animal => unit) => Animal) : dt_co_twice(Animal)  // success
+        let vj2 : dt_co_twice(Animal) = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success
+        let vj3 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_a : (Animal => unit) => Animal) : dt_co_twice(Animal)  // fail
+        let vj4 : dt_co_twice(Cat)    = DT_CO_TWICE(f_c_to_u_to_c : (Cat    => unit) => Cat   ) : dt_co_twice(Cat)     // success
+
+        let vk01 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk02 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
+        let vk03 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
+        let vk04 : dt_a_contra_b_contra(Animal, Animal) = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk05 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk06 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
+        let vk07 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // fail
+        let vk08 : dt_a_contra_b_contra(Animal, Cat)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk09 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk10 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // fail
+        let vk11 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
+        let vk12 : dt_a_contra_b_contra(Cat, Animal)    = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // fail
+        let vk13 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_a_to_u)  // success
+        let vk14 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_a_to_c_to_u)  // success
+        let vk15 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_a_to_u)  // success
+        let vk16 : dt_a_contra_b_contra(Cat, Cat)       = DT_A_CONTRA_B_CONTRA(f_c_to_c_to_u)  // success
+
+        let vl1 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
+        let vl2 : dt_contra_twice(Animal) = DT_CONTRA_TWICE(f_a_to_c_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // fail
+        let vl3 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_a_to_a_to_u : Animal => Animal => unit) : dt_contra_twice(Animal)  // success
+        let vl4 : dt_contra_twice(Cat)    = DT_CONTRA_TWICE(f_c_to_a_to_u : Cat    => Cat    => unit) : dt_contra_twice(Cat)     // success
+
+        ()