Bind implicit parameter in patterns

Is there any reason why variables for ImplicitParams can't be bound in patterns, so you can write

data Exp = Val Int | Op Op Exp Exp

data Op = Add | Mul

data Protect where
  Protect :: (?op :: Op) => Protect

protectOp :: Exp -> Maybe Protect
protectOp (Op ?op _ _) = Just Protect
protectOp _            = Nothing

instead of

protectOp :: Exp -> Maybe Protect
protectOp (Op op _ _) = Just Protect where ?op = op
protectOp _           = Nothing

Trac metadata

Trac field	Value
Version	8.0.1
Type	Task
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture