Opened 4 months ago

Last modified 3 days ago

#14880 new bug

GHC panic: updateRole

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

Description (last modified by RyanGlScott)

The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:

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

import Data.Kind
import Data.Type.Equality ((:~:))

type SameKind (a :: k) (b :: k) = (() :: Constraint)

data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2

data WhyCongSym1 (x :: Type) :: forall (a :: x)
                                       (y :: Type)
                                       (z :: x).
                                Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type

data WhyCongSym0 :: forall (x :: Type)
                           (a :: x)
                           (y :: Type)
                           (z :: x).
                    Type ~> Type ~> (x ~> y) ~> x ~> x ~> (a :~: z) ~> Type
  where
    WhyCongSym0KindInference :: forall x arg.
                                SameKind (Apply WhyCongSym0 arg) (WhyCongSym1 arg) =>
                                WhyCongSym0 x
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: 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.2 for x86_64-unknown-linux):
        updateRole
  WhyCongSym0
  arg_a1A6[sk:1]
  [a1A5 :-> 4, a2Cy :-> 0, a2Cz :-> 1, a2CA :-> 2, a2CB :-> 3]
  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/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls

Change History (19)

comment:1 Changed 4 months ago by RyanGlScott

Description: modified (diff)

comment:2 Changed 4 months ago by RyanGlScott

Here's as minimal of an example as I can conjure up:

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

import Data.Kind
import Data.Proxy

data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

data Bar :: Type -> Type where
    MkBar :: forall x arg.
             -- Commenting out the line below makes the issue go away
             Foo arg ~ Foo arg =>
             Bar x
$ /opt/ghc/8.2.2/bin/ghci Bug.hs
GHCi, version 8.2.2: 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.2 for x86_64-unknown-linux):
        updateRole
  Bar
  arg_a1vT[sk:1]
  [a1vS :-> 0]
  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/typecheck/TcTyDecls.hs:656:23 in ghc:TcTyDecls

comment:3 Changed 4 months ago by simonpj

Even simpler

 data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

 data Bar :: Type -> Type where
     MkBar :: forall x arg.
              -- Commenting out the line below makes the issue go away
              Proxy (Foo arg) ->
              Bar x

The panic is caused because the existentials for MkBar are messed up;

{-  MkBar
    univ_tvs:   (x :: *)
    ex_tvs:     (a :: arg_aZv)
                (arg_XZx :: *)
    arg ty:     Proxy @arg_XZx a
    result ty:  Foo @arg_XZx a

Note the confusion of two arg variables. Ran out of time at that point.

comment:4 Changed 4 months ago by simonpj

Keywords: TypeInType added; Roles removed
Owner: set to goldfire

The trouble is that the type of MkBar should really be

MkBar :: forall (x:Type) (arg:Type) {a:arg}.
         Proxy @(Proxy @arg a -> Type)
               (Foo arg @a)
      -> Bar x

where I have put in all the kind applications. The trouble is that MkBar has an implicit forall's variable a, whose kind mentions an explicit type variable arg. So the implicit argument must appear later in the telescope. But tcConDecl (the ConDeclGADT case) doesn't allow that:

             tkv_bndrs      = mkTyVarBinders Inferred  tkvs'
             user_tv_bndrs  = mkTyVarBinders Specified user_tvs'
             all_user_bndrs = tkv_bndrs ++ user_tv_bndrs

Notice that the inferred ones always come first. But here they can't!

Solution: do a topo-sort of the tyvars that is allowed to interleave the Inferred and Specified ones.

But is that the only place? If we try something like this with a function type signature thus

f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a
f = f

we get the error message

T14880.hs:24:6: error:
    * The kind of variable `k', namely `v',
      depends on variable `v' from an inner scope
      Perhaps bind `k' sometime after binding `v'
      NB: Implicitly-bound variables always come before other ones.
    * In the type signature:
        f :: forall (v :: *) (a :: Proxy (k :: v)). Proxy a

But is there anything really wrong with this signature? It we topo-sorted the type variables we'd be fine.

There are other places (exp in TcTyClsDecls) where we seem to put all the inferred variables around the outside. I don't know how to be sure in which, if any, of these case we have a bug. Maybe we need more topo-sorts?

Amnother oddd thing about this ticket is the data decl for Foo:

data Foo (v :: Type) :: forall (a :: v). Proxy a -> Type

That is a strange kind signature. I don't expect to see foralls to the right of the :: in such a decl. So, more questions

  • Is it valuable to permit TyCons whose kinds are not in prenex form (i.e. all foralls at the front)?

If so, we should document it.

Meanwhile I'm not going to fix this because it may all come out in the wash of Richards's upcoming kind-inference patch.

It's nothing to do with roles!

comment:5 Changed 4 months ago by goldfire

The updateRole panic triggers on various invalid-tycon problems. I'm not surprised that roles aren't involved.

Yes, a forall to the right of the :: in a data declaration makes fine sense. For example, here is one way to define heterogeneous equality:

data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
  HRefl :: a :~~: a

This definition is actually a touch more general than one where k1 and k2 are quantified prenex, as the "Practical Type Inference" paper explains.

I don't see a need to document this specially.

As for the toposorting suggestions: I've considered it a design principle that implicit quantification comes before all explicit quantification. Of course, we can't panic when something goes wrong here, but I think this design is a good one, just to have some rules that users can rely on.

My existing patch still panics on this case, but I agree that no one should spend time on this until that patch lands.

comment:6 Changed 3 months ago by goldfire

With the Foo in comment:3, this also panics:

quux :: forall x arg. Proxy (Foo arg) -> Maybe x
quux = undefined

comment:7 in reply to:  6 Changed 2 months ago by RyanGlScott

Replying to goldfire:

With the Foo in comment:3, this also panics:

It does? I must be doing something wrong, since this appears to compile for me:

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

import Data.Kind
import Data.Proxy

data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

quux :: forall x arg. Proxy (Foo arg) -> Maybe x
quux = undefined

comment:8 Changed 2 months ago by simonpj

My existing patch still panics on this case, but I agree that no one should spend time on this until that patch lands.

Richard, now that the patch has landed, and this stuff is in your head, might you look at this? I doubt it's hard.

comment:9 Changed 2 months ago by RyanGlScott

I think that this ticket and #15076 share a symptom in common. This claim is based on the fact that slightly tweaking the program in comment:6 / comment:7 :

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

import Data.Kind
import Data.Proxy

data Foo (x :: Type) :: forall (a :: x). Proxy a -> Type

quux :: forall arg. Proxy (Foo arg) -> ()
quux (_ :: _) = ()

Yields:

$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:12:12: error:ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.5.20180420 for x86_64-unknown-linux):
        No skolem info:
  [arg_aZr[sk:1]]
  Call stack:
      CallStack (from HasCallStack):
        callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
        pprPanic, called at compiler/typecheck/TcErrors.hs:3224:5 in ghc:TcErrors

