Coerce array to subarray at fn call site

Stream: new members

[Somo S.]

Suppose I have a function that naturally accepts a subarray but I want it to be invocable using an array as well (i.e. so it behaves "polymophically"). How might one achieve this?

[Somo S.]

Here is my naive attempt:

instance : Coe (Array α) (Subarray α) :=
  ⟨Array.toSubarray⟩

def foo (_ : Subarray α) : Unit := ()

#check foo (#[-0, 1] : Subarray Int)-- WORKS

def x : Subarray Int := #[-0, 1]
#check foo x -- WORKS


-- But what I want to work is like:
#check foo #[-0, 1] -- FIXME
/-
application type mismatch
  foo #[-0, 1]
argument
  #[-0, 1]
has type
  Array Int : Type
but is expected to have type
  Subarray ?m.754 : Type
 -/


-- Or:
def y : Array Int := #[-0, 1]
#check foo ↑y -- FIXME
/-
type mismatch
  y
has type
  Array Int : Type
but is expected to have type
  Subarray ?m.1411 : Type
 -/

[Eric Wieser]

foo (α := Int) #[-0, 1] works too, but I agree this is suboptimal

[Somo S.]

thanks thats actually helpful. for some reason, i hadn't realized i could also redefine the signature of foo so the type is expicit

[Somo S.]

indeed not optimal, but atleast it works.

[Notification Bot]

Somo S. has marked this topic as resolved.

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

I've unresolved this; I think this is a good question, and suggests either a shortcoming in the coercion system, or a use-case for unif_hint which is otherwise totally unused.

[Somo S.]

i guess a good candidate for RFC then?

[Kim Morrison]

Maybe you could show us some code where this would be useful? I suspect this is mostly an #xy problem, and the real solution is to want something else. :-)

[Mario Carneiro]

@Somo S. Here's an implementation of my suggestion:

class ArrayLike (σ : Type u) (α : outParam (Type v)) where
  toSubarray : σ → Subarray α

instance : ArrayLike (Array α) α := ⟨Array.toSubarray⟩
instance : ArrayLike (Subarray α) α := ⟨id⟩

instance : Coe (Array α) (Subarray α) :=
  ⟨Array.toSubarray⟩

def foo [ArrayLike σ α] (_ : σ) : Unit := ()

def y : Array Int := #[-0, 1]
def x : Subarray Int := #[-0, 1]

#check foo (#[-0, 1] : Subarray Int)
#check foo x
#check foo #[-0, 1]
#check foo ↑y

[Somo S.]

great @Mario Carneiro .. this is actually perfect! I had tried this.. but dont yet understand when is a good time to use outParam (so i didn't include outparam) thanks for this!