Confusing behavior when using a constraint name in interface parameters

[spcfox]

Steps to Reproduce

This code compiles successfully:

import Data.So

interface (b : Bool) => Iface (prf : So b) where
  constructor MkIface

It may seem that the parameter depends on the constraint. But it doesn't. Currently, constraints depend on parameters, not the other way around. The b in a parameter is implicitly bound and has nothing to do with the b in a constrain:

Main> :ti MkIface
Main.MkIface : {0 b : Bool} -> {prf : So b} -> Bool => Iface {b} prf
               ^----------^                   ^----^
             b from parameter           b from constraint

We can try to prove it:

0 getConstraint : Iface prf -> Bool
getConstraint (MkIface @{b}) = b

0 getParameter : Iface prf -> Bool
getParameter (MkIface {b}) = b

failing "Mismatch between: b (implicitly bound at Main:14:3--14:11) and b (implicitly bound at Main:14:12--14:19)"
  0 tryProof : (x : Iface prf) -> getConstraint x === getParameter x
  tryProof MkIface = Refl

Expected Behavior

Warning or error

Observed Behavior

Successful compilation

[spcfox]

Also now conflicting names of parameters, arguments, and constraints behave differently

failing "Mismatch between: Nat and Bool"
  interface Iface (b : Bool) (b : Nat) where

-- Produce warning about shadowing
f : (b : Bool) -> (b : Nat) -> ()

-- Successful compilation without warning
interface (b : Bool) => (b : Nat) => Iface where

[spcfox]

I find it odd that function arguments can have the same names, because it's very unintuitive

f : {b : Bool} -> {b : Nat} -> ()

g : ()
g = f {b = True} {b = 0}

[andrevidela]

yeah that should probably not be allowed

[spcfox]

One more strange thing:

f : {b : Bool} -> {b : Nat} -> ()

failing "While processing left hand side of f. Non linear pattern b"
  f = ()

-- Successful compilation
f {b=_} = ()

[andrevidela]

So I've been playing with this for a bit in the past few days and my conclusion is that interface elaboration is subtly broken in very annoying ways.

Like you point our, the way the constraints are elaborated is confusing, some parameters get lifted as arguments, sometimes shadowing each other. %unbound_implicits off does not seem to help at all which is counter-intuitive. Interestingly enough using a parameters block helps but messes up instance resolution.

The conclusion I've come to is that elaborating constraints as record fields is problematic. They should be record parameters, or at least there should be a meta-operation to move fields into parameters and vice-versa to help with instance search. Do you think this would lead to a resolution of the problem? Let me know if you think this is going in the right direction of I'm off-base completely

[buzden]

They should be record parameters, or at least there should be a meta-operation to move fields into parameters and vice-versa to help with instance search.

It looks like this move would switch resolution of parent implementation to a cite of use rather than to the cite of declaration of implementation. This seems to be a big change in the semantics: e.g. it means that, say, an implementation cannot reduce bodies of particular parent ever. Also, it seems to make using not work for implementations. This may be not really a problem when implementations are coherent, but this is not the case for Idris.
UPD: I realised that I seem to misunderstood what is proposed, sorry

Anyway, it's not clear how this would solve the original problem.

[spcfox]

Do you think this would lead to a resolution of the problem?

I don't think this solves the problem because all I'm suggesting is adding a warning here, and it's weird to change semantics just for the sake of it. So further my text is off-topic.

However, making constraints parameters of the interface can be useful. In Haskell, each type can have only one instance of an interface, so constraints are resolved unambiguously. In Idris, implementations can have different constraints, and sometimes it is useful to specify this at the type level. A common example is VerifiedFunctor and similar interfaces. It is important at the type level to know the proofs for which particular Functor implementation they contain.

One solution was suggested in #777 — the ability to make constraints parameters.

Another solution was suggested in #3420 — auto-parameters, which are similar to constraints, and they are sufficient for interfaces with proofs.

If I understand correctly, you are proposing to make all constraints implicit parameters. I'm not sure this would always work well, but I think it might be useful sometimes. In fact, this is a special case of the first solution. However, constraints also need to remain fields in order to be available at runtime.

[andrevidela]

constraints also need to remain fields in order to be available at runtime.

That is not the case! Parameters are available at runtime as long as they are not marked as 0

[spcfox]

That is not the case! Parameters are available at runtime as long as they are not marked as 0

Arguments of the record constructor for parameters are erased

record X (n : Nat) where
  constructor MkX

failing "While processing right hand side of getn. n is not accessible in this context"
  getn : X n -> Nat
  getn (MkX {n}) = n

Main> :ti MkX
Main.MkX : {0 n : Nat} -> X n

[andrevidela]

It took me a second to realise why my statement was wrong, but it's because the type constructor has the unrestricted multiplicity not the data-constructor.