merge-expressions with additional arguments are also formatted with
consistent indentation for all arguments. E.g.
merge
{ x = Natural/even }
< x >.x
1111111111111111111111111111111111111111111111111111111111
Fixes a small regression introduced in 7634ee7.
The loss of indentation for toMap and merge was due to
75e6cc5ca7. I have included Some for
consistency.
Fixes#1376.
Also improve format test failure messages
* Fix pretty-printing precedence of `toMap`
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1358
* Also correctly format `merge` expressions without a type annotation
... as suggested by @sjakobi
* Add test for formatting "function-like" expressions
This verifies that the code correctly handles `toMap` expressions with
type annotations as @sjakobi was asking about
… as standardized in https://github.com/dhall-lang/dhall-lang/pull/745.
This also adds proper error handling for the free variable case
discussed in https://github.com/dhall-lang/dhall-lang/issues/749:
Sample output for the MergeHandlerFreeVar test case:
Error: Disallowed handler type
Explanation: You can ❰merge❱ the alternatives of a union using a record with one
handler per alternative, like this:
┌─────────────────────────────────────────────────────────────────┐
│ let union = < Left : Natural | Right : Bool >.Left 2 │
│ let handlers = { Left = Natural/even, Right = λ(x : Bool) → x } │
│ in merge handlers union : Bool │
└─────────────────────────────────────────────────────────────────┘
... but the output type of a handler may not depend on the input value.
For example, the following expression is not valid:
Invalid: The output type is ❰Optional A❱, which references the input
value ❰A❱.
⇩
┌──────────────────────────────────────────┐
│ merge { x = None } (< x : Type >.x Bool) │
└──────────────────────────────────────────┘
Your handler for the following alternative:
↳ x
... has type:
↳ ∀(A : Type) → Optional A
... where the output type:
↳ Optional A
... references the handler's input value:
↳ A
────────────────────────────────────────────────────────────────────────────────
1│ merge { x = None } (<x: Type>.x Bool)
dhall/dhall-lang/tests/type-inference/failure/unit/MergeHandlerFreeVar.dhall:1:1
Since Val contains functions, its Show instance cannot be
derived in the usual way without exposing a non-standard Show
instance for (Val a -> Val a). Instead, we rely on the user to
provide a fitting instance, e.g. by importing Text.Show.Functions.
* Warning action about missing cache dir
* Add warning to executable
* Correct duplicate cacheName in getCacheFile
* Warn if dhall-haskell cache dir is not usable
* Improve warn message
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Correct plural
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Improve syntax
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
* Use runMaybeT to make 2 step warnings
* Add FlexibleContexts to make happy lts-6
* Catch IOException's when handling cache dir
This make the haskell impl follow the standard.
* Correct unwanted identantion
* Push warnings to get* wrapper functions
* Remove unnecessary lang extension
* Inline warnings in get* functions
* Being consistent with break lines
* Apply suggestions from code review
About phrasing, formatting, syntax, etc
Co-Authored-By: Gabriel Gonzalez <Gabriel439@gmail.com>
* doesPathExist is not in directory-1.2.2.0
* Make message fit in 80 cols
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1306
The following comment describe how this works in depth:
https://github.com/dhall-lang/dhall-haskell/issues/1129#issuecomment-532928798
The short explanation is that we can substantially speed up type-checking
by not substituting `let` expressions and instead adding the bound variable
to the context. This is the same as the type-checking "fast path" that
we had before adding dependent types, except this time it works even in the
presence of dependent types.
The main difference is that we add the `let`-bound type *and* value to the
context and use `Dhall.Eval.conv` to perform equivalence checking instead of
`Dhall.Core.judgmentallyEqual`.
* Add `--censor` flag support for censoring type errors
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1294
* Reuse `censorText`
... as caught by @sjakobi
* Remove `typeWith` refactor
... as caught by @sjakobi
This is a vestige of a refactor that I reverted incompletely
* Reuse `Dhall.Core.censorText` in `Dhall.Parser` module
... as suggested by @sjakobi
* Disable 1-field simplification by default
This builds on top of #1315 to minimize disruption by disabling the
breaking change by default and instead requiring the user to opt in
by setting a new `collapseSingletonRecords` option to `True`.
The additional tests added to verify this also caught a bug in the
`Interpret` instance for functions, which this change also fixes.
* Change to three-valued option
... based on feedback from @sjakobi
This change the option to a three-valued option:
* `Bare` - 1-field constructor does not include a nested record
* `Wrapped` - 1-field constructor always includes a nested record
* `Smart` - Named fields that don't begin with `_` include a nested record
The default is `Wrapped` (for backwards compatibility), but users will
probably want to eventually switch to `Smart`
* Don't depend on `fieldModifier` for determining if a field is anonymous
... as suggested by @sjakobi
* Refactor `Dhall.Eval`
This updates the style of `Dhall.Eval` to match the stylistic
and naming conventions of the rest of the `dhall` package.
* Import `Data.Set` fully qualified
... as suggested by @sjakobi
* Re-enable warnings
... as wished by @sjakobi
* Remove `{eval,conv,quote}E` synonyms
... as suggested by @sjakobi
* INLINE `qVar`
... literally
... as suggested by @sjakobi
* Remove unnecessary `MIN_VERSION_base(4,8,0)`
... as caught by @sjakobi
We still need `CPP` elsewhere within the same file, though
* Fix style of `vProjectByFields` function
... as caught by @sjakobi
* Simplify `Inject`/`Interpret` for 1-field records
Fixes https://github.com/dhall-lang/dhall-haskell/issues/346
Now a Haskell type like:
```haskell
data Example = Foo Bool | Bar Text
```
... corresponds to this Dhall type:
```dhall
{ Foo : Bool | Bar : Text }
```
* Fix documentation
* Add additional test cases
... as suggested by @sjakobi
* Test all permutations of:
* 0, 1, or 2 fields
* Fields of type `()` or `Double`
* Named or anonymous fields
To type-check and evaluate inputs in the context of previous
inputs, the repl constructs a let-expression that includes
the previous input and variable assignments as bindings.
Previously these bindings would also be annotated with
inferred types. For example a session like
⊢ Kind
⊢ "foo"
would be represented as
let it : Sort = Kind
in "foo"
However `Sort` does not typecheck as an annotation of a let-binding,
resulting in the confusing message
Error: ❰Sort❱ has no type, kind, or sort
Constructing the let-bindings without the type annotations fixes the
problem.
Fixes#1193.
Since some inferred types are in non-normal form, `dhall type`
would previously return types that weren't strictly
standard-conforming. This change prevents further confusion.
Closes#1300.
* Add `--censor` switch for disabling source code display
Related to #1294
This currently only affects parse errors, but can later be extended
to type errors, too
* Fix type blindiness
... as requested by @sjakobi
* Replace `Bool` with `Censor`
* Replace `Maybe FilePath` with `Input`
* Simplify recursive `Interpret` instance
Related to https://github.com/dhall-lang/dhall-haskell/issues/1297
The motivation behind this change is to:
* Remove the dependency on `free` and `distributive`
* Simplify the API and the implementation
* Fix `stack-lts-6` build
* Remove now-unused test files
... as caught by @sjakobi
When enabled, we handle protected imports as if the semantic cache was
empty:
* Protected imports are resolved again, downloaded or read from
the filesystem as necessary.
* Protected imports are β-normalized, not αβ-normalized.
* Protected imports are checked against their SHA256 hashes,
failing to resolve if they don't match.
Context:
https://github.com/dhall-lang/dhall-haskell/pull/1275#issuecomment-528847192
* Add a haddock to explain the various `Binding` fields.
* Add combinators to make dealing with `Binding` less awkward.
With all of the source information flying around, manually
deconstructing and reconstructing `Binding`s is a pain. These
combinators cover some very common cases.
* Use `bindingExprs` to simplify `subExpressions`.
* Use bindingExprs and chunkExprs to simplify another traversal.
Full coverage of all Expr constructors is now checked by the
type-checker. This revealed that that the IntegerToDouble, TextShow,
Some and None constructors were missing.
Also:
* Increase frequency for Lam, Pi and App
* Fix a few inconsistencies in normalization
* Remove some dead code in D.T.QuickCheck
Closes#1256.
* Change `dhall type` to resolve imports
Fixes https://github.com/dhall-lang/dhall-haskell/issues/1277
The original motivation was that `dhall type` would represent a
type-inference-only phase. However, in practice that wasn't very useful
so `dhall type` now performs import resolution followed by type inference.
* Fix loading relative to root directory
... as caught by @sjakobi
Co-Authored-By: Simon Jakobi <simon.jakobi@gmail.com>
