Binary `All`-like type not inferring types

[joelberkeley]

I'm somewhat confident this is a type checker bug.

gist ... out of curiosity, why is a gist helpful?

This is a little difficult to give an example for because every variant I construct of this problem gives a different error message. Here's one ...

Steps to Reproduce

data All2 : (a -> b -> Type) -> List a -> List b -> Type where
  Nil : All2 f [] []
  (::) : forall xs, ys . f x y -> All2 f xs ys -> All2 f (x :: xs) (y :: ys)

data Foo : List Nat -> Type -> Type where
data Bar : List Nat -> Type -> Type where

interface Convert (a : Type) (b : Type) | a where

go : All2 Foo xs as -> All2 Convert as bs => All2 Bar xs bs

data A = MkA
data B = MkB
Convert A B where

z : ()
z = let x : Foo [] A
        [y] := go [x]
     in ()

Expected Behavior

Type of y is inferred as Bar [] B. Andre mentioned that the let means it's a case expression and that might be complicating matters, but he said that for a very different setup and I think here the types are failing to be resolved on the RHS ... if we give idris a hint on the constraint it compiles

z : ()
z = let x : Foo [] A
        [y] := go @{[%search]} [x]
     in ()

Observed Behavior

[ build ] Error: While processing right hand side of z. Can't find an implementation for All2 Convert [A] [?y].
[ build ] 
[ build ]  170 | 
[ build ]  171 | z : ()
[ build ]  172 | z = let x : Foo [] A
[ build ]  173 |         [y] := go [x]
[ build ]                       ^^^^^^

[gallais]

Implementation resolution does not solve metas so it's not surprising that All2 Convert [A] [?y] does not get solved as that would require solving ?y.

[joelberkeley]

ok thanks. Why in that case does it work with @{[%search]}? With that, the only extra information I'm giving it is the length of the constraint. But I would have thought it could infer that from the structure of All2 and [A], before it starts resolving any Converts