[Agda] Re: Implicit vs. explicit function types

[Roly Perera]

My original example had some spurious explicit arguments.  I hope this
is a better version. I still can't form the pair f , g although to my
beginner's eyes they look like they have exactly the types that are
passed to ×.

thanks again,
Roly
-----------
module test where

open import Data.Product
open import Relation.Binary
open import Relation.Binary.Core
open import Data.Function

postulate
  World : Set
  _≤_ : Rel World
  f : (∀ {x} → _≤_ x       Respects _≡_)
  g : (∀ {y} → flip₁ _≤_ y Respects _≡_)

test : (∀ {x} → _≤_ x Respects _≡_) × (∀ {y} → flip₁ _≤_ y Respects _≡_)
test = f , g

2009/9/27 Roly Perera <roly.perera at dynamicaspects.org>:
> Hi,
>
> I've been using Agda for a couple of weeks and really enjoying it.
> I'm now stuck understanding an error message which complains that (of
> two function types) "one is an implicit function type and the other is
> an explicit function type".
>
> The code below repeats it.  I'm sure it's something very basic that
> I'm missing but I'd really appreciate some help.  The problem is with
> the type of the pair f , g.
>
> many thanks,
> Roly
>
>
> open import Data.Product
> open import Relation.Binary
> open import Relation.Binary.Core
>
> postulate
>  World : Set
>  _≤_ : Rel World
>
> ≤-resp-≡ : _≤_ Respects₂ _≡_
> ≤-resp-≡ = f , g where
>  f : ∀ {w₁ w₂ w₃} → w₂ ≡ w₃ → w₁ ≤ w₂ → w₁ ≤ w₃
>  f {w} {w′} .{w′} refl w≤w′ = w≤w′
>  g : ∀ {w₁ w₂ w₃} → w₂ ≡ w₃ → w₂ ≤ w₁ → w₃ ≤ w₁
>  g {w} {w′} .{w′} refl w′≤w = w′≤w