Can't use parent constraint in function

[shmish111]

https://github.com/shmish111/Idris-Bifunctors/blob/master/Data/Bimonad.idr#L42

Steps to Reproduce

idris2 Data/Bimonad.idr

Expected Behavior

Type checks successfully

Observed Behavior

Data/Bimonad.idr:33:38--33:47:While processing right hand side of Data.Bimonad.Default implementation of >>== at Data/Bimonad.idr:33:3--41:1:
Can't find an implementation for Bifunctor p
Data/Bimonad.idr:42:15--42:25:While processing right hand side of Data.Bimonad.biunit at Data/Bimonad.idr:42:1--44:1:
Can't find an implementation for Biapplicative p
Data/Bimonad.idr:44:1--46:1:Undefined name Bimonad

If I explicitly add the Biapplicative p q constraint I get a different error that I don't understand at all:

Data/Bimonad.idr:33:38--33:47:While processing right hand side of Data.Bimonad.Default implementation of >>== at Data/Bimonad.idr:33:3--41:1:
Can't find an implementation for Bifunctor p
Data/Bimonad.idr:41:11--41:28:While processing type of Data.Bimonad.biunit at Data/Bimonad.idr:41:1--42:1:
When unifying Type and (Type -> Type -> Type) -> ?a
Mismatch between:
	Type
and
	(Type -> Type -> Type) -> ?a
Data/Bimonad.idr:42:1--44:1:No type declaration for Data.Bimonad.biunit
Data/Bimonad.idr:44:1--46:1:Undefined name Bimonad

[edwinb]

What happens if you remove the default implementation of >>== and add it to the implementation explicitly?

[shmish111]

Same issue with biunit but the missing Bifunctor issue goes away.

I then put the default back and tried adding Bifunctor p, Bifunctor q constraint to the interface definition and weirdly it still complained about missing Bifunctor p?

[edwinb]

I imagine there's still some corners of auto implicit search that need work.

Another thing you could try is to write the constraints in the form Foo a => Bar a => a, rather than (Foo a, Bar a) => a. If that makes any difference, it's an interesting piece of information...

[shmish111]

Yeah I tried that on biunit and got a very weird error:

Data/Bimonad.idr:41:10--41:28:While processing type of Data.Bimonad.biunit at Data/Bimonad.idr:41:1--42:1:
When unifying Type and ?argTy -> Type
Mismatch between:
	Type
and
	?argTy -> Type
Data/Bimonad.idr:42:1--44:1:No type declaration for Data.Bimonad.biunit

Strangely changing for the interface definition gave the same result as previously.

[shmish111]

related question, in idris 2 is there a way to make the default access in a module public export? It seems that’s what %access did in idris 1.

[edwinb]

I haven't implemented %access and I'd rather not, because it's too easy to export things accidentally.

[shmish111]

makes total sense however I was looking at writing Data.Morphisms from Idris 1 base and it really seems like a lot of work to add it to everything?

[edwinb]

It will be a bit annoying to add them all, unfortunately. I've done it for quite a few things so far, though, and I think it's still better this way, and has at least made me think about whether things really need to be public export.

Meanwhile, I think I see what's going on here. There's a couple of things I haven't got quite right in the search algorithm which only crop up when chasing parent interfaces with multiple constraints and multiple parameters. I'll explain in full once I've fixed it...

[edwinb]

I expect it's worth saying a bit more about this, in case it helps someone understand a bit more about how things work internally. The two problems were about determining arguments, and pairs in parent constraints. The implicit search will only start looking when the type is completely resolved (up to determining arguments), so it will search for, say...

Bimonad p q

...but not

Bimonad p ?unknown

This is fine at the top level, but here when looking for parent constraints, it encounters...

Bimonad p q => Biapplicative p

...which means in order to resolve Biapplicative p it has a new constraint Bimonad p ?q. That is, it doesn't know what q is, so gives up the search. But away from the top level, it doesn't matter what q is - any one will do! So the fix is to only check that the goal is complete at the top level search.

The other bit is a bit annoying, and is about pairing constraints. Ordinarily, constraints written as (Foo a, Foo b) are just pairs, but on interface definitions, this generates a constraint chasing function. In this case, we have something like...

constraint : Bimonad p q -> (Biapplicative p, Biapplicative q)

...which gives back a pair, but to keep things reasonably efficient the search algorithm will only look for things with the appropriate target type, so it won't check this when looking for a Biapplicative and even if it did, it's a bit fiddly to find the relevant part of the pair. So, instead, in this case, it deconstructs the pair before elaborating, which leads to:

constraintP : Bimonad p q -> Biapplicative p
constraintQ : Bimonad p q -> Biapplicative q