dhall-docs jump to definition of names introduced by `Lam` and `Pi` constructor

[german1608]

I'd like to work on this, but currently the Lam and Pi constructor don't have the Src or SourcePos of the parsed label.

There are two ways to solve this:

• Record the whitespace on Lam and Pi bindings similar to what we do on Binding. This will help in the context of dhall-format removes comments #145
  The new constructors would look roughly like this:

  data FunctionBinding = FunctionBinding {...}
  data Expr s a
      = ...
      | Lam (Maybe s, Text) (Expr s a) (Expr s a)
      | Pi (Maybe s, Text) (Expr s a) (Expr s a)
      ....

• Use the parent Note Src of the Lam or Pi expression and run a parser to get the relative location of the label in the src and add it to the srcStart. This would only affect dhall-docs and it's somewhat similar to how dhall-lsp-server computes the source spans for source code messages.

What do you think is the best way to tackle this? cc: @sjakobi @Gabriel439 @Profpatsch

[sjakobi]

• Record the whitespace on Lam and Pi bindings similar to what we do on Binding. This will help in the context of dhall-format removes comments #145
  The new constructors would look roughly like this:

  data FunctionBinding = FunctionBinding {...}
  data Expr s a
      = ...
      | Lam (Maybe s, Text) (Expr s a) (Expr s a)
      | Pi (Maybe s, Text) (Expr s a) (Expr s a)
      ....

Could you flesh out that code a bit? Where is FunctionBinding used in Expr? Could you produce examples similar to what we have in the haddocks for Binding?

• Use the parent Note Src of the Lam or Pi expression and run a parser to get the relative location of the label in the src and add it to the srcStart. This would only affect dhall-docs and it's somewhat similar to how dhall-lsp-server computes the source spans for source code messages.

This sounds as if it could be implemented much faster.

I guess Gabriel's golden rule of software quality suggests the first option though. And we could indeed use your work to make progress on #145.

While the RecordField refactoring probably wasn't a lot of fun, I suspect doing something similar for Lam and Pi would be much easier for you now.

[Gabriella439]

One possible thing to consider is that the current way of encoding these annotation is a bit weakly-typed. Specifically, while we can guarantee that the Just constructor for a value of type Maybe s is uninhabited when s = Void, we cannot guarantee that the Just is inhabited when s = Src. Similarly, we cannot guarantee that if one source span is present then the other ones are also present.

One extreme way to solve that problem would be to keep two separate expression types, one without any Note constructors or Src spans and one with all of the Src spans. I don't know if there is a simpler solution, though.

[german1608]

Could you flesh out that code a bit? Where is FunctionBinding used in Expr? Could you produce examples similar to what we have in the haddocks for Binding?

Oops:

-- | > ∀( {- A -} a {- B -} : T) -> e ~ FunctionBinding "{- A -}" "a" "{- B -}"
data FunctionBinding s = FunctionBinding
    { functionBindingSrc0 :: Maybe s
    , label :: Text
    , functionBindingSrc :: Maybe s
    }
data Expr s a
    = ...
    | Lam (FunctionBinding s) (Expr s a) (Expr s a)
    | Pi (FunctionBinding s) (Expr s a) (Expr s a)
    ....

[german1608]

Similarly, we cannot guarantee that if one source span is present then the other ones are also present.

This could be solved by wrapping all source spans in the same Maybe constructor to ensure atomicity: either all are present or none. Sadly that doesn't solve all our problems

[Gabriella439]

@german1608: That would work for one constructor, but we'd also like to guarantee that all constructors within the syntax tree also stay in sync with respect to whether or not they have Src spans.

[german1608]

@Gabriel439: Although what you're suggesting to solve is important, we could tackle that in another moment. Maybe record an issue to not forget that?

[Gabriella439]

@german1608: Yeah, it's not urgent. If we work within the existing set of solutions then I would recommend adding additional Maybe fields to Lam/Pi

[Gabriella439]

Also, to make things more ergonomic, it might help to use PatternSynonyms to make the transition smoother for end users. For example, we could create new Lam/Pi pattern synonyms representing the old behavior and then make LamAnnot/PiAnnot the underlying constructors with the full annotations. Then you wouldn't need smart constructors/destructors.

[german1608]

Cool. I'll read about that. Thanks @Gabriel439

[Gabriella439]

You're welcome! 🙂

[german1608]

I have a doubt about pattern synonyms, and although I don't like posting coding questions here on GitHub issues I'll do so since I don't have enough for a Draft PR 😄

---

I changed the Lam type constructor to the following:

data FunctionBinding s a = FunctionBinding
    { fbSrc0 :: Maybe s
    , fbVariable :: Text
    , fbSrc1 :: Maybe s
    , fbSrc2 :: Maybe s
    , fbAnnotation :: Expr s a
    } deriving (Data, Eq, Foldable, Functor, Generic, Lift, NFData, Ord, Show, Traversable)

data Expr s a = ... | LamAnnot (FunctionBinding s a) (Expr s a) | ...

...and I added the following pattern for backwards compatibility:

pattern Lam :: Text -> Expr s a -> Expr s a -> Expr s a
pattern Lam l t e <- LamAnnot (FunctionBinding _ l _ _ t) e
  where
    Lam l t e = LamAnnot (FunctionBinding Nothing l Nothing Nothing t) e

and in an usage of the Lam constructor on other module of the dhall package, I got this warning:

/home/german/Documents/gsoc/dhall-haskell/dhall/src/Dhall/Binary.hs:596:12: warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: (LamAnnot _ _)
    |       
596 |     go e = case e ofa
    |            ^^^^^^^^^...

I enabled PatternSynonyms and imported the Lam pattern on that module before compiling to get that error. In that case clause there is a branch for Lam l t s. Why does GHC reports that? Isn't the Lam pattern enough to cover all cases?

[Gabriella439]

@german1608: You will also want a COMPLETE pragma:

https://downloads.haskell.org/ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-pragmas

[german1608]

@Gabriel439: Forgot to post here, I tried using that pragma specifying all constructors but I got this warning from GHC:

Pattern match checker exceeded (2000000) iterations

the full GHC log is lost sadly, I moved on and decided to tackle the pattern synonym issue later. Do you know what could be the reason for that?