Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Proper type instantiation discipline #1473

Merged
merged 7 commits into from
Jul 25, 2023
Merged

Proper type instantiation discipline #1473

merged 7 commits into from
Jul 25, 2023

Commits on Jul 25, 2023

  1. Proper type instantiation discipline 

    This commit is the last missing piece (at least for the time being)
toward a reasonable bidirectional typechecking algorithm that properly
handle higher-rank types.

Instantiation of polymorphic types has been ad-hoc and full of issues.
Simple programs such as:

```nickel
let r : { id : forall a. a -> a } = { id = fun r => r } in
r.id "x"
```

or

```nickel
let eval : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
(eval (fun x => x) 1) : Number
```

wouldn't typecheck. Previously introduced variable levels were required
before we could change that.

This commit is building on the variable level to use a proper
instantiation discipline from the specification of the Nickel type
system located in this repository, and the original inspiration, [A
Quick Look at Impredicativity]() (although type instantiation is
currently predicative, the general structure of the bidirectional
type system is similar). Doing so, we also move code between `check` and
`infer` to better reflect the specification: `infer` is not
wrapper around check + unification anymore, but it actually implements
infer rules (function application, primop application, variable and annotation).

Instantiation is taken care of when switching from infer mode to check
mode within `subsumption` and at function application.
    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    57d2966 View commit details
    Browse the repository at this point in the history

  2. Add test for unsound generalization 

    And fix the error expectation for `TypecheckError::VarLevelMismatch`
that still had the old longer name `VariableLevelMismatch`.
    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    14e77f8 View commit details
    Browse the repository at this point in the history

  3. Update core/tests/integration/main.rs 

    Co-authored-by: Viktor Kleen <viktor.kleen@tweag.io>
    @yannham @vkleen
    yannham and vkleen committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    719e5da View commit details
    Browse the repository at this point in the history

  4. Update core/src/typecheck/mod.rs

    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    9cb4a69 View commit details
    Browse the repository at this point in the history

  5. Update core/src/typecheck/mod.rs

    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    c07ca73 View commit details
    Browse the repository at this point in the history

  6. Post-rebase fixup + clippy warnings

    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    e315036 View commit details
    Browse the repository at this point in the history

  7. Formatting of Nickel test files

    @yannham
    yannham committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    f381e5f View commit details
    Browse the repository at this point in the history