GHC indecisive whether matching on GADT constructors in arrow notation is allowed
Oleg Grenrus
oleg.grenrus at iki.fi
Tue Oct 5 16:49:09 UTC 2021
A simple desugaring example may illustrate:
{-# LANGUAGE Arrows, GADTs #-}
import Control.Arrow
data X a where
X :: Bool -> Int -> X (Bool, Int)
ex1 :: Arrow a => a (X x) (Int, Bool)
ex1 = proc (X b i) -> returnA -< (i, b)
ex1expl :: Arrow a => a (X x) (Int, Bool)
ex1expl =
arr f >>> -- pattern match
arr g >>> -- expression
returnA
where
f :: X a -> (Bool, Int)
f (X b i) = (b, i)
g :: (Bool, Int) -> (Int, Bool)
g (b, i) = (i, b)
If we want to desugar Alexis' example
data T where
T :: a -> T
panic :: (Arrow arrow) => arrow T T
panic = proc (T x) -> do returnA -< T x
which has the same shape, what would the type of `f` be?
f :: T -> a -- doesn't work
If we had sigmas, i.e. dependent pairs and type level lambdas, we could have
f :: T -> Sigma Type (\a -> a) -- a pair like (Bool, Int) but fancier
i.e. the explicit desugaring could look like
panicExplicit :: (Arrow arrow) => arrow T T
panicExplicit =
arr f >>>
arr g >>>
returnA
where
f :: T -> Sigma Type (\a -> a)
f (T @a x) = (@a, x)
g :: Sigma Type (\a -> a)
g (@a, x) = T @a x
My gut feeling says that the original arrow desugaring would just work,
but instead of tuples for context, we'd need to use telescopes.
Not that earth-shattering of a generalization.
The evidence could be explicitly bound already today,
but I guess it's not, and simply thrown away:
{-# LANGUAGE Arrows, GADTs, ConstraintKinds #-}
import Control.Arrow
data Showable a where
Showable :: Show a => a -> Showable a
data Dict c where
Dict :: c => Dict c
ex2explicit :: Arrow a => a (Showable x) (Showable x)
ex2explicit =
arr f >>> -- pattern match
arr g >>> -- expression
returnA
where
f :: Showable x -> (x, Dict (Show x))
f (Showable x) = (x, Dict)
g :: (x, Dict (Show x)) -> Showable x
g (x, Dict) = Showable x
The
ex2 :: Arrow a => a (Showable x) (Showable x)
ex2 = proc (Showable x) -> returnA -< Showable x
works today, surprisingly. Looks like GHC does something as above,
if I read the -ddump-ds output correctly:
ex2
:: forall (a :: * -> * -> *) x.
Arrow a =>
a (Showable x) (Showable x)
[LclIdX]
ex2
= \ (@ (a_a2ja :: * -> * -> *))
(@ x_a2jb)
($dArrow_a2jd :: Arrow a_a2ja) ->
break<1>()
let {
arr' :: forall b c. (b -> c) -> a_a2ja b c
[LclId]
arr' = arr @ a_a2ja $dArrow_a2jm } in
let {
(>>>>) :: forall a b c. a_a2ja a b -> a_a2ja b c -> a_a2ja a c
[LclId]
(>>>>) = GHC.Desugar.>>> @ a_a2ja $dArrow_a2jn } in
(>>>>)
@ (Showable x_a2jb)
@ ((Show x_a2jb, x_a2jb), ())
@ (Showable x_a2jb)
(arr'
@ (Showable x_a2jb)
@ ((Show x_a2jb, x_a2jb), ()) -- this is interesting
(\ (ds_d2kY :: Showable x_a2jb) ->
case ds_d2kY of { Showable $dShow_a2je x_a2hL ->
(($dShow_a2je, x_a2hL), ghc-prim-0.5.3:GHC.Tuple.())
}))
((>>>>)
@ ((Show x_a2jb, x_a2jb), ())
@ (Showable x_a2jb)
@ (Showable x_a2jb)
(arr'
@ ((Show x_a2jb, x_a2jb), ())
@ (Showable x_a2jb)
(\ (ds_d2kX :: ((Show x_a2jb, x_a2jb), ())) ->
case ds_d2kX of { (ds_d2kW, _ [Occ=Dead]) ->
case ds_d2kW of { ($dShow_a2jl, x_a2hL) ->
break<0>() Main.Showable @ x_a2jb $dShow_a2jl x_a2hL
}
}))
(returnA @ a_a2ja @ (Showable x_a2jb) $dArrow_a2jd))
- Oleg
On 5.10.2021 19.12, Richard Eisenberg wrote:
> 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.lambda at gmail.com
>> <mailto:lexi.lambda at 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 at haskell.org <mailto:ghc-devs at haskell.org>
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211005/d0b6c883/attachment.html>
More information about the ghc-devs
mailing list