Auto-implicits don't show up in :doc

[arianvp]

Idris Version: 0.12

Given the following datatype:

data Api : capture -> query -> req -> resp -> Type where
  |||
  ||| @ paths  a list of paths we can choose from
  ||| @ thereShouldBePaths  A proof that we have at least one path defined
  ||| @ noOverlappingPaths  A Proof that we have no paths that overlap
  OneOf : (Eq capture, Eq query)
        => (paths : List (Path capture query req resp))
       -> {auto thereShouldBePaths: NonEmpty paths}
       -> {auto noOverlappingPaths: map Servis.extractPathInfo paths = nub (map Servis.extractPathInfo paths)}
       -> Api capture query req resp

Expected behaviour of :doc:

Servis.OneOf : Eq capture => Eq query => (paths : List (Path capture
                                                             query
                                                             req
                                                             resp)) ->
    Api capture query req resp

    Arguments:
        paths : List (Path capture query req resp)  -- a list of paths we can choose from

        (implicit) thereShouldBePaths : NonEmpty paths  -- A proof that we have at least one
        path defined

        (implicit) noOverlappingPaths : map extractPathInfo paths =
                                        nub (map extractPathInfo paths)  -- A Proof that we have no paths
        that overlap

    The function is Total

Actual behaviour:

Servis.OneOf : Eq capture => Eq query => (paths : List (Path capture
                                                             query
                                                             req
                                                             resp)) ->
    {auto thereShouldBePaths : NonEmpty paths} ->
    {auto noOverlappingPaths : map extractPathInfo paths =
                               nub (map extractPathInfo paths)} -> Api capture query req resp

    Arguments:
        paths : List (Path capture query req resp)  -- a list of paths we can choose from

    The function is Total

[jfdm]

@arianvp Thanks for the issue report. IdrisDoc was a contributed feature of Idris, as part of a Student Project. It is my understanding that the scope of the project was purposefully constrained. An understandable notion, so it is possible that auto implicit were not added.

I think that all labelled documentation should be present. I shall have a quick look today to see if I can fix it, otherwise: PRs welcome!

[jfdm]

So, from a cursory glance something interesting is happening with Idris and implicits. I have filed an Issue in #3266. This may or may not be the cause of auto implicit documentation not being displayed.

I am still investigating the problem.

I hope this hasn't caused too much issue in your workflow.

However, for those interested in this issue, here is a small MFE:

module IdrisDocIssue

import Data.List

%default total

||| A foobar with an auto implicit
data Foobar : Type where
  ||| New Foo
  |||
  ||| @xs Some `xs`
  ||| @ys Some `ys`
  ||| @prf1 A prf
  NewFoo : (xs : List String)
        -> (ys : List Nat)
        -> {auto prf : NonEmpty ys}
        -> Foobar

[jfdm]

There seems to be a case missing in the showing of arguments. Will try and fix if possible.

[jfdm]

There is a PR #3267 that fixes IdrisDoc to print documentation for auto implicits. This issue should auto close once the PR has been merged.

[arianvp]

Thanks a bunch!