Overly eager auto implicit in GADT ctor field's type results in typechecking failure

[0xd34df00d]

Steps to Reproduce

Try typechecking

module Foo

interface SomeMonad (s : Type) (m : Type -> Type) where

data Operation : (res : Type) -> Type where
  Op : (opFun : forall s, m. SomeMonad s m => m r1) -> (cont : r1 -> Operation r2) -> Operation r2

Functor Operation where
  map f (Op opFun cont) = Op opFun (map f . cont)

Expected Behavior

Typechecks fine.

Observed Behavior

Fails with

Error: While processing right hand side of map. Can't find an implementation for SomeMonad ?s ?m.

Foo:9:30--9:35
 5 | data Operation : (res : Type) -> Type where
 6 |   Op : (opFun : forall s, m. SomeMonad s m => m r1) -> (cont : r1 -> Operation r2) -> Operation r2
 7 | 
 8 | Functor Operation where
 9 |   map f (Op opFun cont) = Op opFun (map f . cont)
                                  ^^^^^

If we replace the opFun at the rhs with a hole and look at its type, it'd be

rhs : m r1

instead of the (expected) SomeMonad s m => m r1, so surely it fails to find the implementation.

Note 1: removing s from both SomeMonad definition and from forall in the Op definition makes it compile, albeit the hole type is still funny and lacks the SomeMonad m => constraint.

Note 2: adding a dummy argument like

data Operation : (res : Type) -> Type where
  Op : (opFun : () -> forall s, m. SomeMonad s m => m r1) -> (cont : r1 -> Operation r2) -> Operation r2

also makes things compile.