Opened 4 months ago
Last modified 5 weeks ago
#14873 new bug
GHC HEAD regression (piResultTy)
Reported by: | RyanGlScott | Owned by: | goldfire |
---|---|---|---|
Priority: | highest | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.5 |
Keywords: | TypeInType | Cc: | simonpj |
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
(Originally noticed here.)
The following program typechecks on GHC 8.2.2 on GHC 8.4.1, but panics on GHC HEAD:
{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} module Bug where import Data.Kind (Type) data family Sing (a :: k) newtype instance Sing (f :: k1 ~> k2) = SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) } data TyFun :: Type -> Type -> Type type a ~> b = TyFun a b -> Type infixr 0 ~> type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 class SingI (a :: k) where sing :: Sing a data ColSym1 :: f a -> a ~> Bool type instance Apply (ColSym1 x) y = Col x y class PColumn (f :: Type -> Type) where type Col (x :: f a) (y :: a) :: Bool class SColumn (f :: Type -> Type) where sCol :: forall (x :: f a) (y :: a). Sing x -> Sing y -> Sing (Col x y :: Bool) instance (SColumn f, SingI x) => SingI (ColSym1 (x :: f a) :: a ~> Bool) where sing = SLambda (sCol (sing @_ @x))
$ /opt/ghc/head/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) ghc: panic! (the 'impossible' happened) (GHC version 8.5.20180201 for x86_64-unknown-linux): piResultTy k_aZU[tau:1] (a_aW8[sk:1] |> <*>_N) Call stack: CallStack (from HasCallStack): callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type
Change History (7)
comment:1 Changed 4 months ago by
Cc: | simonpj added |
---|
comment:2 Changed 4 months ago by
Urk! Patch coming -- but validation is not complete and I have to go home, so probably Monday.
comment:4 Changed 4 months ago by
Owner: | set to goldfire |
---|
OK done. Richard: could you have a look, to check my work?
comment:5 Changed 2 months ago by
Keywords: | TypeInType added |
---|
comment:6 Changed 2 months ago by
I think we need these invariants:
- If
ty <- tc_hs_type ... exp_kind
, thentypeKind ty == exp_kind
.
- If
(ty, ki) <- tc_infer_hs_type ...
, thentypeKind ty == ki
.
- If
(ty, ki) <- tc_infer_hs_type ...
, thenzonk ki == ki
.
- If
(ty, ki) <- tcTyVar ...
, thentypeKind ty == ki
.
- If
(ty, ki) <- tcTyVar ...
, thenzonk ki == ki
.
All of these appear to be true now, except I'm worried about the tcTyVar
case for TcTyCon
s -- I think TcTyCon
kinds can have unzonked metavariables, if the TcTyCon
comes from the non-CUSK case in kcLHsQTyVars
. Do you also think this is possible? If so, we need to zonk the kind and wrap the (knot-tied) type in a reflexive coercion (with mkNakedCastTy
) to fix its kind. Do you agree?
comment:7 Changed 5 weeks ago by
Milestone: | → 8.6.1 |
---|
This regression was introduced in commit 0a12d92a8f65d374f9317af2759af2b46267ad5c (
Further improvements to well-kinded types
).