GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:17:02Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14441GHC HEAD regression involving type families in kinds2019-07-07T18:17:02ZRyan ScottGHC HEAD regression involving type families in kindsIn GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k)...In GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
data Prox (a :: k) = P
type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
$(return [])
type instance DemoteX P = P
```
(Note that the `$(return [])` line is essential, as it works around #13790.)
However, on GHC HEAD, this now fails:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:27: error:
• Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’
• In the type ‘P’
In the type instance declaration for ‘DemoteX’
|
15 | type instance DemoteX P = P
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression involving type families in kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In GHC 8.2.1, this file typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\ndata Prox (a :: k) = P\r\n\r\ntype instance Demote (Prox (a :: k)) = Prox (DemoteX a)\r\n$(return [])\r\ntype instance DemoteX P = P\r\n}}}\r\n\r\n(Note that the `$(return [])` line is essential, as it works around #13790.)\r\n\r\nHowever, on GHC HEAD, this now fails:\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\n\r\nBug.hs:15:27: error:\r\n • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’\r\n • In the type ‘P’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n15 | type instance DemoteX P = P\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14450GHCi spins forever2019-07-07T18:16:59ZIcelandjackGHCi spins foreverThe following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import ...The following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type Cat ob = ob -> ob -> Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (->)
type Cod (IddSym0 :: Type ~> Type) = (->)
varpa :: (a -> a') -> (a -> a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (->)
```
it sends GHC for a spin.
<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":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type -> Type -> Type\r\n\r\ntype a ~> b = TyFun a b -> Type\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n type Cod (IddSym0 :: Type ~> Type) = (->)\r\n\r\n varpa :: (a -> a') -> (a -> a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14507Core Lint error with Type.Reflection and pattern synonyms2019-07-07T18:16:45ZIcelandjackCore Lint error with Type.Reflection and pattern synonyms```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
impor...```hs
{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}
import Type.Reflection
import Prelude
import Data.Kind
data Dict c where
Dict :: c => Dict c
data N = O | S N
foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)
foo krep rep = do
HRefl <- eqTypeRep krep (typeRepKind rep)
pure (HRefl, rep)
pattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)
pattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))
where Bloop' HRefl rep = rep
type family
SING = (res :: k -> Type) | res -> k where
-- Core Lint error disappears with this line:
SING = (TypeRep :: N -> Type)
pattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)
pattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))
where RepN tr = tr
asTypeable :: TypeRep a -> Dict (Typeable a)
asTypeable rep =
withTypeable rep
Dict
pattern TypeRep :: () => Typeable a => TypeRep a
pattern TypeRep <- (asTypeable -> Dict)
where TypeRep = typeRep
-- error
pattern SO = RepN TypeRep
```
triggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.
<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":"Core Lint error with Type.Reflection and pattern synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PatternSynonyms"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies #-}\r\n\r\nimport Type.Reflection\r\nimport Prelude\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata N = O | S N\r\n\r\nfoo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a)\r\nfoo krep rep = do\r\n HRefl <- eqTypeRep krep (typeRepKind rep)\r\n pure (HRefl, rep)\r\n\r\npattern Bloop' :: forall k' (a::k). Typeable k' => k':~~:k -> TypeRep (a::k) -> TypeRep (a::k)\r\npattern Bloop' hrefl rep <- (foo (typeRep @k') -> Just (hrefl, rep))\r\n where Bloop' HRefl rep = rep\r\n\r\ntype family \r\n SING = (res :: k -> Type) | res -> k where\r\n -- Core Lint error disappears with this line:\r\n SING = (TypeRep :: N -> Type)\r\n\r\npattern RepN :: forall (a::kk). Typeable a => N~kk => SING a -> TypeRep (a::kk)\r\npattern RepN tr <- Bloop' (HRefl::N:~~:kk) (tr :: TypeRep (a::N))\r\n where RepN tr = tr\r\n\r\nasTypeable :: TypeRep a -> Dict (Typeable a)\r\nasTypeable rep =\r\n withTypeable rep\r\n Dict\r\n\r\npattern TypeRep :: () => Typeable a => TypeRep a\r\npattern TypeRep <- (asTypeable -> Dict)\r\n where TypeRep = typeRep\r\n\r\n-- error \r\npattern SO = RepN TypeRep\r\n}}}\r\n\r\ntriggers “Core Lint errors” on 8.2.1, 8.3.20170920 when run with `ghci -ignore-dot-ghci -dcore-lint`.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14515"Same" higher-rank kind synonyms behave differently2019-07-07T18:16:43ZIcelandjack"Same" higher-rank kind synonyms behave differentlyAs you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL ...As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind
```hs
-- Different from
-- HREFL :: forall k1 k2. k1 -> k2 -> Type
--
data HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where
HREFL :: HREFL a a
```
Let us capture `forall k2. k2 -> ..` with a kind synonym
```hs
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: forall k. k -> HRank2 Type where
HREFL :: HREFL a a
```
Works fine. Phew. Let's do the same for `forall k1. k1 -> ..`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty
data HREFL :: HRank1 (HRank2 Type) where
HREFL :: HREFL a a
```
Works fine. Phew.
“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!
```hs
data HREFL :: HRank1 (HRank1 Type) -- FAILS
data HREFL :: HRank1 (HRank2 Type) -- OK
data HREFL :: HRank2 (HRank1 Type) -- OK
data HREFL :: HRank2 (HRank2 Type) -- FAILS
```
```
$ ghci -ignore-dot-ghci /tmp/Weird.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )
/tmp/Weird.hs:8:1: error:
• These kind and type variables: (b :: k2) k2 (d :: k2)
are out of dependency order. Perhaps try this ordering:
k2 (b :: k2) (d :: k2)
• In the data type declaration for ‘HREFL’
|
8 | data HREFL :: HRank2 (HRank2 Type)
| ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude>
```
Same happens defining `HRank2` in terms of `HRank1`
```hs
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = HRank1 ty
```
<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":"\"Same\" higher-rank kind synonyms behave differently","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As you know type-level `forall`s don't float, so we may want to write `HRefl`'s kind\r\n\r\n{{{#!hs\r\n-- Different from\r\n-- HREFL :: forall k1 k2. k1 -> k2 -> Type\r\n-- \r\ndata HREFL :: forall k1. k1 -> (forall k2. k2 -> Type) where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nLet us capture `forall k2. k2 -> ..` with a kind synonym\r\n\r\n{{{#!hs\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: forall k. k -> HRank2 Type where\r\n HREFL :: HREFL a a\r\n}}}\r\n\r\nWorks fine. Phew. Let's do the same for `forall k1. k1 -> ..`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = forall k2. k2 -> ty\r\n\r\ndata HREFL :: HRank1 (HRank2 Type) where\r\n HREFL :: HREFL a a \r\n}}}\r\n\r\nWorks fine. Phew. \r\n\r\n“Didn't you just define the same kind synonym twice?” The funny thing is that this fails to compile when they coincide!\r\n\r\n{{{#!hs\r\ndata HREFL :: HRank1 (HRank1 Type) -- FAILS\r\ndata HREFL :: HRank1 (HRank2 Type) -- OK\r\ndata HREFL :: HRank2 (HRank1 Type) -- OK \r\ndata HREFL :: HRank2 (HRank2 Type) -- FAILS\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/Weird.hs\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/Weird.hs, interpreted )\r\n\r\n/tmp/Weird.hs:8:1: error:\r\n • These kind and type variables: (b :: k2) k2 (d :: k2)\r\n are out of dependency order. Perhaps try this ordering:\r\n k2 (b :: k2) (d :: k2)\r\n • In the data type declaration for ‘HREFL’\r\n |\r\n8 | data HREFL :: HRank2 (HRank2 Type) \r\n | ^^^^^^^^^^\r\nFailed, 0 modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nSame happens defining `HRank2` in terms of `HRank1`\r\n\r\n{{{#!hs\r\ntype HRank1 ty = forall k1. k1 -> ty\r\ntype HRank2 ty = HRank1 ty\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->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/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/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":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14556Core Lint error: Ill-kinded result in coercion2019-07-07T18:16:31ZIcelandjackCore Lint error: Ill-kinded result in coercion```hs
{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type ...```hs
{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
data Fn a b where
IdSym :: Fn Type Type
type family
(@@) (f::Fn k k') (a::k)::k' where
IdSym @@ a = a
data KIND = X | FNARR KIND KIND
data TY :: KIND -> Type where
ID :: TY (FNARR X X)
FNAPP :: TY (FNARR k k') -> TY k -> TY k'
data TyRep (kind::KIND) :: TY kind -> Type where
TID :: TyRep (FNARR X X) ID
TFnApp :: TyRep (FNARR k k') f
-> TyRep k a
-> TyRep k' (FNAPP f a)
type family
IK (kind::KIND) :: Type where
IK X = Type
IK (FNARR k k') = Fn (IK k) (IK k')
type family
IT (ty::TY kind) :: IK kind where
IT ID = IdSym
IT (FNAPP f x) = IT f @@ IT x
zero :: TyRep X a -> IT a
zero = undefined
```
which gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-lint` (8.3.20171122) attached.
It compiles fine with
```hs
zero :: TyRep X a -> IT a
zero = zero
```
but fails with `zero = let x = x in x`. See #14554.
<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":"Core Lint error: Ill-kinded result in coercion","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":"{{{#!hs\r\n{-# Language UndecidableInstances, DataKinds, TypeOperators, KindSignatures, PolyKinds, TypeInType, TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata Fn a b where\r\n IdSym :: Fn Type Type\r\n\r\ntype family\r\n (@@) (f::Fn k k') (a::k)::k' where\r\n IdSym @@ a = a\r\n\r\ndata KIND = X | FNARR KIND KIND\r\n\r\ndata TY :: KIND -> Type where\r\n ID :: TY (FNARR X X)\r\n FNAPP :: TY (FNARR k k') -> TY k -> TY k'\r\n\r\ndata TyRep (kind::KIND) :: TY kind -> Type where\r\n TID :: TyRep (FNARR X X) ID\r\n TFnApp :: TyRep (FNARR k k') f\r\n -> TyRep k a\r\n -> TyRep k' (FNAPP f a)\r\n\r\ntype family\r\n IK (kind::KIND) :: Type where\r\n IK X = Type\r\n IK (FNARR k k') = Fn (IK k) (IK k')\r\n\r\ntype family\r\n IT (ty::TY kind) :: IK kind where\r\n IT ID = IdSym\r\n IT (FNAPP f x) = IT f @@ IT x\r\n\r\nzero :: TyRep X a -> IT a\r\nzero = undefined \r\n}}}\r\n\r\nwhich gives Core lint error when run with `ghci -ignore-dot-ghci -dcore-lint` (8.3.20171122) attached. \r\n\r\nIt compiles fine with\r\n\r\n{{{#!hs\r\nzero :: TyRep X a -> IT a\r\nzero = zero\r\n}}}\r\n\r\nbut fails with `zero = let x = x in x`. See #14554.","type_of_failure":"OtherFailure","blocking":[]} -->https://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/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/14605Core Lint error2019-07-07T18:16:19ZIcelandjackCore Lint errorThis piece of code fails when run with `ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs`, maybe same as my previous #14584.
```hs
{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language ...This piece of code fails when run with `ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs`, maybe same as my previous #14584.
```hs
{-# Language DerivingStrategies #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language ScopedTypeVariables #-}
{-# Language TypeApplications #-}
{-# Language TypeFamilies #-}
{-# Language TypeInType #-}
{-# Language TypeOperators #-}
{-# Language UndecidableInstances #-}
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Product
type a <-> b = a -> b -> Type
class Iso (iso :: a <-> b) where
iso :: a -> b
osi :: b -> a
data Iso_Bool :: Either () () <-> Bool
instance Iso Iso_Bool where
class Representable f where
type Rep f :: Type
index :: f a -> (Rep f -> a)
tabulate :: (Rep f -> a) -> f a
class Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
newtype Co f a = Co (f a) deriving newtype (Functor, Representable)
instance (Representable f, Monoid (Rep f)) => Comonad (Co f) where
extract = (`index` mempty)
newtype WRAP (iso::old <-> new) f a = WRAP (f a)
instance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <-> new) f) where
type Rep (WRAP (iso :: old <-> new) f) = new
index :: WRAP iso f a -> (new -> a)
index (WRAP fa) = index fa . osi @old @new @iso
tabulate :: (new -> a) -> WRAP iso f a
tabulate gen = WRAP $
tabulate (gen . iso @old @new @iso)
newtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)
deriving newtype
Comonad
```
I unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.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":"Core Lint error","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["DeferredTypeErrors","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This piece of code fails when run with `ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs`, maybe same as my previous #14584.\r\n\r\n{{{#!hs\r\n{-# Language DerivingStrategies #-}\r\n{-# Language GeneralizedNewtypeDeriving #-}\r\n{-# Language InstanceSigs #-}\r\n{-# Language KindSignatures #-}\r\n{-# Language PolyKinds #-}\r\n{-# Language ScopedTypeVariables #-}\r\n{-# Language TypeApplications #-}\r\n{-# Language TypeFamilies #-}\r\n{-# Language TypeInType #-}\r\n{-# Language TypeOperators #-}\r\n{-# Language UndecidableInstances #-}\r\n\r\nimport Data.Kind\r\nimport Data.Functor.Identity\r\nimport Data.Functor.Product\r\n\r\ntype a <-> b = a -> b -> Type\r\n\r\nclass Iso (iso :: a <-> b) where\r\n iso :: a -> b\r\n osi :: b -> a\r\n\r\ndata Iso_Bool :: Either () () <-> Bool\r\n\r\ninstance Iso Iso_Bool where\r\n\r\nclass Representable f where\r\n type Rep f :: Type\r\n\r\n index :: f a -> (Rep f -> a)\r\n tabulate :: (Rep f -> a) -> f a\r\n\r\nclass Comonad w where\r\n extract :: w a -> a\r\n duplicate :: w a -> w (w a)\r\n\r\nnewtype Co f a = Co (f a) deriving newtype (Functor, Representable)\r\n\r\ninstance (Representable f, Monoid (Rep f)) => Comonad (Co f) where\r\n extract = (`index` mempty)\r\n\r\nnewtype WRAP (iso::old <-> new) f a = WRAP (f a)\r\n\r\ninstance (Representable f, Rep f ~ old, Iso iso) => Representable (WRAP (iso :: old <-> new) f) where\r\n type Rep (WRAP (iso :: old <-> new) f) = new\r\n\r\n index :: WRAP iso f a -> (new -> a)\r\n index (WRAP fa) = index fa . osi @old @new @iso\r\n\r\n tabulate :: (new -> a) -> WRAP iso f a\r\n tabulate gen = WRAP $ \r\n tabulate (gen . iso @old @new @iso)\r\n\r\nnewtype PAIR a = PAIR (Co (WRAP Iso_Bool (Product Identity Identity)) a)\r\n deriving newtype\r\n Comonad \r\n}}}\r\n\r\nI unfortunately don't have time to find a more minimal example. Core linter vomits a lot of errors on 8.2.1 & 8.3.20171208. ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14607Core Lint error2019-07-07T18:16:18ZIcelandjackCore Lint errorThis produces a long Core lint error:
```hs
{-# Language DerivingStrategies #-}
{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #...This produces a long Core lint error:
```hs
{-# Language DerivingStrategies #-}
{-# Language GADTs #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs #-}
{-# Language KindSignatures #-}
{-# Language TypeFamilies #-}
{-# Language TypeInType #-}
{-# Language TypeOperators #-}
import Data.Kind
data DEFUNC :: Type -> Type -> Type where
(:~>) :: a -> b -> DEFUNC a b
type a ~> b = DEFUNC a b -> Type
data LamCons a :: Type ~> Type where
LamCons :: a -> LamCons a ([a] :~> [a])
class Mk (app :: Type ~> Type) where
type Arg app :: Type
mk :: Arg app -> app (a :~> b)
instance Mk (LamCons a :: Type ~> Type) where
type Arg (LamCons a) = a
mk :: a -> LamCons (a :~> b)
mk = LamCons
```
with `ghci -ignore-dot-ghci -fdefer-type-errors -dcore-lint bug.hs` on GHC 8.2.1 and 8.3.20171208.https://gitlab.haskell.org/ghc/ghc/-/issues/14720GHC 8.4.1-alpha regression with TypeInType2019-07-07T18:15:53ZRyan ScottGHC 8.4.1-alpha regression with TypeInTypeGHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Ty...GHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
class Generic (a :: Type) where
type Rep a :: Type
from :: a -> Rep a
to :: Rep a -> a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
data Decision a = Proved a
| Disproved (a -> Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
=> Sing a -> Sing b -> Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) ->
case (sTof s1, sTof s2) of
(Refl, Refl) -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
```
But GHC 8.4.1-alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:37-40
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a non-injective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl -> contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a -> Sing b -> Decision (a :~: b)
(bound at Bug.hs:40:3)
|
44 | Disproved contra -> Disproved (\Refl -> contra Refl)
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1-alpha1 |
| 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 8.4.1-alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a -> Rep a\r\n to :: Rep a -> a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)\r\n\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\r\n sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a\r\n\r\ndata Decision a = Proved a\r\n | Disproved (a -> Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))\r\n => Sing a -> Sing b -> Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) ->\r\n case (sTof s1, sTof s2) of\r\n (Refl, Refl) -> Proved Refl\r\n Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1-alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:37-40\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a non-injective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl -> contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a -> Sing b -> Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n |\r\n44 | Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14749T13822 fails2019-07-07T18:15:46ZSimon Peyton JonesT13822 failsConsider this cut-down T13822
```
{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
module T13822 where
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TMaybe :: Ty (STAR :> ...Consider this cut-down T13822
```
{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, TypeInType #-}
module T13822 where
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family IK (k :: KIND) = (res :: Type) where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family I (t :: Ty k) = (res :: IK k) where
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
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 x = case x of
TyApp TyMaybe _ -> Nothing
```
With a stage-1 compiler with DEBUG enabled, this program yields a Lint error in all recent versions of GHC. (NB: Lint, not an assertion failure.)
With stage-2 it succeeds, and passes Lint. Reason: without DEBUG the output of the typechecker is not Linted until after a run of the `CoreOpt`; and that simplifies the coercions; which somehow eliminates the Lint error.
I added`-ddump-ds-preopt` to made the pre-core-opt dump optional -- it is sometimes useful in a non-DEBUG compiler. But that makes Lint run on the pre-core-opt code, and that shows up the bug always.
But an apparently unrelated patch makes it fail Lint even in stage 2. So it's kind of harmless; but a clear bug that we should fix.
I'll mark T13822 as expect-broken; you can re-enable it when this ticket is fixed.
The Lint error is pretty obscure
```
*** Core Lint errors : in result of Desugar (before optimization) ***
<no location info>: warning:
[in body of letrec with binders co_a10u :: (f_a10g :: Ty
(a_a10f ':> 'STAR))
~# (('TMaybe |> (Ty
(Sym co_a10r
':> <'STAR>_N)_N)_N) :: Ty
(a_a10f
':> 'STAR))]
Kind application error in
coercion ‘(Maybe
(Sym (Coh <I (x_a10h |> Sym (Ty (Sym co_a10r))_N)>_N
(D:R:IK[0]) ; Coh <(I (x_a10h |> Sym (Ty
(Sym co_a10r))_N) |> D:R:IK[0])>_N
(Sym (D:R:IK[0]))) ; Coh <I (x_a10h |> Sym (Ty
(Sym co_a10r))_N)>_N
(D:R:IK[0])))_N’
Function kind = * -> *
Arg kinds = [(I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR)]
Fun: *
(I (x_a10h |> Sym (Ty (Sym co_a10r))_N), IK 'STAR)
```Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14764Make $! representation-polymorphic2019-07-07T18:15:43ZDavid FeuerMake $! representation-polymorphicCurrently,
```hs
($) :: forall r a (b :: TYPE r). (a -> b) -> a -> b
```
but
```hs
($!) :: (a -> b) -> a -> b
```
It seems fairly obvious that we should generalize `($!)`.
<details><summary>Trac metadata</summary>
| Trac field ...Currently,
```hs
($) :: forall r a (b :: TYPE r). (a -> b) -> a -> b
```
but
```hs
($!) :: (a -> b) -> a -> b
```
It seems fairly obvious that we should generalize `($!)`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.2.2 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Core Libraries |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Make $! representation-polymorphic","status":"New","operating_system":"","component":"Core Libraries","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Currently,\r\n\r\n{{{#!hs\r\n($) :: forall r a (b :: TYPE r). (a -> b) -> a -> b\r\n}}}\r\n\r\nbut\r\n\r\n{{{#!hs\r\n($!) :: (a -> b) -> a -> b\r\n}}}\r\n\r\nIt seems fairly obvious that we should generalize `($!)`.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14845TypeInType, index GADT by constraint witness2019-07-07T18:15:21ZIcelandjackTypeInType, index GADT by constraint witnessJust wondering if it would ever make sense to allow or use constraints like this
```hs
{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
import Data.Kind
data Struct :: (k -> Constraint) -> (k -...Just wondering if it would ever make sense to allow or use constraints like this
```hs
{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
import Data.Kind
data Struct :: (k -> Constraint) -> (k -> Type) where
S :: cls a => Struct cls a
data Foo a where
F :: Foo (S::Struct Eq a)
```
```
$ ghci -ignore-dot-ghci /tmp/test.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )
/tmp/test.hs:9:13: error:
• Illegal constraint in a type: cls0 a0
• In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
In the type ‘Foo (S :: Struct Eq a)’
In the definition of data constructor ‘F’
|
9 | F :: Foo (S::Struct Eq a)
| ^
Failed, no modules loaded.
Prelude>
```
Please close the ticket if it doesn't
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.5 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeInType, index by GADT witnessing constraint","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Just wondering if it would ever make sense to allow or use constraints like this\r\n\r\n{{{#!hs\r\n{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Struct :: (k -> Constraint) -> (k -> Type) where\r\n S :: cls a => Struct cls a\r\n\r\ndata Foo a where\r\n F :: Foo (S::Struct Eq a)\r\n}}}\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci /tmp/test.hs\r\nGHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( /tmp/test.hs, interpreted )\r\n\r\n/tmp/test.hs:9:13: error:\r\n • Illegal constraint in a type: cls0 a0\r\n • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’\r\n In the type ‘Foo (S :: Struct Eq a)’\r\n In the definition of data constructor ‘F’\r\n |\r\n9 | F :: Foo (S::Struct Eq a)\r\n | ^\r\nFailed, no modules loaded.\r\nPrelude> \r\n}}}\r\n\r\nPlease close the ticket if it doesn't","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14846Renamer hangs (because of -XInstanceSigs?)2019-07-07T18:15:20ZIcelandjackRenamer hangs (because of -XInstanceSigs?)```hs
{-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
type Cat ob = ob -> ob...```hs
{-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
type Cat ob = ob -> ob -> Type
data Struct :: (k -> Constraint) -> Type where
S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls -> Type where
AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k -> Constraint)) where
struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where
struct :: AStruct (Structured xx cls)
struct = AStruct
data Hom :: Cat k -> Cat (Struct cls) where
class Category (cat::Cat ob) where
i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
-- Commenting out this instance signature makes the issue go away
i :: forall a. StructI a => Hom ríki a a
i = case struct :: AStruct (Structured a cls) of
```
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
```
$ ghci -ignore-dot-ghci 199.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 199.hs, interpreted )
^CInterrupted.
>
>
```8.4.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14847Inferring dependent kinds for non-recursive types2019-07-07T18:15:20ZSimon Peyton JonesInferring dependent kinds for non-recursive typesConsider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#inferring-dependency-in-...Consider this
```
data Proxy k (a :: k) = MkProxy
data Proxy2 k a = MkP (Proxy k a)
```
which is discussed in [a corner of the user manual](http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#inferring-dependency-in-datatype-declarations).
Surprisingly, we reject `Proxy2` -- but there is nothing difficult about inferring its kind. There would be if it was recursive -- but it isn't.
Simple solution: for non-recursive type declarations (we do SCC analysis so we know which these are) do not call `getInitialKinds`; instead, just infer the kind of the definition! Simple.
Warning: is this recursive?
```
data Proxy2 k a where
MkP :: Proxy k a -> Proxy2 k a
```
Presumably no more than the other definition. But currently we need `Proxy2` in the environment during kind inference, because we kind-check the result type. That seems jolly odd and inconsistent. Needs more thought.
Similar questions for
```
data T a where
T :: Int -> T Bool
type family F a where
F Int = True
F _ = False
```
See also:
- #14451
- #12088
- #9427https://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/14887Explicitly quantifying a kind variable causes a telescope to fail to kind-check2019-07-07T18:15:11ZRyan ScottExplicitly quantifying a kind variable causes a telescope to fail to kind-checkConsider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type...Consider the following program:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -fprint-explicit-kinds #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where
Foo1 (e :: a :~: a) = a :~: a
type family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where
Foo2 k (e :: a :~: a) = a :~: a
```
`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!
```
$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:13:10: error:
• Couldn't match kind ‘k’ with ‘k1’
When matching the kind of ‘a’
Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’
• In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’
In the type family declaration for ‘Foo2’
|
13 | Foo2 k (e :: a :~: a) = a :~: a
| ^^^^^^^^^^^^^^
```
(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.2 |
| 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":"Explicitly quantifying a kind variable causes a type family to fail to typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# OPTIONS_GHC -fprint-explicit-kinds #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\ntype family Foo1 (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo1 (e :: a :~: a) = a :~: a\r\n\r\ntype family Foo2 (k :: Type) (e :: (a :: k) :~: (a :: k)) :: Type where\r\n Foo2 k (e :: a :~: a) = a :~: a\r\n}}}\r\n\r\n`Foo2` is wholly equivalent to `Foo1`, except that in `Foo2`, the `k` kind variable is explicitly quantified. However, `Foo1` typechecks, but `Foo2` does not!\r\n\r\n{{{\r\n$ /opt/ghc/8.2.2/bin/ghci Bug.hs -fprint-explicit-kinds\r\nGHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:13:10: error:\r\n • Couldn't match kind ‘k’ with ‘k1’\r\n When matching the kind of ‘a’\r\n Expected kind ‘(:~:) k a a’, but ‘e’ has kind ‘(:~:) k a a’\r\n • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’\r\n In the type family declaration for ‘Foo2’\r\n |\r\n13 | Foo2 k (e :: a :~: a) = a :~: a\r\n | ^^^^^^^^^^^^^^\r\n}}}\r\n\r\n(Moreover, there seems to be a tidying bug, since GHC claims that `(:~:) k a a` is not the same kind as `(:~:) k a a`.)","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev