From 711164a7a24ab832006b72cac162e78cf434861a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 4 Aug 2019 11:11:37 +0200
Subject: Remove old-style optional literals

---
 tests_buffer | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tests_buffer')

diff --git a/tests_buffer b/tests_buffer
index 1ea9a1c..deb245d 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -86,6 +86,8 @@ success/
 failure/
     ProjectionByExpressionNeedsParens r.{ x: T }
 
+binary decoding:
+decode old-style optional literals ?
 
 import:
 success/
@@ -104,6 +106,7 @@ variables across import boundaries
 
 typecheck:
 something that involves destructuring a recordtype after merge
+failure on old-style optional literal
 success/
     MergeEmptyAlternative merge { x = 1 } < x >.x
     MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
-- 
cgit v1.3.1


From 2551e6f91110bfe385fa65dd63e576df637c26fa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 5 Aug 2019 18:18:45 +0200
Subject: Add some tests

---
 dhall-lang                   |  2 +-
 dhall/build.rs               | 20 ++++++++++++++++++--
 dhall/src/phase/normalize.rs | 10 ++++++++++
 tests_buffer                 |  3 +++
 4 files changed, 32 insertions(+), 3 deletions(-)

(limited to 'tests_buffer')

diff --git a/dhall-lang b/dhall-lang
index dbf4ebc..e01c734 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit dbf4ebcfabf499e87c27e75bec108d91929ccc31
+Subproject commit e01c734e612daac327b06845e45c34552d65d9e1
diff --git a/dhall/build.rs b/dhall/build.rs
index 5a99def..7e320c5 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -90,6 +90,10 @@ fn main() -> std::io::Result<()> {
             // TODO: Inline headers are not implemented
             || path == "success/unit/import/parenthesizeUsing"
             || path == "success/unit/import/inlineUsing"
+            // TODO: projection by expression
+            || path == "success/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpressionEmpty"
         },
     )?;
 
@@ -105,6 +109,10 @@ fn main() -> std::io::Result<()> {
             || path == "success/largeExpression"
             // TODO: Inline headers are not implemented
             || path == "success/unit/import/inlineUsing"
+            // TODO: projection by expression
+            || path == "success/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpressionEmpty"
         },
     )?;
 
@@ -124,8 +132,11 @@ fn main() -> std::io::Result<()> {
             // See https://github.com/pyfisch/cbor/issues/109
             || path == "success/double"
             // TODO: Inline headers are not implemented
-            || path == "success/unit/import/parenthesizeUsing"
             || path == "success/unit/import/inlineUsing"
+            // TODO: projection by expression
+            || path == "success/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpression"
+            || path == "success/unit/recordProjectionByExpressionEmpty"
         },
     )?;
 
