Opened 6 weeks ago
Last modified 3 days ago
#15142 new bug
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: | |
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 (12)
comment:1 Changed 6 weeks ago by
Cc: | goldfire added |
---|
comment:2 Changed 6 weeks 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 6 weeks 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 4 weeks 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 4 weeks 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:7 Changed 4 weeks ago by
Keywords: | CUSKs added |
---|
comment:8 Changed 3 weeks ago by
Owner: | set to goldfire |
---|
comment:9 Changed 3 weeks 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 3 weeks 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 2 weeks 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 3 days ago by
Some thoughts have been written up here. But there's no real progress on what the right answer is.
This was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (
Track type variable scope more carefully.
).