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
| ^^^^^
Try:
{r : _} -> Functor (Foo r) where
map f (MkFoo v) = MkFoo (ff v) where
ff : {r' : Nat} -> Vect r' a -> Vect r' b