- ghc-devs - Haskell.org

To allow deriving poly-kinded Generic1 instances
by Fumiaki Kinoshita 12 Oct '21

12 Oct '21

I was hacking GHC to see if it's able to derive Generic1 instance for datatypes with kind (Type -> Type) -> Type by omitting some checks. I noticed that the type parameter is substituted by GHC.Types.Any, preventing higher-kinded instances from typechecking. I found a comment implying that this is intentional; in GHC.Tc.Deriv.Generic.hs:977, Alternatively, we could have avoided this problem by expanding all type synonyms on the RHSes of Rep1 instances. But we might blow up the size of these types even further by doing this, so we choose not to do so. It wasn't obvious to me if binding a parameter in the type synonym instance declaration of Rep1 cause problems, because that's what I'd do if I were to define an instance by hand. Is there any offending example? I'm also trying to make such change myself (it doesn't add a type parameter and I'm not sure why) https://gitlab.haskell.org/fumieval/ghc/-/commit/bfe7766af80d90590b6b032d18…

1 0

help validating a modified compiler?
by Norman Ramsey 12 Oct '21

12 Oct '21

I've made a minor change to GHC, and before submitting a PR, I'd like to validate the change. But I don't really know how to interpret the output of the `validate` script. Mine runs for about 40 minutes and then ends in an error: # We are installing wrappers to programs by searching corresponding # wrappers. If wrapper is not found, we are attaching the common wrapper # to it. This implementation is a bit hacky and depends on consistency # of program names. For hadrian build this will work as programs have a # consistent naming procedure. if [ -L wrappers/ghc ]; then echo "ghc is a symlink"; fi ghc is a symlink cp: target 'dir/bin/ghc' is not a directory make: *** [Makefile:197: install_wrappers] Error 1 ________________________________________________________ Executed in 39.60 mins fish external usr time 146.65 mins 0.00 millis 146.65 mins sys time 9.55 mins 1.60 millis 9.55 mins I'm in the process of trying `validate` on a fresh checkout, but at 40 minutes per shot, I feel like I might be on the wrong track. Should I just create a merge request and rely on CI for the validation? Or do something else? Norman

3 3

-O* does more than what's in optLevelFlags?
by Erdi, Gergo 11 Oct '21

11 Oct '21

