Prevent repl from inserting inferred 'Sort's into context (#1318)

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.
This commit is contained in:
Simon Jakobi 2019-09-15 04:16:26 +02:00 committed by mergify[bot]
parent 9d4fa51450
commit 1fed9063d5

View File

@ -170,8 +170,8 @@ applyContext context expression =
where
definitions = reverse $ Dhall.Context.toList context
convertBinding (variable, Binding expr type_) =
Dhall.Core.Binding Nothing variable Nothing (Just (Nothing, type_)) Nothing expr
convertBinding (variable, Binding expr _) =
Dhall.Core.Binding Nothing variable Nothing Nothing Nothing expr
bindings = fmap convertBinding definitions