Opened 12 months ago
Closed 6 months 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 )
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 12 months ago by
Summary: | Location of `forall` matters with higher-rank kind polymorphism → Location of `forall` matters with kind polymorphism |
---|
comment:2 Changed 12 months ago by
Description: | modified (diff) |
---|
comment:3 Changed 12 months ago by
Summary: | Location of `forall` matters with kind polymorphism → Location of `forall` matters with higher-rank kind polymorphism |
---|
comment:4 Changed 12 months ago by
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 12 months ago by
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 12 months ago by
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 forall
s 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 12 months ago by
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 12 months ago by
I suppose you're implying that this ticket become the first bullet. Then, yes.
comment:10 Changed 6 months ago by
Differential Rev(s): | → Phab:D3860 |
---|---|
Status: | new → patch |
comment:12 Changed 6 months ago by
Description: | modified (diff) |
---|---|
Milestone: | → 8.4.1 |
Resolution: | → fixed |
Status: | patch → closed |
I don't think we have a very consistent story for higher-rank polymorphism at the kind level. The kind of C is
which has higher rank.
I'm interested in your use-cases for this.