PUBLIC What is set by -O* that is not included in optLevelFlags? I would have thought that setting all the flags implied by, e.g., -O1, would be the same as setting -O1 itself. But this is not the case! Here are all the flags for O1 from optLevelFlags: Opt_DoLambdaEtaExpansion Opt_DoEtaReduction Opt_LlvmTBAA Opt_CallArity Opt_Exitification Opt_CaseMerge Opt_CaseFolding Opt_CmmElimCommonBlocks Opt_CmmSink Opt_CmmStaticPred Opt_CSE Opt_StgCSE Opt_EnableRewriteRules Opt_FloatIn Opt_FullLaziness Opt_IgnoreAsserts Opt_Loopification Opt_CfgBlocklayout Opt_Specialise Opt_CrossModuleSpecialise Opt_InlineGenerics Opt_Strictness Opt_UnboxSmallStrictFields Opt_CprAnal Opt_WorkerWrapper Opt_SolveConstantDicts Opt_NumConstantFolding And here are the ones that are set by O0 (the default) but not by O1: Opt_IgnoreInterfacePragmas Opt_OmitInterfacePragmas So I expected that the following two invocations of GHC would be equivalent: 1. ghc -O1 2. ghc -fdo-lambda-eta-expansion -fdo-eta-reduction -fllvm-tbaa -fcall-arity -fexitification -fcase-merge -fcase-folding -fcmm-elim-common-blocks -fcmm-sink -fcmm-static-pred -fcse -fstg-cse -fenable-rewrite-rules -ffloat-in -ffull-laziness -fignore-asserts -floopification -fblock-layout-cfg -fspecialise -fcross-module-specialise -finline-generics -fstrictness -funbox-small-strict-fields -fcpr-anal -fworker-wrapper -fsolve-constant-dicts -fnum-constant-folding -fno-ignore-interface-pragmas -fno-omit-interface-pragmas However, just by observing the output of -dshow-passes, I can see that while -O1 applies all these optimizations, the second version does NOT, even though I have turned on each and every one of them one by one. Looking at compiler/GHC/Driver/Session.hs, it is not at all clear that -O* should do more than just setting the flags from optLevelFlags. What other flags are implied by -O*? This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at https: //www.sc.com/en/our-locations Where you have a Financial Markets relationship with Standard Chartered PLC, Standard Chartered Bank and their subsidiaries (the "Group"), information on the regulatory standards we adhere to and how it may affect you can be found in our Regulatory Compliance Statement at https: //www.sc.com/rcs/ and Regulatory Compliance Disclosures at http: //www.sc.com/rcs/fm Insofar as this communication is not sent by the Global Research team and contains any market commentary, the market commentary has been prepared by the sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied on for any other purpose and is subject to the relevant disclaimers available at https: //www.sc.com/en/regulatory-disclosures/#market-disclaimer. Insofar as this communication is sent by the Global Research team and contains any research materials prepared by members of the team, the research material is for information purpose only and shall not be relied on for any other purpose, and is subject to the relevant disclaimers available at https: //research.sc.com/research/api/application/static/terms-and-conditions. Insofar as this e-mail contains the term sheet for a proposed transaction, by responding affirmatively to this e-mail, you agree that you have understood the terms and conditions in the attached term sheet and evaluated the merits and risks of the transaction. We may at times also request you to sign the term sheet to acknowledge the same. Please visit https: //www.sc.com/en/regulatory-disclosures/dodd-frank/ for important information with respect to derivative products.

3 6

Specialisation doesn't kick in (RE: Instantiation of overloaded definition *in Core*)
by Erdi, Gergo 11 Oct '21

11 Oct '21

PUBLIC PUBLIC Hi, Thanks! Originally I was going to reply to this saying that my transformation isn't running in CoreM so where do I get that environment from, but then I realized I can just build it from the md_insts field of ModDetails. However, after thinking more about it, I also realized that I shouldn't ever really need to conjure up dictionaries from thin air: the whole reason I am making a specific specialization of an overloaded function is because I found somewhere a call at that type. But then, that call also gives me the dictionary! Of course at this point, this sounds exactly like what GHC already does in `specProgram`. So maybe I should be able to just use that? Unfortunately, my initial testing seems to show that even if I run `specBind` manually on my whole-program collected CoreProgram, it doesn't do the work I would expect from it! In the following example, I have only kept the definitions that are relevant. Before specialisation, I have the following whole-program Core: (>>=) :: forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b [GblId[ClassOp], Arity=1, Caf=NoCafRefs, Str=<S(LSL),U(A,U,A)>] (>>=) = \ (@(m :: * -> *)) (v_sGm [Occ=Once1!] :: Monad m) -> case v_sGm of { C:Monad _ [Occ=Dead] v_sGp [Occ=Once1] _ [Occ=Dead] -> v_sGp } $dm>> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b [GblId, Arity=3, Unf=OtherCon []] $dm>> = \ (@(m :: * -> *)) ($dMonad [Occ=Once1] :: Monad m) (@a) (@b) (ma [Occ=Once1] :: m a) (mb [Occ=OnceL1] :: m b) -> let { sat_sGQ [Occ=Once1] :: a -> m b [LclId] sat_sGQ = \ _ [Occ=Dead] -> mb } in >>= @m $dMonad @a @b ma sat_sGQ C:Monad [InlPrag=NOUSERINLINE CONLIKE] :: forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> Monad m [GblId[DataCon], Arity=3, Caf=NoCafRefs, Cpr=m1, Unf=OtherCon []] C:Monad = \ (@(m :: * -> *)) (eta_B0 [Occ=Once1] :: Applicative m) (eta_B1 [Occ=Once1] :: forall a b. m a -> (a -> m b) -> m b) (eta_B2 [Occ=Once1] :: forall a b. m a -> m b -> m b) -> C:Monad @m eta_B0 eta_B1 eta_B2 $fMonadIO [InlPrag=NOUSERINLINE CONLIKE] :: Monad IO [GblId[DFunId]] $fMonadIO = C:Monad @IO $fApplicativeIO bindIO $fMonadIO_$c>>; $fMonadIO_$c>> [Occ=LoopBreaker] :: forall a b. IO a -> IO b -> IO b [GblId] $fMonadIO_$c>> = \ (@a) (@b) -> $dm>> @IO $fMonadIO @a @b; sat_sHr :: IO () [LclId] sat_sHr = returnIO @() () sat_sHq :: IO () [LclId] sat_sHq = returnIO @() () main :: IO () [GblId] main = $fMonadIO_$c>> @() @() sat_sHq sat_sHr Now I pass this to GHC's `specBind`, but the output is exactly the same as the input! (or it's close enough that I can't spot the difference). (>>=) :: forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b [GblId[ClassOp], Arity=1, Caf=NoCafRefs, Str=<S(LSL),U(A,U,A)>] (>>=) = \ (@(m :: * -> *)) (v_sGm [Occ=Once1!] :: Monad m) -> case v_sGm of { C:Monad _ [Occ=Dead] v_sGp [Occ=Once1] _ [Occ=Dead] -> v_sGp } $dm>> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b [GblId, Arity=3, Unf=OtherCon []] $dm>> = \ (@(m :: * -> *)) ($dMonad [Occ=Once1] :: Monad m) (@a) (@b) (ma [Occ=Once1] :: m a) (mb [Occ=OnceL1] :: m b) -> let { sat_MHt [Occ=Once1] :: a -> m b [LclId] sat_MHt = \ _ [Occ=Dead] -> mb } in >>= @m $dMonad @a @b ma sat_MHt C:Monad [InlPrag=NOUSERINLINE CONLIKE] :: forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> Monad m [GblId[DataCon], Arity=3, Caf=NoCafRefs, Cpr=m1, Unf=OtherCon []] C:Monad = \ (@(m :: * -> *)) (eta_B0 [Occ=Once1] :: Applicative m) (eta_B1 [Occ=Once1] :: forall a b. m a -> (a -> m b) -> m b) (eta_B2 [Occ=Once1] :: forall a b. m a -> m b -> m b) -> C:Monad @m eta_B0 eta_B1 eta_B2 $fMonadIO [InlPrag=NOUSERINLINE CONLIKE] :: Monad IO [GblId[DFunId]] $fMonadIO = C:Monad @IO $fApplicativeIO bindIO $fMonadIO_$c>>; $fMonadIO_$c>> [Occ=LoopBreaker] :: forall a b. IO a -> IO b -> IO b [GblId] $fMonadIO_$c>> = \ (@a) (@b) -> $dm>> @IO $fMonadIO @a @b; sat_sHr :: IO () [LclId] sat_sHr = returnIO @() () sat_sHq :: IO () [LclId] sat_sHq = returnIO @() () main :: IO () [GblId] main = $fMonadIO_$c>> @() @() sat_sHq sat_sHr Why is that? I would have expected that the call chain main >-> $fMonadIO_$c>> >-> $dm>> would have resulted in a specialization along the lines of: $dm>>_IO :: forall a b. IO a -> IO b -> IO b >>=_IO :: forall a b. IO a -> (a -> IO b) -> IO b With appropriate definitions that can then be simplified away. But none of this seems to happen -- $dm>> doesn't get an IO-specific version, and so $fMonadIO_$c>> still ends up with a dictionary-passing call to $dm>>. Isn't this exactly the situation that the specialiser is supposed to eliminate? Thanks, Gergo From: Simon Peyton Jones <simonpj(a)microsoft.com> Sent: Monday, October 4, 2021 7:29 PM To: Erdi, Gergo <Gergo.Erdi(a)sc.com> Cc: Montelatici, Raphael Laurent <Raphael.Montelatici(a)sc.com>; GHC <ghc-devs(a)haskell.org> Subject: [External] RE: Instantiation of overloaded definition *in Core* PUBLIC You can look it up in the class instance environment, which the Simplifier does have access to it. That's relatively easy when you have a simple dictionary like (Monad IO). But if you want (Eq [Int]) you first of all have to look up the (Eq [a]) dictionary, then the Eq Int dictionary, and apply the former to the latter. We don't (yet) have a simple API to do that, although it would not be hard to create one. Simon PS: I am leaving Microsoft at the end of November 2021, at which point simonpj(a)microsoft.com<mailto:simonpj@microsoft.com> will cease to work. Use simon.peytonjones(a)gmail.com<mailto:simon.peytonjones@gmail.com> instead. (For now, it just forwards to simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>.) From: ghc-devs <ghc-devs-bounces(a)haskell.org<mailto:ghc-devs-bounces@haskell.org>> On Behalf Of Erdi, Gergo via ghc-devs Sent: 04 October 2021 10:30 To: 'GHC' <ghc-devs(a)haskell.org<mailto:ghc-devs@haskell.org>> Cc: Montelatici, Raphael Laurent <Raphael.Montelatici(a)sc.com<mailto:Raphael.Montelatici@sc.com>> Subject: Instantiation of overloaded definition *in Core* PUBLIC Hi, I'd like to instantiate Core definitions. For example, suppose I have the following Core definition: foo :: forall m a b. Monad m => m a -> m b -> m b foo = \ @m ($d :: Monad m) @a @b (ma :: m a) (mb :: m b) -> ... Now let's say I'd like to instantiate it for m ~ IO. It is quite straightforward to go from the above to: foo_IO_0 :: forall a b. Monad IO => IO a -> IO b -> IO b foo_IO_0 = \ ($d :: Monad IO) @a @b (ma :: IO a) (mb :: IO b) -> ... However, I would like to go all the way to: foo_IO :: forall a b. IO a -> IO b -> IO b foo_IO = \ @a @b (ma :: IO a) (mb :: IO b) -> ... Because instances are coherent, it should be sound to replace all occurrences of $d with "the" dictionary for Monad IO. However, the places I've found for this kind of query seem to live in the typechecker. How do I access this information while working with Core? Thanks, Gergo This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at https: //www.sc.com/en/our-locations Where you have a Financial Markets relationship with Standard Chartered PLC, Standard Chartered Bank and their subsidiaries (the "Group"), information on the regulatory standards we adhere to and how it may affect you can be found in our Regulatory Compliance Statement at https: //www.sc.com/rcs/ and Regulatory Compliance Disclosures at http: //www.sc.com/rcs/fm Insofar as this communication is not sent by the Global Research team and contains any market commentary, the market commentary has been prepared by the sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied on for any other purpose and is subject to the relevant disclaimers available at https: //www.sc.com/en/regulatory-disclosures/#market-disclaimer. Insofar as this communication is sent by the Global Research team and contains any research materials prepared by members of the team, the research material is for information purpose only and shall not be relied on for any other purpose, and is subject to the relevant disclaimers available at https: //research.sc.com/research/api/application/static/terms-and-conditions. Insofar as this e-mail contains the term sheet for a proposed transaction, by responding affirmatively to this e-mail, you agree that you have understood the terms and conditions in the attached term sheet and evaluated the merits and risks of the transaction. We may at times also request you to sign the term sheet to acknowledge the same. Please visit https: //www.sc.com/en/regulatory-disclosures/dodd-frank/ for important information with respect to derivative products.

