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.

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

Fix type-checking bug that permits infinite loop #153

Merged
merged 2 commits into from Oct 7, 2017

Conversation

Projects
None yet
2 participants
@Gabriel439
Collaborator

Gabriel439 commented Oct 7, 2017

Fixes #151

Dhall is based on a pure type system that has the following rule:

Γ ⊢ A : s
────────────────
Γ, x : A ⊢ x : A

Γ ⊢ b : B   Γ ⊢ A : s
────────────────
Γ, x : A ⊢ b : B

... which both enforce that all terms in the context have to be type-checked
themselves before you can use the context to type-check other terms

You can introduce type-checking bugs if you don't type-check terms before adding
them to the context. The reason why is that the type-checking logic often
normalizes types retrieved from the context and this normalization is not safe
if the terms have not been type-checked first. Ill-typed terms can introduce
infinite loops when normalized, such as the following term:

(λ(x : A) → x x) (λ(x : A) → x x)

Dhall's type-checking logic had exactly this issue before this change due to
not type-checking terms added to the context. This change fixes the problem
and also adds a regression test to prevent this problem from recurring.

Fix type-checking bug that permits infinite loop
Fixes #151

Dhall is based on a pure type system that has the following rule:

    Γ ⊢ A : s
    ────────────────
    Γ, x : A ⊢ x : A

    Γ ⊢ b : B   Γ ⊢ A : s
    ────────────────
    Γ, x : A ⊢ b : B

... which both enforce that all terms in the context have to be type-checked
themselves before you can use the context to type-check other terms

You can introduce type-checking bugs if you don't type-check terms before adding
them to the context.  The reason why is that the type-checking logic often
normalizes types retrieved from the context and this normalization is not safe
if the terms have not been type-checked first.  Ill-typed terms can introduce
infinite loops when normalized, such as the following term:

    (λ(x : A) → x x) (λ(x : A) → x x)

Dhall's type-checking logic had exactly this issue before this change due to
not type-checking terms added to the context.  This change fixes the problem
and also adds a regression test to prevent this problem from recurring.

@bosu bosu merged commit 62d3c4a into master Oct 7, 2017

2 checks passed

continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment