#15778 closed bug (fixed)

GHC HEAD-only panic (zonkTcTyVarToTyVar)

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.7
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: typecheck/should_compile/T15778
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

The following program typechecks on GHC 8.0.1 through 8.6.1:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind

type a ~> b = a -> b -> Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing (a :: k)

data Flarble (a :: Type) where
  MkFlarble :: Flarble Bool
data instance Sing (z :: Flarble a) where
  SMkFlarble :: Sing MkFlarble

elimFlarble :: forall a
                      (p :: forall x. Flarble x ~> Type)
                      (f :: Flarble a).
               Sing f
            -> Apply p MkFlarble
            -> Apply p f
elimFlarble s@SMkFlarble pMkFlarble =
  case s of
    (_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) ->
      pMkFlarble

However, it panics on GHC HEAD:

$ ~/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.7.20181015 for x86_64-unknown-linux):
        zonkTcTyVarToTyVar
  probablyABadIdea_aWn[tau:2]
  Bool
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType

If I replace probablyABadIdea with Bool, then it typechecks again.

Change History (8)

comment:1 Changed 11 months ago by RyanGlScott

Version: 8.58.7

comment:2 Changed 11 months ago by RyanGlScott

This regression was introduced in commit 4d91cabcd5e3c603997d9876f6d30204a9b029c6 (Allow scoped type variables refer to types).

comment:3 Changed 11 months ago by RyanGlScott

Keywords: TypeInType added

Marginally simpler example:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

data Flarble (a :: Type) where
  MkFlarble :: Flarble Bool
data SFlarble (z :: Flarble a) where
  SMkFlarble :: SFlarble MkFlarble

foo :: SFlarble z -> ()
foo s@SMkFlarble =
  case s of
    (_ :: SFlarble (MkFlarble :: Flarble probablyABadIdea))
      -> ()

comment:4 Changed 11 months ago by RyanGlScott

The following code does not compile on earlier versions of GHC, but it is the simplest way to trigger the panic that I've discovered:

{-# LANGUAGE PolyKinds, ScopedTypeVariables #-}
foo (_ :: (a :: probablyABadIdea)) = ()
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Main             ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.7.20181015 for x86_64-unknown-linux):
        zonkTcTyVarToTyVar
  probablyABadIdea_arQ[tau:1]
  TYPE t_arX[tau:1]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType

comment:5 Changed 11 months ago by simonpj

I know what is happening here. In tcHsPatSigType we have

    mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
                       ; return (tyVarName tv, tv') }

But now the tyvar might have unified with a type not a type variable. And in these cases it does. I think that the right thing is simply to remove the zonk. I'll act on this.

comment:6 Changed 11 months ago by Simon Peyton Jones <simonpj@…>

In 29978ef/ghc:

Remove a zonkTcTyVarToTyVar

This patch fixes Trac #15778 by removing a zonkTcTyVarToTyVar
from tcHsSigType.

Nww that a pattern-bound type variable can refer to a type, it's
obvoiusly wrong to expect it to be a TyVar!  Moreover, that zonk
is entirely unnecessary.

I added a new Note [Type variables in the type environment]
in TcRnTypes

comment:7 Changed 11 months ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T15778

Thanks! fixed.

comment:8 Changed 11 months ago by RyanGlScott

Resolution: fixed
Status: mergeclosed

This shouldn't be merged. This fix relies on commit 4d91cabcd5e3c603997d9876f6d30204a9b029c6, which wasn't merged to the 8.6 branch.

Note: See TracTickets for help on using tickets.