idris-make-lemma doesn't extract implict arguments

[xoltar]

When extracting lemmas, idris-mode sometimes generates code that won't compile because it doesn't copy implicit args declarations.

For example:

data V : Nat -> Type -> Type where
     Nil : V Z t
     (::) : t -> V k t -> V (S k) t

head_unequal : DecEq a => {xs : V n a} -> {ys : V n a} ->
                              (contra : (x = y) -> Void -> (x :: xs) = (y :: ys)) -> Void

head_unequal {x} {y} contra = case decEq x y of
                                  No c => ?n
                                  Yes Refl => ?hole

Put your cursor on ?hole and run idris-make-lemma, it creates:

hole : (contra : (y = y) -> Void -> (y :: xs) = (y :: ys)) -> Void

Which then fails to compile because:

- + Errors (1)
 `-- checkeq_dec.idr line 32 col 5:
     When checking type of Main.hole:
     Can't disambiguate name: Prelude.List.::, 
                              Main.::, 
                              Prelude.Stream.::, 
                              Data.Vect.::

Manually copying the implicit parameters xs and ys from head_unequal to hole fixes the compile issue

[david-christiansen]

Sorry for the slow response.

This is an Idris issue that will need some updates.

[keram]

in idris2

head_unequal : DecEq a => {1 xs : V n a}
  -> {1 ys : V n a}
  -> {x : a}
  -> {y : _}
  -> (contra : (x = y)
  -> Void -> (x :: xs) = (y :: ys))
  -> Void
head_unequal {x} {y} contra = case decEq x y of
                                   No c => ?n
                                   Yes Refl => ?hole

generates:

hole : DecEq a -> (1 xs : V n_0 a) -> (1 ys : V n_0 a) -> (x : a) -> (x = x -> Void -> x :: xs = x :: ys) -> a -> Void

head_unequal : DecEq a => {1 xs : V n a}
  -> {1 ys : V n a}
  -> {x : a}
  -> {y : _}
  -> (contra : (x = y)
  -> Void -> (x :: xs) = (y :: ys))
  -> Void
head_unequal {x} {y} contra = case decEq x y of
                                   No c => ?n
                                   Yes Refl => hole conArg xs ys x contra y

And then errors with:

- + Errors (1)
 `-- x.idr line 40 col 53:
     While processing right hand side of head_unequal. Undefined name conArg. 

Not a idris-mode issue though