customHeadersUsingBoundVariable test

[sjakobi]

dhall-lang/tests/type-inference/failure/customHeadersUsingBoundVariable.dhall

Lines 1 to 15 in 06b2dfc

	{- 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 [ { mapKey = "Foo", mapValue = x } ]
	as Text

Which part of the standard says that this is illegal?

In particular, I don't find anything in type-inference.md, so I'm wondering why this is part of the type-inference tests.

[Gabriella439]

@sjakobi: It's in imports.md, specifically in the import resolution judgment for custom headers:

(Δ, parent) × Γ₀ ⊢ requestHeaders ⇒ resolvedRequestHeaders ⊢ Γ₁
ε ⊢ resolvedRequestHeaders : H  ; ← Here
…
──────────────────────────────────────────────────────────────────────────  ; * child ∉ Δ
(Δ, parent) × Γ₀ ⊢ https://authority directory file using requestHeaders ⇒ e₁ ⊢ Γ₂

That says that when type-checking the custom headers expression you have to type check it with an empty context.

[sjakobi]

That says that when type-checking the custom headers expression you have to type check it with an empty context.

Ah, thanks. Maybe we should add a verbal note to point this out.

I'd also like to move the customHeadersUsingBoundVariable test (and importBoundary) into the import tests. The motivation is that in the dhall-haskell's test setup for type-inference failure tests, we currently have to handle both import resolution errors and errors from the following type-checking phase. Handling multiple failure modes can mask issues where tests (expectedly) fail for the wrong reason. I'm currently fixing such an issue in dhall-lang/dhall-haskell#1326.

Or are there good reasons why these tests should be part of the type-inference tests?

[Gabriella439]

I think those tests make sense to put under import tests