Opened 4 weeks ago

Last modified 4 weeks ago

#15658 new bug

strange inferred kind with TypeInType

Reported by: dmwit Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.4.2
Keywords: TypeInType, GHCProposal Cc:
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

This type family has a strange kind to begin with:

{-# Language TypeFamilies , TypeInType #-}
type family F f a :: a

But it gets even stranger when you ask ghci what it thinks about F:

> :k F
F :: * -> forall a -> a

There is a forall which doesn't seem to bind any variables and hasn't got the customary delimiting dot.

Change History (3)

comment:1 Changed 4 weeks ago by RyanGlScott

Keywords: TypeInType GHCProposal added

This is expected: TypeInType gives programmers a limited ability to write dependent quantification in kinds. The Inferring dependency in datatype declarations section of the users' guide documents this feature to some degree. The part that is not documented is the forall k -> bit, which I'll briefly explain here.

Here is the type family you wrote (with explicit kinds for clarity):

type family F (f :: *) (a :: *) :: a

This binds the f and a type variables, and interestingly enough, it reuses the bound a type variable later in the return kind. In other words, a is used in a dependent fashion, so the kind for F is (again, with explicit kinds for clarity):

F :: * -> forall (a :: *) -> a

This kind says that F takes two type arguments of kind * and returns a type of kind a, where a is the second type argument. Importantly, the kind of F is not * -> forall (a :: *). a, since that would imply that a is insivible (i.e., that you don't explicitly pass it as an argument to F). You can think of the use of -> versus . as indicating visible arguments versus invisible ones.

As I briefly mentioned before, this aspect of kinds is not really documented at the moment. This is partly because while you can observe these kinds in GHCi (through :kind), you cannot write them yourself (they'll simply fail to parse at the moment). This GHC proposal aims to rectify this.

comment:2 Changed 4 weeks ago by dmwit

I agree: it should be documented with some care. Here is another case worth discussing when writing the documentation.

If I try to follow your reasoning for a modified type family, say:

type family G a :: a

I reason that it should be:

G :: forall (a :: *) -> a

So without the explicit kinding, I would expect ghci to give G the kind forall a -> a. But ghci does not agree:

> :k G
G :: a

comment:3 in reply to:  2 Changed 4 weeks ago by RyanGlScott

Replying to dmwit:

So without the explicit kinding, I would expect ghci to give G the kind forall a -> a. But ghci does not agree:

> :k G
G :: a

That's due to a separate GHC bug, #14238, which has been fixed in GHC 8.6.1.

Note: See TracTickets for help on using tickets.