Re: GHC indecisive whether matching on GADT constructors in arrow notation is allowed

[Alexis King]

I have already discussed this particular issue at some length in #20470
, and I propose a
possible desugaring, using higher-rank lambdas to encode existential
quantification, in a comment
. This is
fine, since we only need to desugar to Core, not source Haskell.

Alexis


On Tue, Oct 5, 2021 at 11:50 AM Oleg Grenrus  wrote:

> 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 

Re: GHC indecisive whether matching on GADT constructors in arrow notation is allowed

[Oleg Grenrus]

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 > > 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
>>  and #18950
>>  provide examples
>> of using GADT 

Re: GHC indecisive whether matching on GADT constructors in arrow notation is allowed

[Richard Eisenberg]

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  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 
>  and #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

GHC indecisive whether matching on GADT constructors in arrow notation is allowed

[Alexis King]

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  and #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