[ fix ] Fix interface elaboration when %unbound_implicits is off

[dunhamsteve]

Description

A user on discord reported problems defining interfaces with constraints if unbound_implicits is disabled. The error was undefined names on the type of the Constraint that was being generated. The missing names are always the parameters of the interface (because the interface with parameters is part of the type), so I implicitly pi-bind in all of the parameters. This is also done in the existing code when generating the type for the data.

Prior to the fix the following code:

%unbound_implicits off
interface Foo a where
interface Foo a => Bar (a : Type) where

reports the error

Error: While processing type of Constraint (Foo a). Undefined name a.

tests.idris2.interface030.NoUnbound:3:1--3:40
 1 | %unbound_implicits off
 2 | interface Foo a where
 3 | interface Foo a => Bar (a : Type) where
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

with the patch we get no error.

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.md (and potentially also
  CONTRIBUTORS.md).

[gallais]

I don't think that's appropriate: a is indeed unbound here.
You should write something like (I don't have idris on this laptop yet):

%unbound_implicits off
interface {0 a : Type} -> Foo a where
interface {0 a : Type} -> Foo a => Bar a where

[dunhamsteve]

I had tried that, and I thouht that would be more consistent with implementation. But the syntax you used does not exist on interface. I added the syntax yesterday and threaded it through to the interface elaboration. The issue that I ran into was that the Constraint types were the only ones relying on unbound implicits (IBindHere, etc). In all the other cases (the data type, etc), the parameters were explicitly added.

Here they are added to the data type:

Idris2/src/Idris/Elab/Interface.idr

Lines 448 to 450 in 86c53e6

	let dty = bindPs params -- bind parameters
	$ bindIFace vdfc ity -- bind interface (?!)
	$ substNames vars methNameMap dty

And to the top level methods:

Idris2/src/Idris/Elab/Interface.idr

Line 192 in 86c53e6

ty_imp <- bindTypeNames EmptyFC [] vars (bindPs params $ bindIFace vfc ity ty_constr)

with a note down here:

Idris2/src/Idris/Elab/Interface.idr

Lines 213 to 218 in 86c53e6

	-- Bind the type parameters given explicitly - there might be information
	-- in there that we can't infer after all
	bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
	bindPs [] ty = ty
	bindPs ((n, rig, pty) :: ps) ty
	= IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

Adding those implicits up front, we could have the type of a declared twice:

interface {0 a : Type} -> Foo (a : Type -> Type)  where

So I had figured in for a penny, in for a pound, and have getConstraintHint work like everything else.

Currently params are added to the top level methods (see above) and the data type. Constraints (and only constraints) rely on unbound implicits. And they're added and then removed from the method declaration within the data (presumably because the data already has them up front):

Idris2/src/Idris/Elab/Interface.idr

Lines 213 to 218 in 86c53e6

	-- Bind the type parameters given explicitly - there might be information
	-- in there that we can't infer after all
	bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
	bindPs [] ty = ty
	bindPs ((n, rig, pty) :: ps) ty
	= IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

If we want to add that syntax, we need to decide how it interacts with the (a : Type) declarations at the end, whether we want to continue to inject the params when unbound_implicits is off, and how it interacts with the injection of params when unbound_implicits is on (to avoid duplicate binders).

[mattpolzin]

This PR's changelog entry will likely end up under the v0.7.0 heading unintentionally if git is left to its own devices.