GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:30:31Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/11416GHC mistakenly believes datatype with type synonym in its type can't be eta-r...2019-07-07T18:30:31ZRyan ScottGHC mistakenly believes datatype with type synonym in its type can't be eta-reducedI uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deri...I uncovered this when playing around with `-XTypeInType`:
```hs
{-# LANGUAGE DeriveFunctor, TypeInType #-}
module CantEtaReduce1 where
import Data.Kind
type ConstantT a b = a
newtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor
```
This fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):
```
• Cannot eta-reduce to an instance of form
instance (...) => Functor (T f)
• In the newtype declaration for ‘T
```
But it *should* be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.
I marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:
```hs
{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}
module CantEtaReduce2 where
type ConstantT a b = a
data family T (f :: * -> *) (a :: *)
newtype instance T f (ConstantT a f) = T (f a) deriving Functor
```
I believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC mistakenly believes datatype with type synonym in its type can't be eta-reduced","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"I uncovered this when playing around with `-XTypeInType`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, TypeInType #-}\r\nmodule CantEtaReduce1 where\r\n\r\nimport Data.Kind\r\n\r\ntype ConstantT a b = a\r\nnewtype T (f :: * -> *) (a :: ConstantT * f) = T (f a) deriving Functor\r\n}}}\r\n\r\nThis fails because it thinks that you can't reduce the last type variable of `T`, since it mentions another type variable (`f`):\r\n\r\n{{{\r\n • Cannot eta-reduce to an instance of form\r\n instance (...) => Functor (T f)\r\n • In the newtype declaration for ‘T\r\n}}}\r\n\r\nBut it ''should'' be able to, since `ConstantT * f` reduces to `*`, and the equivalent declaration `newtype T (f :: * -> *) (a :: *) = ...` eta-reduces just fine.\r\n\r\nI marked this as appearing in GHC 8.1 since you need `-XTypeInType` to have kind synonyms, but this can also happen in earlier GHC versions with data families:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DeriveFunctor, PolyKinds, TypeFamilies #-}\r\nmodule CantEtaReduce2 where\r\n\r\ntype ConstantT a b = a\r\ndata family T (f :: * -> *) (a :: *)\r\nnewtype instance T f (ConstantT a f) = T (f a) deriving Functor\r\n}}}\r\n\r\nI believe the fix will be to apply `coreView` with precision to parts of the code which typecheck `deriving` statements so that these type synonyms are peeled off.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/13822GHC not using injectivity?2019-07-07T18:19:56ZIcelandjackGHC not using injectivity?This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds...This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TInt :: Ty STAR
TBool :: Ty STAR
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family
IK (k :: KIND) = (res :: Type) | res -> k where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family
I (t :: Ty k) = (res :: IK k) | res -> t where
I TInt = Int
I TBool = Bool
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyInt :: TyRep STAR TInt
TyBool :: TyRep STAR TBool
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
zero :: TyRep STAR a -> I a
zero = \case
TyInt -> 0
TyBool -> False
TyApp TyMaybe _ -> Nothing
```
When I ask it to infer the representation for `Int` and `Bool` it does so with no surprises
```hs
-- Inferred type:
--
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int
-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool
```
but inferring the representation for `Maybe Int` fails
```hs
-- v.hs:43:16: error:
-- • Couldn't match kind ‘k’ with ‘'STAR’
-- ‘k’ is a rigid type variable bound by
-- the inferred type of
-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- at v.hs:25:3
-- When matching the kind of ‘'TMaybe’
-- Expected type: Maybe Int
-- Actual type: I ('TApp 'TMaybe 'TInt)
-- • In the expression: zero rep :: Maybe Int
-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
-- • Relevant bindings include
-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int
```
even though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`
```
>>> :kind! I (TMaybe `TApp` TInt)
I (TMaybe `TApp` TInt) :: IK 'STAR
= Maybe Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC not using injectivity?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be normal behavior but.. (Example from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality])\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}\r\n\r\nimport Data.Kind\r\n\r\ndata KIND = STAR | KIND :> KIND\r\n\r\ndata Ty :: KIND -> Type where\r\n TInt :: Ty STAR\r\n TBool :: Ty STAR\r\n TMaybe :: Ty (STAR :> STAR)\r\n TApp :: Ty (a :> b) -> (Ty a -> Ty b)\r\n\r\ntype family\r\n IK (k :: KIND) = (res :: Type) | res -> k where\r\n IK STAR = Type\r\n IK (a:>b) = IK a -> IK b\r\n\r\ntype family\r\n I (t :: Ty k) = (res :: IK k) | res -> t where\r\n I TInt = Int\r\n I TBool = Bool\r\n I TMaybe = Maybe\r\n I (TApp f a) = (I f) (I a)\r\n\r\ndata TyRep (k :: KIND) (t :: Ty k) where\r\n TyInt :: TyRep STAR TInt\r\n TyBool :: TyRep STAR TBool\r\n TyMaybe :: TyRep (STAR:>STAR) TMaybe\r\n TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)\r\n\r\nzero :: TyRep STAR a -> I a\r\nzero = \\case\r\n TyInt -> 0\r\n TyBool -> False\r\n TyApp TyMaybe _ -> Nothing\r\n}}}\r\n\r\nWhen I ask it to infer the representation for `Int` and `Bool` it does so with no surprises\r\n\r\n{{{#!hs\r\n-- Inferred type: \r\n-- \r\n-- int :: TyRep STAR TInt -> Int\r\nint rep = zero rep :: Int\r\n\r\n\r\n-- bool:: TyRep STAR TBool -> Bool\r\nbool rep = zero rep :: Bool\r\n}}}\r\n\r\nbut inferring the representation for `Maybe Int` fails\r\n\r\n{{{#!hs\r\n-- v.hs:43:16: error:\r\n-- • Couldn't match kind ‘k’ with ‘'STAR’\r\n-- ‘k’ is a rigid type variable bound by\r\n-- the inferred type of\r\n-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>\r\n-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- at v.hs:25:3\r\n-- When matching the kind of ‘'TMaybe’\r\n-- Expected type: Maybe Int\r\n-- Actual type: I ('TApp 'TMaybe 'TInt)\r\n-- • In the expression: zero rep :: Maybe Int\r\n-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int\r\n-- • Relevant bindings include\r\n-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)\r\n-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- (bound at v.hs:43:1)\r\n-- Failed, modules loaded: none.\r\nmaybeInt rep = zero rep :: Maybe Int\r\n}}}\r\n\r\neven though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`\r\n\r\n{{{\r\n>>> :kind! I (TMaybe `TApp` TInt)\r\nI (TMaybe `TApp` TInt) :: IK 'STAR\r\n= Maybe Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/11356GHC panic2019-07-07T18:30:46ZIcelandjackGHC panicThe attached file causes GHC (version 8.1.20160102) panic.
I tried shrinking, attached code is bogus at this point.
Interestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regu...The attached file causes GHC (version 8.1.20160102) panic.
I tried shrinking, attached code is bogus at this point.
Interestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regular error.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The attached file causes GHC (version 8.1.20160102) panic.\r\n\r\nI tried shrinking, attached code is bogus at this point.\r\n\r\nInterestingly inlining the type synonym `T = Nat` into Category's superclass context fixes the panic, and causes a regular error.","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1https://gitlab.haskell.org/ghc/ghc/-/issues/15881GHC Panic: data A n (a :: n) :: a -> Type2019-07-07T18:02:35ZIcelandjackGHC Panic: data A n (a :: n) :: a -> Type```hs
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Kind
data A n (a :: n) :: a -> Type
```
causes a panic on 8.7.20181017
```
$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_b...```hs
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import Data.Kind
data A n (a :: n) :: a -> Type
```
causes a panic on 8.7.20181017
```
$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 665_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
Type-correct unfilled coercion hole {co_a1xR}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
and an assertion failure in 8.7.20181029
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 665_bug.hs, interpreted )
*** Exception: ASSERT failed! file compiler/types/TyCon.hs, line 420
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC Panic: data A n (a :: n) :: a -> Type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language KindSignatures #-}\r\n{-# Language PolyKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ndata A n (a :: n) :: a -> Type\r\n}}}\r\n\r\ncauses a panic on 8.7.20181017\r\n\r\n{{{\r\n$ ~/code/headghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 665_bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n\tASSERT failed!\r\n Type-correct unfilled coercion hole {co_a1xR}\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}\r\n\r\nand an assertion failure in 8.7.20181029\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 665_bug.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 665_bug.hs, interpreted )\r\n*** Exception: ASSERT failed! file compiler/types/TyCon.hs, line 420\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.3https://gitlab.haskell.org/ghc/ghc/-/issues/15692GHC panic from pattern synonyms + deferred type errors2019-07-07T18:03:25ZIcelandjackGHC panic from pattern synonyms + deferred type errors```hs
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
{-# Options_GHC -dcore-lint -fdefer-type-errors #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a...```hs
{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}
{-# Options_GHC -dcore-lint -fdefer-type-errors #-}
import Data.Kind
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
data ApplyT (k::Type) :: k -> Ctx(k) -> Type where
AO :: a -> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) ctx
-> ApplyT(k -> ks) f (a:&:ctx)
pattern ASSO = AS (AS (AO False))
```
```
$ ghci -ignore-dot-ghci 463.hs
hs/463.hs:16:27: warning: [-Wdeferred-type-errors]
• Couldn't match type ‘a a1 a2’ with ‘Bool’
Expected type: a3
Actual type: Bool
• In the pattern: False
In the pattern: AO False
In the pattern: AS (AO False)
|
16 | pattern ASSO = AS (AS (AO False))
| ^^^^^
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180828 for x86_64-unknown-linux):
urk! lookup local fingerprint
$mASSO
[iESflb :-> ($trModule, 1ca40dc83a9c879effdb760462cc9a2d),
iESgKD :-> ($tc'E, 79f67a27a14dc1bb6eecb39e4b061e2c),
iESgKF :-> ($tc':&:, 24793c0c1652ffcf92e04f47d38fa075),
iESgKH :-> ($tcCtx, a3f9358cbfe161bf59e75500d70ce0ae),
iESgKI :-> ($tc'AO, 72111d1891cb082e989c20a2191a8b4b),
iESgKK :-> ($tc'AS, ff019c04c400d5fbdd46ff8a816d4913),
iESgKM :-> ($tcApplyT, cbfe28374b4115925c7213e6330ab115)]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/iface/MkIface.hs:524:37 in ghc:MkIface
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic from pattern synonyms + deferred type errors","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["PatternSynonyms,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language DataKinds, TypeOperators, PolyKinds, PatternSynonyms, GADTs #-}\r\n\r\n{-# Options_GHC -dcore-lint -fdefer-type-errors #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Ctx :: Type -> Type where\r\n E :: Ctx(Type)\r\n (:&:) :: a -> Ctx(as) -> Ctx(a -> as)\r\n\r\ndata ApplyT (k::Type) :: k -> Ctx(k) -> Type where\r\n AO :: a -> ApplyT(Type) a E\r\n AS :: ApplyT(ks) (f a) ctx\r\n -> ApplyT(k -> ks) f (a:&:ctx)\r\n\r\npattern ASSO = AS (AS (AO False))\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 463.hs\r\nhs/463.hs:16:27: warning: [-Wdeferred-type-errors]\r\n • Couldn't match type ‘a a1 a2’ with ‘Bool’\r\n Expected type: a3\r\n Actual type: Bool\r\n • In the pattern: False\r\n In the pattern: AO False\r\n In the pattern: AS (AO False)\r\n |\r\n16 | pattern ASSO = AS (AS (AO False))\r\n | ^^^^^\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180828 for x86_64-unknown-linux):\r\n\turk! lookup local fingerprint\r\n $mASSO\r\n [iESflb :-> ($trModule, 1ca40dc83a9c879effdb760462cc9a2d),\r\n iESgKD :-> ($tc'E, 79f67a27a14dc1bb6eecb39e4b061e2c),\r\n iESgKF :-> ($tc':&:, 24793c0c1652ffcf92e04f47d38fa075),\r\n iESgKH :-> ($tcCtx, a3f9358cbfe161bf59e75500d70ce0ae),\r\n iESgKI :-> ($tc'AO, 72111d1891cb082e989c20a2191a8b4b),\r\n iESgKK :-> ($tc'AS, ff019c04c400d5fbdd46ff8a816d4913),\r\n iESgKM :-> ($tcApplyT, cbfe28374b4115925c7213e6330ab115)]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/iface/MkIface.hs:524:37 in ghc:MkIface\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.2https://gitlab.haskell.org/ghc/ghc/-/issues/13871GHC panic in 8.2 only: typeIsTypeable(Coercion)2019-07-07T18:19:45ZRyan ScottGHC panic in 8.2 only: typeIsTypeable(Coercion)This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data...This code works fine in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
```
But in GHC 8.2 and HEAD, it panics:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170622 for x86_64-unknown-linux):
typeIsTypeable(Coercion)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic in 8.2 only: typeIsTypeable(Coercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code works fine in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n}}}\r\n\r\nBut in GHC 8.2 and HEAD, it panics:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170622: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.0.20170622 for x86_64-unknown-linux):\r\n\ttypeIsTypeable(Coercion)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/15883GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)2020-01-17T16:43:24ZIcelandjackGHC panic: newtype F rep = F (forall (a :: TYPE rep). a)```hs
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interact...```hs
{-# Language RankNTypes #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
import GHC.Exts
newtype Foo rep = MkFoo (forall (a :: TYPE rep). a)
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci /tmp/U.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64-unknown-linux):
isUnliftedType
forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type
isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic: newtype F rep = F (forall (a :: TYPE rep). a)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.3","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language PolyKinds #-}\r\n\r\nimport GHC.Exts\r\n\r\nnewtype Foo rep = MkFoo (forall (a :: TYPE rep). a)\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci /tmp/U.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/U.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64-unknown-linux):\r\n isUnliftedType\r\n forall (a :: TYPE rep_a1AA[sk:0]). a :: TYPE rep_a1AA[sk:0]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:2332:10 in ghc:Type\r\n isUnliftedType, called at compiler/typecheck/TcTyClsDecls.hs:3055:25 in ghc:TcTyClsDecls\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/16245GHC panic (No skolem info) with RankNTypes and strange scoping2020-12-31T13:44:06ZRyan ScottGHC panic (No skolem info) with RankNTypes and strange scopingThe following program panics with GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Bug where
import Data.Kind
type Const a b...The following program panics with GHC 8.6.3 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Bug where
import Data.Kind
type Const a b = a
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class (forall (b :: k). SameKind a b) => C (k :: Const Type a)
```
```
$ /opt/ghc/8.6.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:36: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.3 for x86_64-unknown-linux):
No skolem info:
[k1_a1X4[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors
```
As with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be ill-scoped.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic (No skolem info) with QuantifiedConstraints and strange scoping","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.3","keywords":["QuantifiedConstraints","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics with GHC 8.6.3 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE QuantifiedConstraints #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype Const a b = a\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\nclass (forall (b :: k). SameKind a b) => C (k :: Const Type a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:11:36: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.3 for x86_64-unknown-linux):\r\n No skolem info:\r\n [k1_a1X4[sk:1]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2891:5 in ghc:TcErrors\r\n}}}\r\n\r\nAs with #16244, I imagine that the real culprit is that `SameKind a b` would force `a :: k`, which would be ill-scoped.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14552GHC panic on pattern synonym2019-07-07T18:16:32ZIcelandjackGHC panic on pattern synonym```hs
{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
import Data.Kind
data family Sing a
type a --> b = (a, b) -> Type
type family (@@)...```hs
{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}
import Data.Kind
data family Sing a
type a --> b = (a, b) -> Type
type family (@@) (f::a --> b) (x::a) :: b
data Proxy a = Proxy
newtype Limit' :: (k --> Type) -> Type where
Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f
data Exp :: [Type] -> Type -> Type where
TLam' :: Proxy f
-> (forall aa. Proxy aa -> Exp xs (f @@ aa))
-> Exp xs (Limit' f)
pattern FOO f <- TLam' Proxy (($ Proxy) -> f)
```
---\>
```
$ ghci -ignore-dot-ghci 119-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 119-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
ASSERT failed!
in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC}
tenv [a1MC :-> r_a1MC]
cenv []
tys [k_a1Mj[ssk:3]]
cos []
needInScope [a1Mj :-> k_a1Mj[ssk:3]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable
assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable
assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep
checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep
substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep
substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic on pattern synonym","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["PatternSynonyms,","TypeInType,","ViewPatterns"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing a\r\n\r\ntype a --> b = (a, b) -> Type\r\n\r\ntype family (@@) (f::a --> b) (x::a) :: b\r\n\r\ndata Proxy a = Proxy\r\n\r\nnewtype Limit' :: (k --> Type) -> Type where\r\n Limit' :: (forall xx. Proxy xx -> f@@xx) -> Limit' f\r\n\r\ndata Exp :: [Type] -> Type -> Type where\r\n TLam' :: Proxy f\r\n -> (forall aa. Proxy aa -> Exp xs (f @@ aa))\r\n -> Exp xs (Limit' f)\r\n\r\npattern FOO f <- TLam' Proxy (($ Proxy) -> f)\r\n}}}\r\n\r\n--->\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 119-bug.hs \r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 119-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tASSERT failed!\r\n in_scope InScope {a_a1Mh b_a1Mi rep_a1MB r_a1MC}\r\n tenv [a1MC :-> r_a1MC]\r\n cenv []\r\n tys [k_a1Mj[ssk:3]]\r\n cos []\r\n needInScope [a1Mj :-> k_a1Mj[ssk:3]]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1205:22 in ghc:Outputable\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep\r\n substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep\r\n substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1203:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/types/TyCoRep.hs:2136:51 in ghc:TyCoRep\r\n checkValidSubst, called at compiler/types/TyCoRep.hs:2159:29 in ghc:TyCoRep\r\n substTy, called at compiler/types/TyCoRep.hs:2364:41 in ghc:TyCoRep\r\n substTyVarBndr, called at compiler/coreSyn/CoreSubst.hs:571:10 in ghc:CoreSubst\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/18714GHC panic (tcInvisibleTyBinder) when using constraint in a kind2020-09-21T21:17:06ZRyan ScottGHC panic (tcInvisibleTyBinder) when using constraint in a kindThe following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts
type Id...The following program will panic when compiled with GHC 8.10 or HEAD:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Bug where
import GHC.Exts
type Id a = a
type F = Id (Any :: forall a. Show a => a -> a)
```
```
$ /opt/ghc/8.10.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.10.2:
tcInvisibleTyBinder
Show a_avp[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1179:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/Inst.hs:460:5 in ghc:Inst
```
I'm a bit surprised that this happens, since GHC has a validity check intended to rule out the use of arbitrary constraints in kinds. This check is implemented by [`GHC.Tc.Validity.allConstraintsAllowed`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L473-480):
```hs
allConstraintsAllowed :: UserTypeCtxt -> Bool
-- We don't allow arbitrary constraints in kinds
allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
allConstraintsAllowed _ = True
```
Upon closer inspection, `allConstraintsAllowed` appears to be incomplete. Compare this to [`GHC.Tc.Validity.vdqAllowed`](https://gitlab.haskell.org/ghc/ghc/-/blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Validity.hs#L496-507), which must also make a distinction between types and kinds:
```hs
vdqAllowed :: UserTypeCtxt -> Bool
-- Currently allowed in the kinds of types...
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
vdqAllowed (TySynKindCtxt {}) = True
vdqAllowed (TyFamResKindCtxt {}) = True
-- ...but not in the types of terms.
...
```
Note that `vdqAllowed` identifies more `UserTypeCtxt`s as being kind-level positions than `allConstraintsAllowed` does. Crucially, `allConstraintsAllowed` omits a case for `KindSigCtxt`. If I add such as case:
```diff
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..39ebc260da 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -479,6 +479,7 @@ allConstraintsAllowed (DataKindCtxt {}) = False
allConstraintsAllowed (TySynKindCtxt {}) = False
allConstraintsAllowed (TyFamResKindCtxt {}) = False
allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
+allConstraintsAllowed (KindSigCtxt {}) = False
allConstraintsAllowed _ = True
-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
```
Then the program above no longer panics:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:11:14: error:
• Illegal constraint in a kind: forall a. Show a => a -> a
• In the first argument of ‘Id’, namely
‘(Any :: forall a. Show a => a -> a)’
In the type ‘Id (Any :: forall a. Show a => a -> a)’
In the type declaration for ‘F’
|
11 | type F = Id (Any :: forall a. Show a => a -> a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/14520GHC panic (TypeInType)2019-07-07T18:16:41ZIcelandjackGHC panic (TypeInType)```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp:...```hs
{-# Language TypeInType, TypeFamilies, TypeOperators #-}
import Data.Kind
type a ~>> b = (a, b) -> Type
data family Sing (a::k)
type family
(·) (f::a~>>b) (x::a)::b
class PCategory kat where
type Id ::kat·a·a
type Comp::kat·b·c -> kat·a·b -> kat·a·c
class SCategory kat where
sId :: Sing a -> Sing (Id::kat a a)
sComp :: Sing f -> Sing g -> Sing (Comp f g)
```
triggers a panic
```
$ ghci -ignore-dot-ghci Bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
piResultTy
k_a1KI[tau:1]
a_a1vb[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type
typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type
typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic (TypeInType)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language TypeInType, TypeFamilies, TypeOperators #-}\r\n\r\nimport Data.Kind\r\n\r\ntype a ~>> b = (a, b) -> Type\r\n\r\ndata family Sing (a::k)\r\n\r\ntype family\r\n (·) (f::a~>>b) (x::a)::b\r\n\r\nclass PCategory kat where\r\n type Id ::kat·a·a\r\n type Comp::kat·b·c -> kat·a·b -> kat·a·c\r\n\r\nclass SCategory kat where\r\n sId :: Sing a -> Sing (Id::kat a a)\r\n sComp :: Sing f -> Sing g -> Sing (Comp f g)\r\n}}}\r\n\r\ntriggers a panic\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci Bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a1KI[tau:1]\r\n a_a1vb[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n piResultTy, called at compiler/types/Type.hs:2309:34 in ghc:Type\r\n typeKind, called at compiler/types/Type.hs:2309:46 in ghc:Type\r\n typeKind, called at compiler/typecheck/TcType.hs:1706:11 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14580GHC panic (TypeInType) (the 'impossible' happened)2019-07-07T18:16:25ZIcelandjackGHC panic (TypeInType) (the 'impossible' happened)```
$ ghci -ignore-dot-ghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators
Prelude Data.Kind> type Cat ob = ob ...```
$ ghci -ignore-dot-ghci
GHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help
Prelude> import Data.Kind
Prelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators
Prelude Data.Kind> type Cat ob = ob -> ob -> Type
Prelude Data.Kind> data ISO' :: Cat i -> i -> i -> Type
Prelude Data.Kind> type ISO cat a b = ISO' cat a b -> Type
Prelude Data.Kind> type (a <--> b) iso cat = ISO (iso :: cat a b)
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171208 for x86_64-unknown-linux):
piResultTy
k_a1x1[tau:1]
a_a1wU[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
Prelude Data.Kind>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic (TypeInType) (the 'impossible' happened)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{\r\n$ ghci -ignore-dot-ghci\r\nGHCi, version 8.3.20171208: http://www.haskell.org/ghc/ :? for help\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> :set -XPolyKinds -XDataKinds -XTypeInType -XTypeOperators \r\nPrelude Data.Kind> type Cat ob = ob -> ob -> Type\r\nPrelude Data.Kind> data ISO' :: Cat i -> i -> i -> Type\r\nPrelude Data.Kind> type ISO cat a b = ISO' cat a b -> Type\r\nPrelude Data.Kind> type (a <--> b) iso cat = ISO (iso :: cat a b)\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171208 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a1x1[tau:1]\r\n a_a1wU[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1144:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:951:35 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\nPrelude Data.Kind> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14880GHC panic: updateRole2019-07-07T18:15:13ZRyan ScottGHC panic: updateRoleThe following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE...The following program panics on GHC 8.0.2, 8.2.2, 8.4.1, and HEAD:
```hs
{-# 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
```8.6.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15787GHC panic using kind application2019-07-07T18:02:59ZIcelandjackGHC panic using kind applicationUsing GHC head at diff [Visible kind application D5229](https://phabricator.haskell.org/D5229) (#12045),
bug goes away if you remove `@ob`.
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds ...Using GHC head at diff [Visible kind application D5229](https://phabricator.haskell.org/D5229) (#12045),
bug goes away if you remove `@ob`.
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
import Data.Kind
class Ríki (ob :: Type) where
type Hom :: ob -> ob -> Type
data
Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
Kl :: k -> Kl_kind @ob (m) k
type family
UnKl (kl :: Kl_kind m k) = (res :: k) where
UnKl (Kl a) = a
```
```
$ ghci -ignore-dot-ghci 543_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 543_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
Type-correct unfilled coercion hole {co_a1yH}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic using kind application","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Using GHC head at diff [https://phabricator.haskell.org/D5229 Visible kind application D5229] (#12045), \r\n\r\nbug goes away if you remove `@ob`.\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n{-# Language TypeFamilies #-}\r\n\r\nimport Data.Kind\r\n\r\nclass Ríki (ob :: Type) where\r\n type Hom :: ob -> ob -> Type\r\n\r\ndata\r\n Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where\r\n Kl :: k -> Kl_kind @ob (m) k\r\n\r\ntype family\r\n UnKl (kl :: Kl_kind m k) = (res :: k) where\r\n UnKl (Kl a) = a\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 543_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 543_bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181017 for x86_64-unknown-linux):\r\n ASSERT failed!\r\n Type-correct unfilled coercion hole {co_a1yH}\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable\r\n pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable\r\n assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.2https://gitlab.haskell.org/ghc/ghc/-/issues/15709GHC panic using TypeInType with minimal source code2019-07-07T18:03:20ZjnapeGHC panic using TypeInType with minimal source codeThe following source code causes GHC 8.4.3 on 64bit Linux to panic:
```haskell
{-# LANGUAGE TypeInType #-}
module Lib where
import Data.Kind
class Contravariant f where
contramap :: (a -> b) -> f b -> f a
dimap :: (Contravariant...The following source code causes GHC 8.4.3 on 64bit Linux to panic:
```haskell
{-# LANGUAGE TypeInType #-}
module Lib where
import Data.Kind
class Contravariant f where
contramap :: (a -> b) -> f b -> f a
dimap :: (Contravariant (p :: * -> b -> p * b), Functor (p a)) => (z -> a) -> (b -> c) -> p a b -> p z c
dimap f g = contramap f . fmap g
```
I have no idea if it should compile or not, but it shouldn't do this:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.3 for x86_64-unknown-linux):
piResultTy
k_a34u[tau:1]
*
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
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic using TypeInType with minimal source code","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following source code causes GHC 8.4.3 on 64bit Linux to panic:\r\n\r\n{{{#!haskell\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nmodule Lib where\r\n\r\nimport Data.Kind\r\n\r\nclass Contravariant f where\r\n contramap :: (a -> b) -> f b -> f a\r\n\r\ndimap :: (Contravariant (p :: * -> b -> p * b), Functor (p a)) => (z -> a) -> (b -> c) -> p a b -> p z c\r\ndimap f g = contramap f . fmap g\r\n}}}\r\n\r\nI have no idea if it should compile or not, but it shouldn't do this:\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.3 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_a34u[tau:1]\r\n *\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:947:35 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15789GHC panic using visible kind applications and a higher-rank kind2019-07-07T18:02:59ZIcelandjackGHC panic using visible kind applications and a higher-rank kindUsing visible kind applications (#12045):
```hs
{-# Language LiberalTypeSynonyms #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
import Data.Kind
type Cat ob = ob -> o...Using visible kind applications (#12045):
```hs
{-# Language LiberalTypeSynonyms #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
import Data.Kind
type Cat ob = ob -> ob -> Type
data Zero :: forall (cat :: forall xx. xx -> Type) a. forall b. Cat (forall b. cat b u)
```
```
$ ghci -ignore-dot-ghci 546_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 546_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
Type-correct unfilled coercion hole {co_a1yl}
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/utils/Outputable.hs:1219:5 in ghc:Outputable
assertPprPanic, called at compiler/typecheck/TcHsSyn.hs:1805:99 in ghc:TcHsSyn
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```https://gitlab.haskell.org/ghc/ghc/-/issues/11334GHC panic when calling typeOf on a promoted data constructor2019-07-07T18:30:53ZRyan ScottGHC panic when calling typeOf on a promoted data constructorHere's what I did in GHCi to trigger the panic:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help
λ> :set -XDataKinds
λ> :m Data.Typeable Data.Functor.Compose
λ> typeOf (Prox...Here's what I did in GHCi to trigger the panic:
```
$ inplace/bin/ghc-stage2 --interactive
GHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help
λ> :set -XDataKinds
λ> :m Data.Typeable Data.Functor.Compose
λ> typeOf (Proxy :: Proxy 'Compose)
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.1.20160101 for x86_64-unknown-linux):
piResultTy
*
TYPE 'Lifted *
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Enabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:
```
λ> :set -XPolyKinds
λ> typeOf (Proxy :: Proxy 'Compose)
<interactive>:5:1: error:
• No instance for (Typeable a0) arising from a use of ‘typeOf’
• In the expression: typeOf (Proxy :: Proxy Compose)
In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic when calling typeOf on a promoted data constructor","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"Here's what I did in GHCi to trigger the panic:\r\n\r\n{{{\r\n$ inplace/bin/ghc-stage2 --interactive\r\nGHCi, version 8.1.20160101: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XDataKinds\r\nλ> :m Data.Typeable Data.Functor.Compose\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.1.20160101 for x86_64-unknown-linux):\r\n piResultTy\r\n *\r\n TYPE 'Lifted *\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nEnabling `-XPolyKinds` doesn't trigger the error, though; #10343 will be triggered instead:\r\n\r\n{{{\r\nλ> :set -XPolyKinds\r\nλ> typeOf (Proxy :: Proxy 'Compose)\r\n\r\n<interactive>:5:1: error:\r\n • No instance for (Typeable a0) arising from a use of ‘typeOf’\r\n • In the expression: typeOf (Proxy :: Proxy Compose)\r\n In an equation for ‘it’: it = typeOf (Proxy :: Proxy Compose)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.0.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14174GHC panic with TypeInType and type family2019-07-07T18:18:09ZDavid FeuerGHC panic with TypeInType and type familyThis rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y...This rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y
```
produces the following panic:
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
piResultTy
k_a1LK[tau:1]
p_a1Lz[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
```
This happens with both GHC 8.2.1 and something very close to HEAD.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic with TypeInType and type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This rather simple type family,\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}\r\n\r\nmodule GenWhoops where\r\nimport GHC.Generics\r\n\r\ntype family GenComp k (x :: k) (y :: k) :: Ordering where\r\n GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y\r\n}}}\r\n\r\nproduces the following panic:\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n piResultTy\r\n k_a1LK[tau:1]\r\n p_a1Lz[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type\r\n}}}\r\n\r\nThis happens with both GHC 8.2.1 and something very close to HEAD.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/14563GHC Panic with TypeInType / levity polymorphism2019-07-07T18:16:30ZIcelandjackGHC Panic with TypeInType / levity polymorphismThis code is rightfully rejected.
```hs
-- {-# Language TypeInType #-}
{-# Language RankNTypes, KindSignatures, PolyKinds #-}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a w...This code is rightfully rejected.
```hs
-- {-# Language TypeInType #-}
{-# Language RankNTypes, KindSignatures, PolyKinds #-}
import GHC.Types (TYPE)
import Data.Kind
data Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. (g xx -> a) -> h xx -> Lan g h a
```
But uncomment first line and it panics
```
$ ghci2 ~/hs/132-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/132-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
>
```
Maybe the same as #14555.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code is rightfully rejected.\r\n\r\n{{{#!hs\r\n-- {-# Language TypeInType #-}\r\n{-# Language RankNTypes, KindSignatures, PolyKinds #-}\r\n\r\nimport GHC.Types (TYPE)\r\nimport Data.Kind\r\n\r\ndata Lan (g::TYPE rep -> TYPE rep') (h::TYPE rep -> TYPE rep'') a where Lan :: forall xx (g::TYPE rep -> TYPE rep') (h::TYPE rep -> Type) a. (g xx -> a) -> h xx -> Lan g h a\r\n}}}\r\n\r\nBut uncomment first line and it panics\r\n\r\n{{{\r\n$ ghci2 ~/hs/132-bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/132-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n\r\n> \r\n}}}\r\n\r\nMaybe the same as #14555.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14555GHC Panic with TypeInType / levity polymorphism2019-07-07T18:16:32ZIcelandjackGHC Panic with TypeInType / levity polymorphism```hs
{-# Language TypeInType #-}
{-# Language TypeOperators, DataKinds, PolyKinds #-}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] -> TYPE rep -> Type where
Lam :: Exp (a:xs) b -> Exp xs (a -> b)
```
gives
```
$...```hs
{-# Language TypeInType #-}
{-# Language TypeOperators, DataKinds, PolyKinds #-}
import Data.Kind
import GHC.Types (TYPE)
data Exp :: [TYPE rep] -> TYPE rep -> Type where
Lam :: Exp (a:xs) b -> Exp xs (a -> b)
```
gives
```
$ ghci -ignore-dot-ghci hs/126-bug.hs
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20171122 for x86_64-unknown-linux):
zonkTcTyVarToVar
'LiftedRep
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
caused by `TypeInType`. Removing the first line, we get an error
```
GHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )
hs/126-bug.hs:7:19: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] -> TYPE rep -> Type’
|
7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where
| ^^^
hs/126-bug.hs:7:32: error:
• Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’
• In the first argument of ‘TYPE’, namely ‘rep’
In the kind ‘[TYPE rep] -> TYPE rep -> Type’
|
7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where
| ^^^
Failed, no modules loaded.
Prelude>
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC Panic with TypeInType / levity polymorphism","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language TypeInType #-}\r\n{-# Language TypeOperators, DataKinds, PolyKinds #-}\r\n\r\nimport Data.Kind\r\nimport GHC.Types (TYPE)\r\n\r\ndata Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n Lam :: Exp (a:xs) b -> Exp xs (a -> b)\r\n}}}\r\n\r\ngives\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci hs/126-bug.hs\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20171122 for x86_64-unknown-linux):\r\n\tzonkTcTyVarToVar\r\n 'LiftedRep\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1147:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcType.hs:1640:17 in ghc:TcType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\ncaused by `TypeInType`. Removing the first line, we get an error\r\n\r\n{{{\r\nGHCi, version 8.3.20171122: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( hs/126-bug.hs, interpreted )\r\n\r\nhs/126-bug.hs:7:19: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] -> TYPE rep -> Type’\r\n |\r\n7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n | ^^^\r\n\r\nhs/126-bug.hs:7:32: error:\r\n • Expected kind ‘GHC.Types.RuntimeRep’, but ‘rep’ has kind ‘*’\r\n • In the first argument of ‘TYPE’, namely ‘rep’\r\n In the kind ‘[TYPE rep] -> TYPE rep -> Type’\r\n |\r\n7 | data Exp :: [TYPE rep] -> TYPE rep -> Type where\r\n | ^^^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->