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 RyanGlScott

Cc: goldfire added

This was introduced in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.).

comment:2 Changed 6 weeks ago by RyanGlScott

Some more observations about this:

  • If you swap out TypeInType for just DataKinds and PolyKinds, then the program no longer panics, so TypeInType 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 RyanGlScott

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 RyanGlScott

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 simonpj

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 does T? Well hsDeclHasCusk reports True for the class decl, without even looking at T. This seems wrong.
  • C has a CUSK, but in class C (a :: Type) (b :: k), I'm not sure how we get to know that k :: Type. Yet, without that C would not have a CUSK.
  • getInitialKinds returns this very bogus kind for T:
    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 mysterious kcLHsQTyVars function, which does something very like quantifyTyVars, but by steam. It uses tyCoVarsOfTypeWellScoped, but neglects to filter out coercion variables; hence the bugos quantification over co_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 a LHsSigType like forall a. a->a we have some LHsQTyVars like data T (a :: k) (b :: *). But it's basically all one kind signature, pretty much the same as forall (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 its data T (a :: ...) (b :: ...) then we can make T :: kappa1 -> kappa2 -> *. But we don't have to look into those "..." parts; that's going to happen later. No solveEqualities 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 allow a not to be annotated in F's defn because it comes from C which itself has a CUSK.

The present code does not do this, and it's buggy as this ticket shows. Let's discuss.

Last edited 3 weeks ago by simonpj (previous) (diff)

comment:6 Changed 4 weeks ago by goldfire

Oh dear is right. No time to look right now. Will do so next week.

comment:7 Changed 4 weeks ago by RyanGlScott

Keywords: CUSKs added

comment:8 Changed 3 weeks ago by bgamari

Owner: set to goldfire

comment:9 Changed 3 weeks ago by simonpj

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 simonpj

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 goldfire

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 goldfire

Some thoughts have been written up here. But there's no real progress on what the right answer is.

Note: See TracTickets for help on using tickets.