edwinb/idris2-vim

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

Closed this issue · 3 comments

stephen-smith commented 
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 commented

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 commented

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.