weird typechecking error

Stream: general

[Johan Commelin]

I have

ghost_map.zero :
  ∀ {p : ℕ} [_inst_3 : nat.prime p] {R : Type u_6} [_inst_4 : decidable_eq R] [_inst_5 : comm_ring R],
    ghost_map 0 = 0

And when I apply ghost_map.zero I get the following error:

type mismatch at application
  comm_ring_of_injective ghost_map ?m_12 ghost_map.zero
term
  ghost_map.zero
has type
  @ghost_map ?m_2 ?m_3 ?m_1 (λ (a b : ?m_1), ?m_4 a b) ?m_5 0 = 0
but is expected to have type
  @ghost_map ?m_2 ?m_3 ?m_1 ?m_4 ?m_5 0 = 0

I don't understand what's going on.

[Reid Barton]

what's the type of ghost_map?

[Johan Commelin]

I worked around it by using lots of @ and filling in a lot of underscores.

instance : comm_ring (𝕎 p R) :=
@comm_ring_of_surjective _ _ _ _ _ _ _
  (have hom : is_ring_hom (mv_polynomial.map coe : mv_polynomial R ℤ → mv_polynomial R ℚ), by apply_instance,
    @comm_ring_of_injective _ _ _ _ _ _ _
      (@comm_ring_of_injective _ _ _ _ _ _ _ _
        (ghost_map) sorry
        (@ghost_map.zero p _ (mv_polynomial R ℚ) _ _)
        (ghost_map.one) (ghost_map.add) (ghost_map.mul) (ghost_map.neg))
    (map $ mv_polynomial.map (coe : ℤ → ℚ))
    (map_injective _ $ mv_polynomial.coe_int_rat_map_injective _)
      (@map_zero _ _ _ _ _ _ _ _ _ hom)
      (@map_one _ _ _ _ _ _ _ _ _ hom)
      (@map_add _ _ _ _ _ _ _ _ _ hom)
      (@map_mul _ _ _ _ _ _ _ _ _ hom)
      (@map_neg _ _ _ _ _ _ _ _ _ hom))
(map $ mv_polynomial.counit _) (map_surjective _ $ counit_surjective _)
  (@map_zero _ _ _ _ _ _ _ _ _ (mv_polynomial.counit.is_ring_hom R))
  _
  -- (@map_one _ _ _ _ _ _ _ _ _ (mv_polynomial.counit.is_ring_hom R))
  (@map_add _ _ _ _ _ _ _ _ _ (mv_polynomial.counit.is_ring_hom R))
  (@map_mul _ _ _ _ _ _ _ _ _ (mv_polynomial.counit.is_ring_hom R))
  (@map_neg _ _ _ _ _ _ _ _ _ (mv_polynomial.counit.is_ring_hom R))

[Johan Commelin]

We almost know that witt vectors are a ring

[Johan Commelin]

For some reason that map_one line doesn't work. Even though it is completely analogous to its siblings.