Record elaboration can't handle parameter types that contain implicit function types

[mjustus]

Example

Elaboration of a record that has an implicit function as one of its parameters

record R (A : Type) (B : {a : A} -> Type) where
  constructor MkR

currently fails with an error message

While processing constructor MkR. Can't bind implicit Main.{a:838} of type A[2]

Explanation

elabRecord generates the following type for MkR

(%claim Main.MkR
  (%pi Rig0 Implicit (Just A) %type
  (%pi Rig0 Implicit (Just B)
  (%pi RigW Implicit (Just v) A %type)
    ((Main.R A) B)))
)

To make it work, Idris would need to insert an implicit lambda around B, producing the TTImp equivalent of

data R : (A : Type) -> (B : {a : A} -> Type) -> Type where
  MkR : {0 A : Type} -> {0 B : {a : A} -> Type} -> R A (\{a : A} => B {a = a})

where \{a : A} => ... is made-up syntax for an implicit lambda.

Note that this would need to be a recursive process:

record R2 (A : Type) (B : {f : {a : A} -> Type} -> Type) where
  constructor MkR2

should turn into

data R2 : (A : Type) -> (B : {f : {a : A} -> Type} -> Type) -> Type where
  MkR2 : {0 A : Type} -> {0 B : {f : {a : A} -> Type} -> Type} -> R2 A (\{f : {a : A} -> Type} => B {f = \{a : A} => f {a}})