Re: Q: Types in GADT pattern match

[Gabor Greif]

On 10/30/17, Csongor Kiss  wrote:
> Right, but I think Gabor's suggestion here is for type checking of the
> pattern to be done first, and then capturing the coercions
> that were brought into scope by the pattern match.
>
> data Foo a where
>   Bar :: Foo [a]
>
> foo :: Foo a -> ()
> foo Bar =  -- we know (a ~ [b]) here, for some b
>
> The pattern match on Bar in foo gives us the equality assumption on the
> right hand side, but
> we don't have an easy way of capturing 'b' - which we might want to do for,
> say, visible type application inside .


Yep. Visible type application on the RHS is what I am after. It is
just user-unfriendly that one has to doubly pattern match on the same
object in order to bring the GADT constructor's type equality into
play.

Thanks Csongor for the expanded reasoning!

Gabor


>
> foo' :: Foo a -> ()
> foo' (Bar :: Foo a) = 
>
> of course works, but it only gives us access to 'a' in .
>
> foo'' :: Foo a -> ()
> foo'' (Bar :: Foo [c]) = 
>
> This would mean that in addition to (a ~ [b]), for some b, we would get (a ~
> [c]), for our new c. This then gives (b ~ c),
> essentially giving us access to the existential b. Of course we would need
> to check that our scoped type signature
> doesn't introduce bogus coercions, like
>
> foo''' :: Foo a -> ()
> foo''' (Bar :: Foo [[c]]) = 
>
> is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]),
> which we can't prove from the given assumptions.
>
>
> Cheers,
> Csongor
>
> On 30 Oct 2017, 12:13 +, Brandon Allbery , wrote:
>> > On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif  wrote:
>> > > My original question, though, is not answered yet, namely why not to
>> > > detect that we are about to pattern match on a GADT constructor and
>> > > allow the programmer to capture the *refined* type with her type
>> > > annotation. Sure this would necessitate a change to the type checker,
>> > > but would also increase the expressive power a bit.
>> > >
>> > > Is there some fundamental problem with this? Or simply nobody wanted
>> > > to do this yet? Would it be hard to implement type checking *after*
>> > > refinement on GADT(-like) patterns?
>>
>> I wouldn't be surprised if type checking is precisely what enables
>> refinement, making this a bit chicken-and-egg.
>>
>> --
>> brandon s allbery kf8nh   sine nomine
>> associates
>> allber...@gmail.com
>>  ballb...@sinenomine.net
>> unix, openafs, kerberos, infrastructure, xmonad
>>  http://sinenomine.net
>> ___
>> 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

Re: Types in GADT pattern match

[Gabor Greif]

On 10/30/17, Simon Peyton Jones  wrote:
> foo b@(Bar :: Foo [a]) = quux b
> The pattern (p :: ty) checks that the thing being matched has type ‘ty’ and
> THEN matches ‘p’.  You expected it to FIRST match ‘p’, and THEN check that
> the thing being matched has type ‘ty’.  But that’s not the way it works.

Yep. Understood. I was just hoping that one could annotate the
"insider view" of GADT pattern matches (considering the equality
constraints of the constructor) as well as the "outsider view", namely
'foo's external signature.

>
> e.g what about this
>
> rats ([Just (Bar, True)] :: [Maybe (Foo [a], Bool)]) = …
>
> Here the pattern to be matched is deep, with the Bar part deep inside.  Do
> you still expect it to work?

Well, it reflects a truth, so I'd expect it to work, yes :-)

>
> This would be hard to change.  And I’m not sure it’d be an improvement.

Hmmm, sure. There are probably better areas to invest effort into.

Thanks,

Gabor