Which is the same panic as in #15076. Plus, if you run this program with -ddump-tc-trace, you see:

reportUnsolved (after zonking):
  Free tyvars: arg_aZr[sk:1]
  Tidy env: ([ESf71 :-> 1], [aZr :-> arg_aZr[sk:1]])
  Wanted: WC {wc_impl =
                Implic {
                  TcLevel = 2
                  Skolems = (a_a1p8[sk:2] :: arg_aZr[sk:1]) arg_a1p9[sk:2]
                  No-eqs = True
                  Status = Unsolved
                  Given =
                  Wanted =
                    WC {wc_simple =
                          [D] _ {0}:: Proxy
                                        (Foo arg_a1p9[sk:2] a_a1p8[sk:2]) (CHoleCan: TypeHole(_))}
                  Binds = EvBindsVar<a1pg>
                  Needed inner = []
                  Needed outer = []
                  the type signature for:
                    quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo arg a) -> () }}

Just like in #15076, arg_aZr is not bound in any implication. On the other hand, there is another type variable, arg_a1p9, that is suspiciously similar. Moreover, the type signature it gives for quux:

quux :: forall (a :: arg_aZr[sk:1]) arg. Proxy (Foo arg a) -> ()

Seems to have two different copies of arg! This is especially interesting in light of comment:3, where simonpj discovered that the existentially quantified tyvars in MkBar were screwed up, leading to two copies of arg.

comment:10 Changed 8 weeks ago by simonpj

The trouble is that MkBar has an implicit forall's variable a, whose kind mentions an explicit type variable arg.

Richard and I discussed this on Monday. Our conclusions

  • Inferred variables should always precede Specified ones. That is, do not top-sort
  • Idea: simply refrain from quantifying any inferred variables that mention specified ones. They'll get defaulted to Any which is probably fine. This refraining can readily be done in candidatesQTyVarsOfType.
  • Also came up: close over kinds once in tyCoVarsOfType instead of at every leaf. This is not just an efficiency issue: consider
    tyCoVarsOfType (forall a. b::a)
    

Richard is on the job

comment:11 Changed 8 weeks ago by simonpj

Trac #15076 is another example of the same phenomenon.

comment:12 Changed 8 weeks ago by simonpj

And probably #14040 too.

comment:13 Changed 8 weeks ago by goldfire

Yes, I have a fix here, but it causes a failure in, e.g., indexed-types/should_compile/T12369. Haven't had time to investigate.

comment:14 Changed 8 weeks ago by simonpj

Maybe #14887 too!

comment:15 Changed 5 weeks ago by simonpj

Blocking: 15170 added

comment:16 Changed 5 weeks ago by simonpj

Blocking: 15170 removed

I believe that #15170 is also blocked on this.

comment:17 Changed 3 weeks ago by simonpj

In a call today Richard and Simon decided:

  • Kill decideKindGeneralisationPlan; instead always generalise. (Explain why we don't need to worry about local generalisation as we do with terms.)
  • And hence kill tc_hs_sig_type, leaving tc_hs_sig_type_and_gen
  • tc_hs_sig_type_and_gen should not call solveEqualities (which fails if there are unsolved equalities)
  • Instead call solveLocalEqualities, gather unsolved equalities, and do not quantify over their free vars. NB: tcImplicitTKBndrs already calls solveLocalEqualities, and must do so. Needs a Note to explain why: it's so that we can top-sort the bound variables
  • Promote all the free vars of the unsolved constraints. Principle: all free vars should either be generalised or promoted.
  • Get rid of zonkPromote and friends altogether
Last edited 3 weeks ago by simonpj (previous) (diff)

comment:18 Changed 3 weeks ago by goldfire

While I agree with comment:17, that doesn't have anything to do with this ticket...

comment:19 Changed 3 days ago by goldfire

Differential Rev(s): Phab:D4769

Since my last update, the patch in Phab:D4769 works but has performance trouble. I've asked Ben & friends for help.

Note: See TracTickets for help on using tickets.