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