Standardize support for header forwarding and inline headers (#560)

The immediate motivation for this change was the following issue against
the Haskell implementation:

#396

... which unearthed two problems:

* First, I realized that I had not yet standardized the Haskell implementation's
  support for forwarding custom headers

  This is a feature that allows transitive imports to the same domain to
  reuse headers (mainly to reuse authentication headers).  This comes in handy
  when importing from private expression repositories that contain internal
  imports.

* Second, I learned why the Haskell support for forwarding headers was broken

  The issue was that custom headers were being forwarded by a (referentially
  opaque) reference instead of being forwarded by value.

  Fixing this requires generalizing the `using` clause for custom headers to
  be able to store an arbitrary expression so that it could store the
  fully resolved and normalized headers.

So this change bundles two logical changes:

* Generalizing `using` to store an inline expression

  This is a useful change in its own right because now users can specify
  custom headers inline within the same file instead of having to provide them
  in a separate file.

  This is not a breaking change to the grammar, but it is a minor breaking
  change to the binary encoding.  Specifically, the expression for custom
  headers will now be encoded as an expression and not an import, meaning
  that it is now wrapped in an extra `[24, ... ]` label that was previously not
  there before.

  This doesn't affect semantic integrity checks since the hashed expressions are
  import free.

* Adding support for header forwarding if the parent/child import share the
  same authority and both use HTTPS

  I thought I had already standardized this, but apparently not! 🙂

  This forwards them by value instead of by reference in order to avoid
  introducing the bug caught by the linked issue.

standard/dhall.abnf

@@ -489,9 +489,9 @@ scheme = %x68.74.74.70 [ %x73 ]  ; "http" [ "s" ]
 ;   not valid
 ; * this does not support fragment identifiers, which have no meaning within
 ;   Dhall expressions and do not affect import resolution
-;
-; Unquoted path components should be percent-decoded according to
-; https://tools.ietf.org/html/rfc3986#section-2
+;
+; Unquoted path components should be percent-decoded according to
+; https://tools.ietf.org/html/rfc3986#section-2
 http-raw = scheme "://" authority path [ "?" query ]
 
 ; NOTE: Backtrack if parsing the optional user info prefix fails
@@ -543,9 +543,7 @@ unreserved  = ALPHA / DIGIT / "-" / "." / "_" / "~"
 
 sub-delims = "!" / "$" / "&" / "'" / "(" / ")" / "*" / "+" / "," / ";" / "="
 
-http =
-    http-raw
-    [ whsp using whsp1 (import-hashed / "(" whsp import-hashed whsp ")") ]
+http = http-raw [ whsp using whsp1 import-expression ]
 
 ; Dhall supports unquoted environment variables that are Bash-compliant or
 ; quoted environment variables that are POSIX-compliant

standard/imports.md

@@ -314,20 +314,34 @@ the parent and child directories:
     https://authority path₀ file₀ </> .. path₂ file₁ = https://authority path₃ file₁
 
 
-Import chaining ignores any `using` clause on the parent import:
+Import chaining preserves the header clause on the child import:
 
 
     import₀ </> import₁ = import₂
-    ───────────────────────────────────────────
-    import₀ using headers </> import₁ = import₂
+    ─────────────────────────────────────────────────────────
+    import₀ </> import₁ using headers = import₂ using headers
+
+
+... and the child import can reuse custom headers from the parent import if
+the child is a relative import
+
+
+    path₀ </> path₁ = path₂
+    ───────────────────────────────────────────────────────────────────────────────────────────────────────────
+    https://authority path₀ file₀ using headers </> . path₁ file₁ = https://authority path₂ file₁ using headers
 
 
-... but does preserve the header clause on the child import:
+    path₀ </> /.. = path₁   path₁ </> path₂ = path₃
+    ────────────────────────────────────────────────────────────────────────────────────────────────────────────
+    https://authority path₀ file₀ using headers </> .. path₂ file₁ = https://authority path₃ file₁ using headers
+
+
+Otherwise, import chaining ignores the `using` clause on the parent import:
 
 
     import₀ </> import₁ = import₂
-    ─────────────────────────────────────────────────────────
-    import₀ </> import₁ using headers = import₂ using headers
+    ───────────────────────────────────────────
+    import₀ using headers </> import₁ = import₂
 
 
 If the child is an absolute import, then the path to the parent import does not
@@ -585,13 +599,14 @@ resolve imports within the retrieved expression:
     parent </> import₀ = import₁
     canonicalize(import₁) = child
     referentiallySane(parent, child)
-    Γ(child) = e₀ using responseHeaders     ; Retrieve the expression, possibly
-                                            ; binding any response headers to
-                                            ; `responseHeaders` if child was a
-                                            ; remote import
-    corsCompliant(parent, responseHeaders)  ; If `child` was not a remote import
-                                            ; and therefore had no response
-                                            ; headers then skip this CORS check
+    Γ(child) = e₀ using responseHeaders  ; Retrieve the expression, possibly
+                                         ; binding any response headers to
+                                         ; `responseHeaders` if child was a
+                                         ; remote import
+    corsCompliant(parent, child, responseHeaders)  ; If `child` was not a remote
+                                                   ; import and therefore had no
+                                                   ; response headers then skip
+                                                   ; this CORS check
     (Δ, parent, child) × Γ₀ ⊢ e₀ ⇒ e₁ ⊢ Γ₁
     ε ⊢ e₁ : T
     ────────────────────────────────────  ; * child ∉ (Δ, parent)
@@ -613,7 +628,7 @@ If an import ends with `as Text`, import the raw contents of the file as a
     canonicalize(import₁) = child
     referentiallySane(parent, child)
     Γ(child) = "s" using responseHeaders  ; Read the raw contents of the file
-    corsCompliant(parent, responseHeaders)
+    corsCompliant(parent, child, responseHeaders)
     ───────────────────────────────────────────
     (Δ, parent) × Γ ⊢ import₀ as Text ⇒ "s" ⊢ Γ
 
@@ -622,21 +637,22 @@ If an import ends with `using headers`, resolve the `headers` import and use
 the resolved expression as additional headers supplied to the HTTP request:
 
 
-    (Δ, parent) × Γ₀ ⊢ headers ⇒ h₀ ⊢ Γ₁
-    ε ⊢ headers : List { header : Text, value : Text }
-    headers ⇥ requestHeaders
-    parent </> import₀ = import₁
-    canonicalize(import₁) = child
+    (Δ, parent) × Γ₀ ⊢ requestHeaders ⇒ resolvedRequestHeaders ⊢ Γ₁
+    ε ⊢ resolvedRequestHeaders : List { header : Text, value : Text }
+    resolvedRequestHeaders ⇥ normalizedRequestHeaders
+    parent </> https://authority directory file using normalizedRequestHeaders = import
+    canonicalize(import) = child
     referentiallySane(parent, child)
-    Γ₁(https://authority directory file using requestHeaders) = e₀ using responseHeaders ; Append requestHeaders to the request's headers
-    corsCompliant(parent, responseHeaders)
+    Γ₁(child) = e₀ using responseHeaders
+      ; Append normalizedRequestHeaders to the above request's headers
+    corsCompliant(parent, child, responseHeaders)
     (Δ, parent, child) × Γ₁ ⊢ e₀ ⇒ e₁ ⊢ Γ₂
     ε ⊢ e₁ : T
     ──────────────────────────────────────────────────────────────────────────  ; * child ∉ Δ
-    (Δ, parent) × Γ₀ ⊢ https://authority directory file using headers ⇒ e₁ ⊢ Γ₂  ; * import₀ ≠ missing
+    (Δ, parent) × Γ₀ ⊢ https://authority directory file using requestHeaders ⇒ e₁ ⊢ Γ₂
 
 
-For example, if `requestHeaders` in the above judgment normalized to:
+For example, if `normalizedRequestHeaders` in the above judgment was:
 
     [ { header = "Authorization", value = "token 5199831f4dd3b79e7c5b7e0ebe75d67aa66e79d4" }
     ]

tests/import/success/customHeadersA.dhall

@@ -0,0 +1,3 @@
+https://httpbin.org/user-agent
+  using [ { header = "User-Agent", value = "Dhall" } ]
+  as Text

tests/import/success/customHeadersB.dhall

@@ -0,0 +1,5 @@
+''
+{
+  "user-agent": "Dhall"
+}
+''

tests/import/success/headerForwardingA.dhall

@@ -0,0 +1,16 @@
+{- This test verifies that header-forwarding works correctly for relative
+   imports within the same domain
+
+   `test.dhall-lang.org` is the same as `prelude.dhall-lang.org` except that
+   `test.dhall-lang.org` rejects all requests without a `Test` header.
+
+   This test requires that the initial import to
+   `https://test.dhall-lang.org/Bool/package.dhall` forwards the `Test` header
+   to the transitive relative imports of `https://test.dhall-lang.org/Bool/*` in
+   order to succeed.
+
+   Note: You will need to update this test whenever the `Bool` package in the
+   Prelude changes (sorry)
+-}
+https://test.dhall-lang.org/Bool/package.dhall
+  using [ { header = "Test", value = "Example" } ]

tests/import/success/headerForwardingB.dhall

@@ -0,0 +1,26 @@
+{ and =
+      λ(xs : List Bool)
+    → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l && r) True
+, build =
+      λ(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool)
+    → f Bool True False
+, even =
+      λ(xs : List Bool)
+    → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x == y) True
+, fold =
+      λ(b : Bool)
+    → λ(bool : Type)
+    → λ(true : bool)
+    → λ(false : bool)
+    → if b then true else false
+, not =
+    λ(b : Bool) → b == False
+, odd =
+      λ(xs : List Bool)
+    → List/fold Bool xs Bool (λ(x : Bool) → λ(y : Bool) → x != y) False
+, or =
+      λ(xs : List Bool)
+    → List/fold Bool xs Bool (λ(l : Bool) → λ(r : Bool) → l || r) False
+, show =
+    λ(b : Bool) → if b then "True" else "False"
+}

