Re: [GHC] #8968: Pattern synonyms and GADTs

8 Apr 2014

      #8968: Pattern synonyms and GADTs
----------------------------------------------+----------------------------
        Reporter:  kosmikus                   |            Owner:
            Type:  bug                        |           Status:  new
        Priority:  normal                     |        Milestone:
       Component:  Compiler (Type checker)    |          Version:
      Resolution:                             |  7.8.1-rc2
Operating System:  Unknown/Multiple           |         Keywords:
 Type of failure:  GHC rejects valid program  |     Architecture:
       Test Case:                             |  Unknown/Multiple
        Blocking:                             |       Difficulty:  Unknown
                                              |       Blocked By:
                                              |  Related Tickets:
----------------------------------------------+----------------------------
Changes (by simonpj):

 * cc: cactus, dimitris@… (added)

Comment:

 Harump.  This is a real shortcoming in the pattern-synonym stuff.
 Consider
 {{{
 data T a b where
         MkT :: a -> T a Bool
         MkX :: T a b

 pattern P = MkT True
 }}}
 What type should pattern P have?  It could be
 {{{
         P :: T Bool b
 or      P :: T b b
 }}}
 Both would work, because pattern matching on `MkT` ensures that `b~Bool`.
 But neither is more general than the other.  So GHC rejects it, with the
 (confusing) errors.
 {{{
 T8968.hs:9:17:
     Couldn't match expected type ‘t’ with actual type ‘Bool’
       ‘t’ is untouchable
         inside the constraints (t1 ~ Bool)
         bound by a pattern with constructor
                    MkT :: forall a. a -> T a Bool,
                  in a pattern synonym declaration
         at T8968.hs:9:13-20
       ‘t’ is a rigid type variable bound by
           the inferred type of P :: T t t1 at T8968.hs:1:1
     In the pattern: True
     In the pattern: MkT True

 T8968.hs:9:17:
     Could not deduce (t ~ Bool)
     from the context (t1 ~ Bool)
       bound by the type signature for T8968.$WP :: t1 ~ Bool => T t t1
       at T8968.hs:9:9
       ‘t’ is a rigid type variable bound by
           the type signature for T8968.$WP :: t1 ~ Bool => T t t1
           at T8968.hs:1:1
     Relevant bindings include $WP :: T t t1 (bound at T8968.hs:9:9)
     In the first argument of ‘MkT’, namely ‘True’
     In the expression: MkT True
 }}}
 (There are two errors, one `P` in matching and one for `P` in an
 expression.  I think we can fix that part by failing earlier.)

 This ambiguity is the cause of the error kosmikus came across, I think.
 In the !OutsideIn algorithm we insist on a type signature for functions
 like this.
 My conclusion
  * We need signatures for pattern synonyms.  Do such signatures exist yet?
  * Ideally we would find a more civilised way to reject such programs,
 perhaps suggesting a signature.

 But first, have I analysed this right. Copying Dimitrios.

 Simon

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8968#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler