How can I create a function for casting values: x `as` T = y?

Question

I have the interface for converting things of some type this to another type target.

interface ConvertibleTo (target : Type) (this : Type) where
    convert : this -> target

Can I somehow write a function, that takes some value of this, then the target type, and then produces a value of target type?

I've tried to write this

-- Example: 1 `as` String = "1"
as : ConvertibleTo target this => this -> (target : Type) -> target
as value _ = convert value

but it doesn't work. The compiler says

   |
27 | as value _ = convert value
   |              ~~~~~~~~~~~~~

When checking right hand side of as with expected type
    iType

Can't find implementation for ConvertibleTo iType this

And I do not understand that message, because I've already added a constraint.

Answer 1

Problem is, with (target : Type) you introduce a new variable internally called iType (as target is already assigned elsewhere), which -> target refers to. Because the constraint uses target, it should come after this argument. Constraints are just magic implicit arguments, so you don't have to put them first:

interface ConvertibleTo (target : Type) (this : Type) where
    convert : this -> target

as : this -> (target : Type) -> ConvertibleTo target this => target
as x _ = convert x

ConvertibleTo String Nat where
    convert = show

> as (S Z) String
"1"

(In case you didn't know, there is already a ConvertibleTo interface in the standard library with some useful implementations: Cast from to)