tests/import/success/noHeaderForwardingA.dhall

@@ -0,0 +1,6 @@
+{- The purpose of this test is to verify that the custom headers supplied to
+   this import are not forwarded to the transitive import of
+   https://httpbin.org/user-agent
+-}
+https://raw.githubusercontent.com/dhall-lang/dhall-lang/master/tests/import/success/customHeadersA.dhall
+  using [ { header = "User-Agent", value = "Secret" } ]

tests/import/success/noHeaderForwardingB.dhall

@@ -0,0 +1,5 @@
+''
+{
+  "user-agent": "Dhall"
+}
+''

tests/parser/success/unit/import/inlineUsingA.dhall

@@ -0,0 +1,14 @@
+{- The language standard used to require that custom headers were provided via
+   an external import, but was later amended to support inline headers as part
+   of:
+
+   https://github.com/dhall-lang/dhall-lang/pull/560
+
+   This test verifies that an implementation supports such inline custom headers
+-}
+
+https://example.com/foo using
+    [ { header = "Authorization"
+      , value  = "token 5199831f4dd3b79e7c5b7e0ebe75d67aa66e79d4"
+      }
+    ]

tests/typecheck/failure/customHeadersUsingBoundVariable.dhall

@@ -0,0 +1,15 @@
+{- This is a type error because the custom headers are type-checked with an
+   empty context.  This is necessary because:
+
+   * import resolution precedes β-normalization
+   * we also don't want custom headers to leak program state anyway
+
+   This should fail due to the `x` within the custom header being an unbound
+   variable
+-}
+
+let x = "Bar"
+
+in https://httpbin.org/headers
+     using [ { header = "Foo", value = x } ]
+     as Text