Opened 2 years ago

Closed 21 months ago

Last modified 21 months ago

#11334 closed bug (fixed)

GHC panic when calling typeOf on a promoted data constructor

Reported by: RyanGlScott Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler (Type checker) Version: 8.0.1-rc1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case: dependent/should_fail/T11334
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1757
Wiki Page:

Description

Here's what I did in GHCi to trigger the panic:

$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160101: http://www.haskell.org/ghc/  :? for help
λ> :set -XDataKinds
λ> :m Data.Typeable Data.Functor.Compose
λ> typeOf (Proxy :: Proxy 'Compose)
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160101 for x86_64-unknown-linux):
        piResultTy
  *
  TYPE 'Lifted *

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

Enabling -XPolyKinds doesn't trigger the error, though; #10343 will be triggered instead:

λ> :set -XPolyKinds
λ> typeOf (Proxy :: Proxy 'Compose)

<interactive>:5:1: error:
    • No instance for (Typeable a0) arising from a use of ‘typeOf’
    • In the expression: typeOf (Proxy :: Proxy Compose)
      In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)

Change History (23)

comment:1 Changed 2 years ago by RyanGlScott

Keywords: TypeInType added

comment:2 Changed 2 years ago by RyanGlScott

Milestone: 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.

comment:3 Changed 2 years ago by RyanGlScott

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.

comment:4 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D1757

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 Phab:D1757 to fix that.

comment:5 Changed 2 years ago by thomie

Version: 8.18.0.1-rc1

comment:6 Changed 2 years ago by Ben Gamari <ben@…>

In 65b810b/ghc:

Show TYPE 'Lifted/TYPE 'Unlifted as */# in Show TypeRep instance

Kind equalities changed how `*`/`#` are represented internally, which
means that showing a `TypeRep` that contains either of those kinds
produces a rather gross-looking result, e.g.,

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

We can at least special-case the `Show` instance for `TypeRep` so that
it prints `*` to represent `TYPE 'Lifted` and `#` to represent `TYPE
'Unlifted`.

Addresses one of the issues uncovered in #11334.

Test Plan: ./validate

Reviewers: simonpj, hvr, austin, goldfire, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1757

GHC Trac Issues: #11334

comment:7 Changed 23 months ago by bgamari

Owner: set to bgamari
Priority: highhighest

comment:8 Changed 23 months ago by bgamari

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.

comment:9 Changed 23 months ago by bgamari

I believe this is happening in TcMType.quantifyTyVars.

comment:10 Changed 23 months ago by goldfire

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

comment:11 Changed 23 months ago by bgamari

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.

comment:12 Changed 23 months ago by simonpj

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?

comment:13 Changed 23 months ago by simonpj

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.

comment:14 Changed 23 months ago by goldfire

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.

comment:15 Changed 23 months ago by RyanGlScott

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?).

comment:16 Changed 23 months ago by goldfire

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. :)

comment:17 Changed 23 months ago by bgamari

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.

comment:18 Changed 23 months ago by simonpj

Owner: changed from bgamari to goldfire

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

comment:19 Changed 22 months ago by bgamari

Status: newpatch

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

comment:20 Changed 21 months ago by Richard Eisenberg <eir@…>

In 84c773e/ghc:

Fix #11334.

Now we fail when trying to default non-*-kinded kind variables
with -XNoPolyKinds.

test case: dependent/should_fail/T11334

[skip ci]

comment:21 Changed 21 months ago by goldfire

Status: patchmerge
Test Case: dependent/should_fail/T11334

comment:22 Changed 21 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Last edited 21 months ago by bgamari (previous) (diff)

comment:23 Changed 21 months ago by Richard Eisenberg <eir@…>

In f8ab575/ghc:

Rename test for #11334 to 11334b, fixing conflict
Note: See TracTickets for help on using tickets.