Opened 7 months ago

Closed 7 months ago

#15170 closed bug (fixed)

GHC HEAD panic (dischargeFmv)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.5
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: polykinds/T15170
Blocked By: Blocking:
Related Tickets: #14880, #15076 Differential Rev(s):
Wiki Page:

Description

The following program panics on GHC HEAD:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where

import Data.Kind
import Data.Proxy

data family Sing (a :: k)
data SomeSing :: Type -> Type where
  SomeSing :: Sing (a :: k) -> SomeSing k

class SingKind k where
  type Demote k = (r :: Type) | r -> k
  fromSing :: Sing (a :: k) -> Demote k
  toSing :: Demote k -> SomeSing k

withSomeSing :: forall k r
              . SingKind k
             => Demote k
             -> (forall (a :: k). Sing a -> r)
             -> r
withSomeSing x f =
  case toSing x of
    SomeSing x' -> f x'

newtype instance Sing (f :: k1 ~> k2) =
  SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }

instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
  type Demote (k1 ~> k2) = Demote k1 -> Demote k2
  fromSing sFun x = withSomeSing x (fromSing . applySing sFun)
  toSing = undefined

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@

dcomp :: forall (a :: Type)
                (b :: a ~> Type)
                (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
                (g :: forall (x :: a). Proxy x ~> b @@ x)
                (x :: a).
         SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
      => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
      -> Sing g
      -> Sing a
      -> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
dcomp _sf _ _ = undefined
$ /opt/ghc/head/bin/ghc Bug2.hs
[1 of 1] Compiling Bug              ( Bug2.hs, Bug2.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180501 for x86_64-unknown-linux):
        dischargeFmv
  [D] _ {0}:: (Apply
                 (f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] |> Sym ((TyFun
                                                                        <Proxy xx_a1iA[tau:3]>_N
                                                                        ((TyFun
                                                                            (Proxy
                                                                               (Sym {co_a1jm})
                                                                               (Coh <yy_a1iB[tau:3]>_N
                                                                                    {co_a1jm}))_N
                                                                            (Sym {co_a1jB} ; (Apply
                                                                                                (Sym {co_a1jm})
                                                                                                <*>_N
                                                                                                (Coh ((Coh <s_a1jn[fmv:0]>_N
                                                                                                           ((TyFun
                                                                                                               (Sym {co_a1jm})
                                                                                                               <*>_N)_N
                                                                                                            ->_N <*>_N) ; Sym {co_a1jA}) ; (Apply
                                                                                                                                              <Proxy
                                                                                                                                                 xx_a1iA[tau:3]>_N
                                                                                                                                              ((TyFun
                                                                                                                                                  (Sym {co_a1jm})
                                                                                                                                                  <*>_N)_N
                                                                                                                                               ->_N <*>_N)
                                                                                                                                              (Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N
                                                                                                                                                   (Sym ((TyFun
                                                                                                                                                            <Proxy
                                                                                                                                                               xx_a1iA[tau:3]>_N
                                                                                                                                                            ((TyFun
                                                                                                                                                                (Sym {co_a1jm})
                                                                                                                                                                <*>_N)_N
                                                                                                                                                             ->_N <*>_N))_N
                                                                                                                                                         ->_N <*>_N)))
                                                                                                                                              <'Proxy>_N)_N)
                                                                                                     (Sym ((TyFun
                                                                                                              (Sym {co_a1jm})
                                                                                                              <*>_N)_N
                                                                                                           ->_N <*>_N)))
                                                                                                (Coh <yy_a1iB[tau:3]>_N
                                                                                                     {co_a1jm}))_N))_N
                                                                         ->_N <*>_N))_N
                                                                     ->_N <*>_N))
                 'Proxy :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm}) ~> s_a1jp[fmv:0]))
              ~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm})
                                    ~> s_a1jp[fmv:0]))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad

On GHC 8.4.2, it simply throws an error:

$ /opt/ghc/8.4.2/bin/ghci Bug2.hs
GHCi, version 8.4.2: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug2.hs, interpreted )

Bug2.hs:53:71: error:
    • Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’
    • In the first argument of ‘Proxy’, namely ‘y’
      In the first argument of ‘(~>)’, namely ‘Proxy y’
      In the second argument of ‘(~>)’, namely
        ‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’
   |