>
> Simon
>
> From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Gabor
> Greif
> Sent: 29 October 2017 17:43
> To: ghc-devs 
> Subject: Q: Types in GADT pattern match
>
> Hi Devs!
>
> I encountered a curious restriction with type signatures (tyvar bindings) in
> GADT pattern matches.
>
> GHC won't let me directly capture the refined type structure of GADT
> constructors like this:
>
>
> {-# Language GADTs, ScopedTypeVariables #-}
>
> data Foo a where
>   Bar :: Foo [a]
>
> foo :: Foo a -> ()
> foo b@(Bar :: Foo [a]) = quux b
>   where quux :: Foo [b] -> ()
> quux Bar = ()
>
>
> I get:
>
>
>
> test.hs:7:8: error:
>
> • Couldn't match type ‘a1’ with ‘[a]’
>
>   ‘a1’ is a rigid type variable bound by
>
> the type signature for:
>
>   foo :: forall a1. Foo a1 -> ()
>
> at test.hs:6:1-18
>
>   Expected type: Foo a1
>
> Actual type: Foo [a]
>
>
> To me it appears that the type refinement established by the GADT pattern
> match is not accounted for.
>
> Of course I can write:
>
> foo :: Foo a -> ()
> foo b@Bar | (c :: Foo [a]) <- b = quux c
>   where quux :: Foo [b] -> ()
> quux Bar = ()
>
> but it feels like a complicated way to do it...
>
> My question is whether this is generally seen as the way to go or whether
> ScopedTypeVariables coming from a GADT pattern match should be able to
> capture the refined type. To me the latter seems more useful.
>
> Just wanted to feel the waters before writing a ticket about this.
>
> Cheers and thanks,
>
> Gabor
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

FW: How does GHC's testsuite work?

[Simon Peyton Jones via ghc-devs]

Forwarding to ghc-devs, a better list for this question.

Simon 

-Original Message-
From: Glasgow-haskell-users [mailto:glasgow-haskell-users-boun...@haskell.org] 
On Behalf Of Sébastien Hinderer
Sent: 30 October 2017 15:18
To: glasgow-haskell-us...@haskell.org
Subject: How does GHC's testsuite work?

Dear all,

I am a member of OCaml's developement team. More specifically, I am working on 
a test-driver for the OCaml compiler, which will be part of OCaml's 4.06 
release.

I am currently writing an article to describe the tool and its principles. In 
this article, I would like to also talk about how other compilers' testsuites 
are handled and loking how things are done in GHC is natural.

In OCaml, our testsuite essentially consist in whole programs that we compile 
and run, checking that the compilation and execution results match the expected 
ones.

From what I could see from GHC's testsuite, it seemed to me that it uses Python 
to drive the tests. I also understood that the testsuite has tests that are 
more kind of unit-tests, in the .T file. Am I correct here? Or do you guys also 
have whole program tests?
If you do, how do you compile and run them?

Any comment / hint on this aspect of the test harness' design would be really 
helpful.

Many thanks in advance,

Sébastien.





___
Glasgow-haskell-users mailing list
glasgow-haskell-us...@haskell.org
https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fglasgow-haskell-users=02%7C01%7Csimonpj%40microsoft.com%7C293aac933ae143b8690308d51fa9681f%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636449734850370955=SY4ABziBhV4MxLwTpJ5bFyS8GJfHLL%2FZrTxQc90EGDs%3D=0
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Q: Types in GADT pattern match

[Csongor Kiss]

Right, but I think Gabor's suggestion here is for type checking of the pattern 
to be done first, and then capturing the coercions
that were brought into scope by the pattern match.

data Foo a where
  Bar :: Foo [a]

foo :: Foo a -> ()
foo Bar =  -- we know (a ~ [b]) here, for some b

The pattern match on Bar in foo gives us the equality assumption on the right 
hand side, but
we don't have an easy way of capturing 'b' - which we might want to do for, 
say, visible type application inside .

foo' :: Foo a -> ()
foo' (Bar :: Foo a) = 

of course works, but it only gives us access to 'a' in .

foo'' :: Foo a -> ()
foo'' (Bar :: Foo [c]) = 

This would mean that in addition to (a ~ [b]), for some b, we would get (a ~ 
[c]), for our new c. This then gives (b ~ c),
essentially giving us access to the existential b. Of course we would need to 
check that our scoped type signature
doesn't introduce bogus coercions, like

foo''' :: Foo a -> ()
foo''' (Bar :: Foo [[c]]) = 

is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]), 
which we can't prove from the given assumptions.


Cheers,
Csongor

On 30 Oct 2017, 12:13 +, Brandon Allbery , wrote:
> > On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif  wrote:
> > > My original question, though, is not answered yet, namely why not to
> > > detect that we are about to pattern match on a GADT constructor and
> > > allow the programmer to capture the *refined* type with her type
> > > annotation. Sure this would necessitate a change to the type checker,
> > > but would also increase the expressive power a bit.
> > >
> > > Is there some fundamental problem with this? Or simply nobody wanted
> > > to do this yet? Would it be hard to implement type checking *after*
> > > refinement on GADT(-like) patterns?
>
> I wouldn't be surprised if type checking is precisely what enables 
> refinement, making this a bit chicken-and-egg.
>
> --
> brandon s allbery kf8nh                               sine nomine associates
> allber...@gmail.com                                  ballb...@sinenomine.net
> unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
> ___
> 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

Re: Q: Types in GADT pattern match

[Brandon Allbery]

On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif  wrote:

> My original question, though, is not answered yet, namely why not to
> detect that we are about to pattern match on a GADT constructor and
> allow the programmer to capture the *refined* type with her type
> annotation. Sure this would necessitate a change to the type checker,
> but would also increase the expressive power a bit.
>
> Is there some fundamental problem with this? Or simply nobody wanted
> to do this yet? Would it be hard to implement type checking *after*
> refinement on GADT(-like) patterns?
>

I wouldn't be surprised if type checking is precisely what enables
refinement, making this a bit chicken-and-egg.

-- 
brandon s allbery kf8nh   sine nomine associates
allber...@gmail.com  ballb...@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonadhttp://sinenomine.net
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Types in GADT pattern match

[Simon Peyton Jones via ghc-devs]

foo b@(Bar :: Foo [a]) = quux b
The pattern (p :: ty) checks that the thing being matched has type ‘ty’ and 
THEN matches ‘p’.  You expected it to FIRST match ‘p’, and THEN check that the 
thing being matched has type ‘ty’.  But that’s not the way it works.

e.g what about this

rats ([Just (Bar, True)] :: [Maybe (Foo [a], Bool)]) = …

Here the pattern to be matched is deep, with the Bar part deep inside.  Do you 
still expect it to work?

This would be hard to change.  And I’m not sure it’d be an improvement.

Simon

From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Gabor Greif
Sent: 29 October 2017 17:43
To: ghc-devs 
Subject: Q: Types in GADT pattern match

Hi Devs!

I encountered a curious restriction with type signatures (tyvar bindings) in 
GADT pattern matches.

GHC won't let me directly capture the refined type structure of GADT 
constructors like this:


