Zulip Chat Archive

Stream: general

Topic: weird typechecking error


view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 14 2019 at 15:01):

what's the type of ghost_map?

view this post on Zulip 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 ) _ _)
        (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))

view this post on Zulip Johan Commelin (Jun 14 2019 at 15:33):

We almost know that witt vectors are a ring

view this post on Zulip 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