53 |                 (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
   |                                                                       ^

Change History (7)

comment:1 Changed 7 months ago by RyanGlScott

Here's as small of an example as I can muster:

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

import Data.Kind
import Data.Proxy

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@

wat :: forall (a :: Type)
              (b :: a ~> Type)
              (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
              (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
              (x :: a).
      (forall (xx :: a) (yy :: b @@ xx). Proxy (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
   -> ()
wat _ = ()
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.5.20180501 for x86_64-unknown-linux):
        dischargeFmv
  [D] _ {0}:: (Apply
                 (f_a1rx[sk:2] xx_a1rH[tau:3] yy_a1rI[tau:3] |> Sym ((TyFun
                                                                        <Proxy xx_a1rH[tau:3]>_N
                                                                        ((TyFun
                                                                            (Proxy
                                                                               (Sym {co_a1rP})
                                                                               (Coh <yy_a1rI[tau:3]>_N
                                                                                    {co_a1rP}))_N
                                                                            (Sym {co_a1s4} ; (Apply
                                                                                                (Sym {co_a1rP})
                                                                                                <*>_N
                                                                                                (Coh ((Coh <s_a1rQ[fmv:0]>_N
                                                                                                           ((TyFun
                                                                                                               (Sym {co_a1rP})
                                                                                                               <*>_N)_N
                                                                                                            ->_N <*>_N) ; Sym {co_a1s3}) ; (Apply
                                                                                                                                              <Proxy
                                                                                                                                                 xx_a1rH[tau:3]>_N
                                                                                                                                              ((TyFun
                                                                                                                                                  (Sym {co_a1rP})
                                                                                                                                                  <*>_N)_N
                                                                                                                                               ->_N <*>_N)
                                                                                                                                              (Coh <c_a1rw[sk:2] xx_a1rH[tau:3]>_N
                                                                                                                                                   (Sym ((TyFun
                                                                                                                                                            <Proxy
                                                                                                                                                               xx_a1rH[tau:3]>_N
                                                                                                                                                            ((TyFun
                                                                                                                                                                (Sym {co_a1rP})
                                                                                                                                                                <*>_N)_N
                                                                                                                                                             ->_N <*>_N))_N
                                                                                                                                                         ->_N <*>_N)))
                                                                                                                                              <'Proxy>_N)_N)
                                                                                                     (Sym ((TyFun
                                                                                                              (Sym {co_a1rP})
                                                                                                              <*>_N)_N
                                                                                                           ->_N <*>_N)))
                                                                                                (Coh <yy_a1rI[tau:3]>_N
                                                                                                     {co_a1rP}))_N))_N
                                                                         ->_N <*>_N))_N
                                                                     ->_N <*>_N))
                 'Proxy :: (Proxy (yy_a1rI[tau:3] |> {co_a1rP}) ~> s_a1rS[fmv:0]))
              ~# (s_a1sj[fmv:0] :: (Proxy (yy_a1rI[tau:3] |> {co_a1rP})
                                    ~> s_a1rS[fmv:0]))
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad

comment:2 Changed 7 months ago by RyanGlScott

This flipped from an error to a panic in commit faec8d358985e5d0bf363bd96f23fe76c9e281f7 (Track type variable scope more carefully.).

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

In 57858fc/ghc:

Make dischargeFmv handle Deriveds

A Derived CFunEqCan does not "own" its FlatMetaTv (fmv), and should not
update it.  But one caller (canCFunEqCan) was failing to satisfy the
precondition to dischargeFmv, which led to a crash (Trac #15170).

I fixed this by making dischargeFmv handle Deriveds (to avoid forcing
each caller to do so separately).

NB: this does not completely fix the original #15170 bug, but I'll
explain that on the ticket.  The test case for this patch is actually
the program in comment:1.

comment:4 Changed 7 months ago by simonpj

The patch in comment:3 makes the program in comment:1 compile fine.

However, the program in the Description now fails with a Lint error:

*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
    In the type ‘forall (x :: a_a10V[sk:0]) a (b :: a
                                                    ~> *) (c :: forall (x :: a).
                                                                Proxy x
                                                                ~> ((b @@ x)
                                                                    ~> *)) (f :: forall (x :: a) (y :: b
                                                                                                       @@ x).
                                                                                 Proxy x
                                                                                 ~> (Proxy y
                                                                                     ~> ((c x
                                                                                          @@ 'Proxy)
                                                                                         @@ y))) (g :: forall (x :: a).
                                                                                                       Proxy
                                                                                                         x
                                                                                                       ~> (b
                                                                                                           @@ x)) (x :: a).
                 SingKind ((c x @@ 'Proxy) @@ (g x @@ 'Proxy)) =>
                 (forall (xx :: a) (yy :: b @@ xx).
                  Sing ((f xx yy @@ 'Proxy) @@ 'Proxy))
                 -> Sing (g x)
                 -> Sing a
                 -> Demote ((c x @@ 'Proxy) @@ (g x @@ 'Proxy))’
    @ a_a10V[sk:0] is out of scope

I believe that the cause is the same as #14880, which I would love to get nailed.

comment:5 Changed 7 months ago by simonpj

Blocked By: 14880 added
Test Case: polykinds/T15170

comment:6 Changed 7 months ago by simonpj

Blocked By: 14880 removed

comment:7 Changed 7 months ago by RyanGlScott

Resolution: fixed
Status: newclosed

Thanks, Simon!

Ironically, I was writing this to work around #14880/#15076, and while I applied the workaround to f, I forgot to apply it to g. This is the function that I meant to write:

dcomp :: forall (a :: Type)
                (b :: a ~> Type)
                (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
                (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
                (g :: forall (x :: a). Proxy x ~> b @@ x)
                (x :: a).
         SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
      => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
      -> (forall (xx :: a). Sing (g @@ ('Proxy :: Proxy xx)))
      -> Sing a
      -> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
dcomp _sf _ _ = undefined

And after your most recent patch, this compiles without a hitch, even with -dcore-lint! I think we can close this in favor of #14880/#15076, as the Core Lint error in the original program is just a dressed-up version of the program in #15076.

Note: See TracTickets for help on using tickets.