From 91db824bfa4d66f29066a381e88e6e3125e15576 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 3 Apr 2014 15:33:06 +0200 Subject: fix compilation for Agda 2.3.0.1 again It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly. --- Instances.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Instances.agda b/Instances.agda index 2e4ed3e..3f69627 100644 --- a/Instances.agda +++ b/Instances.agda @@ -26,7 +26,8 @@ MaybeFunctor = record ; identity = identity ; composition = composition } } - where _<$>_ = RawFunctor._<$>_ M.functor + where _<$>_ : {α β : Set} → (α → β) → Maybe α → Maybe β + _<$>_ = RawFunctor._<$>_ M.functor cong : {α β : Set} {g h : α → β} → g ≗ h → _<$>_ g ≗ _<$>_ h cong g≗h (M.just x) = P.cong M.just (g≗h x) -- cgit v1.2.3