Selecting a named implementation in Idris 2

Question

According to this old answer, Idris 1 has the using syntax to select default implementations for a block of code. What is the corresponding Idris 2 syntax?

I've tried using the syntax from the answer:

using implementation Any
  tick1 : Time -> Writer Bool Time
  tick1 t = pure t

but this one doesn't even parse:

 `-- src/HL2/Clock.idr line 14 col 0:
     Expected end of input.
     
     HL2.Clock:14:1--14:6
      14 | using implementation Any
           ^^^^^

Answer 1

@{name} syntax allows custom implementations to be passed to functions.

[reverseOrd] Ord Nat where
   compare Z (S n)     = GT
   compare (S n) Z     = LT
   compare Z Z         = EQ
   compare (S x) (S y) = compare @{reverseOrd} x y


main : IO ()
main = printLn $ sort @{reverseOrd} [1,2,3,4,5]

This prints [5, 4, 3, 2, 1]

Answer 2

Based on discussions on an Idris community running on an unfortunately proprietary and commercial platform, the best bet seems to be:

1. Bind a name to the desired Monoid Bool implementation and mark it as %hint so that Idris2 will use it to resolve Monoid Bool constraints:

   %hint
   Any' : Monoid Bool
   Any' = Any
   

2. To avoid polluting the module's name space (you might of course have two functions in the same module that wish to use two different Monoid Bool implementations), put the whole thing (both the binding of Any' and the Writer-using definition) in a namespace.

Putting it all together, we get:

namespace Tick
  %hint
  Any' : Monoid Bool
  Any' = Any

  tick1 : Time -> Writer Bool Time
  tick1 = ...