GHC panic when calling typeOf on a promoted data constructor

changed weight to 7

added Tbug Trac import typechecker labels

changed milestone to %8.0.1

I'm going to set the milestone to 8.0.1, since this affects the upcoming GHC 8.0 and I'd hate to see so much Typeable-related code break. Please change the milestone if you disagree.

I dug a little more into the issue, and it looks like the issue is specifically with typeOf, not, say, typeRep. Compare:

$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160108: http://www.haskell.org/ghc/  :? for help
λ> :set -XDataKinds
λ> :m Data.Proxy Data.Functor.Compose Data.Typeable
λ> typeRep (Proxy :: Proxy 'Compose)
'Compose
λ> typeRep (Proxy :: Proxy 'Just)
'Just
λ> typeRep (Proxy :: Proxy 'Proxy)
'Proxy

versus

λ> typeOf (Proxy :: Proxy 'Compose)
ghc: panic! (the 'impossible' happened)
  (GHC version 8.1.20160108 for x86_64-unknown-linux):
        piResultTy
  *
  TYPE 'Lifted *

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

λ> typeOf (Proxy :: Proxy 'Just)
Proxy (TYPE 'Lifted -> Maybe (TYPE 'Lifted)) 'Just
λ> typeOf (Proxy :: Proxy 'Proxy)
Proxy (Proxy (TYPE 'Lifted) (TYPE 'Lifted)) 'Proxy

Those last two results definitely look funny. I'm guessing that the issue pertains to levity polymorphism. I'll try to see what I can find about how typeOf works.

I still haven't figured out what's going on with typeOf (Proxy :: Proxy 'Compose), but we can at least be comforted by the fact that executing it wasn't possible before GHC 8.0, since Compose is poly-kinded. The "regression" here is that * now shows up as TYPE 'Lifted, which I don't think is desirable. I've opened D1757 to fix that.

Trac metadata

Trac field	Value
Differential revisions	- → D1757

Trac metadata

Trac field	Value
Version	8.1 → 8.0.1-rc1

mentioned in commit 65b810bd

changed weight to 10

assigned to @bgamari

Trac metadata

Trac field	Value
Priority	high → highest

This fails,

{-# LANGUAGE DataKinds #-}
import Data.Typeable
import Data.Functor.Compose
main :: IO ()
main = print $ typeOf (undefined :: Proxy 'Compose)

with a compiler panic due to TcInteract.mk_typeable_pred calling typeKind on an ill-kinded type, TYPE 'Lifted (TYPE 'Lifted *) -> Compose * * *. Note the application TYPE 'Lifted (TYPE 'Lifted *), which oversaturates TYPE. The problem here is apparently that the kind variables of Compose are all instantiated with * with -XNoPolyKinds I haven't yet determined where this occurs.

I believe this is happening in TcMType.quantifyTyVars.

Oh dear.

Something seems terribly terribly wrong.

newtype Compose (f :: k -> *) (g :: k1 -> k) (a :: k1)
  = Compose {getCompose :: f (g a)}

This gives Compose :: forall k k1. (k -> *) -> (k1 -> k) -> k1 -> *. But your code above has three *s passed to Compose. Somehow the third one is wrong. (I think the first two are correct, as set in quantifyTyVars. I'm unconvinced that quantifyTyVars is to blame.) GHC is getting duped into thinking * :: * -> *, which would, actually, make the TYPE 'Lifted (TYPE 'Lifted *) bit well kinded.

I've no clue where this is going wrong, but it's going wrong rather spectacularly. My next step would be -ddump-tc-trace -fprint-explicit-kinds and search for the first occurrence of Compose * * *.

*Disclaimer**: The following commentary is dangerously ignorant. I've glanced at a few papers and read a bit of code but otherwise have vanishingly little knowledge about the type checker.

I'm looking at this slightly easier example (which still replicates the failure),

{-# LANGUAGE PolyKinds #-}

module Other where

data Other (f :: k -> *) (a :: k) = Other (f a)

{-# LANGUAGE DataKinds #-}
module Main where

import Data.Typeable
import Other

main :: IO ()
main = let a = typeOf (undefined :: Proxy 'Other) in return ()

As before enabling PolyKinds in Main results in the expected insoluble Typeable error.

-ddump-tc-trace -fprint-explicit-kinds produces the following suspicious output,

decideKindGeneralisationPlan
  type: (Proxy k1_aJt[tau:5] ('Other k_aJB[tau:5] f_aJC[tau:5] a_aJD[tau:5] |> <f_aJC[tau:5] a_aJD[tau:5] -> Other k_aJB[tau:5] f_aJC[tau:5] a_aJD[tau:5]>_N) |> <*>_N)
  ftvs: [k1_aJt[tau:5], f_aJC[tau:5], a_aJD[tau:5], k_aJB[tau:5]]
  should gen? True
writeMetaTyVar k_aJB[tau:5] :: * := *
writeMetaTyVar f_aJC[tau:5] :: k_aJB[tau:5] -> * := *
writeMetaTyVar a_aJD[tau:5] :: k_aJB[tau:5] := *

If I'm interpreting this correctly f (which is of kind k -> *) is being instantiated as *.

I'm going to eat some food; more later.

Easier example is good (comment:11).

Hint: always debug a compiler built with -DDEBUG. My build shows

decideKindGeneralisationPlan
  type: (Proxy
           k1_aCf[tau:5]
           ('Other
              k_aCn[tau:5]
              f_aCo[tau:5]
              a_aCp[tau:5] |> <f_aCo[tau:5] a_aCp[tau:5]
                               -> Other k_aCn[tau:5] f_aCo[tau:5] a_aCp[tau:5]>_N) |> <*>_N)
  ftvs: [k1_aCf[tau:5], f_aCo[tau:5], a_aCp[tau:5], k_aCn[tau:5]]
  should gen? True
writeMetaTyVar k_aCn[tau:5] := *
writeMetaTyVar f_aCo[tau:5] := *
WARNING: file compiler\typecheck\TcMType.hs, line 553
  Ill-kinded update to meta tyvar
    f_aCo[tau:5] :: k_aCn[tau:5] -> *
                    * -> * := * :: *
                                   *
writeMetaTyVar a_aCp[tau:5] := *
quantifyTyVars
  globals: []
  nondep: []
  dep: [k_aCn[tau:5], f_aCo[tau:5], a_aCp[tau:5]]
  dep2: []
  quant_vars: []

Note the WARNING.

The bug is this code in quantifyTyVars:

             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
             -- may make quantifyTyVars return a shorter list
             -- than it was passed, but that's ok
       ; poly_kinds <- xoptM LangExt.PolyKinds
       ; dep_vars2 <- if poly_kinds
                      then return dep_kvs
                      else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
                                    is_meta kv = isTcTyVar kv && isMetaTyVar kv

                              ; mapM_ defaultKindVar meta_kvs
                              ; return skolem_kvs }  -- should be empty

But in this case the variables we are quantifying over (I hardly know whether to call them type or kind variables now) are:

k_aCn :: *
f_aCo :: k_aCn -> *
a_aCp :: k_aCn

These appear in the user-written type signature which elaborates to:

Proxy ... (Other k_aCn f_aCo a_aCp)

It's clearly NOT RIGHT in the non-poly-kind case to default the "kind" variables to *. I guess we have to use Any in the same way that we do for types.

Can't do more tonight. Richard how are you set?

Before I forget there is a bug in decideKindGeneralisationPlan, which is taking the free vars of an unzonked type. But I don't understand that function really.

Yech.

First off, let's rename the data constructor and type constructor differently. I got quite confused about that!

data Ty (f :: k -> *) (a :: k) = Con (f a)

This produces

Ty :: forall k. (k -> *) -> k -> *
Con :: forall k (f :: k -> *) (a :: k). (f a) -> Ty k f a

The question is: how should we interpret Proxy 'Con with -XNoPolyKinds?

The old rule for -XNoPolyKinds was "set all kind variables to *", which is still what quantifyTyVars is doing. This used to make sense, because all kind variables used to have sort BOX, never something like BOX -> BOX. But those halcyon days are now gone.

I suppose it would be reasonable to set all kind variables of kind * to be *, and use Any for the others. We don't want to just use Any all the time, because that wouldn't be backwards compatible and defaulting to * is quite sensible.

The other reasonable way forward is to issue an error at Proxy 'Con without having more direction. For example, the user could say Proxy ('Con :: Maybe Bool -> Ty * Maybe Bool) to get the right instantiation.

I actually prefer the "issue an error" option. The user could use a kind signature, but more likely should just enable -XPolyKinds. Using a promoted data constructor taken from a polykinded datatype without -XPolyKinds is asking for trouble.

I'm happy to put this change in when I get to rounding up these tickets.

I'm very confused. Why would we error in the case of calling print (typeOf (Proxy :: Proxy 'Comp)) whenever -XNoPolyKinds is enabled, whereas something like print (typeOf (Proxy :: Proxy 'Proxy)) is OK? The latter currently yields "Proxy (Proxy * *) 'Proxy" when -XNoPolyKinds is on (or is this a bug?).

Proxy :: Proxy 'Proxy should also be an error in my "issue an error" option. It's a use of a promoted data constructor of a datatype whose type parameters are not all *.

To be honest, -XNoPolyKinds always confuses me now. :)

Indeed I have also wondered how NoPolyKinds is supposed to behave.

In fact, this is something that could probably use more explanation in the users guide. We discuss the behavior of -XPolyKinds in great depth but hardly mention how poly-kinded types should behave in modules with -XNoPolyKinds.

assigned to @rae and unassigned @bgamari

I suppose it would be reasonable to set all kind variables of kind * to be *, and use Any for the others. We don't want to just use Any all the time, because that wouldn't be backwards compatible and defaulting to * is quite sensible. The other reasonable way forward is to issue an error at Proxy 'Con without having more direction

I think I favour:

Default kind vars of kind * to *
Don't default others; instead error.

But note that if we have {k1:k2, k2:*} then defaulting k2 to * might mean we could then default k1.

We do need to do deafulting somehow because even without PolyKinds consider

data T f a = MkT (f a)

We get {f :: k -> *, a :: k} and we can't reject the program.

Anyway, Richard, thanks for saying you'll get to it.

Simon

There is a patch for this in goldfire's branch which he'll hopefully submit soon.

mentioned in commit 84c773e1

Trac metadata

Trac field	Value
Test case	- → dependent/should_fail/T11334

added 1 deleted label

closed

Merged #11334 (closed) as 44a95c6f.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

removed 1 deleted label

mentioned in issue #11715 (closed)

mentioned in commit f8ab5754

added compiler crash label

added Phighest label

GHC panic when calling typeOf on a promoted data constructor

Child items 0

Activity

Trac field	Value
Version	8.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	high
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	goldfire
Operating system
Architecture