@@ -139,9 +150,14 @@ fn main() -> std::io::Result<()> {
             path == "success/simple/integerToDouble"
             // Too slow
             || path == "success/remoteSystems"
-            // TODO: selection by expression
+            // TODO: projection by expression
             || path == "success/unit/RecordProjectionTypeEmpty"
             || path == "success/unit/RecordProjectionTypeNonEmpty"
+            || path == "success/unit/RecordProjectionTypeNormalizeProjection"
+            // TODO: fix Double/show
+            || path == "success/prelude/JSON/number/1"
+            // the test is wrong
+            || path == "success/prelude/JSON/Type/0"
         },
     )?;
 
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index f3684d1..d5bdc9e 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -72,6 +72,16 @@ pub fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
         (TextShow, [v, r..]) => match &*v.as_value() {
             TextLit(elts) => {
                 match elts.as_slice() {
+                    // Empty string literal.
+                    [] => {
+                        // Printing InterpolatedText takes care of all the escaping
+                        let txt: InterpolatedText<X> = std::iter::empty().collect();
+                        let s = txt.to_string();
+                        Ok((
+                            r,
+                            TextLit(vec![InterpolatedTextContents::Text(s)]),
+                        ))
+                    }
                     // If there are no interpolations (invariants ensure that when there are no
                     // interpolations, there is a single Text item) in the literal.
                     [InterpolatedTextContents::Text(s)] => {
diff --git a/tests_buffer b/tests_buffer
index deb245d..5234562 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -98,6 +98,8 @@ failure/
 
 normalization:
 variables across import boundaries
+Text/show ""
+Double/show -1.5e-10
     TextLitNested1 "${""}${x}"
     TextLitNested2 "${"${x}"}"
     TextLitNested3 "${"${""}"}${x}"
@@ -106,6 +108,7 @@ variables across import boundaries
 
 typecheck:
 something that involves destructuring a recordtype after merge
+add some of the more complicated Prelude tests back, like List/enumerate
 failure on old-style optional literal
 success/
     MergeEmptyAlternative merge { x = 1 } < x >.x
-- 
cgit v1.3.1


From 482be29e0f03e10c2469ef80bdd6ac7593207dc5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 6 Aug 2019 20:38:06 +0200
Subject: RFC3986 URLs

---
 dhall-lang                                       |  2 +-
 dhall/build.rs                                   | 20 ++++++++++++++++++--
 dhall/src/phase/binary.rs                        |  8 +++++++-
 dhall_generated_parser/build.rs                  |  6 ++++++
 dhall_generated_parser/src/dhall.pest.visibility |  1 +
 dhall_syntax/src/core/import.rs                  |  1 +
 dhall_syntax/src/parser.rs                       |  7 +++++++
 dhall_syntax/src/printer.rs                      |  1 +
 tests_buffer                                     |  1 +
 9 files changed, 43 insertions(+), 4 deletions(-)

(limited to 'tests_buffer')

diff --git a/dhall-lang b/dhall-lang
index e01c734..2c0f238 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit e01c734e612daac327b06845e45c34552d65d9e1
+Subproject commit 2c0f2389e11597131b8ce021344322e5ed3a9131
diff --git a/dhall/build.rs b/dhall/build.rs
index 7e320c5..cdbd560 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -94,6 +94,12 @@ fn main() -> std::io::Result<()> {
             || path == "success/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpressionEmpty"
+            // TODO: RFC3986 URLs
+            || path == "success/unit/import/urls/emptyPath0"
+            || path == "success/unit/import/urls/emptyPath1"
+            || path == "success/unit/import/urls/emptyPathSegment"
+            // Test is broken
+            || path == "success/unit/import/asLocation"
         },
     )?;
 
@@ -113,6 +119,12 @@ fn main() -> std::io::Result<()> {
             || path == "success/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpressionEmpty"
+            // TODO: RFC3986 URLs
+            || path == "success/unit/import/urls/emptyPath0"
+            || path == "success/unit/import/urls/emptyPath1"
+            || path == "success/unit/import/urls/emptyPathSegment"
+            // Test is broken
+            || path == "success/unit/import/asLocation"
         },
     )?;
 
@@ -137,6 +149,12 @@ fn main() -> std::io::Result<()> {
             || path == "success/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpression"
             || path == "success/unit/recordProjectionByExpressionEmpty"
+            // TODO: RFC3986 URLs
+            || path == "success/unit/import/urls/emptyPath0"
+            || path == "success/unit/import/urls/emptyPath1"
+            || path == "success/unit/import/urls/emptyPathSegment"
+            // Test is broken
+            || path == "success/unit/import/asLocation"
         },
     )?;
 
@@ -156,8 +174,6 @@ fn main() -> std::io::Result<()> {
             || path == "success/unit/RecordProjectionTypeNormalizeProjection"
             // TODO: fix Double/show
             || path == "success/prelude/JSON/number/1"
-            // the test is wrong
-            || path == "success/prelude/JSON/Type/0"
         },
     )?;
 
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 443af7e..bab3fd8 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -195,8 +195,13 @@ fn cbor_value_to_dhall(
             }
             [U64(24), hash, U64(mode), U64(scheme), rest..] => {
                 let mode = match mode {
+                    0 => ImportMode::Code,
                     1 => ImportMode::RawText,
-                    _ => ImportMode::Code,
+                    2 => ImportMode::Location,
+                    _ => Err(DecodeError::WrongFormatError(format!(
+                        "import/mode/unknown_mode: {:?}",
+                        mode
+                    )))?,
                 };
                 let hash = match hash {
                     Null => None,
@@ -545,6 +550,7 @@ where
     let mode = match import.mode {
         ImportMode::Code => 0,
         ImportMode::RawText => 1,
+        ImportMode::Location => 2,
     };
     ser_seq.serialize_element(&U64(mode))?;
 
diff --git a/dhall_generated_parser/build.rs b/dhall_generated_parser/build.rs
index 744cb3d..2c1a8f5 100644
--- a/dhall_generated_parser/build.rs
+++ b/dhall_generated_parser/build.rs
@@ -27,6 +27,7 @@ fn main() -> std::io::Result<()> {
         }
     }
     rules.remove("http");
+    rules.remove("url_path");
     rules.remove("simple_label");
     rules.remove("nonreserved_label");
 
@@ -53,6 +54,11 @@ fn main() -> std::io::Result<()> {
                 ~ (import_hashed | ^\"(\" ~ whsp ~ import_hashed ~ whsp ~ ^\")\"))?
     }}"
     )?;
