[GHC] #14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull)

[GHC]

#14135: PatternSynonyms regression in GHC HEAD (expectJust mkOneConFull)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  carlostome
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.3
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):  Phab:D3981
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 OK I can see what is happening here.  The trouble is with the COMPLETE
 pragma (again!).

 Suppose we'd written
 {{{
 f :: Foo a -> a
 f (Foo1 x)   = x
 f (MyFoo2 y) = y
 }}}
 This definition is rejected as ill-typed:
 {{{
 T14135.hs:13:4: error:
     * Couldn't match type `a' with `Int'
       `a' is a rigid type variable bound by
         the type signature for:
           f :: forall a. Foo a -> a
         at T14135.hs:11:1-15
       Expected type: Foo a
         Actual type: Foo Int
 }}}
 Reason: the pattern synonym `MyFoo2` demands that its scrutinee has type
 `Foo Int`.  This is unlike a GADT, whose data constructors can have a
 return type `Foo Int` but which can match a scrutinee of type `Foo a`.
 It's a conscious design choice, described in the user manual (I hope). See
 `Note [Pattern synonym result type]` in `PatSyn`.

 Now, the overlap checker, when looking for missing patterns, effectively
 adds that extra equation.  But the extra equation is ill-typed which
 crashes the overlap checker.   (So yes, I think the `tcMatchTy` is fine;
 it's relying on the scrutinee having the right type.)

 So what are we to make of `{-# COMPLETE Foo1, MyFoo2 #-}`?  The simplest
 thing to do is to insist that all the constructors in a COMPLETE pragma
 match the same type of scrutinee, where

 * A constructor `K` declared thus
 {{{
 data T a b where
   K :: ....
 }}}
   matches a scrutinee of type `T a b` (NB: NOT the return type in K's
 signature which for a GADT might be `T Int Bool`)

 * A constructor `K` declared in a `data instance`
 {{{
 data instance T ty1 ty2 where
   K :: ....
 }}}
   matches a scrutinee of type `T ty1 ty2`.  (NB: again, not the return
 type in K's signature which may an instance of `K ty1 ty2`)

 * A constructor `K` declared in a pattern synonym
 {{{
 pattern K :: .... -> T ty1 ty2
 }}}
   matches a scrutinee of type `T ty1 ty2`.

 If we did this check when dealing with the COMPLETE pragma, I think that's
 solve this crash.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14135#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler