[GHC] #11449: Treat '_' consistently in type declarations
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- GHC doesn't treat `_` consistently in type declarations {{{ -- Example A data T _ = MkT -- Not allowed -- Example B class C a where type T a -- Example C class C [_] where -- Not allowed type T [_] = Int -- Not allowed -- Example D data family D a data instance D [_] = MkD -- Allowed -- Example E type family F a type instance F [_] = Int -- Allowed }}} This seems inconsistent and annoying (see [https://mail.haskell.org/pipermail/glasgow-haskell- users/2016-January/026114.html email thread]). Really, we should consistently treat `_` in a binding position simply as ''a binder that binds nothing'', just like at the term level. But in Haskell 98 `_` is a reserved identifier, so these programs are illegal. We use `PartialTypeSignatures` to allow `_` in occurrence positions in types. Should the same flag enable `_` in binding positions? It would seem a little odd to require `PartialTypeSignatures` for (A) and (C). Any suggestions? A couple of wrinkles. First, since `_` binds nothing, it certainly doesn't bind occurrences of `_`. Thus for example, with `PartialTypeSignatures` {{{ instance C [_] where op = .... (let f :: _ -> _ f = e in ...) ... }}} The occurrences of `_` in `op`'s RHS are ''not'' bound by the `_` in the `instance` header. (The would be if all three were `a`, say.) Rather the occurrences of `_` are holes in the type signature and should be separately reported as such. Second, the implementation would be tricky in one spot: {{{ class C a where type T a instance C (Either _ _) where type T (Either _ _) = ... }}} We must check that the type family instance is at the same type as the class. Do we want to insist that it looks ''exactly'' the same, or would you be allowed to say this? {{{ instance C (Either _ _) where type T (Either a b) = a -> b }}} My instinct is to say "exactly the same" for now anyway. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Lemming): * cc: ghc@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I would love to see (A) accepted (perhaps with some language extension). I think (C) should be rejected. After all, the type variable ''is'' used there. It's used in the type family declaration, where `a` is not ''bound'' -- it is ''used''. Accordingly, {{{ class C a where type F a type F a = Int }}} should not emit any warnings. The only bound variable, `a`, is indeed used. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm a bit confused about example (C), since I don't think this: {{{#!hs class C [a] where type T [a] = Int }}} is legal (which is what example (C) is, just with `_` instead of `a`). Did you mean something like this? {{{#!hs class C _ where type T _ = Int }}} or this? {{{#!hs instance C [_] where type T [_] = Int }}} I can understand objecting to the former (similarly, you'd reject `data T _ = MkT _`, right?), but I certainly want the latter to be legal, especially if we require the class instance types to be the same as the associated type family types—otherwise, I'd have no way of [https://ghc.haskell.org/trac/ghc/ticket/11450#comment:16 wildcard-ing out unused types in such a scenario]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by simonpj: @@ -11,2 +11,2 @@ - class C [_] where -- Not allowed - type T [_] = Int -- Not allowed + instance C [_] where -- Not allowed + type T [_] = Int -- Not allowed New description: GHC doesn't treat `_` consistently in type declarations {{{ -- Example A data T _ = MkT -- Not allowed -- Example B class C a where type T a -- Example C instance C [_] where -- Not allowed type T [_] = Int -- Not allowed -- Example D data family D a data instance D [_] = MkD -- Allowed -- Example E type family F a type instance F [_] = Int -- Allowed }}} This seems inconsistent and annoying (see [https://mail.haskell.org/pipermail/glasgow-haskell- users/2016-January/026114.html email thread]). Really, we should consistently treat `_` in a binding position simply as ''a binder that binds nothing'', just like at the term level. But in Haskell 98 `_` is a reserved identifier, so these programs are illegal. We use `PartialTypeSignatures` to allow `_` in occurrence positions in types. Should the same flag enable `_` in binding positions? It would seem a little odd to require `PartialTypeSignatures` for (A) and (C). Any suggestions? A couple of wrinkles. First, since `_` binds nothing, it certainly doesn't bind occurrences of `_`. Thus for example, with `PartialTypeSignatures` {{{ instance C [_] where op = .... (let f :: _ -> _ f = e in ...) ... }}} The occurrences of `_` in `op`'s RHS are ''not'' bound by the `_` in the `instance` header. (The would be if all three were `a`, say.) Rather the occurrences of `_` are holes in the type signature and should be separately reported as such. Second, the implementation would be tricky in one spot: {{{ class C a where type T a instance C (Either _ _) where type T (Either _ _) = ... }}} We must check that the type family instance is at the same type as the class. Do we want to insist that it looks ''exactly'' the same, or would you be allowed to say this? {{{ instance C (Either _ _) where type T (Either a b) = a -> b }}} My instinct is to say "exactly the same" for now anyway. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I meant `instance` sorry. I've fixed the ticket description. Remember the description describes current behaviour. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Never mind, I don't think things like {{{#!hs instance C [_] where type T [_] = Int }}} should be allowed after all (see [https://ghc.haskell.org/trac/ghc/ticket/11450#comment:18 my comment] in #11450 for rationale). That being said, I don't know if we should rule out putting wildcards in class instances altogether. Typeclasses without associated type families or methods wouldn't have the issue of requiring the types to be the same, so you could conceivably have something like this: {{{#!hs class C a where instance C _ where }}} Although I don't know how useful this is. And I really don't know how to feel about things like `data T _ = T` or `class C a _`, since we'd be allowing wildcards in place of `TyVar`s, which is uncharted territory. Neither are Haskell98 for sure, so I agree that if we allow such a thing, you should need a language extension to turn it on. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11449: Treat '_' consistently in type declarations -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by WrenThornton): * cc: wren@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11449#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC