[GHC] #13430: Can't scope type variables when pattern matching on GADTs
#13430: Can't scope type variables when pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I was very surprised that the following doesn't compile: {{{ {-# LANGUAGE GADTs, ScopedTypeVariables #-} data Foo x where A :: Foo Bool B :: Foo Int foo :: Foo x -> () foo (A :: Foo Bool) = () }}} GHC says that it couldn't match the type `y` with `Bool`. See [this question](http://stackoverflow.com/questions/42824949/type-inference-with- gadts) for a simple motivating example. As someone there pointed out, the situation would be improved with type application (#11350), but this ticket is about bringing the output type in scope with `ScopedTypeVariables`. This most closely reminds me of #1823 (!), but that was resolved many moons ago. This behavior also exists in 7.10.3. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13430 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13430: Can't scope type variables when pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Looks absolutely right to me. `foo`'s argument type is `Foo x` not `Foo Bool`. Only ''after'' matching A do we get `Foo Bool`. But the type signature is matched before we get to the A part. Better to consider something more like the original question: {{{ data Bar x where MkBar :: Typeable b => a -> Bar (a,b) bar :: Bar x -> string bar (MkBar @a @b _) = show (typeRep (Proxy :: Proxy b)) }}} Here you want to use mention the type variable `b`. But there is no way to bring it into scope since we don't have visible type applications in patterns (yet #11350). I think that's really the right solution too. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13430#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13430: Can't scope type variables when pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): BTW here is a workaround: {{{ bar :: Bar x -> String bar x@(MkBar _) = case x of (x :: Bar (a, b)) -> show (typeRep (Proxy :: Proxy b)) }}} Here, ''inside'' the pattern match for `MkBar` we make a new pattern-match on `x`, and give it a scoped type signature. Not beautiful but it works. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13430#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13430: Can't scope type variables when pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by crockeea):
the type signature is matched before we get to the A part
That may be the case, but it's quite strange that I wrote `A :: Foo Bool` in the GADT definition, but I can't write `A :: Foo Bool` in the pattern. `A` certainly does have that type. I think the notation is natural enough that it should work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13430#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13430: Can't scope type variables when pattern matching on GADTs -------------------------------------+------------------------------------- Reporter: crockeea | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.2 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #12018 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: => #12018 Comment: I'm opting to close this as a duplicate of #12018. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13430#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC