Zulip Chat Archive

Stream: general

Topic: Weird type class resolution behavior of subtype coercion


view this post on Zulip Eric Wieser (Oct 03 2020 at 10:35):

I'm surprised to find that only the first of these four instances works:

import algebra.free_algebra

open free_algebra

variables {R : Type*} [comm_semiring R] {X : Type*}

structure add_proof (C : free_algebra R X  Prop) : Prop :=
(add : Π {a b}, C a  C b  C (a + b))

def aux {C : free_algebra R X  Prop}  (p : add_proof C) := {value // C value}

variables {C : free_algebra R X  Prop} (p : add_proof C)

-- with a proof present, this works
instance ok : has_add (aux p) := λ a b, a + b, p.add a.prop b.prop⟩⟩

-- without it fails to find `has_lift_t (aux p) (free_algebra R X)`
instance fail1 : has_add (aux p) := λ a b, a + b, sorry⟩⟩

-- even with a type annotation
instance fail2 : has_add (aux p) := λ a b, ⟨(a + b : free_algebra R X), sorry⟩⟩

-- or show, from
instance fail3 : has_add (aux p) := λ a b, show free_algebra R X, from a + b, sorry⟩⟩

view this post on Zulip Reid Barton (Oct 03 2020 at 12:34):

Since there is no instance for aux I guess the real question is why ok does work. I think the variables a b in λ a b, must be inferred as having type {value // C value} somehow, in order to make sense of a.prop and b.prop. In the other cases they would be inferred as having type aux p.

view this post on Zulip Reid Barton (Oct 03 2020 at 12:34):

I also didn't know subtype.prop existed.

view this post on Zulip Eric Wieser (Oct 03 2020 at 13:04):

docs#subtype.prop looks to be an alias for docs#subtype.property


Last updated: May 14 2021 at 22:15 UTC