dhall lint produces ill-typed program if names are shadowed

[mmhat]

Consider the following Dhall files:

-- File: schema.dhall
{ Type = {}, default = {=} }
-- File: bug.dhall
let Foo = (./schema.dhall).Type

let f : Foo -> Foo = \(x : Foo) -> x

let Foo = ./schema.dhall

in {Foo, f}

When one runs dhall lint bug.dhall the content of the file is

let Foo = ./schema.dhall

let f
    : Foo -> Foo
    = \(x : Foo) -> x

in  { Foo, f }

which is ill-typed.

[Gabriella439]

So I think I know what's going wrong here, although I'm still working on a solution to fix it

First off, you can simplify the reproduction a little bit to:

let Foo = { }

let f : Foo -> Foo = \(x : Foo) -> x

let Foo = ./schema.dhall

in {Foo, f}

The root of the problem is that sortImports first rearranges the let bindings like this:

let Foo = { }

let Foo = ./schema.dhall

let f : Foo -> Foo = \(x : Foo) -> x

in {Foo, f}

…which is not correct (because now the second Foo is shadowing the first Foo within f), and then removeUnusedBindings gets rid of the first Foo (which is still a correct transformation):

let Foo = ./schema.dhall

let f : Foo -> Foo = \(x : Foo) -> x

in {Foo, f}

So really the issue is with sortImports. It doesn't correctly detect when sorting an import will cause some identifier to be shadowed in this way and fixing it is possible, but probably tricky, and that's what I'm working on.

[Gabriella439]

This is proving to be particularly tricky to fix, so I think in the short term I'll remove the sortImports transformation because I think it's most important that all transformations are sound