Opened 7 months ago

Closed 5 weeks ago

#13399 closed bug (fixed)

Location of `forall` matters with higher-rank kind polymorphism

Reported by: crockeea Owned by:
Priority: normal Milestone: 8.4.1
Component: Compiler Version: 8.0.2
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D3860
Wiki Page:

Description (last modified by bgamari)

The following code fails to compile, but probably should:

{-# LANGUAGE RankNTypes, TypeInType #-}

import Data.Kind

data Foo :: forall k . (* -> *) -> k -> * -- Decl 1

class C (a :: forall k . k -> *)

instance C (Foo a) -- error on this line

with the error

• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
  In the instance declaration for ‘C (Foo a)’

Similarly, the following declarations of Foo also cause a similar error at the instance declaration:

Decl 2: data Foo :: (* -> *) -> k -> *

Decl 3: data Foo (a :: * -> *) (b :: k)

However, if I move the forall to a point after the first type parameter (which is where the instance is partially applied) thusly:

Decl 4: data Foo :: (* -> *) -> forall k . k -> *

then GHC happily accepts the instance of C.

From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the forall can be floated to the front of Decl 4. GHC should accept any of the four versions of Foo, since they are all equivalent.

Change History (12)

comment:1 Changed 7 months ago by crockeea

Summary: Location of `forall` matters with higher-rank kind polymorphismLocation of `forall` matters with kind polymorphism

comment:2 Changed 7 months ago by crockeea

Description: modified (diff)

comment:3 Changed 7 months ago by simonpj

Summary: Location of `forall` matters with kind polymorphismLocation of `forall` matters with higher-rank kind polymorphism

I don't think we have a very consistent story for higher-rank polymorphism at the kind level. The kind of C is

c :: (forall k. k->*) -> Constraint

which has higher rank.

I'm interested in your use-cases for this.

comment:4 Changed 7 months ago by crockeea

Use case:

I'm working on a HOAS for a tagless final DSL. That approach uses GADTs for "interpreters" of various languages (classes). The class C in my example comes from the language for lambda abstractions in our depth-indexed language. Namely,

class LambdaD (expr :: forall k . k -> * -> *) where
  lamD :: (expr da a -> expr db b) -> expr '(da,db) (a -> b)
  appD :: expr '(da,db) (a -> b) -> expr da a -> expr db b

where expr is one of the GADT interpreters. We need to remember the depth of the input and output of the function, so we change the kind of the "depth" to a pair.

Back to this ticket:

However, I just realized you don't actually need higher-rank polymorphism to see this bug. You can do the following in GHCi:

> :set -XTypeInType
> :set -XRankNTypes
> :set -fprint-explicit-foralls
> data Bar :: forall k. (* -> *) -> k -> *
> :kind! Bar
Bar :: forall k. (* -> *) -> k -> *              -- precisely what I wrote, no surprise here
> :kind! (Bar Maybe :: forall k. k -> *)
<interactive>:1:2: error:
  • Expected kind ‘forall k. k -> *’,
      but ‘Bar Maybe’ has kind ‘k0 -> *’
  • In the type ‘(Bar Maybe :: forall k. k -> *)’

comment:5 Changed 7 months ago by RyanGlScott

Cc: goldfire added

This does indeed seem strange. Simon is right that there aren't many examples of higher-rank kinds in the wild from which to draw inspiration (OtToMH, I can only think of this example from A Dependent Haskell Triptych). But I agree that there appears to be some inconsistencies between the ways that higher-rank types and higher-rank kinds are handled.

Some other oddities: if you define this:

data Foo :: (* -> *) -> (forall k. k -> *)

and type :i Foo into GHCi, you get this back:

type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)

This seems to imply that Foo has three visible type parameters, which isn't true at all!

Moreover, this works:

data Foo :: (* -> *) -> (k -> *)
type Goo = Foo

But this does not:

data Foo :: (* -> *) -> (forall k. k -> *)
type Goo = Foo
    • Expecting two more arguments to ‘Foo’
      Expected kind ‘k0’,
        but ‘Foo’ has kind ‘(* -> *) -> forall k. k -> *’
    • In the type ‘Foo’
      In the type declaration for ‘Goo’

This seems to be exclusive to higher-rank kinds, as the type-level equivalents work just fine:

λ> let foo1 :: (* -> *) -> (k -> *); foo1 = undefined
λ> let goo1 = foo1
λ> let foo2 :: (* -> *) -> (forall k. k -> *); foo2 = undefined
λ> let goo2 = foo2

goldfire, is this expected behavior? And are these idiosyncrasies documented somewhere? I find the current behavior extremely confusing.

comment:6 Changed 7 months ago by goldfire

This is all expected behavior, for a sufficiently nuanced expectation. This behavior may be undocumented however, which would be a bug.

The problem all boils down to this: there are no type-level lambdas.

When GHC transforms the term-level f :: forall a. Int -> a -> a to have type Int -> forall a. a -> a, it does this by generating the Core \(n :: Int) @(a :: *) -> f a n, which indeed works with f of the given type and is an expression of the desired type. Note that there is a lambda there. This is impossible at the type level. Thus: type-level foralls don't "float".

The output from :i in comment:5 is an unrelated (but quite legitimate) bug.

The Foo/Goo example comes from a nice rule around higher-rank types/kinds: GHC never infers a higher-rank type (or kind). So, the first (non-higher-rank) example with Foo/Goo succeeds. The second fails, because GHC won't infer a higher-rank kind for Goo. If you make a complete user-specified kind signature by putting a top-level kind signature on the right-hand side of the Goo declaration, GHC will accept, as it no longer needs to infer a higher-rank kind.

At the term level, GHC makes an exception to the never-infer-higher-rank rule: when a term-level definition is by only one equation, and there is no type signature, GHC computes the (potentially higher-rank) type of the RHS and uses it as the type of the LHS. So, it's really the term level that's behaving strangely by accepting goo2, not the type level. Looking at this all, it seems sensible to propagate this exception to type declarations, which are required to obey the one-equation rule used at the term level.

Admittedly, the lack of "floating" makes higher-rank kinds unwieldy. I do have a second use-case though:

data (a :: k1) :~~: (b :: k2) where
  HRefl :: a :~~: a

class HTestEquality (t :: forall k. k -> Type) where
  hTestEquality :: t a -> t b -> Maybe (a :~~: b)

data TypeRep (a :: k) where  -- or, this could be the new proper Data.Reflection.TypeRep
  TInt :: TypeRep Int
  TMaybe :: TypeRep Maybe
  TApp :: TypeRep a -> TypeRep b -> TypeRep (a b)

instance HTestEquality TypeRep where
  hTestEquality TInt TInt = Just HRefl
  hTestEquality TMaybe TMaybe = Just HRefl
  hTestEquality (TApp a1 b1) (TApp a2 b2) = do
    HRefl <- hTestEquality a1 a2
    HRefl <- hTestEquality b1 b2
    return HRefl
  hTestEquality _ _ = Nothing

The need for this came up while experimenting with (prototypes of) the new TypeRep. See also this related example, necessary to power the dependently typed database example I used in my job talk.

comment:7 Changed 7 months ago by RyanGlScott

Thanks Richard, that's a tremendously helpful explanation. So to recap, there are three bugs:

  • crockeea was unable to figure out that this is expected behavior. We should document this behavior of higher-rank kinds.
  • There is a bug in how higher-rank kinds are pretty-printed (comment:5)
  • Type synonyms don't obey the "one-equation-rule" (as defined in comment:6)

Should we open separate tickets for the last two?

comment:8 Changed 7 months ago by goldfire

I suppose you're implying that this ticket become the first bullet. Then, yes.

comment:9 Changed 7 months ago by goldfire

Bullets 2 and 3 spun off as #13407 and #13408, respectively.

comment:10 Changed 6 weeks ago by goldfire

Differential Rev(s): Phab:D3860
Status: newpatch

comment:11 Changed 5 weeks ago by Ben Gamari <ben@…>

In dc42c0dc/ghc:

Fix #13399 by documenting higher-rank kinds.

Test Plan: Read it.

Reviewers: simonpj, RyanGlScott, austin, bgamari

Reviewed By: RyanGlScott

Subscribers: rwbarton, thomie

GHC Trac Issues: #13399

Differential Revision: https://phabricator.haskell.org/D3860

comment:12 Changed 5 weeks ago by bgamari

Description: modified (diff)
Milestone: 8.4.1
Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.