Inner `parameters` block breaks visibily of overloaded names later in outer `mutual` block

[stephen-smith]

Steps to Reproduce

Broken:

module AltList

mutual
  record Some (elem : Type) where
    constructor MkSome
    head : elem
    tail : Many elem

  0 Many : Type -> Type
  Many elem = Maybe (Some elem)

mutual
  namespace Some
    parameters (ab : a -> b)
      map : Some a -> Some b
      map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail }

  parameters (f : a -> b)
    map : Many a -> Many b
    map Nothing = Nothing
    map (Just s) = Just (map f s)

Expected Behavior

Some.map definition uses AltList.map defined later in the same mutual block.

Observed Behavior

1/1: Building AltList (AltList.idr)
Error: While processing right hand side of map. Can't find an implementation for Functor ?f.

AltList:16:64--16:75
 12 | mutual
 13 |   namespace Some
 14 |     parameters (ab : a -> b)
 15 |       map : Some a -> Some b
 16 |       map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail }

Workaround

Without the parameters block, Some.map finds AltList.map:

module AltList

mutual
  record Some (elem : Type) where
    constructor MkSome
    head : elem
    tail : Many elem

  0 Many : Type -> Type
  Many elem = Maybe (Some elem)

mutual
  namespace Some
    parameters (ab : a -> b)
      map : Some a -> Some b
      map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail }

  map : (a -> b) -> Many a -> Many b
  map _ Nothing = Nothing
  map f (Just s) = Just (map f s)

Minimization of the example makes using parameters fairly useless, but in practice (e.g. https://gitlab.com/bss03/type-aligned/-/blob/main/src/TypeAligned.idr?ref_type=heads#L384 ) it may be useful to have multiple parameters across multiple definitions.

[dunhamsteve]

Another workaround is to use forward declarations instead of mutual. This essentially is what mutual does , but it looks like it doesn't handle parameters correctly at the moment.

module AltList

0 Many : Type -> Type

record Some (elem : Type) where
  constructor MkSome
  head : elem
  tail : Many elem

Many elem = Maybe (Some elem)

parameters (f : a -> b)
  map : Many a -> Many b
  
namespace Some
  parameters (ab : a -> b)
    map : Some a -> Some b
    map (MkSome head tail) = MkSome { head = ab head, tail = map ab tail }

parameters (f : a -> b)
  map Nothing = Nothing
  map (Just s) = Just (map f s)

[stephen-smith]

Is there a general preference for mutual or forward-declarations? I guess I drifted toward mutual because it felt more tightly "scoped", but I guess that's not really true.

[buzden]

Is there a general preference for mutual or forward-declarations?

There is indeed a lean towards forward-declarations declared several years ago by Edwin and generally preferred at least in the compiler.