[GHC] #11224: Program doesn't preserve semantics after pattern synonym inlining.

[GHC]

#11224: Program doesn't preserve semantics after pattern synonym inlining.
-------------------------------------+-------------------------------------
        Reporter:  anton.dubovik     |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
Operating System:  Windows           |         Architecture:  x86_64
 Type of failure:  Incorrect result  |  (amd64)
  at runtime                         |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11225            |  Differential Rev(s):  Phab:D1632
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Right.  To typecheck a program involving `P` we absolutely need to know
 the universal/existential split.

 Above, I was thinking that we could use the pattern type signature to
 specify the "shape" of the type, but work out the univ/existential split
 from the definition itself.  A bit like a type with wildcards.  But that
 would mean that you could not typecheck uses of a  pattern synonym solely
 from its signature; because the signature does not say enough.  Like
 wildcards, inference would be involved.  But that's obviously
 unsatisfactory; for example, you could not put a pattern synonym signature
 in a hs-boot file.

 So, if we want signatures to be fully precise (i.e. say everything), and I
 think that is a solidly good goal, we'd need to require the user to
 specify the required/provided split for type variables too.

 Terminology:
  * "Universal" for type variables lines up with "required" for the
 constraints
  * "Existential" for type variables lines up with "provided" for the
 constraints

 Now, we need syntax for expressing the split.  I suppose we can use the
 same nested structure as we do for required/provided, like this:
 {{{
 pattern type P1 :: forall a. a -> T a        -- a is universal

 pattern type P2 :: forall a. Eq a => a -> T  -- a is universal, (Eq a) is
 required

 pattern type P3 :: forall a. Eq a =>         -- a is universal, (Eq a) is
 required
                    forall b. a -> b -> T a   -- b is existential

 pattern type P3 :: forall a. Eq a =>         -- a is universal, (Eq a) is
 required
                    forall b. Ord b =>        -- b is existential, (Ord b)
 is provided
                    a -> b -> T a
 }}}
 Note:

  * I think we could safely leave out the leading (universal) `forall`, in
 the usual way.  That is, the free vars of the entire type are considered
 universal.

  * You can never leave out the existential forall, if it binds any
 variables.

  * How can you distinguish the existential forall if the universal forall
 and context are absent?  Only by putting in the universal forall or the
 required context; e.g.
 {{{
 pattern type P5 :: forall. forall b. b -> T
 pattern type P6 :: () => forall b. b -> T
 }}}
 The only downside of this is that you might say that given
 {{{
 pattern type P :: a -> (a->Int) -> T
 }}}
 the `a` is almost certain to be existential.  After all this is
 the type we'd give to a data constructor:
 {{{
 data T where
   MkT :: (a->Int) -> a -> T
 }}}
 So why do we need explicitly-specified existentials in a pattern
 synonym, but not in a data constructor?  Because a view pattern
 could make it universal.  Degenerately in this case:
 {{{
 pattern Q :: a -> (a->Int) -> String
 pattern Q x y <- (odd_fun -> (x,y))

 odd_fun :: String -> (a, a->Int)
 odd_fun _ = (undefined, const 2)
 }}}

 Conclusion: we need the possibility of explicitly-specified existentials.

 However, rather than insisting that you always specify the
 existential forall, here is a rule that would catch the common cases:
 if you don't specify the existential `forall`, you get:
   * the free vars of the arg-tys
   * plus the free vars of the provided constraints (if any),
   * minus
     * the universal forall'd vars, if there is a universal `forall`
     * or the free vars of the result ty, plus required constraints (if
 any), otherwise

 If neither `forall` is given, we compute the existential variables using
 the above rule; then the universals are the remaining free variables.

 So in the signatures that started this ticket
 {{{
 pattern Q1 :: () => Read a => a -> String
 pattern Q2 :: Read a => a -> String
 }}}
 would behave as if you had written
 {{{
 pattern Q1 :: () => forall a. Read a => a -> String
 pattern Q2 :: forall a. Read a => a -> String
 }}}
 The advantage of this rule is that is allows you to omit
 both `forall`s in all but the most degenerate cases like `Q` above.

 How does that sound?  I think it is more or less what Richard was
 proposing in comment:8, but it's taken me a while to catch up.

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