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 )
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
Description: | modified (diff) |
---|
comment:2 Changed 4 months ago by
comment:3 Changed 4 months ago by
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
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
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 follow-up: 7 Changed 3 months ago by
With the Foo
in comment:3, this also panics:
quux :: forall x arg. Proxy (Foo arg) -> Maybe x quux = undefined
comment:7 Changed 2 months ago by
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
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
Related Tickets: | → #15076 |
---|
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
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 precedeSpecified
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 incandidatesQTyVarsOfType
.
- Also came up: close over kinds once in
tyCoVarsOfType
instead of at every leaf. This is not just an efficiency issue: considertyCoVarsOfType (forall a. b::a)
Richard is on the job
comment:13 Changed 8 weeks ago by
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:15 Changed 5 weeks ago by
Blocking: | 15170 added |
---|
comment:16 Changed 5 weeks ago by
Blocking: | 15170 removed |
---|
I believe that #15170 is also blocked on this.
comment:17 Changed 3 weeks ago by
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
, leavingtc_hs_sig_type_and_gen
tc_hs_sig_type_and_gen
should not callsolveEqualities
(which fails if there are unsolved equalities)
- Instead call
solveLocalEqualities
, gather unsolved equalities, and do not quantify over their free vars. NB:tcImplicitTKBndrs
already callssolveLocalEqualities
, 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
comment:18 Changed 3 weeks ago by
While I agree with comment:17, that doesn't have anything to do with this ticket...
comment:19 Changed 3 days ago by
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.
Here's as minimal of an example as I can conjure up: