Cannot construct record value due to failure in constraint solving

[ibbem]

Cannot construct record value due to failure in constraint solving

[andreasabel]

It works if you make parameter B in associative explicit and put it at the beginning.

record Monad (M : Set → Set) : Set₁ where
  field
    bind : {A B : Set} → (A → M B) → M A → M B

    associative : ∀ (B : Set) {A C : Set} → {f : A → M B} → {g : B → M C} → bind g ∘ bind f ≡ bind (bind g ∘ f)

M : Set → Set → Set
M R A = (A → R) → R

bind : {R A B : Set} → (A → M R B) → M R A → M R B
bind f a = λ cont → a (λ a' → f a' cont)

associative : ∀ {R} B {A C} → {f : A → M R B} → {g : B → M R C} → bind g ∘ bind f ≡ bind (bind g ∘ f)
associative B = refl

contMonad : (R : Set) → Monad (M R)
contMonad R = record { bind = bind; associative = associative }

The problem in the OP is that Agda eagerly inserts implicit arguments, but then it cannot recover the solutions for B, g and f because they are not unique in higher-order unification. The cure is to make the first parameter explicit when this happens.

[andreasabel]

Something for consideration is whether we should make the record-from-module syntax behave more akin to the user expectation, so don't just resolve it to a record expression before type-checking, but have a more direct mechanism that short-cuts the insertion of implicit arguments.

[ibbem]

OK, Thanks. I think that I understand the problem now.

I'm quite new to Agda but I intuitively expected that record { associative = associative } would only eagerly apply as many implicit arguments to g until it has the same number (or less) implicit arguments left as f. Then the rest of the type could be unified. As far as I understand this would have the same effect as stopping eager application of implicit arguments by adding a dummy explicit argument as the first parameter, like in this example:

record Monad (M : Set -> Set) : Set₁ where
  field
    bind : {A B : Set} → (A → M B) → M A → M B

    associative : (Z : Set) -> {A B C : Set} → {f : A → M B} → {g : B → M C} → bind g ∘ bind f ≡ bind (bind g ∘ f)

M : Set -> Set -> Set
M R A = (A -> R) -> R

bind : {R A B : Set} → (A → M R B) → M R A → M R B
bind f a = λ cont -> a (λ a' -> f a' cont)

associative : {R : Set} -> (Z : Set) -> {A B C : Set} → {f : A → M R B} → {g : B → M R C} → bind g ∘ bind f ≡ bind (bind g ∘ f)
associative Z = refl

ContMonad : (R : Set) -> Monad (M R)
ContMonad R = record { bind = bind; associative = associative }

I'm note sure, though, if it's necessary to eagerly apply all implicit arguments because, for example, there could be more implicit arguments in the type of the record field, or the implicit arguments could be in different orders. Although, I couldn't find a working example of something like that.

What's the actual reason for eagerly applying all implicit arguments when the required type has implicit arguments?