{-# Language GADTs, ScopedTypeVariables #-}

data Foo a where
  Bar :: Foo [a]

foo :: Foo a -> ()
foo b@(Bar :: Foo [a]) = quux b
  where quux :: Foo [b] -> ()
quux Bar = ()


I get:



test.hs:7:8: error:

• Couldn't match type ‘a1’ with ‘[a]’

  ‘a1’ is a rigid type variable bound by

the type signature for:

  foo :: forall a1. Foo a1 -> ()

at test.hs:6:1-18

  Expected type: Foo a1

Actual type: Foo [a]


To me it appears that the type refinement established by the GADT pattern match 
is not accounted for.

Of course I can write:

foo :: Foo a -> ()
foo b@Bar | (c :: Foo [a]) <- b = quux c
  where quux :: Foo [b] -> ()
quux Bar = ()

but it feels like a complicated way to do it...

My question is whether this is generally seen as the way to go or whether 
ScopedTypeVariables coming from a GADT pattern match should be able to capture 
the refined type. To me the latter seems more useful.

Just wanted to feel the waters before writing a ticket about this.

Cheers and thanks,

Gabor
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: When does GHC produce unlifted `let` bindings?

[Simon Peyton Jones via ghc-devs]

See Note [CoreSyn let/app invariant] in CoreSyn.

Briefly, you can write
let x::Int# = e in …
if e is “ok-for-speculation”.  See extensive comments in CoreUtils on what that 
means.

You could also use case, but let-bindings “float” more easily than cases, 
because they are not worried about preserving exception behaviour.

Simon

From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Sebastian Graf
Sent: 29 October 2017 21:07
To: ghc-devs 
Subject: When does GHC produce unlifted `let` bindings?

Hi folks,

I was debugging a Core-to-Core transform for 
TEST=spec-inline
 and was wondering (yet again) why GHC produces unlifted `let` bindings in Core 
like it seems supposed to be 
doing.

  *   Why doesn't this use `case` instead?
  *   Is there a semantic difference?
  *   Can `case` be used with unlifted types?
  *   And if not, why can `let`?
Unlifted `let` seems much close to `case` than to `let`. Some GHC passes seem 
to 
agree.

Cheers,
Sebastian
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Q: Types in GADT pattern match

[Gabor Greif]

Hi Oleg, Richard,

thanks for your answers! Seems like my original diagnosis is correct and
GADT type refinement is done *after* the checking of the pattern type signature.

My workaround

  >  foo b@Bar | (c :: Foo [x]) <- b = ... @x ...

works perfectly well and is essentially the same what Richard
suggests, while being
a little less gross.

My original question, though, is not answered yet, namely why not to
detect that we are about to pattern match on a GADT constructor and
allow the programmer to capture the *refined* type with her type
annotation. Sure this would necessitate a change to the type checker,
but would also increase the expressive power a bit.

Is there some fundamental problem with this? Or simply nobody wanted
to do this yet? Would it be hard to implement type checking *after*
refinement on GADT(-like) patterns?

Cheers and thanks,

Gabor


On 10/30/17, Richard Eisenberg  wrote:
> Hi Gabor,
>
> Oleg is right that the re-use of type variables obscures the error, but it's
> not quite a scoping error under the hood. The problem is that GHC
> type-checks type signatures on patterns *before* type-checking the pattern
> itself. That means that when GHC checks your `Foo [a]` type signature, we
> haven't yet learned that `a1` (the type variable used in the type signature
> of foo) equals `[a]`. This makes it hard to bind a variable to `a`. Here's
> what I've done:
>
>> foo :: Foo a -> ()
>> foo b@Bar = case b of
>>   (_ :: Foo [c]) -> quux b
>> where
>>   quux :: Foo [c] -> ()
>>   quux Bar = ()
>
> It's gross, but it works, and I don't think there's a better way at the
> moment. A collaborator of mine is working on a proposal (and implementation)
> of binding existentials in patterns (using similar syntax to visible type
> application), but that's still a few months off, at best.
>
> Richard
>
>> On Oct 29, 2017, at 1:42 PM, Gabor Greif  wrote:
>>
>> Hi Devs!
>>
>> I encountered a curious restriction with type signatures (tyvar bindings)
>> in GADT pattern matches.
>>
>> GHC won't let me directly capture the refined type structure of GADT
>> constructors like this:
>>
>>
>> {-# Language GADTs, ScopedTypeVariables #-}
>>
>> data Foo a where
>>   Bar :: Foo [a]
>>
>> foo :: Foo a -> ()
>> foo b@(Bar :: Foo [a]) = quux b
>>   where quux :: Foo [b] -> ()
>> quux Bar = ()
>>
>>
>> I get:
>>
>>
>> test.hs:7:8: error:
>> • Couldn't match type ‘a1’ with ‘[a]’
>>   ‘a1’ is a rigid type variable bound by
>> the type signature for:
>>   foo :: forall a1. Foo a1 -> ()
>> at test.hs:6:1-18
>>   Expected type: Foo a1
>> Actual type: Foo [a]
>>
>>
>> To me it appears that the type refinement established by the GADT pattern
>> match is not accounted for.
>>
>> Of course I can write:
>>
>> foo :: Foo a -> ()
>> foo b@Bar | (c :: Foo [a]) <- b = quux c
>>   where quux :: Foo [b] -> ()
>> quux Bar = ()
>>
>> but it feels like a complicated way to do it...
>>
>> My question is whether this is generally seen as the way to go or whether
>> ScopedTypeVariables coming from a GADT pattern match should be able to
>> capture the refined type. To me the latter seems more useful.
>>
>> Just wanted to feel the waters before writing a ticket about this.
>>
>> Cheers and thanks,
>>
>> Gabor
>> ___
>> 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