Arrow notation, existentials, and TcType demotion

[Alexis King]

Hello,

As I mentioned in a previous email
<https://mail.haskell.org/pipermail/ghc-devs/2021-October/020223.html>, GHC
seems currently somewhat uncertain about whether or not matching on GADTs
is permitted in arrow notation. Sam Derbyshire suggested on Twitter
<https://twitter.com/samderbyshire/status/1444705156583641099> that we
probably do, ideally speaking, want to support them. Unfortunately, I am
confident that the existing implementation is *not* up to this task, as I
have now demonstrated in issues #20469
<https://gitlab.haskell.org/ghc/ghc/-/issues/20469> and #20470
<https://gitlab.haskell.org/ghc/ghc/-/issues/20470>.

The latter of those two issues is particularly challenging to solve, as it
highlights the sorts of tricky interactions that can arise when arrow
notation is mixed with existential quantification. To give an example,
suppose we have the following datatypes:

    data A where
      A :: a -> B a -> A
    data B a where
      B :: B ()

And suppose we have the following proc expression:

    proc a -> case a of
      A x B -> id -< x

The match on the A constructor introduces a locally-scoped skolem, and even
though the use of id appears on the RHS, it is *not* actually within the
match’s scope—rather, its scope is that of the overall proc expression.

This makes it tricky to maintain typechecker invariants, as introduced
metavariables must not accidentally leak into the outer scope via these
strangely-scoped expressions. For example, when typechecking the above
expression, we’ll increment tcl_tclevel before typechecking the id -< x
command, and we may introduce fresh metavariables while doing so. This
means we may end up with an expected type for id that looks like this:

    a1[tau:1] -> a2[tau:1]

However, when we actually check id against that type, we must do so in a
context where tcl_tclevel is 0, not 1. This violates WantedInv from Note
[TcLevel invariants] in GHC.Tc.Utils.TcType. This means we need to do a
three-step process to properly check id’s type:

   1.

   Synthesize a new metavariable a3[tau:0].
   2.

   Emit [W] a3[tau:0] ~ (a1[tau:1] -> a2[tau:1]) within the arrow scope,
   i.e. where tcl_tclevel = 1.
   3.

   Check id against a3[tau:0].

Discerning readers may note that this looks *awfully* similar to the
process by which we promote a type via promoteTcType, as described in Note
[Promoting a type] in GHC.Tc.Utils.TcMType. However, in this case, we
aren’t really promoting a type, but *demoting* it—we ultimately want to
decrease its level, not increase it. However, it seems to me that the
process of doing this demotion is in fact handled perfectly fine by
promoteTcType. So my question is twofold:

   1.

   Is my reasoning about what to do here correct?
   2.

   Is there any harm in using promoteTcType to do this demotion?

Thanks,
Alexis
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211004/81dac803/attachment.html>