Fabrizio Ferrai

@Gabriel439 @arianvp how about making this another behaviour of the import system? Like `./some/import as Hash`

Cool! Then @arianvp you might want to take a look at #585 for how to standardise this - in that case I implemented it in the Haskell side before changing...

@neongreen it should work if you have the imports in different files? I.e. `./a.dhall` would be `import ./Foo.txt as Text` and `./b.dhall` would be `import ./a.dhall as Hash`

@arianvp looks great! 👏 We could probably have there all the current examples with some commentary, some kind of "literate Dhall" maybe Do you have ideas about what kind of...

@Gabriel439 oh yeah, restricting this to immediate values is clever, and it would be consistent with how we treat dependent equality right now. Thought experiment: how would you feel about...

This would get rid of some more awkwardness around our representation too. E.g. right now we represent [a package set](https://github.com/purescript/registry/blob/master/v1/sets/20200418.dhall) as a record because we want to be able to...

I assume that by "require a record literal" here we mean that it has the same semantics of [assertions](https://github.com/dhall-lang/dhall-lang/blob/master/standard/type-inference.md#assertions), i.e. it would work even if it's a symbol, as long...

How about something like `.^`? The mnemonic would be "the arrow up is a 'cast'/'promotion' to a record". Probably the mirrored version `^.` would be nice too, mnemonic: "cast up...

I was thinking that maybe this could be something suitable for having a bounty on it?

Update on this: #1254 implements support for using the `with` syntax with `Optional` through the `?` symbol, which as noted above will help get the ball rolling on this