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 bugs in `let` #136

Merged
merged 1 commit into from Sep 16, 2017

Conversation

Projects
None yet
2 participants
@Gabriel439
Collaborator

Gabriel439 commented Sep 15, 2017

Fixes #135

Dhall requires that a let expression of the form:

let x : t = e1 in e2

... should behave the same as the following equivalent lambda expression:

(λ(x : t)  e2) e1

... meaning that if one type-checks then the other should type-check and (vice
versa) if one does not type-check then the other should not type-check. The
only difference should be either:

  • the error message changes (i.e. to be more let-specific)
  • the order in which errors are checked might differ

I used equational reasoning to discover two corner cases where the two
expressions diverged in their type-checking behavior. This change fixes that
and includes two regression tests to capture the two corner cases to prevent
this problem from recurring

Fix type-checking bugs in `let`
Dhall requires that a `let` expression of the form:

```haskell
let x : t = e1 in e2
```

... should behave the same as the following equivalent lambda expression:

```haskell
(λ(x : t) → e2) e1
```

... meaning that if one type-checks then the other should type-check and (vice
versa) if one does not type-check then the other should not type-check.  The
only difference should be either:

* the error message changes (i.e. to be more `let`-specific)
* the order in which errors are checked might differ

I used equational reasoning to discover two corner cases where the two
expressions diverged in their type-checking behavior.  This change fixes that
and includes two regression tests to capture the two corner cases to prevent
this problem from recurring

@bosu bosu merged commit 8a4e744 into master Sep 16, 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

@Gabriel439 Gabriel439 deleted the gabriel/typecheck_let branch Jan 1, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment