Hello,

As I mentioned in a previous email, GHC seems currently somewhat uncertain about whether or not matching on GADTs is permitted in arrow notation. Sam Derbyshire suggested on Twitter 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 and #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