[GHC] #14395: Redefining pattern synonym in GHCi triggers "‘p’ is untouchable" error

27 Oct 2017

      #14395: Redefining pattern synonym in GHCi triggers "‘p’ is untouchable" error
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.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:
-------------------------------------+-------------------------------------
 Load this file into GHCi:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 module Bug where

 data Foo a where
   FooInt :: Foo Int

 pattern Bar :: () => (a ~ Int) => Foo a
 pattern Bar = FooInt
 }}}

 And attempt to redefine `Bar` as follows:

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )
 Ok, 1 module loaded.
 λ> pattern Bar = Nothing

 <interactive>:1:15: error:
     • Couldn't match expected type ‘p’ with actual type ‘Maybe a0’
         ‘p’ is untouchable
           inside the constraints: a ~ Int
           bound by a pattern with pattern synonym:
                      Bar :: forall a. () => a ~ Int => Foo a,
                    in an equation for ‘pattern’
           at <interactive>:1:9-11
       ‘p’ is a rigid type variable bound by
         the inferred type of pattern :: Foo a -> p at <interactive>:1:1-21
       Possible fix: add a type signature for ‘pattern’
     • In the expression: Nothing
       In an equation for ‘pattern’: pattern Bar = Nothing
     • Relevant bindings include
         pattern :: Foo a -> p (bound at <interactive>:1:1)
 }}}

 There are two issues here:

 1. There are several places in the error message that refer to a `pattern`
 with no name!

 {{{
                    in an equation for ‘pattern’
 }}}
 {{{
         the inferred type of pattern :: Foo a -> p at <interactive>:1:1-21
 }}}
 {{{
     • Relevant bindings include
         pattern :: Foo a -> p (bound at <interactive>:1:1)
 }}}

 2. Why is this error happening in the first place? The error message
 mentions the type `Foo a -> p`, but in `pattern Bar = Nothing`, there
 isn't anything that should touch `Foo`.

 Note that this bug does not occur if a slightly different (but ostensibly
 equivalent) type signature for `Bar` is given in the original source file:

 {{{#!hs
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 module Works where

 data Foo a where
   FooInt :: Foo Int

 pattern Bar :: Foo Int
 pattern Bar = FooInt
 }}}
 {{{
 λ> pattern Bar = Nothing
 λ> :i Bar
 pattern Bar :: Foo Int
 }}}

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