Opened 7 months ago

Last modified 4 months ago

#13910 new bug

Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.2.1-rc2
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case:
Blocked By: #14119 Blocking:
Related Tickets: #13877, #14038, #14175 Differential Rev(s):
Wiki Page:


Here is a program which I believe should typecheck:

{-# LANGUAGE AllowAmbiguousTypes #-}                                                      
{-# LANGUAGE ConstraintKinds #-}                                                          
{-# LANGUAGE GADTs #-}                                                                    
{-# LANGUAGE RankNTypes #-}                                                               
{-# LANGUAGE ScopedTypeVariables #-}                                                      
{-# LANGUAGE TemplateHaskell #-}                                                          
{-# LANGUAGE Trustworthy #-}                                                              
{-# LANGUAGE TypeApplications #-}                                                         
{-# LANGUAGE TypeFamilyDependencies #-}                                                   
{-# LANGUAGE TypeInType #-}                                                               
{-# LANGUAGE TypeOperators #-}                                                            
module Bug where                                                                          
import Data.Kind                                                                          
import Data.Type.Equality                                                                 
data family Sing (a :: k)

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

data SomeSing k where
  SomeSing :: Sing (a :: 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'

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

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

data FunArrow = (:->) | (:~>)

class FunType (arr :: FunArrow) where
  type Fun (k1 :: Type) arr (k2 :: Type) :: Type

class FunType arr => AppType (arr :: FunArrow) where
  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2

type FunApp arr = (FunType arr, AppType arr)

instance FunType (:->) where
  type Fun k1 (:->) k2 = k1 -> k2

$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter

instance AppType (:->) where
  type App k1 (:->) k2 (f :: k1 -> k2) x = f x

instance FunType (:~>) where
  type Fun k1 (:~>) k2 = k1 ~> k2

$(return [])

instance AppType (:~>) where
  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x

infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2

data instance Sing (z :: a :~: b) where
  SRefl :: Sing Refl

instance SingKind (a :~: b) where
  type Demote (a :~: b) = a :~: b
  fromSing SRefl = Refl
  toSing Refl = SomeSing SRefl

(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
           Sing r
        -> p @@ Refl
        -> p @@ r
(~>:~:) SRefl pRefl = pRefl

type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
                    (y :: t) (e :: from :~: y) = App t arr Type p y
data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
  :: forall (y :: t). from :~: y ~> Type
type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
  = WhyReplacePoly arr from p y x

replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
           p from
        -> from :~: to
        -> p to
replace = replacePoly @(:->)

replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
                p @@ from
             -> from :~: to
             -> p @@ to
replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p

replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
                      (p :: (t -?> Type) arr).
               FunApp arr
            => App t arr Type p from
            -> from :~: to
            -> App t arr Type p to
replacePoly from eq =
  withSomeSing eq $ \(singEq :: Sing r) ->
    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from

type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
  = App t arr Type f a -> App t arr Type f z
data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
  :: t ~> Type
type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z

leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
                      (a :: t) (b :: t).
               FunApp arr
            => a :~: b
            -> App t arr Type f a
            -> App t arr Type f b
leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id

leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
           a :~: b
        -> f a
        -> f b
leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
-- The line above is what you get if you inline the definition of leibnizPoly.
-- It causes a panic, however.
-- An equivalent implementation is commented out below, which does *not*
-- cause GHC to panic.
-- leibniz = leibnizPoly @(:->)

leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
                a :~: b
             -> f @@ a
             -> f @@ b
leibnizTyFun = leibnizPoly @(:~>) @_ @f

GHC 8.2.1 and HEAD panic on the definition of leibniz, however:

$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version for x86_64-unknown-linux):
  (f_a5vT[sk:2] |> Sym (Trans
                            (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
                            (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
  (f_a5vT[sk:2] |> Sym (Trans
                            (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
                            (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type

Please report this as a GHC bug:

Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:

$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2:  :? for help                             
Loaded GHCi configuration from /home/rgscott/.ghci                                        
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )                               
Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened)                              
  (GHC version 8.0.2 for x86_64-unknown-linux):                                           
        No skolem info: k2_a4KV                                                           
Please report this as a GHC bug:

Change History (8)

comment:1 Changed 7 months ago by simonpj

Keywords: TypeInType added

comment:2 Changed 5 months ago by goldfire

Blocked By: 14119 added

After some analysis, I'm pretty sure this is #14038 again. Or, at least, that bug is preventing me from seeing this one clearly. Because #14038 is blocked by #14119, so is this one.

comment:3 Changed 5 months ago by RyanGlScott

Humorously enough, the panic is now different on GHC HEAD (likely due to commit a6c448b403dbe8720178ca82100f34baedb1f47e, Small refactor of getRuntimeRep):

$ ghc4/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.3.20170828:  :? 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.20170828 for x86_64-unknown-linux):
  (f_a5yC[sk:2] |> Sym (Sym (D:R:Funk1:->k2[0]
                                 <k1_a5n2>_N <k2_a5n3>_N) ; D:R:Funk1:->k2[0]
                                                                <*>_N)) a_a5yD[sk:2] :: k2_a5n3
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
        pprPanic, called at compiler/types/Type.hs:1982:18 in ghc:Type

comment:4 Changed 5 months ago by RyanGlScott

See #14175 for a much simpler program that gives the same two panics on GHC 8.2.1/HEAD.

comment:5 Changed 5 months ago by simonpj

Richard, I need your help on this.

I don't know whtether this problem is ultimately the source of the crash, but with my stage-1 compiler I get a earlier ASSERT failure, and some investigation shows that a type-family reduction is leading to an entirely bogus result. It's like this. We have an axiom

forall (k1 :: Type)
       (k2 :: Type)
       (f :: k1 ~> k2)
       (x :: k1).
    App k1 (':~>) k2 (f |> Sym (D:R:Funk1:~>k2{tc r14K}[0] <k1>_N <k2>_N)) x
      = @@ k1 k2 f x

But then we come across a call which we give to reduceTyFamApp_maybe:

  App w_a2c6 (':~>) Type ((p :: t ~> Type) |> HoleCo {a2cb}) w_a2c6

This is alraedy odd. I expected the arguments to be zonked before this attempt to do type-family reduction, but they aren't. In this case w_a2c6 is already unified with p.

But it gets worse. When we reduce the application, we get a result looking like

@@ w_a2c6 Type
   (p |> Sym (Sym (D:R:Funk1:~>k2
                      <k2>_N) ; Sym (HoleCo {a2cb})))

Yes, you saw it right. The k1 and k2 from the LHS of the axiom have shown up in the result!!!

Turns out that this is because of the treatment of casts in matching. In Unify.hs we see

unify_ty env ty1 ty2 kco
    -- TODO: More commentary needed here
  | CastTy ty1' co <- ty1     = unify_ty env ty1' ty2 (co `mkTransCo` kco)
  | CastTy ty2' co <- ty2     = unify_ty env ty1 ty2' (kco `mkTransCo` mkSymCo co)

So coercions from the LHS and RHS both end up mixed together in that kco; and it ultimately shows up in the result subsitution.

I'm not sure what the fix is. Maybe we can just apply the ambient substition to the co; but what if template variables it mentions have not yet been bound yet? Or maybe we need to take the fixpoint of the returned substitution; we do this for unification, maybe we need it for matching too?

Last edited 4 months ago by simonpj (previous) (diff)

comment:6 Changed 5 months ago by goldfire

Simon and I met over lunch at ICFP on this one, and I think he solved the immediate problem here... but then ran into another gorilla behind this one. I wait with bated breath to see what shape that gorilla has!

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

In 9218ea60/ghc:

Interim fix for a nasty type-matching bug

The type matcher in types/Unify.hs was producing a substitution
that had variables from the template in its range.  Yikes!

This patch, documented in Note [Matching in the presence of casts],
is an interm fix.  Richard and I don't like it much, and are
pondering a better solution (Trac #14119).

All this came up in investigating Trac #13910. Alas this patch
doesn't fix #13910, which still has ASSERT failures, so I have
not yet added a test.  But the patch does fix a definite bug.

comment:8 Changed 4 months ago by Ben Gamari <ben@…>

In e5beb6ec/ghc:

Make rejigConRes do kind substitutions

This was a lurking bug discovered on the hunt for #13910, but
it doesn't fix that bug. The old version of rejigConRes was
just wrong, forgetting to propagate a kind-change.
Note: See TracTickets for help on using tickets.