diff --git a/Data/Profunctor/Strong.idr b/Data/Profunctor/Strong.idr index da0aba5..3e5d4a7 100644 --- a/Data/Profunctor/Strong.idr +++ b/Data/Profunctor/Strong.idr @@ -48,7 +48,7 @@ uncurry' = rmap (uncurry id) . first public export record GenTambara (ten, p : Type -> Type -> Type) a b where constructor MkTambara - getTambara : {0 c : Type} -> p (a `ten` c) (b `ten` c) + getTambara : forall c. p (a `ten` c) (b `ten` c) export Bifunctor ten => Profunctor p => Profunctor (GenTambara ten p) where diff --git a/Data/Profunctor/Types.idr b/Data/Profunctor/Types.idr index 60ae243..9bc72b4 100644 --- a/Data/Profunctor/Types.idr +++ b/Data/Profunctor/Types.idr @@ -22,7 +22,7 @@ interface Profunctor p where infix 0 :-> public export 0 (:->) : (p, q : k -> k' -> Type) -> Type -p :-> q = {0 a, b : _} -> p a b -> q a b +p :-> q = forall a, b. p a b -> q a b -- Instances for existing types