Overenthusiastic erasure

pairfail.idr

  -- This segfaults, due to an erased name being used in the case
  -- block generated for the 'j'' binding
  foo : Nat -> ((Int, String) -> Nat -> IO a) -> IO a
  foo Z k = k (0, "End") Z
  foo (S j) k = foo j (\(i', s'), j' => k (i'+1, s') j')
  
  -- This doesn't segfault, since Idris treats the \j' as an ordinary binder
  -- rather than a pattern matching one.
  foo' : Nat -> ((Int, String) -> Nat -> IO a) -> IO a
  foo' Z k = k (0, "End") Z
  foo' (S j) k = foo j (\(i', s') => \ j' => k (i'+1, s') j')
  
  main : IO ()
  main = foo 1 (\_, _ => putStrLn "End")