Opened 3 weeks ago

Closed 10 days ago

Last modified 9 days ago

#14175 closed bug (fixed)

Panic repSplitTyConApp_maybe

Reported by: dfeuer Owned by:
Priority: normal Milestone: 8.2.2
Component: Compiler (Type checker) Version: 8.2.1
Keywords: TypeInType Cc: goldfire, RyanGlScott
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: indexed-types/should_fail/T14175
Blocked By: Blocking:
Related Tickets: #13910, #14230 Differential Rev(s):
Wiki Page:

Description

This definition panics!

{-# LANGUAGE TypeFamilies, TypeInType #-}

module Whoops where
import Data.Kind

type family PComp (k :: j -> Type) (x :: k) :: ()
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170828 for x86_64-unknown-linux):
        repSplitTyConApp_maybe
  j_aon[sk:1]
  *
  *
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type

If I make it a type synonym instead, I get a proper error as expected.

Change History (11)

comment:1 Changed 3 weeks ago by RyanGlScott

On HEAD, this gives a slightly different panic:

$ ghc5/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170818: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Whoops           ( Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170818 for x86_64-unknown-linux):
        getRuntimeRep
  j_a1tG[sk:1] :: k_a1tJ[tau:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1142:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1982:18 in ghc:Type

This is a characteristic that it shares with the program in #13910.

comment:2 Changed 3 weeks ago by RyanGlScott

Cc: RyanGlScott added

I suspect that this program (which panics after 0829821a6b886788a3ba6989e57e25a037bb6d05 on GHC HEAD) has the same underlying symptom:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C k where
  data CD :: k -> k -> *

instance C (Maybe a) where
  data CD :: (k -> *) -> (k -> *) -> *
$ inplace/bin/ghc-stage2 --interactive ../Bug.hs
GHCi, version 8.3.20170818: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( ../Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170818 for x86_64-unknown-linux):
        getRuntimeRep
  k_a1v3[sk:1] :: k_a1vl[tau:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1142:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1982:18 in ghc:Type

comment:3 Changed 3 weeks ago by simonpj

Thanks. I have a fix for this on my laptop. Not quite daring to push during ICFP lest I break something (alghoug it validates). With the fix I get

T14175a.hs:11:15: error: Not in scope: type variable    k   
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |               ^

T14175a.hs:11:27: error: Not in scope: type variable    k   
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |                           ^

for comment:1

comment:4 Changed 3 weeks ago by RyanGlScott

I'm confused about what this fix is doing. Isn't k implicitly quantified? In other words, what does your patch do on this program, which explicitly quantifies k but throws the same panic?

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C a where
  data CD k (a :: k) :: k -> *

instance C (Maybe a) where
  data CD k (a :: k -> *) :: (k -> *) -> *

comment:5 Changed 3 weeks ago by simonpj

After my fix I get this for comment:4

c:/code/HEAD/inplace/bin/ghc-stage1 -c  T14175b.hs

T14175b.hs:13:3: error:
        Expected kind    (k1 -> *) -> *   ,
        but    CD k (a :: k -> *) :: (k -> *) -> *    has kind    k1 -> *   
        In the data instance declaration for    CD   
      In the instance declaration for    C (Maybe a)   
   |
13 |   data CD k (a :: k -> *) :: (k -> *) -> *
   |   ^^^^^^^^^^^^^^^^^^^^^^^

That looks pretty weird too. But at least neither crashes, which is the first thing.

comment:6 Changed 2 weeks ago by goldfire

Other than the kind signature in the second full line of the error message there, it looks reasonable to me.

comment:7 Changed 10 days ago by Simon Peyton Jones <simonpj@…>

In 8bf865d3/ghc:

Tidying could cause ill-kinded types

I found (Trac #14175) that the tidying we do when reporting
type error messages could cause a well-kinded type to become
ill-kinded. Reason: we initialised the tidy-env with a
completely un-zonked TidyEnv accumulated in the TcLclEnv
as we come across lexical type-varialbe bindings.

Solution: zonk them.

But I ended up refactoring a bit:

* Get rid of tcl_tidy :: TidyEnv altogether

* Instead use tcl_bndrs :: TcBinderStack
  This used to contain only Ids, but now I've added those
  lexically scoped TyVars too.

* Change names:
     TcIdBinderStack -> TcBinderStack
     TcIdBinder      -> TcBinder
     extendTcIdBndrs -> extendTcBinderStack

* Now tcInitTidyEnv can grab those TyVars from the
  tcl_bndrs, zonk, and tidy them.

The only annoyance is that I had to add TcEnv.hs-boot, to
break the recursion between the zonking code and the
TrRnMonad functions like addErrTc that call tcInitTidyEnv.
Tiresome, but in fact that file existed already.

comment:8 Changed 10 days ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: indexed-types/should_fail/T14175

comment:9 Changed 9 days ago by RyanGlScott

After this patch, GHC HEAD gives this error for the program in comment:2:

Bug.hs:11:3: error:
    • Expected kind ‘(k -> *) -> (k -> *) -> *’,
        but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
                                                        -> Maybe a -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |   ^^^^^^^

And this error for the program in comment:4:

Bug.hs:13:3: error:
    • Expected kind ‘(k -> *) -> *’,
        but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
13 |   data CD k (a :: k -> *) :: (k -> *) -> *
   |   ^^^^^^^^^^^^^^^^^^^^^^^

As you observed, these error messages aren't great and could likely be improved. Should I open a separate ticket for this?

comment:10 Changed 9 days ago by simonpj

Yes please!

comment:11 Changed 9 days ago by RyanGlScott

Note: See TracTickets for help on using tickets.