Opened 15 months ago

Closed 6 months ago

#13910 closed bug (fixed)

Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
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: dependent/should_compile/T13910
Blocked By: Blocking:
Related Tickets: #13877, #14038, #14175 Differential Rev(s):
Wiki Page:

Description

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 8.2.0.20170623: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
  (GHC version 8.2.0.20170623 for x86_64-unknown-linux):
        repSplitTyConApp_maybe
  (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]
  k2_a5l0
  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:  http://www.haskell.org/ghc/reportabug

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: http://www.haskell.org/ghc/  :? 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:  http://www.haskell.org/ghc/reportabug

Change History (10)

comment:1 Changed 15 months ago by simonpj

Keywords: TypeInType added

comment:2 Changed 13 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 13 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: 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.20170828 for x86_64-unknown-linux):
        getRuntimeRep
  (f_a5yC[sk:2] |> Sym (Sym (D:R:Funk1:->k2[0]
                                 <k1_a5n2>_N <k2_a5n3>_N) ; D:R:Funk1:->k2[0]
                                                                <t1_a5yB[sk:2]>_N
                                                                <*>_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 13 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 13 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
                      <k1>_N
                      <k2>_N) ; Sym (HoleCo {a2cb})))
   w_a2ca

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 12 months ago by simonpj (previous) (diff)

comment:6 Changed 13 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 12 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 12 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.

comment:9 Changed 6 months ago by Richard Eisenberg <rae@…>

In e3dbb44f/ghc:

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135ace55ce2572bf4168124d631e386c64bb, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.

comment:10 Changed 6 months ago by RyanGlScott

Blocked By: 14119 removed
Milestone: 8.6.1
Resolution: fixed
Status: newclosed
Test Case: dependent/should_compile/T13910
Note: See TracTickets for help on using tickets.