[GHC] #9953: Pattern synonyms don't work with GADTs

2 Jan 2015

      #9953: Pattern synonyms don't work with GADTs
-------------------------------------+-------------------------------------
              Reporter:  simonpj     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:
             Component:  Compiler    |           Version:  7.8.4
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |        Blocked By:
             Test Case:              |   Related Tickets:
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 Consider this variant of test `T8968-1`:
 {{{
 {-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
 module ShouldCompile where

 data X :: * -> * where
   Y :: a -> X (Maybe a)

 pattern C :: a -> X (Maybe a)
 pattern C x = Y x

 foo :: X t -> t
 foo (C x) = Just x
 }}}
  * If we had `(Y x)` instead of `(C x)` in the LHS of `foo`, then this is
 an ordinary GADT program and typechecks fine.

  * If we omit the pattern signature, it typechecks fine, and `:info C`
 says
 {{{
 pattern C :: t ~ Maybe a => a -> X t    -- Defined in ‘ShouldCompile’
 }}}

  * But as written, it fails with
 {{{
 Foo.hs:11:6:
     Couldn't match type ‘t’ with ‘Maybe a0’
       ‘t’ is a rigid type variable bound by
           the type signature for: foo :: X t -> t at Foo.hs:10:8
     Expected type: X t
       Actual type: X (Maybe a0)
     Relevant bindings include foo :: X t -> t (bound at Foo.hs:11:1)
     In the pattern: C x
     In an equation for ‘foo’: foo (C x) = Just x
 }}}
   Moreover, `:info C` says
 {{{
 pattern C :: a -> X (Maybe a)   -- Defined at Foo.hs:8:9
 }}}

 Do you see the difference?  In the former, the "prov_theta" equality
 constraint is explicit, but in the latter it's implicit.

 The exact thing happens for `DataCons`.  It's handled via the `dcEqSpec`
 field.  Essentially `PatSyn` should have a new field for the implicit
 equality constraints.  And, just as for data consructors, we need to
 generate the equality constraints, and the existentials that are needed,
 when we process the signature.  Use the code in `TcTyClsDecls.rejigConRes`
 (perhaps needs a better name).

 This is all pretty serious. Without fixing it, GADT-style pattern
 signatures are all but useless.

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