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

changed weight to 5

added Ttask Trac import labels

Also applies here maybe,

greet :: (?name :: String) => String
greet = "hi " ++ ?name

-- t1QY.hs:12:4-8: error: Parse error in pattern: ?name
-- Compilation failed.
a :: String
a = greet where
  (?name, False) = ("Iceland_jack", True)

mentioned in issue #15456 (closed)

closed

(Copying the resolution from #15456 (closed), which is a duplicate of this ticket.)

This is a worthwhile idea to consider, but it should really go via the ​https://github.com/ghc-proposals/ghc-proposals process, as it's a user-facing language change.

I'm closing this ticket as invalid, but I really do encourage you to post a proposal. That process is working well and has incorporated quite a few changes into the language.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedInvalid
Related	- → #15456 (closed)

added ImplicitParams label

added Pnormal label