Advice for implementing GADTs?

[Simon Peyton Jones]

>
> 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.redelings at 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220816/12264612/attachment.html>