Opened 12 months ago

Closed 7 months ago

Last modified 7 months ago

#15658 closed bug (fixed)

strange inferred kind with TypeInType

Reported by: dmwit Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler Version: 8.4.2
Keywords: TypeInType, GHCProposal, VisibleDependentQuantification Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #16326 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/378
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 (9)

comment:1 Changed 12 months 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 12 months 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 12 months 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.

comment:4 Changed 7 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/378
Milestone: 8.6.18.10.1
Status: newpatch

https://gitlab.haskell.org/ghc/ghc/merge_requests/378 implements the ability to write this in the source syntax (and documents it in the users' guide).

comment:5 Changed 7 months ago by RyanGlScott

Keywords: VisibleDependentQuantification added

comment:6 Changed 7 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed

comment:7 Changed 7 months ago by simonpj

Should we have a regression test here?

comment:8 Changed 7 months ago by RyanGlScott

No. This ticket is specifically about the users' guide.

#16326 tracks the actual implementation side of things, and makes mention of the relevant regression tests.

comment:9 Changed 7 months ago by Marge Bot <ben+marge-bot@…>

In c26d299/ghc:

Visible dependent quantification

This implements GHC proposal 35
(https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst)
by adding the ability to write kinds with
visible dependent quantification (VDQ).

Most of the work for supporting VDQ was actually done _before_ this
patch. That is, GHC has been able to reason about kinds with VDQ for
some time, but it lacked the ability to let programmers directly
write these kinds in the source syntax. This patch is primarly about
exposing this ability, by:

* Changing `HsForAllTy` to add an additional field of type
  `ForallVisFlag` to distinguish between invisible `forall`s (i.e,
  with dots) and visible `forall`s (i.e., with arrows)
* Changing `Parser.y` accordingly

The rest of the patch mostly concerns adding validity checking to
ensure that VDQ is never used in the type of a term (as permitting
this would require full-spectrum dependent types). This is
accomplished by:

* Adding a `vdqAllowed` predicate to `TcValidity`.
* Introducing `splitLHsSigmaTyInvis`, a variant of `splitLHsSigmaTy`
  that only splits invisible `forall`s. This function is used in
  certain places (e.g., in instance declarations) to ensure that GHC
  doesn't try to split visible `forall`s (e.g., if it tried splitting
  `instance forall a -> Show (Blah a)`, then GHC would mistakenly
  allow that declaration!)

This also updates Template Haskell by introducing a new `ForallVisT`
constructor to `Type`.

Fixes #16326. Also fixes #15658 by documenting this feature in the
users' guide.
Note: See TracTickets for help on using tickets.