## Stream: general

### Topic: weird typechecking error

#### Johan Commelin (Jun 14 2019 at 14:49):

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 (Jun 14 2019 at 15:01):

what's the type of ghost_map?

#### Johan Commelin (Jun 14 2019 at 15:33):

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 ℚ) _ _)
(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 (Jun 14 2019 at 15:33):

We almost know that witt vectors are a ring

#### Johan Commelin (Jun 14 2019 at 15:34):

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

Last updated: May 14 2021 at 04:22 UTC