Can't get at implicit variable

[treeowl]

IsReflexive : Rel a -> Type
IsReflexive {a} r = {x : a} -> x `r` x

lteIsReflexive : IsReflexive LTE
lteIsReflexive = ?lteIsReflexive_rhs

If I hit :p lteIsReflexive_rhs, I can see and use the x, but if I write

lteIsReflexive {x} = ?lteIsReflexive_rhs

I get an error:

builtin:0:0:When elaborating left hand side of lteIsReflexive:
Can't unify
        LTE x x (Type of lteIsReflexive x)
with
        argTy ->
        retTy (Is lteIsReflexive x applied to too many arguments?)

Specifically:
        Can't unify
                LTE x
        with
                \uv => argTy -> uv

I wonder if this might be related to #2211 or #2186.

[ahmadsalim]

@edwinb Why is this tagged as expected behaviour? :)

[ahmadsalim]

@edwinb This does not seem to have been fixed after the new implicit fixes.