3 6

Why can't arguments be levity polymorphic for inline functions?
by Clinton Mead 09 Oct '21

09 Oct '21

Hi All Not sure if this belongs in ghc-users or ghc-devs, but it seemed devy enough to put it here. Section 6.4.12.1 <https://downloads.haskell.org/~ghc/9.0.1/docs/html/users_guide/exts/levity_…> of the GHC user manual points out, if we allowed levity polymorphic arguments, then we would have no way to compile these functions, because the code required for different levites is different. However, if such a function is {-# INLINE #-} or {-# INLINABLE #-} there's no need to compile it as it's full definition is in the interface file. Callers can just compile it themselves with the levity they require. Indeed callers of inline functions already compile their own versions even without levity polymorphism (for example, presumably inlining function calls that are known at compile time). The only sticking point to this that I could find was that GHC will only inline the function if it is fully applied <https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/pragmas.…>, which suggests that the possibility of partial application means we can't inline and hence need a compiled version of the code. But this seems like a silly restriction, as we have the full RHS of the definition in the interface file. The caller can easily create and compile it's own partially applied version. It should be able to do this regardless of levity. It seems to me we're okay as long as the following three things aren't true simultaneously: 1. Blah has levity polymorphic arguments 2. Blah is exported 3. Blah is not inline If a function "Blah" is not exported, we shouldn't care about levity polymorphic arguments, because we have it's RHS on hand in the current module and compile it as appropriate. And if it's inline, we're exposing it's full RHS to other callers so we're still fine also. Only when these three conditions combine should we give an error, say like: "Blah has levity polymorphic arguments, is exported, and is not inline. Please either remove levity polymorphic arguments, not export it or add an {-# INLINE #-} or {-# INLINABLE #-} pragma. I presume however there are some added complications that I don't understand, and I'm very interested in what they are as I presume they'll be quite interesting. Thanks, Clinton

7 10

Temporary Outage
by Ben Gamari 08 Oct '21

08 Oct '21

Hi all, You may notice that currently there are numerous CI failures due to apparent network issues. This appears to be due to a network outage on the part of our hosting providing. Further updates are available from Packet [1]. Hopefully the issue will be resolved within the next few hours. Cheers, - Ben [1] https://status.equinixmetal.com/

1 0

Perf backtrace support.
by Andreas Klebinger 07 Oct '21

07 Oct '21

Hello Devs, as some of you know I've recently been working on #8272. The goal being to use the machine stack register for the STG stack as a means to get perf backtraces. I've succeeded in making a branch that works for the first part but have so far been unable to get perf to generate proper back traces. For various reasons I will stop looking at that particular issue. So if anyone feels interested in figuring out where the interaction between our dwarf info and perf unwinding the stack goes wrong please take a look! There is more information on the ticket. Cheers Andreas

1 0

Re: Specialisation doesn't kick in (RE: Instantiation of overloaded definition *in Core*)
by Erdi, Gergo 06 Oct '21

06 Oct '21

INTERNAL I see. That will be a bit more involved to try out, because I don't have a ModGuts at hand -- I only have the ModDetails, and the collected CoreProgram from the whole program. But it seems `specProgram` only really uses the rules and the binds from the `ModGuts`, so I should be all right. But one thing I can easily try is just printing the UsageDetails as returned by the specBinds part of specProgram, and that seems empty. So if the actual work of specProgram happens by generating rules in specImports, how will specImports know what rules to generate, from an empty UsageDetails? -----Original Message----- From: Matthew Pickering <matthewtpickering(a)gmail.com> Sent: Wednesday, October 6, 2021 4:24 PM To: Erdi, Gergo <Gergo.Erdi(a)sc.com> Cc: Simon Peyton Jones <simonpj(a)microsoft.com>; Montelatici, Raphael Laurent <Raphael.Montelatici(a)sc.com>; GHC <ghc-devs(a)haskell.org> Subject: [External] Re: Specialisation doesn't kick in (RE: Instantiation of overloaded definition *in Core*) I think you need to run at least one simplifier pass as the specialisations are applied via rules (created by specProgram). This email and any attachments are confidential and may also be privileged. If you are not the intended recipient, please delete all copies and notify the sender immediately. You may wish to refer to the incorporation details of Standard Chartered PLC, Standard Chartered Bank and their subsidiaries at https: //www.sc.com/en/our-locations Where you have a Financial Markets relationship with Standard Chartered PLC, Standard Chartered Bank and their subsidiaries (the "Group"), information on the regulatory standards we adhere to and how it may affect you can be found in our Regulatory Compliance Statement at https: //www.sc.com/rcs/ and Regulatory Compliance Disclosures at http: //www.sc.com/rcs/fm Insofar as this communication is not sent by the Global Research team and contains any market commentary, the market commentary has been prepared by the sales and/or trading desk of Standard Chartered Bank or its affiliate. It is not and does not constitute research material, independent research, recommendation or financial advice. Any market commentary is for information purpose only and shall not be relied on for any other purpose and is subject to the relevant disclaimers available at https: //www.sc.com/en/regulatory-disclosures/#market-disclaimer. Insofar as this communication is sent by the Global Research team and contains any research materials prepared by members of the team, the research material is for information purpose only and shall not be relied on for any other purpose, and is subject to the relevant disclaimers available at https: //research.sc.com/research/api/application/static/terms-and-conditions. Insofar as this e-mail contains the term sheet for a proposed transaction, by responding affirmatively to this e-mail, you agree that you have understood the terms and conditions in the attached term sheet and evaluated the merits and risks of the transaction. We may at times also request you to sign the term sheet to acknowledge the same. Please visit https: //www.sc.com/en/regulatory-disclosures/dodd-frank/ for important information with respect to derivative products.

1 0

GHC indecisive whether matching on GADT constructors in arrow notation is allowed
by Alexis King 06 Oct '21

06 Oct '21

Hi, I’ve been working on bringing my reimplementation of arrow notation back up to date, and I’ve run into some confusion about the extent to which arrow notation is “supposed” to support matching on GADT constructors. Note [Arrows and patterns] in GHC.Tc.Gen.Pat suggests they aren’t supposed to be supported at all, which is what I would essentially expect. But issues #17423 <https://gitlab.haskell.org/ghc/ghc/-/issues/17423> and #18950 <https://gitlab.haskell.org/ghc/ghc/-/issues/18950> provide examples of using GADT constructors in arrow notation, and there seems to be some expectation that in fact they *ought* to be supported, and some recently-added test cases verify that’s the case. But this is quite odd, because it means the arrows test suite now includes test cases that verify both that this is supported *and* that it isn’t… and all of them pass! Here’s my understanding of the status quo: - Matching on constructors that bind bona fide existential variables is not allowed, and this is verified by the arrowfail004 test case, which involves the following program: data T = forall a. T a panic :: (Arrow arrow) => arrow T T panic = proc (T x) -> do returnA -< T x This program is rejected with the following error message: arrowfail004.hs:12:15: Proc patterns cannot use existential or GADT data constructors In the pattern: T x - Despite the previous point, matching on constructors that bind evidence is allowed. This is enshrined in test cases T15175, T17423, and T18950, which match on constructors like these: data DecoType a where DecoBool :: Maybe (String, String) -> Maybe (Int, Int) -> DecoType Bool data Point a where Point :: RealFloat a => a -> Point a This seems rather contradictory to me. I don’t think there’s much of a meaningful distinction between these types of matches, as they create precisely the same set of challenges from the Core point of view… right? And even if I’m wrong, the error message in arrowfail004 seems rather misleading, since I would definitely call DecoBool and Point above “GADT data constructors”. So what’s the intended story here? Is matching on GADT constructors in arrow notation supposed to be allowed or not? (I suspect this is really just yet another case of “nobody really knows what’s ‘supposed’ to happen with arrow notation,” but I figured I might as well ask out of hopefulness that someone has some idea.) Thanks, Alexis

3 3

Arrow notation, existentials, and TcType demotion
by Alexis King 05 Oct '21

05 Oct '21

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

1 0