Opened 3 months ago

Closed 3 months ago

#15428 closed bug (fixed)

Oversaturated type family application panicks GHC (piResultTys2)

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

Description

The following program panics when compiled with GHC 8.6.1 or HEAD:

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Proxy
import Data.Type.Equality

type family Flurmp :: k
type family Pure (x :: a) :: f a

wat :: forall (f :: Type -> Type) (p :: Type).
       Proxy (f p) -> ()
wat _ =
  let s ::     (Flurmp :: f p)
           :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
      s = undefined
  in ()
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.6.0.20180714 for x86_64-unknown-linux):
        piResultTys2
  f_aAT a_aAU
  [(->) p_a1uI[sk:1], p_a1uI[sk:1] -> p_a1uI[sk:1], Flurmp, Flurmp]
  [Flurmp]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type

On GHC 8.4 and earlier, this simply gives an error message:

$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:18:16: error:
    • Expecting one more argument to ‘Pure (Flurmp :: p -> p)’
      Expected kind ‘p -> f p’,
        but ‘Pure (Flurmp :: p -> p)’ has kind ‘p -> p -> p’
    • In the second argument of ‘(:~:)’, namely
        ‘Pure (Flurmp :: p -> p) (Flurmp :: p)’
      In the type signature:
        s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
      In the expression:
        let
          s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
          s = undefined
        in ()
    • Relevant bindings include
        wat :: Proxy (f p) -> () (bound at Bug.hs:16:1)
   |
18 |            :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
   |                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Change History (6)

comment:1 Changed 3 months ago by monoidal

Simpler version, also panicks 8.4:

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

data Flurmp
type family Pure (x :: a) :: f a

type T = Pure Flurmp Flurmp

comment:2 Changed 3 months ago by RyanGlScott

Summary: GHC 8.6+ panics (piResultTys2), older GHCs don'tOversaturated type family application panicks GHC (piResultTys2)

Nice find. I've changed the title accordingly, since this affects all GHCs back to 8.0.1.

comment:3 Changed 3 months ago by simonpj

I'm on this

comment:4 Changed 3 months ago by Simon Peyton Jones <simonpj@…>

In e1b5a11/ghc:

Fix a nasty bug in piResultTys

I was failing to instantiate vigorously enough in Type.piResultTys
and in the very similar function ToIface.toIfaceAppArgsX

This caused Trac #15428.  The fix is easy.

See Note [Care with kind instantiation] in Type.hs

comment:5 Changed 3 months ago by simonpj

Status: newmerge
Test Case: typecheck/should_compile/T15428

Thanks for the nice test case.

comment:6 Changed 3 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.