#13159: Allow visible type application with pattern synonyms in patterns -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #13158 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Somewhat related to #13158, it would be nice if pattern synonyms allowed visible type application with the `TypeApplications` extension enabled. This would obviously be tricky due to the existing meaning of `@` in patterns, though I think it would technically be unambiguous here. Still, I’d understand if you didn’t want to complicate the parser that much further. The motivator, though, is that it would be nice to be able to write pattern synonyms with ambiguous types an explicitly instantiate them, for the same reason type applications are useful for terms. As mentioned in #13158, this would permit writing a pattern synonym to emulate case analysis on types: {{{#!hs {-# LANGUAGE GADTs, PatternSynonyms, ScopedTypeVariables, TypeApplications, TypeOperators, ViewPatterns #-} import Data.Typeable viewEqT :: forall b a. (Typeable a, Typeable b) => a -> Maybe ((a :~: b), b) viewEqT x = case eqT @a @b of Just Refl -> Just (Refl, x) Nothing -> Nothing pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a pattern EqT x <- (viewEqT @b -> Just (Refl, x)) }}} If visible type applications were permitted in patterns, then such case analysis could be written like this: {{{#!hs evilId :: Typeable a => a -> a evilId (EqT @Int n) = n + 1 evilId (EqT @String str) = reverse str evilId x = x }}} …which I think looks relatively pleasant! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13159 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler