Opened 13 months ago
Last modified 13 months ago
#12569 new bug
TypeApplications allows instantiation of implicitly-quantified kind variables
Reported by: | vagarenko | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.0.1 |
Keywords: | TypeApplications | Cc: | adamgundry, goldfire |
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
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
Change History (3)
comment:1 Changed 13 months ago by
Cc: | adamgundry goldfire added |
---|---|
Component: | Compiler → Compiler (Type checker) |
Keywords: | TypeApplications added |
Summary: | TypeApplications doesn't allow unticked list constructors. → TypeApplications allows instantiation of implicitly-quantified kind variables |
comment:2 Changed 13 months ago by
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 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.
comment:3 Changed 13 months ago by
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.
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 fromfoo @[0]
.With a tick,
'[0]
is syntactic sugar for0 ': '[]
(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 constructorTrue
, 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 variablek
to givefoo :: forall k (x :: k) . ()
. I would expect thatk
would not be available for instantiation via a type application, but apparently it is, becausefoo @True
is rejected butfoo @Bool @True
is accepted. I think we should havefoo :: 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.