Opened 13 months ago
Last modified 9 months ago
#15869 new bug
Discrepancy between seemingly equivalent type synonym and type family
Reported by: | RyanGlScott | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 8.6.2 |
Keywords: | TypeFamilies, TypeInType, VisibleDependentQuantification | 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 (last modified by )
Consider the following code:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE LiberalTypeSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind type KindOf1 (a :: k) = k type family KindOf2 (a :: k) :: Type where KindOf2 (a :: k) = k data A (a :: Type) :: a -> Type type family Apply1 (f :: KindOf1 A) (a :: Type) (x :: a) :: Type where Apply1 f a x = f a x
Apply1
kind-checks, which is just peachy. Note that Apply1
uses KindOf1
, which is a type synonym. Suppose I wanted to swap out KindOf1
for KindOf2
, which is (seemingly) an equivalent type family. I can define this:
type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where Apply2 f a x = f a x
However, GHC rejects this!
$ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:25:10: error: • Expecting two more arguments to ‘f’ Expected kind ‘KindOf2 A’, but ‘f’ has kind ‘* -> a -> *’ • In the first argument of ‘Apply2’, namely ‘f’ In the type family declaration for ‘Apply2’ | 25 | Apply2 f a x = f a x | ^
I find this quite surprising, since I would have expected KindOf1
and KindOf2
to be functionally equivalent. Even providing explicit forall
s does not make it kind-check:
type family Apply2 (f :: KindOf2 A) -- (f :: forall a -> a -> Type) (a :: Type) (x :: a) :: Type where forall (f :: KindOf2 A) (a :: Type) (x :: a). Apply2 f a x = f a x
Although the error message does change a bit:
$ ~/Software/ghc3/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:26:20: error: • Expected kind ‘* -> a -> *’, but ‘f’ has kind ‘KindOf2 A’ • In the type ‘f a x’ In the type family declaration for ‘Apply2’ | 26 | Apply2 f a x = f a x | ^^^^^
Change History (11)
comment:2 Changed 13 months ago by
Lots of bugs here!
- I would expect
Apply1
to be rejected without an explicitforall
in the equation, giving the polytype off
.
- The error message for
Apply2
shouldn't say that it expects more arguments tof
. The rest of the error message is perhaps confusing, but it's not unreasonable.
- The version of
Apply2
with the explicitforall
in the equation should be accepted.
- In the
g
andh
withKindOf1
: Their types should beforall a -> a -> Type
, not what GHC is reporting.
- Ditto for
h
in theKindOf2
case.
Note that the inferred nature (as opposed to specified) of a
is a non-bug: when you don't write a type signature, you don't get specified variables. But of course these should be required, not invisible or specified.
comment:3 Changed 12 months ago by
Keywords: | TypeInType added |
---|
comment:4 Changed 10 months ago by
Description: | modified (diff) |
---|
comment:5 Changed 10 months ago by
While implementing visible dependent quantification (VDQ), I decided to revisit commment:2. Here are some of my findings:
- I think (4) and (5) are ultimately non-issues, at least for the time being. This is because you won't be able to define
f
(org
orh
) in the first place:
Bug.hs:17:6: error: • Illegal visible, dependent quantification in the type of a term: forall a -> a -> * (GHC does not yet support this) • In the expansion of type synonym ‘KindOf1’ In the type signature: f :: KindOf1 A | 17 | f :: KindOf1 A | ^^^^^^^^^
Since terms aren't meant to have types with VDQ in them, I don't think it's worth fretting over (4) and (5). Of course, if VDQ does ever become permitted in terms, perhaps this will pop back up.
- (1) appears to be unrelated to VDQ and is actually a quirk of
ImpredicativeTypes
. Here is an example to illustrate what I mean:
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type family F (f :: forall a. a -> Type) where F f = f Int
This doesn't typecheck:
Bug.hs:9:5: error: • Expected kind ‘forall a. a -> *’, but ‘f’ has kind ‘* -> k0’ • In the first argument of ‘F’, namely ‘f’ In the type family declaration for ‘F’ | 9 | F f = f Int | ^
However, if you enable
ImpredicativeTypes
, then it does typecheck! It's unclear to me why exactly that is, however.
comment:6 Changed 10 months ago by
If you don't have impredicative-types, then surely the example in the second bullet of comment:5 should be rejected!
But still, the error message looks deeply strange.
comment:7 Changed 10 months ago by
To be clear, I am in agreement with you that the program in the second bullet point of comment:5 should be rejected if ImpredicativeTypes
is not enabled. I am simply wondering if it being accepted with ImpredicativeTypes
enabled should count as a bug in its own right. (It's such a squirrelly extension that I can never tell whether it's working as intended or not.)
comment:8 Changed 10 months ago by
(2) might also be its own issue, since you can trigger the "expecting more arguments" error without VDQ:
{-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where type family F type family G (f :: F) where G f = f Int
$ /opt/ghc/8.6.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:8:5: error: • Expecting one more argument to ‘f’ Expected kind ‘F’, but ‘f’ has kind ‘* -> k0’ • In the first argument of ‘G’, namely ‘f’ In the type family declaration for ‘G’ | 8 | G f = f Int | ^
comment:9 Changed 10 months ago by
I wonder if (3) has anything to do with #9269? KindOf2 A
is a bit weird in that it's an application of a type family that returns forall a -> a -> Type
, which is a polymorphic type. Normally, GHC disallows that—you wouldn't be able to define type family FAA where FAA = forall a -> a -> Type
, for instance. Yet KindOf2
offers a way around this restriction, so perhaps (3) is a manifestation of GHC trying to deal with something it doesn't know how to reason about.
Then again, KindOf2 A
seems to work in other places, as comment:1 demonstrates. It's just in type family equations where things go haywire.
comment:10 Changed 10 months ago by
comment:11 Changed 9 months ago by
Keywords: | VisibleDependentQuantification added |
---|
This isn't the only discrepancy I've encountered (although this is the most prominent example that I've uncovered). Another, slightly more minor discrepancy can be found in this program:
Compiling this yields the following warnings:
Note the inferred type signatures for
g
andh
(Side note: it's a bit weird that their inferred types areforall {a}. a -> *
and not, say,forall a -> a -> *
. But that's not the main issue here.)Now, if you redefine
f
to useKindOf2
in its type signature:Recompiling the module will instead yield these warnings:
Notice that the inferred type of
g
is nowforall a -> a -> *
, whereas before it wasforall {a}. a -> *
! Quite strange. (And to make things stranger, the inferred type ofh
is different from that ofg
.)