[GHC] #15009: Float equalities past local equalities

[GHC]

#15009: Float equalities past local equalities
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  closed
        Priority:  normal            |            Milestone:  8.4.3
       Component:  Compiler          |              Version:  8.2.2
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  gadt/T15009
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by nfrisby):

 Replying to [comment:11 simonpj]:
 > I think you are referring to `Note [Let-bound skolems]` in `TcSMonad`?

 Yep, that's the most relevant Note.

 > ...

 Snipped. (Should it have been "When doing inference on {{{h}}} we'll
 assign {{{z :: alpha[1]}}}"? Since {{{y}}} is already "declared" {{{::
 a}}} from the {{{g}}} signature.)

 > Does that help explain? I could add this to the Note.

 Yes, that explanation does help. I'm ruminating now about how it compares
 to the main jfp-OutsideIn narrative eg so I can better suggest how to
 update the Note.

 Beyond the Note, though, my comment above was asking how feasible it is
 for the following example to work. My intuition (which I'm working to
 unpack) thinks it should. But 1) am I wrong? and 2) how much work to have
 GHC accept it?

 {{{
 data S a where MkS :: (a ~ Int) => S a   -- from your 2nd example

 data Query f b = MkQuery (forall q. f q -> q -> b)   -- a new ingredient

 g3 :: Query S Int   -- GHC 8.6 cannot infer this type. Should a later GHC?
 g3 = MkQuery (\MkS x -> x)
 }}}

 I'm trying to decode my intuition for what exactly is it about {{{g3}}}
 (contrasted with your {{{g}}}) that should justify unifying{{{beta :=
 Int}}} in this case. For example, if we define {{{QueryS}}} as a manual
 specialization of {{{Query}}} with {{{f = S}}}, then your previous commit
 for this ticket works for {{{g2}}} below.

 {{{
 data QueryS b where MkQueryS :: (a ~ Int) => (a -> b) -> QueryS b

 to :: Query S b -> QueryS b
 to (MkQuery f) = MkQueryS (f MkS)
 from :: QueryS b -> Query S b
 from (MkQueryS f) = MkQuery (\MkS -> f)

 g2 = MkQueryS (\x -> x)   -- GHC 8.6 infers QueryS Int
 }}}

 This isomorphism and inference for {{{g2}}} reassures me that my hope for
 {{{g3}}} is at least within the realm of possibility.

 In {{{g3}}} there is nothing between the implicit type lambda binding
 {{{q}}} and the pattern match on {{{MkS}}}. So I think we end up with
 nested implications with nothing in between. (I'm very doubtful that I
 have the level numbers correct here.)

 {{{
 forall[2] a. -- from the type lambda
   forall[3] . (a ~ Int) =>  -- from the MkS pattern
     (a ~ alpha[2],a ~ beta[1])
 }}}

 Perhaps my optimistic intuition for {{{g3}}} is because the outer
 implication here is so trivial: {{{alpha}}} and {{{beta}}} do not occur in
 (any other equality-like constraints in) any siblings of our inner
 implication, so floating {{{alpha ~ beta}}} wouldn't have any
 consequences. Is that suggestive of some refinement to eg
 {{{getNoGivenEqs}}} or am I lost in the weeds? Thank you for your
 patience. -Nick

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