Opened 11 days ago
Last modified 2 days ago
#15370 new bug
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 (4)
comment:1 Changed 11 days ago by
comment:2 Changed 11 days ago by
Cc: | Tritlo added |
---|
This regression was introduced in commit e0b44e2eccd4053852b6c4c3de75a714301ec080 (Improved Valid Hole Fits
).
comment:4 Changed 2 days 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.
Simpler example: