[GHC] #12975: Suggested type signature for a pattern synonym causes program to fail to type check

14 Dec 2016


      #12975: Suggested type signature for a pattern synonym causes program to fail to
type check
-------------------------------------+-------------------------------------
           Reporter:  ocharles       |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
  patternsynonyms                    |
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Take the following program:

 {{{#!hs
 {-# LANGUAGE ViewPatterns, PatternSynonyms, RankNTypes, GADTs #-}

 import Data.Typeable

 data T where
   MkT :: Typeable a => a -> T

 pattern Cast a <- MkT (cast -> Just a)
 }}}

 When compiled with `-Wall`, GHC rightly prompts about a missing signature
 on `Cast`:

 {{{
     Top-level binding with no type signature:
       Cast :: forall b. Typeable b => forall a. Typeable a => b -> T
 }}}

 However, using this suggested type signature causes the program to fail to
 type check:

 {{{#!hs
     • Could not deduce (Typeable a0)
         arising from the "provided" constraints claimed by
           the signature of ‘Cast’
       from the context: Typeable a
         bound by a pattern with constructor:
                    MkT :: forall a. Typeable a => a -> T,
                  in a pattern synonym declaration
         at ../foo.hs:9:19-38
       In other words, a successful match on the pattern
         MkT (cast -> Just a)
       does not provide the constraint (Typeable a0)
       The type variable ‘a0’ is ambiguous
     • In the declaration for pattern synonym ‘Cast’
 }}}

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12975
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler