Right associativity for the arrow operator in the presence of implicit arguments

[anton-trunov]

Steps to Reproduce

data R : Type where
  MkR : (() -> {t : Type} -> t) -> R

f : R -> () -> {t : Type} -> t
f (MkR g) = g

f' : R -> (() -> {t : Type} -> t)
f' (MkR g) = g

Expected Behavior

The code typechecks.

Observed Behavior

Error at line 8, col 3:

 When checking right hand side of f' with expected type
        () -> t
 
Type mismatch between
        () -> t1 (Type of g)
and
        () -> t (Expected type)

Specifically:
        Type mismatch between
                t1
        and
                t

Notes

• The code is inspired by this Stackoverflow question.
• While constructing f and f' the typing contexts are not identical.
• The following piece of code can be used as a workaround for f':

f' : R -> (() -> {t : Type} -> t)
f' (MkR g) u = g u

[ahmadsalim]

Thanks for reporting the issue.
I guess you found the workaround, so I will just tag it as is.