[GHC] #12569: TypeApplications doesn't allow unticked list constructors.
#12569: TypeApplications doesn't allow unticked list constructors. -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 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: -------------------------------------+------------------------------------- TypeApplications doesn't allow unticked list constructor even when it is unambiguous: {{{ GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
:set -XDataKinds :set -XTypeApplications :set -XScopedTypeVariables :set -XKindSignatures let foo :: forall (xs :: [Nat]). (); foo = () foo @'[0] () foo @[0]
<interactive>:17:6: error: * Expected kind `[Nat]', but `[0]' has kind `*' * In the type `[0]' In the expression: foo @[0] In an equation for `it': it = foo @[0] <interactive>:17:7: error: * Expected a type, but `0' has kind `Nat' * In the type `[0]' In the expression: foo @[0] In an equation for `it': it = foo @[0] }}} why `[0]` has kind `*` here? However this is legal: {{{
let foo :: forall (x :: Bool). (); foo = () foo @True () foo @'True () }}}
and this is wierd: {{{
:set -XPolyKinds let foo :: forall (x :: k). (); foo = () foo @'True
<interactive>:12:6: error: * Expected a type, but 'True has kind `Bool' * In the type `True' In the expression: foo @True In an equation for `it': it = foo @True
foo @True
<interactive>:13:6: error: * Expected a type, but 'True has kind `Bool' * In the type `True' In the expression: foo @True In an equation for `it': it = foo @True }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12569 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12569: TypeApplications allows instantiation of implicitly-quantified kind variables -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | TypeApplications 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 adamgundry): * cc: adamgundry, goldfire (added) * keywords: => TypeApplications * component: Compiler => Compiler (Type checker) Comment: I believe the ticked/unticked constructor mechanism is working as designed, but you may be on to something with your "weird" example. == To tick or not to tick == Without a tick, `[0]` as a type is in fact ill-kinded. `[0]` is syntactic sugar for `[] 0` where `[] :: * -> *` is the list type constructor. Moreover, `0` does not have kind `*`. This is why you get two errors from `foo @[0]`. With a tick, `'[0]` is syntactic sugar for `0 ': '[]` (i.e. a promoted list of one element) and has kind `[Nat]` as expected. A tick is necessary when a data constructor and type constructor have the same name, and you want to refer to the data constructor in the type namespace. In the case of `True` and `'True`, in the absence of a type constructor `True`, this is genuinely unambiguous and the tick is optional. == The actual bug == (Whether the constructor is ticked or not is irrelevant here.) When you write `let foo :: forall (x :: k). (); foo = ()`, GHC implicitly quantifies over the kind variable `k` to give `foo :: forall k (x :: k) . ()`. I would expect that `k` would not be available for instantiation via a type application, but apparently it is, because `foo @True` is rejected but `foo @Bool @True` is accepted. I think we should have `foo :: forall {k} (x :: k) . ()` instead. @goldfire, would you agree that this should be changed? In any case, we should document this case in the manual. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12569#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12569: TypeApplications allows instantiation of implicitly-quantified kind variables -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | TypeApplications 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 see no bugs here, except possibly bugs in error messages / documentation. The tick is merely at the level of name resolution. When GHC sees an unticked constructor-like name (that is, a capitalized identifier, an identifier starting with a colon, or a use of list syntax in a type), it looks to see if there is a type constructor of that name. If there is, it uses the type name. If there is not, it looks for a data constructor of that name. And that's it. There is no type-directed lookup here. So, when you say `[0]`, without the tick, GHC uses the type `[]` which has the wrong kind. You're right that you "obviously" mean `'[]`, but this would require type-directed name resolution, which GHC does not support. This all works for `True` because there is no type named `True`. (If there were -- try declaring one! -- then your `True` example wouldn't work.) As for `TypeApplications` quantification: if you have mentioned the name of the type/kind variable in the text of your program, it is available for quantification. That's the simple rule, and there are no exceptions (barring bugs in implementation, of which there are several). So, for `foo :: forall (x :: k). ...`, both `k` and `x` are available for visible type application. GHC quantifies the variables in left-to-right order and then does a stable topological sort, putting depended-on variables before their dependencies. (A topological sort is a sort that puts depended-on things before dependencies, and "stable" here means that there is no extra violations of the left-to-right ordering of quantification.) In this case, we get `k` and then `x`. This is explained in the manual [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... #visible-type-application here]. I'm happy to take concrete suggestions for improvement, either of the manual or of error messages here. Or, of course, we can debate whether the current behavior is desired -- I'm certainly not wedded to it, but it does seem like a good compromise between the availability of visible type application and need to write `forall` a lot. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12569#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12569: TypeApplications allows instantiation of implicitly-quantified kind variables -------------------------------------+------------------------------------- Reporter: vagarenko | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Keywords: Resolution: | TypeApplications 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 adamgundry): Ah, I imagined that the left-to-right collection and topological sorting of variables applied only when there wasn't an explicit `forall`. My expectation was that if the user gives an explicit `forall`, only the binding occurrences would be available for visible type application. Thus `forall (x :: k)` would make `x` available alone, whereas `forall k (x :: k)` would make both `k` and `x` available. I think this alternative would be better, because otherwise there is no way to get at `forall {k} (x :: k)`, is there? Unless we permit visibility annotations in concrete syntax, I suppose... In any case, this deserves explicit mention in the manual, including the `forall (x :: k)` example, whichever treatment it ends up getting. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12569#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC