I think the real difference is whether new type variables are brought into scope. It seems that GHC can't deal with a proc-pattern-match that introduces type variables, but it *can* deal with introduced constraints. I have no idea *why* this is the case, but it seems a plausible (if accidental) resting place for the implementation.
Richard > On Oct 3, 2021, at 12:19 PM, Alexis King <lexi.lam...@gmail.com> wrote: > > 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 > > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
