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 = --
rd 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
> T
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
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 necessi
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
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 Richa
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 signatu
The problem is scoping. The problem is more obvious if you don't reuse
type-variables:
{-# Language GADTs, ScopedTypeVariables #-}
data Foo a where
Bar :: Foo [x]
foo :: Foo a -> ()
foo b@(Bar :: Foo [c]) = quux b
where quux :: Foo [b] -> ()
quux Bar = ()
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 -
