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?

[Gijs van Cuyck]

For future reference, the type Coercion from List Nat to List Int Uses Lean.Internal.coeM trough its monad instance. coeM is not currently recursively applicable, so that is why casting List (List Nat) to List (List Int) does not work. This does not work for Set as the Set Monad instance is hidden by default.

I ended up defining my own recursive coercions as required. They work, but use internal classes not mean for user implementation, so there might still be reasons unknown to me that make this a bad idea. The high priority is an attempt to make type inference choose this option always when applicable, but I don't know enough about the inference system to be sure if that is what is actually happening.

  /-- Converts Set a into Set b, assuming there already is a conversion from a to b.
    This is implemented trough an interal Coe class not meant for user implementation, which is a red flag.
    However, this way it is generally recursively applicable, while this does not seem possible with just the normal Coe classes.-/
instance (priority := high)  coeSetRecInst {a b: Type*} [mapping: CoeHTCT a b]: CoeHTCT (Set a) (Set b) where
  coe set := set.image mapping.coe