Question about an import acceptance test

#1

I was surprised to see the expected result of acceptance test import/success/unit/AlternativeTypeError. This gives an expression of the form exprThatDoesNotTypeCheck ? alt and says that the expected result is alt

The only documentation I could find on the ? operator was the bottom of https://github.com/dhall-lang/dhall-lang/blob/master/standard/imports.md where it says that the rhs should be imported if the lhs fails to resolve Based on this, I was surprised that the test above suggests that the import resolution should be doing type checking as well.

Apologies if I’ve missed something obvious!

#2

Yes, import resolution performs type-checking. This is to ensure that any imported expression typechecks in an empty context - and so cannot refer to variables in the outer document.

The relevant informative text from imports.md is:

Carefully note that the fully resolved import must successfully type-check with an empty context. Imported expressions may not contain any free variables.

which refers to the following line in the preceding judgment in the same document:

ε ⊢ e₁ : T
#3

Apparently I can’t read :sob: Thanks @philandstuff!

#4

Heh, don’t feel bad! :slight_smile: We’ve spoken before about how imports.md is a long and complex document and often is the biggest speedbump for new implementations (I definitely got stuck here for a while when doing dhall-golang).

#5

We’ve also spoken about whether ? should catch all errors and I agree with you that catching type errors is rather surprising. I’d support changing that in the spec

#6

I think the first step is revisiting the requirements for the ? operator. If I remember correctly, the original motivation was for “mirror”-like functionality but it started getting adopted for other purposes (like detecting whether an import like an environment variable was present or ignoring hash mismatches)

Once we have a clear understanding of what use cases are required of the operator then it will be easier to design the appropriate behavior.