Opened 2 years ago

Closed 2 years ago

Last modified 2 years ago

#14348 closed bug (invalid)

Poly-kinded definitions silently introduce extra type arguments captured by TypeApplications

Reported by: gallais Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeApplications Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The first type argument of a poly-kinded definition is not the one explicitly quantified over in the definition but rather the implicitly inserted kind.

This leads to the puzzling error message "Expected a type, but ‘a’ has kind ‘k’" when ghc actually expected a kind.

{-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-}

data EQ :: k -> k -> * where
  Refl :: EQ a a

data Wrap (a :: k) = Wrap (EQ a a)

wrap :: forall (a :: k). Wrap a
wrap = Wrap @a Refl -- fails
-- wrap = Wrap @k @a Refl -- works

Change History (4)

comment:1 Changed 2 years ago by RyanGlScott

Keywords: TypeApplications added
Resolution: invalid
Status: newclosed

This is expected behavior. As noted in the users' guide, GHC determines the order of arguments for type applications by doing a stable topological sort on the user-written type variables, keeping kind variables before type variables. Since k is user-written, this means it's available for type application, and since it's the kind of a, k comes before a.

If you don't want k to be available for type application, then you can do so by not writing it explicitly:

{-# LANGUAGE GADTs, PolyKinds, ScopedTypeVariables, TypeApplications #-}

data EQ :: k -> k -> * where
  Refl :: EQ a a

data Wrap a = Wrap (EQ a a)

wrap :: forall a. Wrap a
wrap = Wrap @a Refl

comment:2 Changed 2 years ago by gallais

If it's expected behaviour then I suppose what I'd really like is a distinction between "user-written" and "user-introduced". So that I may keep the kind annotations (which are helpful documentation when the kinds are complicated) whilst not having these extra arguments.

E.g.

data Wrap (k :: Kind) (a :: k)  -- user introduced: can be explicitly set via @
data Wrap (a :: k)              -- user written: cannot be explicitly set via @

wrap :: forall k (a :: k). Wrap a -- user introduced
wrap :: forall (a :: k). Wrap a   -- user written

comment:3 Changed 2 years ago by RyanGlScott

I believe what you are looking for is explicit specificity. This is a GHC "proposal" that isn't fully baked yet, or even been formally proposed yet—I'm only showing this to you since you asked nicely ;)

This would allow you to write:

data Wrap {k} (a :: k)

To tell GHC to treat k as though it were inferred (even though it's technically written in the source) and thus not available for visible type application.

comment:4 Changed 2 years ago by gallais

This looks great!

Note: See TracTickets for help on using tickets.