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