Re: Q: Types in GADT pattern match

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

Re: Types in GADT pattern match

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

FW: How does GHC's testsuite work?

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

Re: Q: Types in GADT pattern match

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

Re: Q: Types in GADT pattern match

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

RE: Types in GADT pattern match

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

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

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

Re: Q: Types in GADT pattern match

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