No pattern match on `(fun A => (B, f A)) m` with `(x, y)`

Stream: general

[nrs]

structure Functor' where
  obj : Type -> Type
  mor : (α β : Type) -> (α -> β) -> obj α -> obj β


structure Container where
  S : Type
  P : S -> Type

def proj : Container -> Functor'
  | ⟨S, P⟩ => {
    obj := fun α => (s : S) × (P s -> α)
    mor := fun m => fun s f => fun | (a,b) => _
    }

The above gives me the following error:

type mismatch
  (a, b)
has type
  ?m.797 × ?m.800 : Type (max ?u.803 ?u.802)
but is expected to have type
  (fun α => (s : S) × (P s → α)) m : Type

How come? I'd expect the application of (fun α => (s : S) × (P s → α)) to m to produce a product type, so it should be possible to match on it with a pair, right?

[nrs]

ah just realized as I posted this, you have to use Sigma.mk to pattern match here given the fact that it's a dependent pair (or use it anonymously with \< \>

[Mario Carneiro]

yes, the (x, y) syntax only works to produce Prod.mk i.e. nondependent pairs