Opened 7 months ago

Closed 5 months ago

Last modified 5 months ago

#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 7 months ago by RyanGlScott

Cc: goldfire added

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

comment:2 Changed 7 months 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 7 months 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 7 months 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 7 months 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 7 months ago by simonpj (previous) (diff)

comment:6 Changed 7 months ago by goldfire

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

comment:7 Changed 7 months ago by RyanGlScott

Keywords: CUSKs added

comment:8 Changed 7 months ago by bgamari

Owner: set to goldfire

comment:9 Changed 7 months 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 7 months 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 6 months 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 6 months ago by goldfire

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

comment:13 Changed 6 months ago by RyanGlScott

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 6 months ago by RyanGlScott

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:15 Changed 5 months ago by Richard Eisenberg <rae@…>

In 030211d2/ghc:

Kind-check CUSK associated types separately

Previously, we kind-checked associated types while while still
figuring out the kind of a CUSK class. This caused trouble, as
documented in Note [Don't process associated types in kcLHsQTyVars]
in TcTyClsDecls. This commit moves this process after the initial
kind of the class is determined.

Fixes #15142.

Test case: indexed-types/should_compile/T15142.hs

comment:16 Changed 5 months ago by goldfire

Status: newmerge
Test Case: indexed-types/should_compile/T15142

Fixed now. Please merge.

comment:17 Changed 5 months ago by simonpj

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 does T? Well hsDeclHasCusk reports True for the class decl, without even looking at T. This seems wrong.

What is the CUSK status of T? Apparently famDeclHasCusk 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 about type family F (a :: k1 k2) :: *?

  • 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.

I guess that we are defaulting kind variables to *? Well not to *, because we might have class 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 5 months ago by goldfire

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 5 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:20 Changed 5 months ago by simonpj

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 5 months ago by goldfire

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 5 months ago by simonpj

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 5 months ago by goldfire

I fully agree with comment:22, including the "Ugh" and not changing it now.

Note: See TracTickets for help on using tickets.