Make dependent parameter available in Functor definition

I have the following wrapper for Vect

data Foo : (r : Nat) -> (t: Type) -> Type where    MkFoo : Vect r t -> Foo r t  

I'd like to implement Functor for Foo, and use the value of r in the implementation, but I can't get it to compile.

Functor (Foo r) where    map f (MkFoo v) = MkFoo (ff v) where      ff : {r' : Nat} -> Vect r' a -> Vect r' b  

gives

Error: While processing right hand side of map. r is not accessible in this  context.    Foo.idr:61:28--61:32      |   61 |   map f (MkFoo v) = MkFoo (ff v) where      |                            ^^^^  

This worked in Idris 1 but I can't figure out how to port it to Idris2. I've tried making r not erased, with

Functor ({r : _} -> Foo r) where    map f (MkFoo v) = MkFoo (ff v) where      ff : {r' : Nat} -> Vect r' a -> Vect r' b  

but I get

Error: While processing type  of Functor implementation at Foo.idr:60:1--62:46. When  unifying Type -> Type and Type.  Mismatch between: Type -> Type and Type.    Foo.idr:60:21--60:26      |   60 | Functor ({r : _} -> Foo r) where      |                     ^^^^^  

https://stackoverflow.com/questions/66609163/make-dependent-parameter-available-in-functor-definition March 13, 2021 at 09:07AM