polyrith fails if expression is an equality of numerals

[eric-wieser]

This doesn't work, because the translation to python forgets to promote 2 and 0 to sage polynomial objects

import tactic.polyrith
import algebra.char_p.basic

example {R} [comm_ring R] [char_p R 2] (x : R) : x + x = 0 :=
begin
  have : (2 : R) = 0,
  { convert char_p.cast_eq_zero R 2, norm_cast },
  polyrith,
end

polyrith failed to retrieve a solution from Sage! TypeError: object of type 'Ideal_pid' has no len()
state:
R : Type ?,
_inst_1 : comm_ring R,
_inst_2 : char_p R 2,
x : R,
this : 2 = 0
⊢ x + x = 0

Adding a silly *x term resolves the issue

import tactic.polyrith
import algebra.char_p.basic

example {R} [comm_ring R] [char_p R 2] (x : R) : x + x = 0 :=
begin
  have : (2 : R) = 0*x,
  { simp, convert char_p.cast_eq_zero R 2, norm_cast },
  polyrith,
end