> > 3.1: OK, so if the case branch introduces type-class constraints, but not > equality constraints, then the unification variables from an outer level > are still touchable? Presumably because the type-class constraints don't > interact with the equality constraints? >
Yes, but the check is a bit conservative. Look at `inert_given_eqs` in `InertCans`, and `updateGivenEqs`. * implication constraints like (a ~ Int ==> a ~ Int) are never created. > I may be assuming that GHC runs the solver for each GADT pattern match > before creating implication constraints. > That's not right. They can be created, but then get solved, by solving the Wanted from the Given. 3.3: Also, is there a standard way to pretty-print implication > constraints? The OutsideIn paper uses LaTeX \supset I think, but there > isn't an obvious ASCII character to use to for \supset... > Well there is a `Outputable` instance. It uses `=>`. Simon On Mon, 15 Aug 2022 at 20:00, Benjamin Redelings < benjamin.redeli...@gmail.com> wrote: > Thanks a bunch for this! > On 8/4/22 3:45 PM, Simon Peyton Jones wrote: > > QUESTION 1: Are there any obviously important resources that I've > overlooked? > That's a good list. Ningning's thesis https://xnning.github.io/ is also > good stuff. > > Thanks! > > > QUESTION 2: if my quick scan is correct, none of the papers mention the > GHC technique of determining untouchability by assigning "levels" to type > variables. Is there any written paper (outside the GHC sources) that > discusses type levels? > It is disgracefully undocumented, I'm afraid. Sorry. Didier Remy used > similar ideas, in some INRIA papers I think. > > OK, that was my impression, just checking. I think I get the basic idea... > > > QUESTION 3: My impression is that: > > (a) type variable levels were introduced in order to clarify which > MetaTyVars are "untouchable", but > > (b) levels now also check that type variables do not escape their > quantification scope. > > (c) levels can also be used to figure out which variables are free in the > type environment, and therefore should not be generalized over. > > Does this sound right? I suspect that I might be wrong about the last > one... > > > Correct about all three. > > Good to know! > > Except that a unification variable is only untouchable if it comes from an > outer level *and* there are some intervening Given equalities. If there > are no equalities it's not untouchable. E.b. > f = \x -> case x of > Just y -> 3::Int > > Here the (3::Int) can affect the result type of the function because the > Just pattern match does not bind any Given equalities (in a GADT like way). > > 3.1: OK, so if the case branch introduces type-class constraints, but not > equality constraints, then the unification variables from an outer level > are still touchable? Presumably because the type-class constraints don't > interact with the equality constraints? > > 3.2: The OutsideIn paper talks about creating implication constraints, > which then bubble UP to the level where the solver is applied. Maybe only > at the outermost level? > > However, it sounds like GHC pushes given constraints from a GADT pattern > match DOWN into the case branch. Implication constraints would only be > created if the wanted constraints bubble up to a GADT pattern match, and > are not entailed by the givens. So > > * implication constraints like (a ~ Int ==> a ~ Int) are never created. > > * however, implication constraints like (a ~ Int ==> b ~ Int) could be > created. > > I may be assuming that GHC runs the solver for each GADT pattern match > before creating implication constraints. > > Does that sound right? > > 3.3: Also, is there a standard way to pretty-print implication > constraints? The OutsideIn paper uses LaTeX \supset I think, but there > isn't an obvious ASCII character to use to for \supset... > > > I keep meaning to write an updated version of Practical type inference > for arbitrary rank types > <https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/>, > but failing to get around to it! > > That would be great, if you find the time! Are you thinking of adding > practical steps for handling equality constraints to it? Or, removing the > deep-subsumption language? Or something else? It has already been quite > helpful. > > -BenRI > >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
