MakeLemma doesn't transport erasable implicit arguments that must be explicitly bound for type checking

[stephen-smith]

data BNat = BZ | O BNat | E BNat

bnat_ind : {0 p : BNat -> Type}
        -> p BZ
        -> ((bn : BNat) -> p bn -> p (O bn))
        -> ((bn : BNat) -> p bn -> p (E bn))
        -> (bn : BNat) -> p bn
bnat_ind pbz po pe = go
 where
  go : (bn : BNat) -> p bn
  go BZ = ?pbz_hole
  go (O x) = po x (go x)
  go (E x) = pe x (go x)

Using MakeLemma \<LocalLeader>l on the ?pbz_hole in the above results in:

pbz_hole : ((bn : BNat) -> p bn -> p (E bn)) -> ((bn : BNat) -> p bn -> p (O bn)) -> p BZ -> p BZ

being created, but that doesn't type check:

file:loc:While processing type of pbz_hole at talia.idr:16:1--18:1:                                                                              
Undefined name p

(and then further failures since pbz_hole ends up not bound in the global context.)

[edwinb]

This (and the others about what Idris does) should really be on the Idris2 issue tracker. The vim mode doesn't do anything other than send Idris 2 the request.

There's plenty of things that aren't yet fully implemented in Idris2's interactive mode yet I'm afraid... as long as they're on the tracker, we'll get to them eventually!

[stephen-smith]

Fair point. I'm just not always sure it's Idris2 being the problem and not vim bindings, should I just default to the Idris2 tracker for now, or is there a good rule of thumb to follow?

I'm am really just recording these as backlog items, no expecting fixes or even works around. I expect breakage in this release. Plus, it gives me a list of things to work on if I ever decide to fiddle with the actual code.

[stephen-smith]

Migrated to idris-lang/Idris2#185 .