Unbound implicits in record types

[ohad]

(Sorry about the title, happy to change if you have any suggestion!)

Steps to Reproduce

record Fails              (q : a -> a -> Type) (x : (a, a)) where
  Bar : q (fst x) (snd x)

record Works {0 a : Type} (q : a -> a -> Type) (x : (a, a)) where
  Bar' : q (fst x) (snd x)

Expected Behavior

Both typecheck

Observed Behavior

Fails gives the error:

  While processing type of .Bar. Can't solve constraint between: ?a [no locals in scope] and .a rec.

[gallais]

My understanding of the situation: at the moment we introduce implicits when we elaborate the type of the constructor. So all of the unnamed variables become implicit fields in the record.

But when the variable is used in the telescope of parameters we'd like it to be bound as an implicit parameter, not as a field.

We need to add an extra step spotting the unbound implicits in the raw parameters to generate the list of actual parameters.

The file of interest is TTImp.ProcessRecord.