[GHC] #13158: Pattern synonyms should use type annotation information when typechecking

[GHC]

#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