#15142 closed bug (fixed)
GHC HEAD regression: tcTyVarDetails
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | highest | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | TypeInType, TypeFamilies, CUSKs | Cc: | goldfire |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | indexed-types/should_compile/T15142 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
This regression prevents the generic-lens
library from building. Here is a minimized test case:
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class ListTuple (tuple :: Type) (as :: [(k, Type)]) where type ListToTuple as :: Type
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.5.20180511 for x86_64-unknown-linux): tcTyVarDetails co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *) Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
Change History (23)
comment:1 Changed 5 months ago by
Cc: | goldfire added |
---|
comment:2 Changed 5 months ago by
Some more observations about this:
- If you swap out
TypeInType
for justDataKinds
andPolyKinds
, then the program no longer panics, soTypeInType
appears to be critical in triggering this panic. - If you try and give the parameter to
ListToTuple
an explicit kind signature:
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class ListTuple (tuple :: Type) (as :: [(k, Type)]) where type ListToTuple (as :: [(k, Type)]) :: Type
Then this will typecheck on GHC 8.4.2, but on HEAD it will give an error message:
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:9:29: error: • Expected a type, but ‘k’ has kind ‘k0’ • In the kind ‘[(k, Type)]’ | 9 | type ListToTuple (as :: [(k, Type)]) :: Type | ^
comment:3 Changed 5 months ago by
Further observations:
MultiParamTypeClasses
is also important to triggering this, since this panics:
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b
But not this:
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (b :: k) where type T b
- The order of arguments to
C
, as well as the exact kind signatures given to them, also appears to be important, as none of the following panics:
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C1 (b :: k) (a :: Type) where type T1 b class C2 b (a :: Type) where type T2 b class C3 b a where type T3 b class C4 (b :: k) a where type T4 b class C5 a (b :: k) where type T5 b class C6 (a :: Type) b where type T6 b class C7 a b where type T7 b
comment:4 Changed 5 months ago by
Comparing the results of -ddump-tc-trace
on this program:
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b
On GHC 8.4.2, we have:
kcTyClGroup: initial kinds [r1xu :-> ATcTyCon C :: forall k. * -> k -> Constraint, r1xA :-> ATcTyCon T :: forall k. k -> *]
But on GHC HEAD, we have:
kcTyClGroup: initial kinds C :: forall k. * -> k -> Constraint T :: forall (k :: k_a1zm[tau:1]) (co :: k_a1zm[tau:1] GHC.Prim.~# *). (k |> {co_a1zq}) -> *
And indeed, tcTyVarDetails
appears to be panicking on co
. But I haven't the foggiest idea of what it's doing there...
comment:5 Changed 5 months ago by
Oh dear, there are lots of thigs wrong here. I looked at
{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind class C (a :: Type) (b :: k) where type T b
- First,
C
has a CUSK. But doesT
? WellhsDeclHasCusk
reports True for the class decl, without even looking atT
. This seems wrong.
C
has a CUSK, but inclass C (a :: Type) (b :: k)
, I'm not sure how we get to know thatk :: Type
. Yet, without thatC
would not have a CUSK.
getInitialKinds
returns this very bogus kind forT
:kcTyClGroup: initial kinds C :: forall k. * -> k -> Constraint T :: forall (k :: k_aWH[tau:1]) (co :: k_aWH[tau:1] GHC.Prim.~# *). (k |> {co_aWL}) -> *
- What is that
co
binder? It's created in the mysteriouskcLHsQTyVars
function, which does something very likequantifyTyVars
, but by steam. It usestyCoVarsOfTypeWellScoped
, but neglects to filter out coercion variables; hence the bugos quantification overco_aWL
.
I'm reluctant to reach for a quick fix here. It all looks very dodgy to me. The getInitialKinds
function, which is the bit misbehaving here, should be very simple:
- For CUSKs, the idea is that it's a complete, user-specified kind, just like a top-level type signature for a term variable. II expect to do something very akin to
tcHsSigType
: that is, type-check the kind, solve any constraints that arise, and kind-generalise the result. It's made a bit trickier by the fact that instead of aLHsSigType
likeforall a. a->a
we have someLHsQTyVars
likedata T (a :: k) (b :: *)
. But it's basically all one kind signature, pretty much the same asforall (a::k) (b::*). blah
- For non-CUSKs, we can safely simply make
T :: kappa
, without looking at the declaration at all! We can perhaps save ourselves a bit of fruitless unification by seeing that if itsdata T (a :: ...) (b :: ...)
then we can makeT :: kappa1 -> kappa2 -> *
. But we don't have to look into those "..." parts; that's going to happen later. NosolveEqualities
for non-CUSKs.
PS: "later" for the "..." parts means
kcTyClTyVars
; and that currently ignores the signature; we'd need to change that.
- Associated types should not be allowed to mess things up! They must be treated as CUSK-ish only if they are in fact complete. Fundamentally, the same rules should apply: every type variable should be annotated. But maybe we can make an exception for variables from the parent class, if the parent class has a CUSK. Eg
class C (a :: *) where type F a (b :: * -> *) :: *
Here perhaps we can allowa
not to be annotated inF
's defn because it comes fromC
which itself has a CUSK.
The present code does not do this, and it's buggy as this ticket shows. Let's discuss.
comment:6 Changed 5 months ago by
Oh dear is right. No time to look right now. Will do so next week.
comment:7 Changed 5 months ago by
Keywords: | CUSKs added |
---|
comment:8 Changed 5 months ago by
Owner: | set to goldfire |
---|
comment:9 Changed 5 months ago by
Simon says: when there is a CUSK, quantify over any free kind variables. Example at the term level
f :: forall (a :: Proxy k). Proxy a -> Int
Then we infer (notice the k2
):
f :: forall k2 (k :: k2). forall (a :: Proxy k). Proxy a -> Int
So similarly at tke type level if we have this CUSK
data T (a :: Proxy k) :: Proxy a -> Type where ...
we should quantify over the kind to get
T :: forall k2 (k :: k2). forall (a :: Proxy k). Proxy a -> Type
This would require changing code in the CUSK case of kcLHsQTyVars
, which currently calls report_non_cusk_tvs
to complain. Instead, generalise.
comment:10 Changed 4 months ago by
For non-CUSKs, we can safely simply make T :: kappa, without looking at the declaration at all!
Actually this is not true, as things stand. This accepted:
data T k (a::k) = MkT (Proxy (T * Int)) (Proxy (T (*->*) Maybe))
But T
does not have a CUSK, and if we assigned it the mono-kind kappa
, the recursive definition would be rejected.
So currently we are cleverly (and somewhat accidentally) accepting a recursive definition with a partial kind signature.
I think we should just reject this definition unless you write a CUSK. Specifying exactly what is and what is not accepted would be ... difficult.
comment:11 Changed 4 months ago by
This goes back to the kind inference debate we had when working on #14066. The debate is memorialized here, toward the top.
Suppose we have
data Proxy (k :: Type) (a :: k) = Proxy -- NB: CUSK
Do we accept
type ProxySym k a = Proxy k a data ProxyData k a = MkProxyData (Proxy k a)
Related are your thoughts on #14847
comment:12 Changed 4 months ago by
Some thoughts have been written up here. But there's no real progress on what the right answer is.
comment:13 Changed 4 months ago by
I have good news and bad news.
The bad news is that this still does not typecheck on GHC HEAD.
The good news is that it no longer panics! It now gives the following, lovely error message:
$ /opt/ghc/head/bin/ghci Bug.hs GHCi, version 8.7.20180621: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:8:42: error: • Expected a type, but ‘k’ has kind ‘k’ • In the kind ‘[(k, Type)]’ | 8 | class ListTuple (tuple :: Type) (as :: [(k, Type)]) where | ^
So that's... nice, I guess.
comment:14 Changed 4 months ago by
As far as I can tell, the only available workaround for this issue is to explicitly quantify k
, like so:
class ListTuple (tuple :: Type) k (as :: [(k, Type)]) where type ListToTuple as :: Type
generic-lens
may need to employ this hack if this issue hasn't been fixed by 8.6.1's release.
comment:16 Changed 3 months ago by
Status: | new → merge |
---|---|
Test Case: | → indexed-types/should_compile/T15142 |
Fixed now. Please merge.
comment:17 Changed 3 months ago by
In 030211d2/ghc:
Richard, I like this. The code is simpler, kcLHsQTyVars
has a simpler signature. All good.
But you did not respond to these points from comment:5:
- First,
C
has a CUSK. But doesT
? WellhsDeclHasCusk
reports True for the class decl, without even looking atT
. This seems wrong.
What is the CUSK status of
T
? ApparentlyfamDeclHasCusk
returns True if the enclosing class has a CUSK, but is that right? There's a comment "all un-associated open families have CUSKs" which I don't understand.
Ah... I see from the manual that we treat open families as CUSK-ish by defaulting. We should have a Note to explain the rules -- or I suppose a Note that summarises and points clearly to the manual as the reference. But why do we default here? It seems inconsistent with (say)
data T a b = ...
. Is it just an arbitrary choice of convenience? What abouttype family F (a :: k1 k2) :: *
?
C
has a CUSK, but inclass C (a :: Type) (b :: k)
, I'm not sure how we get to know thatk :: Type
. Yet, without thatC
would not have a CUSK.
I guess that we are defaulting kind variables to
*
? Well not to*
, because we might haveclass C (a :: k1 k2) where ...
After typing this in I realise that all I'm seeking is a clearer exposition of the CUSK rules.
comment:18 Changed 3 months ago by
The rules are in the manual. There is also Note [Complete user-supplied kind signatures]
, but I see now that it's a bit out of date. To avoid duplication, I'll just have the Note point to the manual.
comment:19 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged with d0dfc5cc4859a07778bc674eb865811616d4d6c6.
comment:20 Changed 3 months ago by
Richard, I have augmented the Note as below. Do you agree with it?
On the last point, we say that this does not have a CUSK (taken from dependent/should_compile/kind_levels
):
data C :: B a -> *
But why not? The lexical-forall rule means that it's equivalent to
data C :: forall a. B a -> *
which now does have a CUSK. Either the rule needs more justification, or its over-restrictive.
Here's the new Note:
{- Note [CUSKs: complete user-supplied kind signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We kind-check declarations differently if they have a complete, user-supplied kind signature (CUSK). This is because we can safely generalise a CUSKed declaration before checking all of the others, supporting polymorphic recursion. See ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy and #9200 for lots of discussion of how we got here. PRINCIPLE: a type declaration has a CUSK iff we could produce a separate kind signature for it, just like a type signature for a function, looking only at the header of the declaration. Examples: * data T1 (a :: *->*) (b :: *) = .... -- Has CUSK; equivalant to T1 :: (*->*) -> * -> * * data T2 a b = ... -- No CUSK; we do not want to guess T2 :: * -> * -> * -- becuase the full decl might be data T a b = MkT (a b) * data T3 (a :: k -> *) (b :: *) = ... -- CUSK; equivalent to T3 :: (k -> *) -> * -> * -- We lexically generalise over k to get -- T3 :: forall k. (k -> *) -> * -> * -- The generalisation is here is purely lexical, just like -- f3 :: a -> a -- means -- f3 :: forall a. a -> a * data T4 (a :: j k) = ... -- CUSK; equivalent to T4 :: j k -> * -- which we lexically generalise to T4 :: forall j k. j k -> * -- and then, if PolyKinds is on, we further generalise to -- T4 :: forall kk (j :: kk -> *) (k :: kk). j k -> * -- Again this is exactly like what happens as the term level -- when you write -- f4 :: forall a b. a b -> Int NOTE THAT * A CUSK does /not/ mean that everything about the kind signature is fully specified by the user. Look at T4 and f4: we had do do kind inference to figure out the kind-quantification. But in both cases (T4 and f4) that inference is done looking /only/ at the header of T4 (or signature for f4), not at the definition thereof. * The CUSK completely fixes the kind of the type constructor, forever. * The precise rules, for each declaration form, for whethher a declaration has a CUSK are given in the user manual section "Complete user-supplied kind signatures and polymorphic recursion". BUt they simply implement PRINCIPLE above. * Open type families are interesting: type family T5 a b :: * There simply /is/ no accompanying declaration, so that info is all we'll ever get. So we it has a CUSK by definition, and we default any un-fixed kind variables to *. * Associated types are a bit tricker: class C6 a where type family T6 a b :: * op :: a Int -> Int Here C6 does not have a CUSK (in fact we ultimately discover that a :: * -> *). And hence neither does T6, the associated family, because we can't fix its kind until we have settled C6. Another way to say it: unlike a top-level, we /may/ discover more about a's kind from C6's definition. * A data definition with a top-level :: must explicitly bind all kind variables to the right of the ::. See test dependent/should_compile/KindLevels, which requires this case. (Naturally, any kind variable mentioned before the :: should not be bound after it.)
comment:21 Changed 3 months ago by
I agree with everything in that Note.
Why have the explicit forall
? Because perhaps the user wants inference, not CUSKness. By making a decision based on the forall
, then the user can get what they want. For example:
data T1 :: k1 k2 -> Type where MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 x
There are two possible meanings for this. Meaning 1 (M1):
T1 :: forall (k1 :: Type -> Type) (k2 :: Type). k1 k2 -> Type MkT1 :: forall (k1 :: Type -> Type) (k2 :: Type) (x :: k1 k2). T1 k1 k2 x
Meaning 2 (M2):
T1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k). k1 k2 -> Type MkT1 :: forall (k :: Type) (k1 :: k -> Type) (k2 :: k) (x :: k1 k2). (k ~# Type) -> T1 k k1 k2 x
In M1, we do not quantify T1
's kind further, and the data constructor is not GADT-like. In M2, though, we do generalize, making MkT1
a GADT constructor packing an equality.
M1 is what happens if T1
does not have a CUSK. M2
is what happens when it does. Having CUSKness depend on the presence of the forall
allows users to choose which of these interpretations to use. We could absolutely, remove it, but then I don't know how to write T1
with meaning M1.
comment:22 Changed 3 months ago by
comment:21 is quite debatable as Richard and I agreed on the phone today. It's easier to understand at the term level. Suppose you write
f :: forall a b. a b -> Int f x = let y :: b; y = undefined in 5
With -XPolyKinds
the type signature is generalised to
f :: forall k. (a :: k->*) (b :: k). a b -> Int
But then the definition of f
is less polymorphic than that!
The use of y::b
forces b::*
; but the signature says b::k
, so
the definition is rejected.
By omitting a forall
in the final item of the CUSK comment above,
the curren system says "not a CUSK", so inference can do its magic.
But we can't currently do that in terms. Except perhaps by making
a partial type signature like
f :: forall a b. a b -> _
for which inference takes place.
The final bullet in the Note, about data types, amounts to a very ad-hoc way of signaling "don't use a CUSK". Ugh.
We decided to leave it as-is for now, because we'll end up revisiting all this when we introduce separate kind signatures for type constructors.
comment:23 Changed 3 months ago by
I fully agree with comment:22, including the "Ugh" and not changing it now.
This was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (
Track type variable scope more carefully.
).