GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:02:37Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15874Data families with higher-rank kinds2019-07-07T18:02:37ZIcelandjackData families with higher-rank kinds```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
import Data.Kind
data Var where
Op :: Var
Id :: Var
-- type family
-- Fl...```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
import Data.Kind
data Var where
Op :: Var
Id :: Var
-- type family
-- Flip (var :: Var) = (res :: Var) | res -> var where
-- Flip Op = Id
-- Flip Id = Op
type Varianced = (forall (var :: Var). Type)
-- data A :: Varianced where
-- MkA :: Int -> A @Id
-- data OpA :: Varianced where
-- MkOpA :: Int -> OpA @Op
-- data Exp :: Varianced -> Varianced where
-- X :: forall (ext::Varianced) (var :: Var). Exp ext @var
-- OpExp1 :: forall (var :: Varianced). var @op -> Exp var @(Flip op)
data family Parser :: Varianced
data instance Parser = P
```
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 656.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 656.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64-unknown-linux):
ASSERT failed!
kind axiom D:R:Parservar0 ::
Parser = R:Parservar -- Defined at 656.hs:31:15
forall (var :: Var). *
Var -> *
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/FamInst.hs:158:61 in ghc:FamInst
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":"Data families with higher-rank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","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 DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n{-# Language TypeFamilies #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Var where\r\n Op :: Var\r\n Id :: Var\r\n\r\n-- type family\r\n-- Flip (var :: Var) = (res :: Var) | res -> var where\r\n-- Flip Op = Id\r\n-- Flip Id = Op\r\n\r\ntype Varianced = (forall (var :: Var). Type)\r\n\r\n-- data A :: Varianced where\r\n-- MkA :: Int -> A @Id\r\n\r\n-- data OpA :: Varianced where\r\n-- MkOpA :: Int -> OpA @Op\r\n\r\n-- data Exp :: Varianced -> Varianced where\r\n-- X :: forall (ext::Varianced) (var :: Var). Exp ext @var\r\n -- OpExp1 :: forall (var :: Varianced). var @op -> Exp var @(Flip op)\r\n\r\ndata family Parser :: Varianced\r\ndata instance Parser = P\r\n}}}\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 656.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 656.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64-unknown-linux):\r\n ASSERT failed!\r\n kind axiom D:R:Parservar0 ::\r\n Parser = R:Parservar -- Defined at 656.hs:31:15\r\n forall (var :: Var). *\r\n Var -> *\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/FamInst.hs:158:61 in ghc:FamInst\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/15872Odd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)2019-07-07T18:02:37ZIcelandjackOdd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)Maybe indicative of deeper issues:
```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data WHICH = OP | OPOP
data Fun :: forall (a :: WHICH). a ~ OP ...Maybe indicative of deeper issues:
```hs
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
import Data.Kind
data WHICH = OP | OPOP
data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
MkFun :: (a -> b) -> Fun a b
```
There are some artifacts `Fun ('GHC.Type.Eq# <>)` in the type of `MkFun` that shouldn't be there
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/655_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/baldur/hs/655_bug.hs, interpreted )
Ok, one module loaded.
*Main> :t MkFun
MkFun :: (a -> b) -> Fun ('GHC.Types.Eq# <>) a b
*Main> :k Fun
Fun :: (a ~ 'OP) => * -> * -> *
*Main>
```
----
Tangent: Omitting `{-# Language GADTs #-}` we get the term "equational constraint" which is not the term I have seen in the wild
```
$ latestbug 655_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 655_bug.hs, interpreted )
655_bug.hs:9:1: error:
Illegal equational constraint a ~ 'OP
(Use GADTs or TypeFamilies to permit this)
|
9 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Failed, no modules loaded.
Prelude>
```
<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":"Odd pretty printing of equality constraint in kind ('GHC.Types.Eq# <>)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Maybe indicative of deeper issues:\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language GADTs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata WHICH = OP | OPOP\r\n\r\ndata Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where\r\n MkFun :: (a -> b) -> Fun a b\r\n}}}\r\n\r\nThere are some artifacts `Fun ('GHC.Type.Eq# <>)` in the type of `MkFun` that shouldn't be there\r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci ~/hs/655_bug.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /home/baldur/hs/655_bug.hs, interpreted )\r\nOk, one module loaded.\r\n*Main> :t MkFun\r\nMkFun :: (a -> b) -> Fun ('GHC.Types.Eq# <>) a b\r\n*Main> :k Fun\r\nFun :: (a ~ 'OP) => * -> * -> *\r\n*Main>\r\n}}}\r\n\r\n----\r\n\r\nTangent: Omitting `{-# Language GADTs #-}` we get the term \"equational constraint\" which is not the term I have seen in the wild\r\n\r\n{{{\r\n$ latestbug 655_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 655_bug.hs, interpreted )\r\n\r\n655_bug.hs:9:1: error:\r\n Illegal equational constraint a ~ 'OP\r\n (Use GADTs or TypeFamilies to permit this)\r\n |\r\n9 | data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\nFailed, no modules loaded.\r\nPrelude>\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/15862Panic with promoted types that Typeable doesn't support2020-02-25T01:15:47ZRyan ScottPanic with promoted types that Typeable doesn't supportThe following program panics on GHC 8.2 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Type.Reflection
newtype Foo ...The following program panics on GHC 8.2 and later:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Type.Reflection
newtype Foo = MkFoo (forall a. a)
foo :: TypeRep MkFoo
foo = typeRep @MkFoo
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
GHC error in desugarer lookup in Bug:
attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.1 for x86_64-unknown-linux):
initDs
```
<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":"Typeable panic with promoted rank-2 kind (initDs)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.2 and later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE ImpredicativeTypes #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\nnewtype Foo = MkFoo (forall a. a)\r\n\r\nfoo :: TypeRep MkFoo\r\nfoo = typeRep @MkFoo\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nGHC error in desugarer lookup in Bug:\r\n attempting to use module ‘main:Bug’ (Bug.hs) which is not loaded\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.1 for x86_64-unknown-linux):\r\n initDs\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/15859Dependent quantification, GHC panic2019-07-07T18:02:41ZIcelandjackDependent quantification, GHC panicWhile exploring [Ryan's gist for term-level](https://gist.github.com/RyanGlScott/ded669b5ae3db1ce38c4b6021f144776) `f :: forall a -> a -> Type`.
```hs
{-# Language PolyKinds #-}
{-# Language TypeApplications #-}
{-# Language ...While exploring [Ryan's gist for term-level](https://gist.github.com/RyanGlScott/ded669b5ae3db1ce38c4b6021f144776) `f :: forall a -> a -> Type`.
```hs
{-# Language PolyKinds #-}
{-# Language TypeApplications #-}
{-# Language ImpredicativeTypes #-}
import Data.Kind
data A k :: k -> Type
f :: KindOf A
f a = undefined
type KindOf (a :: k) = k
a = f @Int
```
gives
```
$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 630_bug.hs
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 630_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181029 for x86_64-unknown-linux):
ASSERT failed!
KindOf A
forall k -> k -> *
k_a1xQ[sk:0]
k_a1xQ[sk:0] -> *
k_a1xQ[sk:0]
[req]
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/TcExpr.hs:1336:94 in ghc:TcExpr
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":"Dependent quantification, GHC panic","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"While exploring [https://gist.github.com/RyanGlScott/ded669b5ae3db1ce38c4b6021f144776 Ryan's gist for term-level] `f :: forall a -> a -> Type`.\r\n\r\n{{{#!hs\r\n{-# Language PolyKinds #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language ImpredicativeTypes #-}\r\n\r\nimport Data.Kind\r\n\r\ndata A k :: k -> Type\r\n\r\nf :: KindOf A\r\nf a = undefined\r\n\r\ntype KindOf (a :: k) = k\r\n\r\na = f @Int\r\n}}}\r\n\r\ngives \r\n\r\n{{{\r\n$ ~/code/unmodifiedghc/inplace/bin/ghc-stage2 --interactive -ignore-dot-ghci 630_bug.hs\r\nGHCi, version 8.7.20181029: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 630_bug.hs, interpreted )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181029 for x86_64-unknown-linux):\r\n ASSERT failed!\r\n KindOf A\r\n forall k -> k -> *\r\n k_a1xQ[sk:0]\r\n k_a1xQ[sk:0] -> *\r\n k_a1xQ[sk:0]\r\n [req]\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/TcExpr.hs:1336:94 in ghc:TcExpr\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.3https://gitlab.haskell.org/ghc/ghc/-/issues/15852Bad axiom produced for polykinded data family2019-07-07T18:02:43ZRichard Eisenbergrae@richarde.devBad axiom produced for polykinded data familyWhen I say
```hs
data family DF a (b :: k)
data instance DF (Proxy c) :: Proxy j -> Type
```
with `-ddump-tc`, I get
```
axiom Scratch.D:R:DFProxyProxy0 ::
forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
DF (Proxy c) a = ...When I say
```hs
data family DF a (b :: k)
data instance DF (Proxy c) :: Proxy j -> Type
```
with `-ddump-tc`, I get
```
axiom Scratch.D:R:DFProxyProxy0 ::
forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
DF (Proxy c) a = Scratch.R:DFProxyProxy k1 k2 c j
```
This is bogus, because `a` should be on the RHS, too. It's not clear to me whether this is a pretty-printing bug or a real one.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.7 |
| 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":"Bad axiom produced for polykinded data family","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.7","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\ndata family DF a (b :: k)\r\ndata instance DF (Proxy c) :: Proxy j -> Type\r\n}}}\r\n\r\nwith `-ddump-tc`, I get\r\n\r\n{{{\r\n axiom Scratch.D:R:DFProxyProxy0 ::\r\n forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).\r\n DF (Proxy c) a = Scratch.R:DFProxyProxy k1 k2 c j\r\n}}}\r\n\r\nThis is bogus, because `a` should be on the RHS, too. It's not clear to me whether this is a pretty-printing bug or a real one.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15817Data family quantification = GHC panic, ‘impossible’ happened2019-07-07T18:02:52ZIcelandjackData family quantification = GHC panic, ‘impossible’ happened```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
data family Pair :: forall a. forall b. *
data instance Pa...```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language PolyKinds #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
data family Pair :: forall a. forall b. *
data instance Pair @a @b = MkPair a b
```
```
$ ghci -ignore-dot-ghci 593_bug.hs
GHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 593_bug.hs, interpreted )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181017 for x86_64-unknown-linux):
ASSERT failed!
kind axiom D:R:Pairabab0 ::
forall a b (a :: a) (b :: b).
Pair = R:Pairabab -- Defined at 593_bug.hs:8:15
forall k k (a :: k) (b :: k). *
forall a b -> a -> b -> *
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/FamInst.hs:158:61 in ghc:FamInst
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 | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Visible kind application + data family = GHC panic, ‘impossible’ happened","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language TypeFamilies #-}\r\n\r\ndata family Pair :: forall a. forall b. *\r\ndata instance Pair @a @b = MkPair a b\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci 593_bug.hs\r\nGHCi, version 8.7.20181017: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( 593_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 kind axiom D:R:Pairabab0 ::\r\n forall a b (a :: a) (b :: b).\r\n Pair = R:Pairabab -- Defined at 593_bug.hs:8:15\r\n forall k k (a :: k) (b :: k). *\r\n forall a b -> a -> b -> *\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/FamInst.hs:158:61 in ghc:FamInst\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/15795Core lint error with unused kind variable in data type return kind2019-07-07T18:02:57ZIcelandjackCore lint error with unused kind variable in data type return kindFinally managed to trigger a core lint error with #12045
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language TypeOpera...Finally managed to trigger a core lint error with #12045
```hs
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Options_GHC -dcore-lint #-}
import Data.Kind
type Cat ob = ob -> ob -> Type
data (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where
Prod
:: forall
ob1 ob2
cat1 cat2
a1 b1
a2 b2 u.
cat1 a1 b1
-> cat2 a2 b2
-> (×) @u '(a1, a2) '(b1, b2)
```
log attached from running `ghci -ignore-dot-ghci <file>.hs`
<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 | mnguyen |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Core lint error with visible kind patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeApplications"],"differentials":[],"test_case":"","architecture":"","cc":["mnguyen"],"type":"Bug","description":"Finally managed to trigger a core lint error with #12045\r\n\r\n{{{#!hs\r\n{-# Language RankNTypes #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language DataKinds #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language TypeOperators #-}\r\n{-# Language GADTs #-}\r\n{-# Options_GHC -dcore-lint #-}\r\n\r\nimport Data.Kind\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ndata (×) :: forall (cat1 :: Cat ob1) (cat2 :: Cat ob2). Cat (ob1, ob2) where\r\n Prod\r\n :: forall\r\n ob1 ob2\r\n cat1 cat2\r\n a1 b1\r\n a2 b2 u.\r\n cat1 a1 b1\r\n -> cat2 a2 b2\r\n -> (×) @u '(a1, a2) '(b1, b2)\r\n}}}\r\n\r\nlog attached from running `ghci -ignore-dot-ghci <file>.hs`","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/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/15778GHC HEAD-only panic (zonkTcTyVarToTyVar)2019-07-07T18:03:02ZRyan ScottGHC HEAD-only panic (zonkTcTyVarToTyVar)The following program typechecks on GHC 8.0.1 through 8.6.1:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUA...The following program typechecks on GHC 8.0.1 through 8.6.1:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
type a ~> b = a -> b -> Type
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing (a :: k)
data Flarble (a :: Type) where
MkFlarble :: Flarble Bool
data instance Sing (z :: Flarble a) where
SMkFlarble :: Sing MkFlarble
elimFlarble :: forall a
(p :: forall x. Flarble x ~> Type)
(f :: Flarble a).
Sing f
-> Apply p MkFlarble
-> Apply p f
elimFlarble s@SMkFlarble pMkFlarble =
case s of
(_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) ->
pMkFlarble
```
However, it panics on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20181015 for x86_64-unknown-linux):
zonkTcTyVarToTyVar
probablyABadIdea_aWn[tau:2]
Bool
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcMType.hs:1627:34 in ghc:TcMType
```
If I replace `probablyABadIdea` with `Bool`, then it typechecks again.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD-only panic (zonkTcTyVarToTyVar)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.0.1 through 8.6.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype a ~> b = a -> b -> Type\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing (a :: k)\r\n\r\ndata Flarble (a :: Type) where\r\n MkFlarble :: Flarble Bool\r\ndata instance Sing (z :: Flarble a) where\r\n SMkFlarble :: Sing MkFlarble\r\n\r\nelimFlarble :: forall a\r\n (p :: forall x. Flarble x ~> Type)\r\n (f :: Flarble a).\r\n Sing f\r\n -> Apply p MkFlarble\r\n -> Apply p f\r\nelimFlarble s@SMkFlarble pMkFlarble =\r\n case s of\r\n (_ :: Sing (MkFlarble :: Flarble probablyABadIdea)) ->\r\n pMkFlarble\r\n}}}\r\n\r\nHowever, it panics on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20181015 for x86_64-unknown-linux):\r\n zonkTcTyVarToTyVar\r\n probablyABadIdea_aWn[tau:2]\r\n Bool\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/TcMType.hs:1627:34 in ghc:TcMType\r\n}}}\r\n\r\nIf I replace `probablyABadIdea` with `Bool`, then it typechecks again.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15740Type family with higher-rank result is too accepting2019-07-07T18:03:10ZRichard Eisenbergrae@richarde.devType family with higher-rank result is too acceptingGHC accepts this garbage:
```
type family F2 :: forall k. k -> Type
data SBool :: Bool -> Type
data Nat
data SNat :: Nat -> Type
type instance F2 = SBool
type instance F2 = SNat
```
The family `F2` should have an arity of 0, meaning th...GHC accepts this garbage:
```
type family F2 :: forall k. k -> Type
data SBool :: Bool -> Type
data Nat
data SNat :: Nat -> Type
type instance F2 = SBool
type instance F2 = SNat
```
The family `F2` should have an arity of 0, meaning that only one instance is possible -- and the RHS of that instance must have kind `forall k. k -> Type`. In other words, even accepting only one of the instances above is hogwash.
This is from [ticket:11719\#comment:161416](https://gitlab.haskell.org//ghc/ghc/issues/11719#note_161416), but you don't have to read that to understand this.
<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":"Type family with higher-rank result is too accepting","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC accepts this garbage:\r\n\r\n{{{\r\ntype family F2 :: forall k. k -> Type\r\ndata SBool :: Bool -> Type\r\ndata Nat\r\ndata SNat :: Nat -> Type\r\ntype instance F2 = SBool\r\ntype instance F2 = SNat\r\n}}}\r\n\r\nThe family `F2` should have an arity of 0, meaning that only one instance is possible -- and the RHS of that instance must have kind `forall k. k -> Type`. In other words, even accepting only one of the instances above is hogwash.\r\n\r\nThis is from comment:15:ticket:11719, but you don't have to read that to understand this.","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15711Kind inference of class variables does not examine associated types2019-07-07T18:03:20ZRichard Eisenbergrae@richarde.devKind inference of class variables does not examine associated typesIf I say this
```
{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds #-}
module Bug where
class C a where
type F (x :: Maybe a)
```
then GHCi says this
```
*Bug> :k C
C :: k -> Constraint
```
That's silly. `C` should have kind `Type...If I say this
```
{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds #-}
module Bug where
class C a where
type F (x :: Maybe a)
```
then GHCi says this
```
*Bug> :k C
C :: k -> Constraint
```
That's silly. `C` should have kind `Type -> Constraint`, because the usage of `a` in the kind of the associated type constraints `a`'s kind.
Will fix.
<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":"Kind inference of class variables does not examine associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say this\r\n\r\n{{{\r\n{-# LANGUAGE TypeFamilies, PolyKinds, DataKinds #-}\r\n\r\nmodule Bug where\r\n\r\nclass C a where\r\n type F (x :: Maybe a)\r\n}}}\r\n\r\nthen GHCi says this\r\n\r\n{{{\r\n*Bug> :k C\r\nC :: k -> Constraint\r\n}}}\r\n\r\nThat's silly. `C` should have kind `Type -> Constraint`, because the usage of `a` in the kind of the associated type constraints `a`'s kind.\r\n\r\nWill fix.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15710Should GHC accept a type signature that needs coercion quantification?2023-03-23T12:00:56ZSimon Peyton JonesShould GHC accept a type signature that needs coercion quantification?Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being...Consider
```
f :: forall k (f :: k) (x :: k1). (k ~ (k1 -> *)) => f x
f = error "uk"
```
Should we accept it? Now that we have coercion quantification (Trac #15497), I think the answer should be yes, with the elaborated signature being
```
f :: forall k (f::k) (x::k1). forall (co :: k ~# (k1->*)). (f |> co) x
```
But there is a problem: the user wrote `k ~ (k1 -> *)`, and that's a boxed value that we can't take apart in types. I'm not sure what to do here.
These thoughts arose when contemplating `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`; see [ticket:15710\#comment:161240](https://gitlab.haskell.org//ghc/ghc/issues/15710#note_161240) in #15497https://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/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/15664Core Lint error2019-07-07T18:03:32ZIcelandjackCore Lint errorFrom [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
import Data.K...From [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
import Data.Kind
import GHC.Exts
import Data.Function
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
type family
Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where
Apply(Type) a E = a
Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind -> Ctx(kind) -> Type where
A0 :: a
-> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as
-> ApplyT(k -> ks) f (a:&:as)
type f ~> g = (forall xx. f xx -> g xx)
unravel :: ApplyT(k) f ~> Apply(k) f
unravel (A0 a) = a
unravel (AS fa) = unravel fa
```
gives a core lint error
```
$ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15629"No skolem info" panic (GHC 8.6 only)2019-07-07T18:03:40ZRyan Scott"No skolem info" panic (GHC 8.6 only)The following program:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug wher...The following program:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Proxy
import GHC.Generics
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: forall k. k -> Type
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
singFun1 :: forall f. (forall t. Sing t -> Sing (Apply f t)) -> Sing f
singFun1 f = SLambda f
data From1Sym0 :: forall k (f :: k -> Type) (a :: k). f a ~> Rep1 f a
data To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a
type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
(f :. g) x = Apply f (Apply g x)
data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
type instance Apply (f .@#@$$$ g) x = (f :. g) x
(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
(sf %. sg) sx = applySing sf (applySing sg sx)
(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).
Sing f -> Sing g -> Sing (f .@#@$$$ g)
sf %.$$$ sg = singFun1 (sf %. sg)
f :: forall (m :: Type -> Type) x. Proxy (m x) -> ()
f _ = ()
where
sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)
sFrom1Fun = undefined
sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)
sTo1Fun = undefined
sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
```
Panics on GHC 8.6:
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab1’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)
|
50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180823 for x86_64-unknown-linux):
No skolem info:
[ab_a1UW[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
```
But merely errors on GHC 8.4.3:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:50:39: error:
• Expected kind ‘m z ~> Rep1 m ab2’,
but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’
• In the first argument of ‘(.@#@$$$)’, namely
‘(From1Sym0 :: m z ~> Rep1 m z)’
In the first argument of ‘Sing’, namely
‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)’
In the type signature:
sFrom1To1Fun :: forall ab.
Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab
~> Rep1 m ab)
|
50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:51:20: error:
• Couldn't match type ‘ab1’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5-112
Expected type: Sing From1Sym0
Actual type: Sing From1Sym0
• In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)
|
51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
| ^^^^^^^^^
Bug.hs:51:36: error:
• Couldn't match type ‘ab’ with ‘z1’
because type variable ‘z1’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)
at Bug.hs:50:5-112
Expected type: Sing To1Sym0
Actual type: Sing To1Sym0
• In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’
In the expression: sFrom1Fun %.$$$ sTo1Fun
In an equation for ‘sFrom1To1Fun’:
sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
• Relevant bindings include
sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)
(bound at Bug.hs:51:5)
|
51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun
| ^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.6.1-beta1 |
| 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":"\"No skolem info\" panic (GHC 8.6 only)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.6.1-beta1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport GHC.Generics\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata family Sing :: forall k. k -> Type\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }\r\nsingFun1 :: forall f. (forall t. Sing t -> Sing (Apply f t)) -> Sing f\r\nsingFun1 f = SLambda f\r\n\r\ndata From1Sym0 :: forall k (f :: k -> Type) (a :: k). f a ~> Rep1 f a\r\ndata To1Sym0 :: forall k (f :: k -> Type) (a :: k). Rep1 f a ~> f a\r\n\r\ntype family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where\r\n (f :. g) x = Apply f (Apply g x)\r\n\r\ndata (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)\r\ntype instance Apply (f .@#@$$$ g) x = (f :. g) x\r\n\r\n(%.) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)\r\n(sf %. sg) sx = applySing sf (applySing sg sx)\r\n\r\n(%.$$$) :: forall a b c (f :: b ~> c) (g :: a ~> b) (x :: a).\r\n Sing f -> Sing g -> Sing (f .@#@$$$ g)\r\nsf %.$$$ sg = singFun1 (sf %. sg)\r\n\r\nf :: forall (m :: Type -> Type) x. Proxy (m x) -> ()\r\nf _ = ()\r\n where\r\n sFrom1Fun :: forall ab. Sing (From1Sym0 :: m ab ~> Rep1 m ab)\r\n sFrom1Fun = undefined\r\n\r\n sTo1Fun :: forall ab. Sing (To1Sym0 :: Rep1 m ab ~> m ab)\r\n sTo1Fun = undefined\r\n\r\n sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n}}}\r\n\r\nPanics on GHC 8.6:\r\n\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab1’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n |\r\n50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180823 for x86_64-unknown-linux):\r\n No skolem info:\r\n [ab_a1UW[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\nBut merely errors on GHC 8.4.3:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs \r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:50:39: error:\r\n • Expected kind ‘m z ~> Rep1 m ab2’,\r\n but ‘(From1Sym0 :: m z ~> Rep1 m z)’ has kind ‘m z ~> Rep1 m z’\r\n • In the first argument of ‘(.@#@$$$)’, namely\r\n ‘(From1Sym0 :: m z ~> Rep1 m z)’\r\n In the first argument of ‘Sing’, namely\r\n ‘(((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)’\r\n In the type signature:\r\n sFrom1To1Fun :: forall ab.\r\n Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab\r\n ~> Rep1 m ab)\r\n |\r\n50 | sFrom1To1Fun :: forall ab. Sing (((From1Sym0 :: m z ~> Rep1 m z) .@#@$$$ To1Sym0) :: Rep1 m ab ~> Rep1 m ab)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:51:20: error:\r\n • Couldn't match type ‘ab1’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5-112\r\n Expected type: Sing From1Sym0\r\n Actual type: Sing From1Sym0\r\n • In the first argument of ‘(%.$$$)’, namely ‘sFrom1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n |\r\n51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n | ^^^^^^^^^\r\n\r\nBug.hs:51:36: error:\r\n • Couldn't match type ‘ab’ with ‘z1’\r\n because type variable ‘z1’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n sFrom1To1Fun :: forall z1 ab3. Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n at Bug.hs:50:5-112\r\n Expected type: Sing To1Sym0\r\n Actual type: Sing To1Sym0\r\n • In the second argument of ‘(%.$$$)’, namely ‘sTo1Fun’\r\n In the expression: sFrom1Fun %.$$$ sTo1Fun\r\n In an equation for ‘sFrom1To1Fun’:\r\n sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n • Relevant bindings include\r\n sFrom1To1Fun :: Sing (From1Sym0 .@#@$$$ To1Sym0)\r\n (bound at Bug.hs:51:5)\r\n |\r\n51 | sFrom1To1Fun = sFrom1Fun %.$$$ sTo1Fun\r\n | ^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1https://gitlab.haskell.org/ghc/ghc/-/issues/15597GHC shouting: panic!2019-07-07T18:03:54ZtstrGHC shouting: panic!This program makes the impossible happen:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import GHC.Types
data Bug :: (f x -> Type) -> Type where
Bug :: forall
(r::h -> forall x. f x -> Type)
(a::f x)
. (r::...This program makes the impossible happen:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
import GHC.Types
data Bug :: (f x -> Type) -> Type where
Bug :: forall
(r::h -> forall x. f x -> Type)
(a::f x)
. (r::((f x -> Type) -> Type) -> forall x. f x -> Type) Bug a
-> Bug (r::f x -> Type)
```
And asked for reporting the error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 8.4.1 for x86_64-unknown-linux):
piResultTy
k_aozeA[tau:1]
(x_aozeN[sk:2] |> {co_aozeO})
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1150:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:950:35 in ghc:Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.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 shouting: panic!","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program makes the impossible happen:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport GHC.Types\r\n\r\ndata Bug :: (f x -> Type) -> Type where\r\n Bug :: forall\r\n (r::h -> forall x. f x -> Type)\r\n (a::f x)\r\n . (r::((f x -> Type) -> Type) -> forall x. f x -> Type) Bug a\r\n -> Bug (r::f x -> Type)\r\n}}}\r\n\r\n\r\nAnd asked for reporting the error:\r\n\r\n{{{\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.4.1 for x86_64-unknown-linux):\r\n\tpiResultTy\r\n k_aozeA[tau:1]\r\n (x_aozeN[sk:2] |> {co_aozeO})\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:950:35 in ghc:Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/15589Always promoting metavariables during type inference may be wrong2019-07-07T18:04:00ZRichard Eisenbergrae@richarde.devAlways promoting metavariables during type inference may be wrongCurrently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{-# LANGUAGE ScopedTypeVariables, Typ...Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.
Consider
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
This panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.
- We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.
- In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.
- If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.
- Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.
- Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.
Yet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these "ambient givens" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.
An alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [my thesis](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs) -- section 6.5 to be specific.)
<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":"Always promoting metavariables during type inference may be wrong","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Currently, when checking a type signature, GHC promotes all the metavariables that arise during checking as soon as it's done checking the signature. This may be incorrect sometimes.\r\n\r\nConsider\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #-}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k -> k -> Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall (cb :: Bool) (c :: Proxy cb). cb :~: True -> ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nThis panics currently (#15588), but I'm pretty sure it will erroneously be rejected even after the panic is fixed. Let's walk through it.\r\n\r\n* We can derive `IfK :: forall (j :: Bool) (m :: Type) (n :: Type). Proxy j -> m -> n -> If j m n`, where `If :: forall k. Bool -> k -> k -> k` is imported from `Data.Type.Bool` and is a straightforward conditional choice operator.\r\n\r\n* In the type of `x`, we see that we need the kind of `IfK c b d` to match the kind of `d`. That is, if `b :: kappa[3]`, we have `[W] If cb kappa[3] a ~ a`. Here, the `forall` in `x`'s type is at level 3; the RHS of `y` is at level 2.\r\n\r\n* If we could reduce `If cb kappa[3] a` to `kappa[3]`, then we would solve `kappa[3] := a`, but we can't make this reduction, because `cb` is a skolem.\r\n\r\n* Instead, we finish checking the type of `x` and promote `kappa[3]` to `kappa[2]`.\r\n\r\n* Later, we'll make an implication constraint with `[G] cb ~ True`. When solving that implication constraint, we'll get `[W] If True kappa[2] a ~ a` and simplify to `[W] kappa[2] ~ a`, but that will be insoluble because we'll be solving at level 3, and now `kappa[2]` is at level 2. We're too late.\r\n\r\nYet, I claim that this program should be accepted, and it would be if GHC tracked a set of ambient givens and used them in local calls to the solver. With these \"ambient givens\" (instead of putting them only in implication constraints), we would know `cb ~ True` the first time we try to solve, and then we'll succeed.\r\n\r\nAn alternative story is to change how levels are used with variables. Currently, levels are, essentially, the number of type variables available from an outer scope. Accordingly, we must make sure that the level of a variable is never higher than the ambient level. (If it were, we wouldn't know what extra variable(s) were in scope.) Instead, we could just store the list of variables that were in scope. We wouldn't then need to promote in this case -- promotion would happen only during floating. But tracking these lists is a real pain. (If we decide to pursue this further, I can add more details, but it's all in Chapter 6 in [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=compsci_pubs my thesis] -- section 6.5 to be specific.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15588Panic when abusing kind inference2019-07-07T18:04:01ZRichard Eisenbergrae@richarde.devPanic when abusing kind inferenceWhen I say
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: foral...When I say
```hs
{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,
AllowAmbiguousTypes #-}
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import Data.Kind
data SameKind :: forall k. k -> k -> Type
type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
IfK (_ :: Proxy True) f _ = f
IfK (_ :: Proxy False) _ g = g
y :: forall ck (c :: ck). ck :~: Proxy True -> ()
y Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d
x = undefined
in ()
```
HEAD says
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.7.20180827 for x86_64-apple-darwin):
ASSERT failed!
Bad coercion hole co_a3iZ: If
j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]
a_a3gV[sk:3]
nominal
If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]
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/TcMType.hs:316:25 in ghc:TcMType
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
It's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| 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":"Panic when abusing kind inference","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I say\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables, TypeInType, TypeOperators, TypeFamilies,\r\n AllowAmbiguousTypes #-}\r\n\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\nimport Data.Type.Bool\r\nimport Data.Kind\r\n\r\ndata SameKind :: forall k. k -> k -> Type\r\ntype family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where\r\n IfK (_ :: Proxy True) f _ = f\r\n IfK (_ :: Proxy False) _ g = g\r\n\r\ny :: forall ck (c :: ck). ck :~: Proxy True -> ()\r\ny Refl = let x :: forall a b (d :: a). SameKind (IfK c b d) d\r\n x = undefined\r\n in ()\r\n}}}\r\n\r\nHEAD says\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.7.20180827 for x86_64-apple-darwin):\r\n\tASSERT failed!\r\n Bad coercion hole co_a3iZ: If\r\n j_a3j0[tau:2] m_a3j1[tau:2] a_a3gV[sk:3]\r\n a_a3gV[sk:3]\r\n nominal\r\n If j_a3j0[tau:2] m_a3j1[tau:2] a_a3jj[sk:3] ~# a_a3jj[sk:3]\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/TcMType.hs:316:25 in ghc:TcMType\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nIt's as yet unclear whether the program should be accepted. My best guess is that it should, but that (even with this panic fixed) GHC isn't up to the task.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1