funny error

Stream: general

[Kenny Lau]

I could not minimize this error.

[Kenny Lau]

https://gist.github.com/kckennylau/a62295136d2daf48146f6fcdb8e37a49

[Kenny Lau]

error:

[Kenny Lau]

type mismatch at field 'right_inv'
  ?m_1
has type
  function.right_inverse (λ (φ : alg_hom (polynomial R) A), φ.val (finsupp.single 1 1))
    (λ (r : A),
       ⟨λ (f : polynomial R),
          finsupp.sum f (λ (n : ℕ) (c : R), (λ (r : R) (x : A), algebra.f A r * x) c (monoid.pow r n)),
        _⟩)
but is expected to have type
  function.right_inverse (λ (φ : alg_hom (polynomial R) A), φ.val (finsupp.single 1 1))
    (λ (r : A), ⟨λ (f : polynomial R), finsupp.sum f (λ (n : ℕ) (c : R), c • r ^ n), _⟩)

[Kenny Lau]

where ?m_1 was a literal underscore

[Kenny Lau]

that's it folks, an underscore has a type error

[Kenny Lau]

@Mario Carneiro

[Kevin Buzzard]

I think we've seen this happen before

[Kevin Buzzard]

were you making a big structure and doing crazy stuff like sorrying out constants?

[Kevin Buzzard]

I find these sorts of things a bit annoying to do for reasons like this