Opened 4 months ago
Closed 3 months ago
#15370 closed bug (fixed)
Typed hole panic on GHC 8.6 (tcTyVarDetails)
Reported by: | RyanGlScott | Owned by: | Tritlo |
---|---|---|---|
Priority: | high | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.4.3 |
Keywords: | TypeInType, TypedHoles | Cc: | Tritlo |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | Compile-time crash or panic | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The following program panics on GHC 8.6 and HEAD:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind import Data.Type.Equality import Data.Void data family Sing :: forall k. k -> Type data (~>) :: Type -> Type -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } mkRefl :: n :~: j mkRefl = Refl right :: forall (r :: (x :~: y) ~> z). Sing r -> () right no = case mkRefl @x @y of Refl -> applySing no _
$ /opt/ghc/8.6.1/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.6.0.20180627 for x86_64-unknown-linux): tcTyVarDetails co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
On GHC 8.4, this simply errors:
$ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:23:10: error: • Couldn't match type ‘n’ with ‘j’ ‘n’ is a rigid type variable bound by the type signature for: mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j at Bug.hs:22:1-17 ‘j’ is a rigid type variable bound by the type signature for: mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j at Bug.hs:22:1-17 Expected type: n :~: j Actual type: n :~: n • In the expression: Refl In an equation for ‘mkRefl’: mkRefl = Refl • Relevant bindings include mkRefl :: n :~: j (bound at Bug.hs:23:1) | 23 | mkRefl = Refl | ^^^^ Bug.hs:29:13: error: • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’ Expected type: () Actual type: Sing (Apply r t0) • In the expression: applySing no _ In a case alternative: Refl -> applySing no _ In the expression: case mkRefl @x @y of { Refl -> applySing no _ } • Relevant bindings include no :: Sing r (bound at Bug.hs:27:7) right :: Sing r -> () (bound at Bug.hs:27:1) | 29 | Refl -> applySing no _ | ^^^^^^^^^^^^^^ Bug.hs:29:26: error: • Found hole: _ :: Sing t0 Where: ‘t0’ is an ambiguous type variable ‘y’, ‘x’, ‘k’ are rigid type variables bound by the type signature for: right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z). Sing r -> () at Bug.hs:(25,1)-(26,21) • In the second argument of ‘applySing’, namely ‘_’ In the expression: applySing no _ In a case alternative: Refl -> applySing no _ • Relevant bindings include no :: Sing r (bound at Bug.hs:27:7) right :: Sing r -> () (bound at Bug.hs:27:1) Valid substitutions include undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a (imported from ‘Prelude’ at Bug.hs:7:8-10 (and originally defined in ‘GHC.Err’)) | 29 | Refl -> applySing no _ | ^
Note that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.
Change History (18)
comment:1 Changed 4 months ago by
comment:2 Changed 4 months ago by
Cc: | Tritlo added |
---|
This regression was introduced in commit e0b44e2eccd4053852b6c4c3de75a714301ec080 (Improved Valid Hole Fits
).
comment:4 Changed 4 months ago by
After some investigation, here is some more info:
I'm running this on the branch on which I've fixed #15384, and now it generates a different panic:
Filling a filled coercion hole co_a1we Sym (S <x_a1vL[sk:1]>_N <x_a1vL[sk:1]>_N (Sym (GRefl nominal r_a1vN[sk:1] (Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)) ; GRefl nominal r_a1vN[sk:1] (Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)))_N ; {co_a1ws} Sym (S <x_a1vL[sk:1]>_N <x_a1vL[sk:1]>_N (Sym (GRefl nominal r_a1vN[sk:1] (Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)) ; GRefl nominal r_a1vN[sk:1] (Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)))_N ; {co_a1wm}
This happens when trying to simplify:
WC {wc_impl = Implic { TcLevel = 1 Skolems = x_a1vL[sk:1] y_a1vM[sk:1] (r_a1vN[sk:1] :: Either x_a1vL[sk:1] y_a1vM[sk:1]) No-eqs = True Status = Insoluble Given = Wanted = WC {wc_impl = Implic { TcLevel = 2 Skolems = No-eqs = False Status = Insoluble Given = co_a1vU :: y_a1vM[sk:1] GHC.Prim.~# x_a1vL[sk:1] Wanted = WC {wc_simple = [WD] hole{co_a1wo} {0}:: (S r_a1vN[sk:1] -> ()) GHC.Prim.~# S (r_a1vN[sk:1] |> Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N) (CNonCanonical) [WD] hole{co_a1we} {1}:: S (r_a1vN[sk:1] |> Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N) GHC.Prim.~# () (CNonCanonical) [WD] $dNum_a1wf {0}:: Num (S (r_a1vN[sk:1] |> Sym (Either <x_a1vL[sk:1]>_N (Sym co_a1vU))_N)) (CNonCanonical)} Binds = EvBindsVar<a1wp> a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in a case alternative }}
where
WC {wc_simple = [WD] hole{co_a1wi} {0}:: y_a1vM[sk:1] GHC.Prim.~# x_a1vL[sk:1] (CNonCanonical)}
is generated by tcSubType_NC
.
I'm not sure how to prevent/catch the filling of the unfilled coercion hole and discard those fits.
comment:5 Changed 4 months ago by
Tritlo, what commit are you on? I just tried compiling the program in comment:1 using commit f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b, and to my surprise, it no longer panics!
$ inplace/bin/ghc-stage2 ../Bug.hs [1 of 1] Compiling Bug ( ../Bug.hs, ../Bug.o ) ../Bug.hs:14:10: error: • Couldn't match type ‘n’ with ‘j’ ‘n’ is a rigid type variable bound by the type signature for: mkRefl :: forall k (n :: k) (j :: k). n :~: j at ../Bug.hs:13:1-17 ‘j’ is a rigid type variable bound by the type signature for: mkRefl :: forall k (n :: k) (j :: k). n :~: j at ../Bug.hs:13:1-17 Expected type: n :~: j Actual type: n :~: n • In the expression: Refl In an equation for ‘mkRefl’: mkRefl = Refl • Relevant bindings include mkRefl :: n :~: j (bound at ../Bug.hs:14:1) | 14 | mkRefl = Refl | ^^^^ ../Bug.hs:20:13: error: • Couldn't match type ‘S r’ with ‘()’ Expected type: () Actual type: S r • In the expression: no + _ In a case alternative: Refl -> no + _ In the expression: case mkRefl @x @y of { Refl -> no + _ } • Relevant bindings include no :: S r (bound at ../Bug.hs:18:7) right :: S r -> () (bound at ../Bug.hs:18:1) | 20 | Refl -> no + _ | ^^^^^^ ../Bug.hs:20:18: error: • Found hole: _ :: S r Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by the type signature for: right :: forall x y (r :: Either x y). S r -> () at ../Bug.hs:(16,1)-(17,18) • In the second argument of ‘(+)’, namely ‘_’ In the expression: no + _ In a case alternative: Refl -> no + _ • Relevant bindings include no :: S r (bound at ../Bug.hs:18:7) right :: S r -> () (bound at ../Bug.hs:18:1) Constraints include y ~ x (from ../Bug.hs:20:5-8) | 20 | Refl -> no + _ | ^
Which seems positive, although I'm not sure which commit would have fixed this.
comment:6 Changed 4 months ago by
I'm on a branch based on 973ff4a142e77e247caebf828aa51f9810394938, with the changes from b202e7a48401bd8e805a92dcfe5ea059cbd8e41c on top. In b202e7a4, I remove the call to tcTyVarLevel
, which was calling tcTyVarDetails
and causing the original panic. I suspect af624071fa063158d6e963e171280676f9c0a0b0, which I believe changes the hole{co_a1wi} {0}:: y_a1vM[sk:1] GHC.Prim.~# x_a1vL[sk:1]
constraint that was causing the crash. I'll check to confirm.
comment:7 Changed 4 months ago by
I'm still getting the latter error on f0d27f515ffbc476144d1d1dd1a71bf9fa93c94b,when I build with the devel2 flavor (even after make distclean). Are you sure you're not seeing it RyanGlScott?
comment:8 Changed 4 months ago by
To be clear, is the error that you're experiencing in comment:4 an assertion failure, or a different form of panic? If it's the former, then that would explain why I'm not seeing it—I'm not using a devel*
build flavor, so I don't have assertions enabled.
comment:10 Changed 4 months ago by
I have a hypothesis about the assertion failure in comment:4
I see in TcHoleErrors.tcCheckHoleFit
; let w_rel_cts = addSimples wanted relevantCts ... ; let w_givens = foldr setWC w_rel_cts outermost_first ... ; rem <- runTcSDeriveds $ simpl_top w_givens
So the same relevantCts
are used in multiple runs of runTcSDerived
.
You are careful to freshen the ic_binds
of the implicatations,
but if relevantCts
contains any equalities they will have HoleDest
,
a coercion hole that is filled in directly. You really need to clone
those holes too. Use TcMType.cloneWanted
as in cloneWC
.
As it happens, this cloneWanted
is overkill, and I'm improving it
in an upcoming patch, but for now I think it'll do what you need.
Does that make sense? Best to verify that this is indeed what is happening.
comment:11 Changed 4 months ago by
That was indeed what was happening. A fix is up on Phabricator (https://phabricator.haskell.org/D5004), including a regression test (the code from comment:4).
comment:12 Changed 4 months ago by
Status: | new → patch |
---|
comment:14 Changed 4 months ago by
Status: | patch → merge |
---|
comment:15 Changed 4 months ago by
Hmm, I'm afraid there is a piece that we are missing on ghc-8.6
. T15370
fails with
ghc-stage2: panic! (the 'impossible' happened) (GHC version 8.6.0.20180802 for x86_64-unknown-linux): tcTyVarDetails co_a1vS :: y_a1vK[sk:1] ~# x_a1vJ[sk:1] Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
when this is cherry-picked on ghc-8.6
.
Tritlo, do you think you could look into this?
comment:16 Changed 4 months ago by
Yes. Does ghc-8.6
include b202e7a48401bd8e805a92dcfe5ea059cbd8e41c already? I think that resolved the original panic.
comment:17 Changed 3 months ago by
bgamari: It appears that the changes in b202e7a48401bd8e805a92dcfe5ea059cbd8e41c (which comes from https://phabricator.haskell.org/D4994) are not yet merged. If you merge that to ghc-8.6
, it fixes the panic in T15370
, and then https://phabricator.haskell.org/D5004 fixes the assertion that was being violated in DEBUG
.
comment:18 Changed 3 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
comment:16 merged in f4e54330d14c1601128d6ab3750a10709c05a427 and comment:13 merged in 588364c38530b51902d79d0175deed359796d172.
Simpler example: