Unable to unify named arguments within a functor

[EmmaTye]

Steps to Reproduce

import Data.Fin

foo : Applicative f =>
      f ((n : Nat) -> Fin n) ->
      f (Fin 2)
foo fun = fun <*> pure 2

Expected Behavior

foo typechecks and compiles successfully.

Observed Behavior

Error when typechecking foo:

Error: While processing right hand side of foo. When unifying: Fin n and: Fin 2 Mismatch between: n and 2.

Extra considerations

• Outside of a functor setting, the following typechecks successfully ✅

bar : ((n : Nat) -> Fin n) ->
      Fin 2
bar fun = fun 2

• Inside a functor, a named argument without a dependent type also typechecks successfully ✅

baz : Applicative f =>
      f ((n : Nat) -> String) ->
      f (String)
baz fun = fun <*> pure 2

• Providing an explicit Applicative instance does not cause the application to typecheck ❌ This gives the exact same error as with foo.

qux : Maybe ((n : Nat) -> Fin n) ->
      Maybe (Fin 2)
qux fun = fun <*> pure 2

[gallais]

It's the expected behaviour although the error message is pretty terrible.

Main> :t (<*>)
Prelude.(<*>) : Applicative f => f (a -> b) -> f a -> f b

As you can see the function type inside apply's first argument f (a -> b) is non-dependent but here you're trying to use it with a function where (a -> b) would need to be the dependent type (n : Nat) -> Fin n. And indeed it can never be a dependent function type: if it were dependent we would not know what a to feed it to describe the b-shaped return type given that we cannot assume that the second argument of type f a is pure in general.

Luckily you can achieve the same result by using the Functor interface instead (and we know from the Applicative laws that it should give you the same result).

I had to feed in the implicit argument a explicitly because it was too difficult for Idris to reconstruct by unification.

import Data.Fin

foo : Applicative f =>
      f ((n : Nat) -> Fin n) ->
      f (Fin 2)
foo = map {a = (n : Nat) -> Fin n} ($ 2)

[EmmaTye]

That's great, thanks!

Is there an equivalent to Haskell's lens (??) in Idris2? See Control.Lens.Lens.(??)

(??) :: Functor f => f (a -> b) -> a -> f b
fab ?? a = fmap ($ a) fab

It's also called flap in relude (in that it's a kind of flipped functorial application).

Here's a quick Idris2 excerpt that shortens the above foo:

import Data.Fin

flap : Functor f => {0b : a -> Type} -> f ((x : a) -> b x) -> (x : a) -> f (b x)
flap fab x = map {a = (x : a) -> b x} ($ x) fab

foo : Applicative f =>
      f ((n : Nat) -> Fin n) ->
      f (Fin 2)
foo fab = flap fab 2

[gallais]

Not that I know of