fix compilation for Agda 2.3.0.1 again
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 3 Apr 2014 13:33:06 +0000 (15:33 +0200)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Thu, 3 Apr 2014 13:33:06 +0000 (15:33 +0200)
It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly.

Instances.agda

index 2e4ed3e..3f69627 100644 (file)
@@ -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)