#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