public export everything in WellFounded

[joelberkeley]

Description

I'd like to use this stuff at the type level, can we make it public export please?

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md (and potentially also
  CONTRIBUTORS.md).

[joelberkeley]

I'm not clear on the semantics of public on interface implementations vs their definitions

[spcfox]

public will be aplied to every definition in implementation. You cannot write visability modifier inside implementation, because it doesn't contain declarations, only definitions

[joelberkeley]

Sorry, I don't understand. the compiler will accept public export on both, but I don't understand the semantics

[spcfox]

Oh, I get it. You mean modifiers on definitions in interfaces? That's the default visibility. They have a lower priority than the modifier on implementations

[joelberkeley]

You mean modifiers on definitions in interfaces?

Either way round, really - definitions or implementations.

They have a lower priority than the modifier on implementations

OK, so if I public export the interface, then the implementations will also be public export regardless of whether they are marked public export or export (of course, they will be private if not marked any kind of export). Similarly, if I mark the interface as export, then the implementations will be export unless marked public export?

[spcfox]

No, if you export an interface, its methods will be exported (I'm surprised, but it seems that visibility modifiers on methods are just ignored)

export
interface Iface where
  public export
  foo : Int

Main> :doc foo
Main.foo : Iface => Int
 Visibility: export

The visibility of the implementation is not related to the visibility of the interface itself. I apologize if I confused you, I'm a bit confused myself.

Here's an example showing the different behaviors:

namespace XX
  public export
  interface Iface where
    foo : Int

  export
  [Imp1] Iface where
    foo = 1

  public export
  [Imp2] Iface where
    foo = 1

failing "Can't solve constraint between: 1 and foo"
  prf1 : foo @{Imp1} = 1
  prf1 = Refl

prf2 : foo @{Imp2} = 1
prf2 = Refl

But for prf2 you need to publicly export the interface itself as well, because foo is just a function whose definition can only be unfolded if it is exported

Main> :set showimplicits
Main> :printdef foo
Main.XX.foo : Iface => Int
foo {__con = Iface at Iface:2:3--4:14 __bind_foo} = __bind_foo

[spcfox]

In the example above, the interfaces are elaborating into approximately this code:

namespace XX
  public export
  data Iface : Type where
    [noHints]
    MkIface : (foo : Int) -> Iface

  public export
  foo : Iface => Int
  foo @{MkIface x} = x

  export
  fooImp1 : Int
  fooImp1 = 1

  export
  Imp1 : Iface
  Imp1 = MkIface fooImp1

  public export
  fooImp2 : Int
  fooImp2 = 1

  public export
  Imp2 : Iface
  Imp2 = MkIface fooImp2

[joelberkeley]

I hadn't even considered public export on the methods themselves. Three different places to mark visibility definitely warrants documentation. The current documentation is lacking*. I don't think I'll have time to update it myself (the same situation for most I imagine). I will look at your example.

* some of it's incorrect too

[joelberkeley]

I understand your example now, thanks. I think that for this PR, my changes are correct. I might come back to updating the docs later