Recursive type coercions

Stream: general

[Gijs van Cuyck]

I would like to apply type coercion to the arguments of types to get the following to typecheck for a custom wrapper type, assuming there already is a type coercion from A to B:

def examp  {A B: Type} (value: Wrapper A) : Wrapper B := value

I can write a Coe instance

instance {A B :Type*} [mapping: Coe A B]: Coe (Wrapper A) (Wrapper B) where ...

but this will only work some of the time, as there seem to be many variations of the Coe typeclass and this only matches one of them. Is there a good more general way to define these sort of recursive type coercions?

I also noticed that these kinds of type conversions seem to exist for some build in types, but not for others. I can for instance convert List Nat to List Int, but not Set Nat to Set Int. I would at least expect something in the direction of

instance {A B :Type*} [mapping: Coe A B]: Coe (Set A) (Set B) where
  coe set := set.image mapping.coe

to already be part of the Set library. Things like

def unioncast  {A: Type} {X Y: Set A} (value: X):  (X ∪ Y  : Set A)  := value

also do not work by default. Is there a reason for this? Should I be doing this in the first place?