+    // TODO: this is a cheat; properly support RFC3986 URLs instead
+    writeln!(
+        &mut file,
+        "url_path = _{{ path }}"
+    )?;
     writeln!(
         &mut file,
         "nonreserved_label = _{{
diff --git a/dhall_generated_parser/src/dhall.pest.visibility b/dhall_generated_parser/src/dhall.pest.visibility
index 2b7c477..97d3a69 100644
--- a/dhall_generated_parser/src/dhall.pest.visibility
+++ b/dhall_generated_parser/src/dhall.pest.visibility
@@ -48,6 +48,7 @@ builtin
 Optional
 Text
 List
+Location
 # Bool
 # True
 # False
diff --git a/dhall_syntax/src/core/import.rs b/dhall_syntax/src/core/import.rs
index 306460b..d41eae2 100644
--- a/dhall_syntax/src/core/import.rs
+++ b/dhall_syntax/src/core/import.rs
@@ -41,6 +41,7 @@ pub enum Scheme {
 pub enum ImportMode {
     Code,
     RawText,
+    Location,
 }
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 2450c76..2c0cee9 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -697,6 +697,7 @@ make_parser! {
     ));
 
     token_rule!(Text<()>);
+    token_rule!(Location<()>);
 
     rule!(import<ParsedSubExpr> as expression; span; children!(
         [import_hashed(location_hashed)] => {
@@ -711,6 +712,12 @@ make_parser! {
                 location_hashed
             }))
         },
+        [import_hashed(location_hashed), Location(_)] => {
+            spanned(span, Embed(Import {
+                mode: ImportMode::Location,
+                location_hashed
+            }))
+        },
     ));
 
     token_rule!(lambda<()>);
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index b585a5b..2b2bbcc 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -435,6 +435,7 @@ impl Display for Import {
         match self.mode {
             Code => {}
             RawText => write!(f, " as Text")?,
+            Location => write!(f, " as Location")?,
         }
         Ok(())
     }
diff --git a/tests_buffer b/tests_buffer
index 5234562..ca578e4 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -6,6 +6,7 @@ remove `double`
 remove imports/parenthesizeUsing
 remove multilet
 selection by expression unit tests
+split aslocation test into actual unit tests
 success/
     imports/
         Missing missing
-- 
cgit v1.3.1


From 00c5b497446d5415c36bfda5ebc0413da9d086dd Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 8 Aug 2019 19:27:50 +0200
Subject: Upstream a bunch of tests

See https://github.com/dhall-lang/dhall-lang/pull/698
---
 tests_buffer | 105 ++++-------------------------------------------------------
 1 file changed, 6 insertions(+), 99 deletions(-)

(limited to 'tests_buffer')

diff --git a/tests_buffer b/tests_buffer
index ca578e4..4f8a375 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -2,90 +2,13 @@ parser:
 ./a%20b
 ./"a%20b"
 text interpolation and escapes
-remove `double`
-remove imports/parenthesizeUsing
-remove multilet
-selection by expression unit tests
-split aslocation test into actual unit tests
+projection by expression unit tests
 success/
