#13158: Pattern synonyms should use type annotation information when typechecking -------------------------------------+------------------------------------- Reporter: lexi.lambda | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- With a small boatload of GHC extensions, I can write a view pattern with `Data.Typeable` that will simulate something like 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 evilId :: Typeable a => a -> a evilId (viewEqT @Int -> Just (Refl, n)) = n + 1 evilId (viewEqT @String -> Just (Refl, str)) = reverse str evilId x = x }}} However, this is ugly. I would like to clean things up with a nice pattern synonym: {{{#!hs pattern EqT :: forall b a. (Typeable a, Typeable b) => (a ~ b) => b -> a pattern EqT x <- (viewEqT @b -> Just (Refl, x)) }}} Sadly, while this pattern typechecks, using it seems to be impossible. This program is rejected: {{{#!hs evilId :: Typeable a => a -> a evilId (EqT (n :: Int)) = n + 1 evilId (EqT (str :: String)) = reverse str evilId x = x }}} Specifically, it produces the following type error: {{{ /private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:9: error: • Could not deduce (Typeable b0) arising from a pattern from the context: Typeable a bound by the type signature for: evilId :: Typeable a => a -> a at library/TypeEqTest.hs:16:1-30 The type variable ‘b0’ is ambiguous • In the pattern: EqT (n :: Int) In an equation for ‘evilId’: evilId (EqT (n :: Int)) = n + 1 /private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:17:14: error: • Could not deduce: a ~ Int from the context: a ~ b0 bound by a pattern with pattern synonym: EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a, in an equation for ‘evilId’ at library/TypeEqTest.hs:17:9-22 ‘a’ is a rigid type variable bound by the type signature for: evilId :: forall a. Typeable a => a -> a at library/TypeEqTest.hs:16:11 Expected type: Int Actual type: b0 • When checking that the pattern signature: Int fits the type of its context: b0 In the pattern: n :: Int In the pattern: EqT (n :: Int) • Relevant bindings include evilId :: a -> a (bound at library/TypeEqTest.hs:17:1) /private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:9: error: • Could not deduce (Typeable b1) arising from a pattern from the context: Typeable a bound by the type signature for: evilId :: Typeable a => a -> a at library/TypeEqTest.hs:16:1-30 The type variable ‘b1’ is ambiguous • In the pattern: EqT (str :: String) In an equation for ‘evilId’: evilId (EqT (str :: String)) = reverse str /private/tmp/wild-patterns-sandbox/library/TypeEqTest.hs:18:14: error: • Could not deduce: a ~ String from the context: a ~ b1 bound by a pattern with pattern synonym: EqT :: forall b a. (Typeable a, Typeable b) => a ~ b => b -> a, in an equation for ‘evilId’ at library/TypeEqTest.hs:18:9-27 ‘a’ is a rigid type variable bound by the type signature for: evilId :: forall a. Typeable a => a -> a at library/TypeEqTest.hs:16:11 Expected type: String Actual type: b1 • When checking that the pattern signature: String fits the type of its context: b1 In the pattern: str :: String In the pattern: EqT (str :: String) • Relevant bindings include evilId :: a -> a (bound at library/TypeEqTest.hs:17:1) }}} I would expect the program to typecheck, since in any other context, GHC would not have any trouble inferring the type of `b` for each use of `EqT`. However, it seems that pattern synonyms do not allow me to provide any type information “in”, only get type information “out”. Is there some fundamental limitation that forces this to be the case, or is this just a missing feature? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13158 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler