Allow documentation of each output of a function individually

[andreasabel]

I can document individual inputs of a function, but not the outputs.

splitTelForWith
  -- Input:
  :: Telescope      -- ^ @Δ@        context of types and with-arguments.
  -> Type           -- ^ @Δ ⊢ t@    type of rhs.
  -> [Type]         -- ^ @Δ ⊢ as@   types of with arguments.
  -> [Term]         -- ^ @Δ ⊢ vs@   with arguments.
  -- Output:
  -> ( Telescope    -- ^ @Δ₁@       part of context not needed for with arguments and their types.
     , Telescope    -- ^ @Δ₂@       part of context needed for with arguments and their types.
     , Permutation  -- ^ @π@        permutation from Δ to Δ₁Δ₂ as returned by 'splitTelescope'.
     , Type         -- ^ @Δ₁Δ₂ ⊢ t'@ type of rhs under @π@
     , [Type]       -- ^ @Δ₁ ⊢ as'@ types with with-arguments depending only on $Δ₁@.
     , [Term]       -- ^ @Δ₁ ⊢ vs'@ with-arguments under @π@.
     )

Error:

src/full/Agda/TypeChecking/With.hs:57:21:
    parse error on input ‘-- ^ @Δ₁@       part of context not needed for with arguments and their types.’

To implement this feature, haddock would need to be extended to document parts of tuples individually.

[expipiplus1]

Along similar lines being able to document tuple elements for inputs to (uncurried) functions would be handy.

[asr]

+1

[bgamari]

There is nothing terribly special about tuples; these are just normal arguments to a type constructor. Are you proposing special treatment of tuples or more generally allowing documentation on parts of type applications?

[expipiplus1]

It would be handy to properly document the idiom of returning multiple values in a tuple. I'd be satisfied with just being able to document elements in a tuple type constructor, although as a "stretch-goal" I don't see why other type applications shouldn't be able to be documented.

[andreasabel]

I keep running into this issue. Anything?

[expipiplus1]

We've found using an operator like type (name :: k) ::: a = a works very well.

foo :: ("something" ::: Int)
    -> ("else" ::: Bool, "altogether" ::: Float)

[harpocrates]

This is a feature I've wanted too.

There is nothing terribly special about tuples; these are just normal arguments to a type constructor. Are you proposing special treatment of tuples or more generally allowing documentation on parts of type applications?

There is something special about tuples compared to general type applications - the documented type is unambiguous. For example, it is not clear in the following if qux is documenting Maybe Int or just Int.

foo :: Int   -- ^ bar
    -> Maybe -- ^ baz
         Int -- ^ qux

I think I may take a stab at implementing a special case for documenting components of tuples - especially since they are the canonical way of returning multiple values from a function.