-    imports/
-        Missing missing
-        Headers https://example.com/foo using ./headers
-        HeadersInteriorHash https://example.com/foo using (./headers sha256:0000000000000000000000000000000000000000000000000000000000000000)
-        HeadersExteriorHash (https://example.com/foo using ./headers) sha256:0000000000000000000000000000000000000000000000000000000000000000
-        HeadersHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000
-        HeadersDoubleHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000 sha256:1111111111111111111111111111111111111111111111111111111111111111
-    DoubleLitPositive 1.23
-    DoubleLitNegative -1.23
-    DoubleLitExponent 1.23e4
-    DoubleLitExponentNoDot 1e4
-    DoubleLitExponentNegative 1.23e-4
-    DoubleLitInfinity Infinity
-    DoubleLitNegInfinity -Infinity
-    DoubleLitNaN NaN
-    DoubleLitSecretelyInt 1.0
-    DoubleLitZero 0.0
-    BuiltinListBuild List/Build
-    FunctionApplicationOneArg f x
-    FunctionApplicationMultipleArgs f x y z
-    Annotation x : T
-    ListLitNonEmpty [x, y]
-    ListLitNonEmptyAnnotated [x, y] : List T
-    OptionalLitEmpty []: Optional T
-    OptionalLitNonEmpty [x]: Optional T
-    Field r.x
-    FieldBuiltinName r.List
-    FieldQuoted r.`x`
-    Projection r.{x, y, z}
-    Let let x: T = v in e
-    LetNested let x: T = v in let y: U = w in e
-    LetMulti let x: T = v let y: U = w in e
-    LambdaUnicode λ(x : T) -> y
-    FunctionTypePi forall(x: T) -> U
-    FunctionTypePiUnicode ∀(x: T) -> U
-    FunctionTypePiNested forall(x: T) -> ∀(y: U) -> V
-    FunctionTypePiUnderscore forall(_: T) -> U
-    FunctionTypeArrow T -> U
-    RecordLit { x = 1, y = 2 }
-    RecordType { x: T, y: U }
     operators/
-        ImportAlt x ? y
-        ImportAltAssoc w ? x ? y ? z
-        BoolOr x || y
-        BoolOrAssoc w || x || y || z
-        NaturalPlus x + y
-        NaturalPlusAssoc w + x + y + z
-        TextAppend x ++ y
-        TextAppendAssoc w ++ x ++ y ++ z
-        ListAppend x # y
-        ListAppendAssoc w # x # y # z
-        BoolAnd x && y
-        BoolAndAssoc w && x && y && z
-        NaturalTimes x * y
-        NaturalTimesAssoc w * x * y * z
-        BoolEQ x == y
-        BoolEQAssoc w == x == y == z
-        BoolNE x != y
-        BoolNEAssoc w != x != y != z
-        RecursiveRecordMerge x //\\ y
-        RecursiveRecordMergeAssoc w //\\ x //\\ y //\\ z
-        RecursiveRecordTypeMerge x /\ y
-        RecursiveRecordTypeMergeAssoc w /\ x /\ y /\ z
-        RightBiasedRecordMerge x // y
-        RightBiasedRecordMergeAssoc w // x // y // z
-        RecursiveRecordMergeUnicode x ∧ y
-        RecursiveRecordMergeUnicodeAssoc w ∧ x /\ y ∧ z
-        RightBiasedRecordMergeUnicode x ⫽ y
-        RightBiasedRecordMergeUnicodeAssoc w ⫽ x // y ⫽ z
-        RecursiveRecordTypeMergeUnicode x ⩓ y
-        RecursiveRecordTypeMergeUnicodeAssoc w ⩓ x //\\ y ⩓ z
         PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
         PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
-        PrecedenceNat a + b * d + e f * (g + h)
-        PrecedenceBool a && b || c d == e || f != g && h || i
-        PrecedenceRecord a // b c /\ d ⫽ e.{x} ∧ f
 failure/
-    ProjectionByExpressionNeedsParens r.{ x: T }
+    AssertNoAnnotation assert
 
 binary decoding:
 decode old-style optional literals ?
@@ -99,39 +22,23 @@ failure/
 
 normalization:
 variables across import boundaries
-Text/show ""
-Double/show -1.5e-10
+    Text/show ""
+    Double/show -1.5e-10
     TextLitNested1 "${""}${x}"
     TextLitNested2 "${"${x}"}"
     TextLitNested3 "${"${""}"}${x}"
-    EquivalenceDouble if b then NaN else NaN
-    EquivalenceAlpha if b then \(x: T) -> x else \(y: T) -> y
 
 typecheck:
 something that involves destructuring a recordtype after merge
 add some of the more complicated Prelude tests back, like List/enumerate
 failure on old-style optional literal
-success/
-    MergeEmptyAlternative merge { x = 1 } < x >.x
-    MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
-    EquivalenceAlpha \(TODO: forall(x: Type) -> x) -> TODO : forall(y: Type) -> y
 failure/
-    MergeEmptyNeedsDirectAnnotation1 \(x: <>) -> (merge {=} x) : Bool
-    MergeEmptyNeedsDirectAnnotation2 \(x: <>) -> let y: Bool = merge {=} x in 1
-    MergeBoolIsNotUnion merge x True
-    MergeOptionalIsNotUnion merge x (Some 1)
-    MergeMissingHandler1 merge {=} < x >.x
-    MergeMissingHandler2 merge {x=...,} <x|y>.x
     merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
     merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
     merge { x = True, y = 1 } < x | y >.x
     merge {x=...,y=...} <x>.x
     merge {x=...,y=...} <x:T>.x
-    MergeHandlerFreeVar merge { x = None } < x = Bool >
-    UnionTypeDuplicateVariants1 <x, x>
-    UnionTypeDuplicateVariants2 <x, x:T>
-    UnionLitDuplicateVariants <x=1|x:T>
-    RecordLitDuplicateFields { x: T, x: T }
-    EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _
+    MergeBoolIsNotUnion merge x True
+    MergeOptionalIsNotUnion merge x (Some 1)
 
 equivalence:
-- 
cgit v1.3.1


From 80c8d87db595c91293af75d710464ac5379c7e28 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 10 Aug 2019 22:48:21 +0200
Subject: Update dhall-lang submodule

---
 dhall-lang                |  2 +-
 dhall/build.rs            | 13 +++++++++----
 dhall/src/phase/binary.rs | 13 +++++++++++++
 tests_buffer              |  3 ++-
 4 files changed, 25 insertions(+), 6 deletions(-)

(limited to 'tests_buffer')

diff --git a/dhall-lang b/dhall-lang
index 9729d89..fb1c41d 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit 9729d8939a6c79adf9a26dd20978fba6ec39bbec
+Subproject commit fb1c41ddec1d35dadd89a70780698e1a73e179bd
diff --git a/dhall/build.rs b/dhall/build.rs
index bcb5d1c..8b23dd9 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -94,8 +94,12 @@ fn main() -> std::io::Result<()> {
         // Too slow in debug mode
         path == "success/largeExpression"
             // TODO: Inline headers
-            || path == "success/unit/import/parenthesizeUsing"
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
+            || path == "success/unit/import/HeadersDoubleHash"
+            || path == "success/unit/import/HeadersDoubleHashPrecedence"
+            || path == "success/unit/import/HeadersHashPrecedence"
+            || path == "success/unit/import/HeadersInteriorHash"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
@@ -117,6 +121,7 @@ fn main() -> std::io::Result<()> {
             || path == "success/largeExpression"
             // TODO: Inline headers
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
@@ -140,13 +145,13 @@ fn main() -> std::io::Result<()> {
             path.starts_with("failure/")
             // Too slow in debug mode
             || path == "success/largeExpression"
-            // Too much of a pain to implement; shouldn't make a difference
-            // since lets disappear on normalization.
-            || path == "success/multilet"
             // See https://github.com/pyfisch/cbor/issues/109
             || path == "success/double"
+            || path == "success/unit/DoubleLitExponentNoDot"
+            || path == "success/unit/DoubleLitSecretelyInt"
             // TODO: Inline headers
             || path == "success/unit/import/inlineUsing"
+            || path == "success/unit/import/Headers"
             // TODO: projection by expression
             || path == "success/recordProjectionByExpression"
             || path == "success/RecordProjectionByType"
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 719b1c7..f4a9cc1 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -178,6 +178,19 @@ fn cbor_value_to_dhall(
                 let l = Label::from(l.as_str());
                 Field(x, l)
             }
+            [U64(10), x, rest..] => {
+                let x = cbor_value_to_dhall(&x)?;
+                let labels = rest
+                    .iter()
+                    .map(|s| match s {
+                        String(s) => Ok(Label::from(s.as_str())),
+                        _ => Err(DecodeError::WrongFormatError(
+                            "projection".to_owned(),
+                        )),
+                    })
+                    .collect::<Result<_, _>>()?;
+                Projection(x, labels)
+            }
             [U64(11), Object(map)] => {
                 let map = cbor_map_to_dhall_opt_map(map)?;
                 UnionType(map)
diff --git a/tests_buffer b/tests_buffer
index 4f8a375..c6366ba 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -7,6 +7,8 @@ success/
     operators/
         PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
         PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
+    LetNoAnnot let x = y in e
+    LetAnnot let x: T = y in e
 failure/
     AssertNoAnnotation assert
 
@@ -23,7 +25,6 @@ failure/
 normalization:
 variables across import boundaries
     Text/show ""
-    Double/show -1.5e-10
     TextLitNested1 "${""}${x}"
     TextLitNested2 "${"${x}"}"
     TextLitNested3 "${"${""}"}${x}"
-- 
cgit v1.3.1