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

14 Dec 2015

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

Comment (by mpickering):

 Here is the result of the trace statement `tc_patsyn_finish`.

 {{{
 tc_patsyn_finish {
   PRead
   (readMaybe -> Just a_aqs)
   ([a_a2aU[sk]], [Read a_a2aU[sk]], EvBindsVar<a2b0>, [$dRead_a2FA])
   ([], [], [], EvBinds{}, [])
   [(a_aqs, <>)]
   String
 }}}

 which is from

 {{{
         traceTc "tc_patsyn_finish {" $
            ppr (unLoc lname) $$ ppr (unLoc lpat') $$
            ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
            ppr (ex_tvs, subst, prov_theta, prov_ev_binds, prov_dicts) $$
            ppr wrapped_args $$
            ppr pat_ty
 }}}

 So here, the `a` is inferred to be *universally* quantified even though it
 doesn't appear in the result type. Which explains why adding a type
 signature which says that `a` is existentially quantified causes the
 program to fail to compile.

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