Profunctor Iso doesn't type check

Question

I'm trying to implement the simplest profunctor optic in Idris. Iso is a function that is supposed to be polymorphic in all profunctors. I think that's the correct syntax.

Everything type-checks, except for the final test.

interface Profunctor (p : Type -> Type -> Type) where
  dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t

-- A pair of functions
data PairFun : Type -> Type -> Type -> Type -> Type where
  MkPair : (s -> a) -> (b -> t) -> PairFun a b s t

-- PairFun a b s t  is a Profunctor in s t
Profunctor (PairFun a b) where
  dimap f g (MkPair get set) = MkPair (get . f) (g . set)

-- Extract a pair of functions from an Iso
fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)

-- Turn a pair of functions to an Iso
toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set

-- forall p. Profunctor p => p Int Int -> p Char String
myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)

x : PairFun Int Int Char String
x = fromIso myIso

I'm getting this error. It looks like Idris is complaining about the assumption that p1 is a Profunctor, but that's the constraint in the definition of Iso.

Can't find implementation for Profunctor p1
    Type mismatch between
            p1 Int Int -> p1 Char String (Type of myIso p1
                                                         constraint)
    and
            p Int Int -> p Char String (Expected type)
                
     Specifically:
            Type mismatch between
                    p1 Int Int
            and
                    p Int Int

Answer 1

The following code worked for me in Idris 2 version 0.3. This is a fairly old version of Idris 2, but it probably works in more recent versions too.

interface Profunctor (0 p : Type -> Type -> Type) where
  dimap : (a' -> a) -> (b -> b') -> p a b -> p a' b'

Iso : Type -> Type -> Type -> Type -> Type
Iso a b s t = {0 p : Type -> Type -> Type} -> Profunctor p => p a b -> p s t

data PairFun : Type -> Type -> Type -> Type -> Type where
  MkPair : (s -> a) -> (b -> t) -> PairFun a b s t

Profunctor (PairFun a b) where
  dimap f g (MkPair get set) = MkPair (get . f) (g . set)

fromIso : Iso a b s t -> PairFun a b s t
fromIso iso = iso (MkPair id id)

toIso : PairFun a b s t -> Iso a b s t
toIso (MkPair get set) = dimap get set

myIso : Iso Int Int Char String
myIso = toIso (MkPair ord show)

x : PairFun Int Int Char String
x = fromIso myIso

Unfortunately I don't know how to make this work in Idris 1. There the issue appears to be generativity of p: the elaborator does not infer p1 = p2 from p1 a b = p2 a b. In any of the Idrises, this does not generally hold, because p1 and p2 can be arbitrary functions. Idris 2 appears to proceed to p1 = p2 anyway at some point; this is a convenience feature at the cost of some robustness of inference.

The irrelevance annotations on p in the above code are not related to the generativity issue that I've just mentioned, they are just required to reproduce the Idris 1 and GHC behavior. In Idris 2, implicitly introduced variables always have 0 multiplicity, so we have to make the p erased as well, to be able to apply it to 0 type parameters. Moreover, the 0 p matches Idris 1 / GHC behavior where types in general are erased. In Idris 2, types are only erased when bound with 0.