GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2022-03-05T13:41:59Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/15561TypeInType: Type error conditioned on ordering of GADT and type family defini...2022-03-05T13:41:59ZBj0rnTypeInType: Type error conditioned on ordering of GADT and type family definitionsConsider this code which successfully compiles:
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Inde...Consider this code which successfully compiles:
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}
module Bug where
class HasIndex a where
type Index a
emptyIndex :: IndexWrapper a
instance HasIndex [a] where
type Index [a] = Int
emptyIndex = Wrap 0
data IndexWrapper a where
Wrap :: Index a -> IndexWrapper a
type family UnwrapAnyWrapperLikeThing (a :: t) :: k
type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
```
The mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:
```
Bug.hs:17:15: error:
• Illegal type synonym family application in instance: Index [b]
• In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’
|
17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
This is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.
The problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.
Ideally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.
I have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.
<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":"TypeInType: Type error conditioned on ordering of GADT and type family definitions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["GADTs","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider this code which successfully compiles:\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs #-}\r\n\r\nmodule Bug where\r\n\r\nclass HasIndex a where\r\n type Index a\r\n emptyIndex :: IndexWrapper a\r\ninstance HasIndex [a] where\r\n type Index [a] = Int\r\n emptyIndex = Wrap 0\r\n\r\ndata IndexWrapper a where\r\n Wrap :: Index a -> IndexWrapper a\r\n\r\ntype family UnwrapAnyWrapperLikeThing (a :: t) :: k\r\n\r\ntype instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n}}}\r\n\r\nThe mere act of moving the definition of `IndexWrapper` anywhere below the definition of `UnwrapAnyWrapperLikeThing` makes the type family instance at the bottom of the example fail compilation, with this error:\r\n{{{\r\nBug.hs:17:15: error:\r\n • Illegal type synonym family application in instance: Index [b]\r\n • In the type instance declaration for ‘UnwrapAnyWrapperLikeThing’\r\n |\r\n17 | type instance UnwrapAnyWrapperLikeThing ('Wrap a :: IndexWrapper [b]) = a\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis is the smallest example that I could come up with; my real scenario of course has more things going on, but I can share if it would help.\r\n\r\nThe problem for me (other than that I'm pretty sure reordering definitions in Haskell should never affect anything) is that I would like just the definition of the type family (`UnwrapAnyWrapperLikeThing` in this example) in module `A` and all of the other definitions in module `B` that imports `A`.\r\n\r\nIdeally, I would have liked to add a `HasIndex a` constraint to the `Wrap` constructor, but that disqualifies use of `'Wrap` on the type level. This does make me feel like I'm on shaky ground to begin with.\r\n\r\nI have reproduced this bug on 8.2.2, 8.4.3 and 8.6.0.20180810 (NixOS). I should note that 8.0.2 rejects even the code that I pasted here.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15545Forced to enable TypeInType because of (i ~ i)2019-07-07T18:04:13ZIcelandjackForced to enable TypeInType because of (i ~ i)I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XPoly...I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XPolyKinds -XGADTs
Prelude> import Data.Kind
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
<interactive>:3:45: error:
• Data constructor ‘NP’ constrains the choice of kind parameter:
i ~ i
Use TypeInType to allow this
• In the definition of data constructor ‘NP’
In the data type declaration for ‘NP’
Prelude Data.Kind>
```
I would rather expect the warning I get after enabling `TypeInType`
```
Prelude Data.Kind> :set -XTypeInType
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
<interactive>:8:28: error:
• Couldn't match ‘k’ with ‘i’
• In the data declaration for ‘NP’
```
----
**ps** making sure this is OK as well; it works after enabling `-XTypeInType` and quantifying with `-XRankNTypes` (is this using polymorphic recursion?)
```
Prelude Data.Kind> :set -XTypeInType -XRankNTypes
Prelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
Prelude Data.Kind> :t NP
NP :: forall i (f :: i -> *) (a :: i). f a -> NP f a
```
it also works for
```hs
data NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a
```
<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":"Forced to enable TypeInType because of (i ~ i)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XPolyKinds -XGADTs\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\n\r\n<interactive>:3:45: error:\r\n • Data constructor ‘NP’ constrains the choice of kind parameter:\r\n i ~ i\r\n Use TypeInType to allow this\r\n • In the definition of data constructor ‘NP’\r\n In the data type declaration for ‘NP’\r\nPrelude Data.Kind> \r\n}}}\r\n\r\nI would rather expect the warning I get after enabling `TypeInType`\r\n\r\n{{{\r\nPrelude Data.Kind> :set -XTypeInType\r\nPrelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\n\r\n<interactive>:8:28: error:\r\n • Couldn't match ‘k’ with ‘i’\r\n • In the data declaration for ‘NP’\r\n}}}\r\n\r\n----\r\n\r\n'''ps''' making sure this is OK as well; it works after enabling `-XTypeInType` and quantifying with `-XRankNTypes` (is this using polymorphic recursion?)\r\n\r\n{{{\r\nPrelude Data.Kind> :set -XTypeInType -XRankNTypes\r\nPrelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\nPrelude Data.Kind> :t NP\r\nNP :: forall i (f :: i -> *) (a :: i). f a -> NP f a\r\n}}}\r\n\r\nit also works for\r\n\r\n{{{#!hs\r\ndata NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\ndata NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\ndata NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15428Oversaturated type family application panicks GHC (piResultTys2)2019-07-07T18:04:56ZRyan ScottOversaturated type family application panicks GHC (piResultTys2)The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
im...The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family Flurmp :: k
type family Pure (x :: a) :: f a
wat :: forall (f :: Type -> Type) (p :: Type).
Proxy (f p) -> ()
wat _ =
let s :: (Flurmp :: f p)
:~: Pure (Flurmp :: p -> p) (Flurmp :: p)
s = undefined
in ()
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64-unknown-linux):
piResultTys2
f_aAT a_aAU
[(->) p_a1uI[sk:1], p_a1uI[sk:1] -> p_a1uI[sk:1], Flurmp, Flurmp]
[Flurmp]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type
```
On GHC 8.4 and earlier, this simply gives an error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:16: error:
• Expecting one more argument to ‘Pure (Flurmp :: p -> p)’
Expected kind ‘p -> f p’,
but ‘Pure (Flurmp :: p -> p)’ has kind ‘p -> p -> p’
• In the second argument of ‘(:~:)’, namely
‘Pure (Flurmp :: p -> p) (Flurmp :: p)’
In the type signature:
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
In the expression:
let
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
s = undefined
in ()
• Relevant bindings include
wat :: Proxy (f p) -> () (bound at Bug.hs:16:1)
|
18 | :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| 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 8.6+ panics (piResultTys2), older GHCs don't","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics when compiled with GHC 8.6.1 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\n\r\ntype family Flurmp :: k\r\ntype family Pure (x :: a) :: f a\r\n\r\nwat :: forall (f :: Type -> Type) (p :: Type).\r\n Proxy (f p) -> ()\r\nwat _ =\r\n let s :: (Flurmp :: f p)\r\n :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n s = undefined\r\n in ()\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: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64-unknown-linux):\r\n piResultTys2\r\n f_aAT a_aAU\r\n [(->) p_a1uI[sk:1], p_a1uI[sk:1] -> p_a1uI[sk:1], Flurmp, Flurmp]\r\n [Flurmp]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type\r\n}}}\r\n\r\nOn GHC 8.4 and earlier, this simply gives an error message:\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:18:16: error:\r\n • Expecting one more argument to ‘Pure (Flurmp :: p -> p)’\r\n Expected kind ‘p -> f p’,\r\n but ‘Pure (Flurmp :: p -> p)’ has kind ‘p -> p -> p’\r\n • In the second argument of ‘(:~:)’, namely\r\n ‘Pure (Flurmp :: p -> p) (Flurmp :: p)’\r\n In the type signature:\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n In the expression:\r\n let\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n • Relevant bindings include\r\n wat :: Proxy (f p) -> () (bound at Bug.hs:16:1)\r\n |\r\n18 | :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15419GHC 8.6.1 regression (buildKindCoercion)2019-07-07T18:04:59ZRyan ScottGHC 8.6.1 regression (buildKindCoercion)The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes ...The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
data family Sing :: forall k. k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data instance Sing :: forall a b. (a, b) -> Type where
STuple2 :: Sing x -> Sing y -> Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }
-----
newtype Par1 p = Par1 p
newtype K1 c p = K1 c
data (f :*: g) p = f p :*: g p
data instance Sing :: forall p. Par1 p -> Type where
SPar1 :: Sing x -> Sing ('Par1 x)
data instance Sing :: forall k c (p :: k). K1 c p -> Type where
SK1 :: Sing x -> Sing ('K1 x)
data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
(f :*: g) p -> Type where
(:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)
class Generic1 (f :: k -> Type) where
type Rep1 f :: k -> Type
from1 :: f a -> Rep1 f a
to1 :: Rep1 f a -> f a
class PGeneric1 (f :: k -> Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k -> Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
instance Generic1 ((,) a) where
type Rep1 ((,) a) = K1 a :*: Par1
from1 (x, y) = K1 x :*: Par1 y
to1 (K1 x :*: Par1 y) = (x, y)
instance PGeneric1 ((,) a) where
type From1 '(x, y) = 'K1 x ':*: 'Par1 y
type To1 ('K1 x ':*: 'Par1 y) = '(x, y)
instance SGeneric1 ((,) a) where
sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y
sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y
-----
type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
GenericFmap g x = To1 (Fmap g (From1 x))
class PFunctor (f :: Type -> Type) where
type Fmap (g :: a ~> b) (x :: f a) :: f b
type Fmap g x = GenericFmap g x
class SFunctor (f :: Type -> Type) where
sFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g -> Sing x -> Sing (Fmap g x)
default sFmap :: forall a b (g :: a ~> b) (x :: f a).
( SGeneric1 f, SFunctor (Rep1 f)
, Fmap g x ~ GenericFmap g x )
=> Sing g -> Sing x -> Sing (Fmap g x)
sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))
-----
instance PFunctor Par1 where
type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
instance PFunctor (K1 c) where
type Fmap _ ('K1 x) = 'K1 x
instance PFunctor (f :*: g) where
type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y
instance SFunctor Par1 where
sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
instance SFunctor (K1 c) where
sFmap _ (SK1 sx) = SK1 sx
instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy
-----
instance PFunctor ((,) a)
-- The line below causes the panic
instance SFunctor ((,) a)
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64-unknown-linux):
buildKindCoercion
K1 a_a1Nj :*: Par1
Rep1 ((,) a_a1Nj)
*
a_a1Nj
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion
```
<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 8.6.1 regression (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k -> Type\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 instance Sing :: forall a b. (a, b) -> Type where\r\n STuple2 :: Sing x -> Sing y -> Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }\r\n\r\n-----\r\n\r\nnewtype Par1 p = Par1 p\r\nnewtype K1 c p = K1 c\r\ndata (f :*: g) p = f p :*: g p\r\n\r\ndata instance Sing :: forall p. Par1 p -> Type where\r\n SPar1 :: Sing x -> Sing ('Par1 x)\r\ndata instance Sing :: forall k c (p :: k). K1 c p -> Type where\r\n SK1 :: Sing x -> Sing ('K1 x)\r\ndata instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).\r\n (f :*: g) p -> Type where\r\n (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)\r\n\r\nclass Generic1 (f :: k -> Type) where\r\n type Rep1 f :: k -> Type\r\n from1 :: f a -> Rep1 f a\r\n to1 :: Rep1 f a -> f a\r\n\r\nclass PGeneric1 (f :: k -> Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k -> Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)\r\n\r\ninstance Generic1 ((,) a) where\r\n type Rep1 ((,) a) = K1 a :*: Par1\r\n from1 (x, y) = K1 x :*: Par1 y\r\n to1 (K1 x :*: Par1 y) = (x, y)\r\n\r\ninstance PGeneric1 ((,) a) where\r\n type From1 '(x, y) = 'K1 x ':*: 'Par1 y\r\n type To1 ('K1 x ':*: 'Par1 y) = '(x, y)\r\n\r\ninstance SGeneric1 ((,) a) where\r\n sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y\r\n sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y\r\n\r\n-----\r\n\r\ntype family GenericFmap (g :: a ~> b) (x :: f a) :: f b where\r\n GenericFmap g x = To1 (Fmap g (From1 x))\r\n\r\nclass PFunctor (f :: Type -> Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\n type Fmap g x = GenericFmap g x\r\n\r\nclass SFunctor (f :: Type -> Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g -> Sing x -> Sing (Fmap g x)\r\n default sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n ( SGeneric1 f, SFunctor (Rep1 f)\r\n , Fmap g x ~ GenericFmap g x )\r\n => Sing g -> Sing x -> Sing (Fmap g x)\r\n sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))\r\n\r\n-----\r\n\r\ninstance PFunctor Par1 where\r\n type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)\r\ninstance PFunctor (K1 c) where\r\n type Fmap _ ('K1 x) = 'K1 x\r\ninstance PFunctor (f :*: g) where\r\n type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y\r\n\r\ninstance SFunctor Par1 where\r\n sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)\r\ninstance SFunctor (K1 c) where\r\n sFmap _ (SK1 sx) = SK1 sx\r\ninstance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where\r\n sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy\r\n\r\n-----\r\n\r\ninstance PFunctor ((,) a)\r\n-- The line below causes the panic\r\ninstance SFunctor ((,) a)\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: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64-unknown-linux):\r\n buildKindCoercion\r\n K1 a_a1Nj :*: Par1\r\n Rep1 ((,) a_a1Nj)\r\n *\r\n a_a1Nj\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15380Infinite typechecker loop in GHC 8.62019-07-07T18:12:54ZRyan ScottInfinite typechecker loop in GHC 8.6The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
class Generic a where...The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
class Generic a where
type Rep a :: Type
class PGeneric a where
type To a (x :: Rep a) :: a
type family MDefault (x :: a) :: a where
MDefault x = To (M x)
class C a where
type M (x :: a) :: a
type M (x :: a) = MDefault x
```
In GHC 8.4.3, however this fails with a proper error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:16: error:
• Occurs check: cannot construct the infinite kind:
a ~ Rep (M x) -> M x
• In the type ‘To (M x)’
In the type family declaration for ‘MDefault’
• Type variable kinds: x :: a
|
15 | MDefault x = To (M x)
| ^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| 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":"Infinite typechecker loop in GHC 8.6","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program loops infinitely during typechecking with GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\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\nclass Generic a where\r\n type Rep a :: Type\r\n\r\nclass PGeneric a where\r\n type To a (x :: Rep a) :: a\r\n\r\ntype family MDefault (x :: a) :: a where\r\n MDefault x = To (M x)\r\n\r\nclass C a where\r\n type M (x :: a) :: a\r\n type M (x :: a) = MDefault x\r\n}}}\r\n\r\nIn GHC 8.4.3, however this fails with a proper error:\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:15:16: error:\r\n • Occurs check: cannot construct the infinite kind:\r\n a ~ Rep (M x) -> M x\r\n • In the type ‘To (M x)’\r\n In the type family declaration for ‘MDefault’\r\n • Type variable kinds: x :: a\r\n |\r\n15 | MDefault x = To (M x)\r\n | ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15370Typed hole panic on GHC 8.6 (tcTyVarDetails)2019-07-07T18:12:57ZRyan ScottTyped hole panic on GHC 8.6 (tcTyVarDetails)The following program panics on GHC 8.6 and HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperat...The following program panics on GHC 8.6 and HEAD:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
import Data.Void
data family Sing :: forall k. k -> Type
data (~>) :: Type -> Type -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
mkRefl :: n :~: j
mkRefl = Refl
right :: forall (r :: (x :~: y) ~> z).
Sing r -> ()
right no =
case mkRefl @x @y of
Refl -> applySing no _
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180627 for x86_64-unknown-linux):
tcTyVarDetails
co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
On GHC 8.4, this simply errors:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:23:10: error:
• Couldn't match type ‘n’ with ‘j’
‘n’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:1-17
‘j’ is a rigid type variable bound by
the type signature for:
mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j
at Bug.hs:22:1-17
Expected type: n :~: j
Actual type: n :~: n
• In the expression: Refl
In an equation for ‘mkRefl’: mkRefl = Refl
• Relevant bindings include
mkRefl :: n :~: j (bound at Bug.hs:23:1)
|
23 | mkRefl = Refl
| ^^^^
Bug.hs:29:13: error:
• Couldn't match type ‘Sing (Apply r t0)’ with ‘()’
Expected type: ()
Actual type: Sing (Apply r t0)
• In the expression: applySing no _
In a case alternative: Refl -> applySing no _
In the expression: case mkRefl @x @y of { Refl -> applySing no _ }
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r -> () (bound at Bug.hs:27:1)
|
29 | Refl -> applySing no _
| ^^^^^^^^^^^^^^
Bug.hs:29:26: error:
• Found hole: _ :: Sing t0
Where: ‘t0’ is an ambiguous type variable
‘y’, ‘x’, ‘k’ are rigid type variables bound by
the type signature for:
right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).
Sing r -> ()
at Bug.hs:(25,1)-(26,21)
• In the second argument of ‘applySing’, namely ‘_’
In the expression: applySing no _
In a case alternative: Refl -> applySing no _
• Relevant bindings include
no :: Sing r (bound at Bug.hs:27:7)
right :: Sing r -> () (bound at Bug.hs:27:1)
Valid substitutions include
undefined :: forall (a :: TYPE r).
GHC.Stack.Types.HasCallStack =>
a
(imported from ‘Prelude’ at Bug.hs:7:8-10
(and originally defined in ‘GHC.Err’))
|
29 | Refl -> applySing no _
| ^
```
Note that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| 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":"Typed hole panic on GHC 8.6 (tcTyVarDetails)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType,","TypedHoles"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.6 and HEAD:\r\n\r\n{{{#!hs\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\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\ndata family Sing :: forall k. k -> Type\r\n\r\ndata (~>) :: Type -> Type -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }\r\n\r\nmkRefl :: n :~: j\r\nmkRefl = Refl\r\n\r\nright :: forall (r :: (x :~: y) ~> z).\r\n Sing r -> ()\r\nright no =\r\n case mkRefl @x @y of\r\n Refl -> applySing no _\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: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180627 for x86_64-unknown-linux):\r\n tcTyVarDetails\r\n co_a1BG :: y_a1Bz[sk:1] ~# x_a1By[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}\r\n\r\nOn GHC 8.4, this simply errors:\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:23:10: error:\r\n • Couldn't match type ‘n’ with ‘j’\r\n ‘n’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:1-17\r\n ‘j’ is a rigid type variable bound by\r\n the type signature for:\r\n mkRefl :: forall k1 (n :: k1) (j :: k1). n :~: j\r\n at Bug.hs:22:1-17\r\n Expected type: n :~: j\r\n Actual type: n :~: n\r\n • In the expression: Refl\r\n In an equation for ‘mkRefl’: mkRefl = Refl\r\n • Relevant bindings include\r\n mkRefl :: n :~: j (bound at Bug.hs:23:1)\r\n |\r\n23 | mkRefl = Refl\r\n | ^^^^\r\n\r\nBug.hs:29:13: error:\r\n • Couldn't match type ‘Sing (Apply r t0)’ with ‘()’\r\n Expected type: ()\r\n Actual type: Sing (Apply r t0)\r\n • In the expression: applySing no _\r\n In a case alternative: Refl -> applySing no _\r\n In the expression: case mkRefl @x @y of { Refl -> applySing no _ }\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r -> () (bound at Bug.hs:27:1)\r\n |\r\n29 | Refl -> applySing no _\r\n | ^^^^^^^^^^^^^^\r\n\r\nBug.hs:29:26: error:\r\n • Found hole: _ :: Sing t0\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘y’, ‘x’, ‘k’ are rigid type variables bound by\r\n the type signature for:\r\n right :: forall k1 (x1 :: k1) (y1 :: k1) z (r :: (x1 :~: y1) ~> z).\r\n Sing r -> ()\r\n at Bug.hs:(25,1)-(26,21)\r\n • In the second argument of ‘applySing’, namely ‘_’\r\n In the expression: applySing no _\r\n In a case alternative: Refl -> applySing no _\r\n • Relevant bindings include\r\n no :: Sing r (bound at Bug.hs:27:7)\r\n right :: Sing r -> () (bound at Bug.hs:27:1)\r\n Valid substitutions include\r\n undefined :: forall (a :: TYPE r).\r\n GHC.Stack.Types.HasCallStack =>\r\n a\r\n (imported from ‘Prelude’ at Bug.hs:7:8-10\r\n (and originally defined in ‘GHC.Err’))\r\n |\r\n29 | Refl -> applySing no _\r\n | ^\r\n}}}\r\n\r\nNote that this is distinct from #15142, as this is still reproducible on HEAD, even after commit 030211d21207dabb7a4bf21cc9af6fa5eb066db1.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Matthías Páll GissurarsonMatthías Páll Gissurarsonhttps://gitlab.haskell.org/ghc/ghc/-/issues/15361Error message displays redundant equality constraint2019-07-07T18:13:00ZRyan ScottError message displays redundant equality constraintWhen compiling this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
foo :: forall (a :: Type)...When compiling this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
foo :: forall (a :: Type) (b :: Type) (c :: Type).
a :~~: b -> a :~~: c
foo HRefl = HRefl
```
GHC complains thus:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:13: error:
• Could not deduce: a ~ c
from the context: (* ~ *, b ~ a)
bound by a pattern with constructor:
HRefl :: forall k1 (a :: k1). a :~~: a,
in an equation for ‘foo’
at Bug.hs:12:5-9
‘a’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) -> a :~~: c
at Bug.hs:(10,1)-(11,27)
‘c’ is a rigid type variable bound by
the type signature for:
foo :: forall a b c. (a :~~: b) -> a :~~: c
at Bug.hs:(10,1)-(11,27)
Expected type: a :~~: c
Actual type: a :~~: a
• In the expression: HRefl
In an equation for ‘foo’: foo HRefl = HRefl
• Relevant bindings include
foo :: (a :~~: b) -> a :~~: c (bound at Bug.hs:12:1)
|
12 | foo HRefl = HRefl
| ^^^^^
```
That `* ~ *` constraint is entirely redundant.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Error message displays redundant equality constraint","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiling this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\n\r\nfoo :: forall (a :: Type) (b :: Type) (c :: Type).\r\n a :~~: b -> a :~~: c\r\nfoo HRefl = HRefl\r\n}}}\r\n\r\nGHC complains thus:\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:12:13: error:\r\n • Could not deduce: a ~ c\r\n from the context: (* ~ *, b ~ a)\r\n bound by a pattern with constructor:\r\n HRefl :: forall k1 (a :: k1). a :~~: a,\r\n in an equation for ‘foo’\r\n at Bug.hs:12:5-9\r\n ‘a’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) -> a :~~: c\r\n at Bug.hs:(10,1)-(11,27)\r\n ‘c’ is a rigid type variable bound by\r\n the type signature for:\r\n foo :: forall a b c. (a :~~: b) -> a :~~: c\r\n at Bug.hs:(10,1)-(11,27)\r\n Expected type: a :~~: c\r\n Actual type: a :~~: a\r\n • In the expression: HRefl\r\n In an equation for ‘foo’: foo HRefl = HRefl\r\n • Relevant bindings include\r\n foo :: (a :~~: b) -> a :~~: c (bound at Bug.hs:12:1)\r\n |\r\n12 | foo HRefl = HRefl\r\n | ^^^^^\r\n}}}\r\n\r\nThat `* ~ *` constraint is entirely redundant.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15346Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed...2019-07-07T18:13:04ZRyan ScottCore Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expressionThe following program typechecks on GHC 8.6.1-alpha1:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedT...The following program typechecks on GHC 8.6.1-alpha1:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where
import Data.Kind
import Data.Type.Equality
import Data.Void
-----
-- singletons machinery
-----
data family Sing :: forall k. k -> Type
data instance Sing :: () -> Type where
STuple0 :: Sing '()
type Refuted a = a -> Void
data Decision a = Proved a | Disproved (Refuted a)
-----
-- A stripped down version of GHC.Generics
-----
data U1 = MkU1
data instance Sing (z :: U1) where
SMkU1 :: Sing MkU1
-----
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)
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
-----
instance Generic () where
type Rep () = U1
from () = MkU1
to MkU1 = ()
instance PGeneric () where
type PFrom '() = MkU1
type PTo 'MkU1 = '()
instance SGeneric () where
sFrom STuple0 = SMkU1
sTo SMkU1 = STuple0
sTof STuple0 = Refl
sFot SMkU1 = Refl
-----
class SDecide k where
-- | Compute a proof or disproof of equality, given two singletons.
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (SGeneric 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) ->
let r :: PTo (PFrom a) :~: PTo (PFrom b)
r = Refl
sTof1 :: PTo (PFrom a) :~: a
sTof1 = sTof s1
sTof2 :: PTo (PFrom b) :~: b
sTof2 = sTof s2
in Proved (sym sTof1 `trans` r `trans` sTof2)
Disproved contra -> Disproved (\Refl -> contra Refl)
instance SDecide U1 where
SMkU1 %~ SMkU1 = Proved Refl
instance SDecide ()
```
However, it throws a Core Lint error with `-dcore-lint`. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit:
```
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
In the expression: <elided>
From-type of Cast differs from type of enclosed expression
From-type: U1
Type of enclosed expr: Rep ()
Actual enclosed expr: PFrom a_a1Fm
Coercion used in cast: Sym (D:R:Rep()[0])
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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":"Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.6.1-alpha1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE EmptyCase #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE GADTs #-}\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\r\nimport Data.Type.Equality\r\nimport Data.Void\r\n\r\n-----\r\n-- singletons machinery\r\n-----\r\n\r\ndata family Sing :: forall k. k -> Type\r\n\r\ndata instance Sing :: () -> Type where\r\n STuple0 :: Sing '()\r\n\r\ntype Refuted a = a -> Void\r\ndata Decision a = Proved a | Disproved (Refuted a)\r\n\r\n-----\r\n-- A stripped down version of GHC.Generics\r\n-----\r\n\r\ndata U1 = MkU1\r\ndata instance Sing (z :: U1) where\r\n SMkU1 :: Sing MkU1\r\n\r\n-----\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 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\n-----\r\n\r\ninstance Generic () where\r\n type Rep () = U1\r\n from () = MkU1\r\n to MkU1 = ()\r\n\r\ninstance PGeneric () where\r\n type PFrom '() = MkU1\r\n type PTo 'MkU1 = '()\r\n\r\ninstance SGeneric () where\r\n sFrom STuple0 = SMkU1\r\n sTo SMkU1 = STuple0\r\n sTof STuple0 = Refl\r\n sFot SMkU1 = Refl\r\n\r\n-----\r\n\r\nclass SDecide k where\r\n -- | Compute a proof or disproof of equality, given two singletons.\r\n (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (SGeneric 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 let r :: PTo (PFrom a) :~: PTo (PFrom b)\r\n r = Refl\r\n\r\n sTof1 :: PTo (PFrom a) :~: a\r\n sTof1 = sTof s1\r\n\r\n sTof2 :: PTo (PFrom b) :~: b\r\n sTof2 = sTof s2\r\n in Proved (sym sTof1 `trans` r `trans` sTof2)\r\n Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n\r\ninstance SDecide U1 where\r\n SMkU1 %~ SMkU1 = Proved Refl\r\n\r\ninstance SDecide ()\r\n}}}\r\n\r\nHowever, it throws a Core Lint error with `-dcore-lint`. The full error is absolutely massive, so I'll attach it separately. Here is the top-level bit:\r\n\r\n{{{\r\n*** Core Lint errors : in result of Simplifier ***\r\n<no location info>: warning:\r\n In the expression: <elided>\r\n From-type of Cast differs from type of enclosed expression\r\n From-type: U1\r\n Type of enclosed expr: Rep ()\r\n Actual enclosed expr: PFrom a_a1Fm\r\n Coercion used in cast: Sym (D:R:Rep()[0])\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15343Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)2019-07-07T18:13:05ZRyan ScottImplicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)The following program panics on GHC 8.6 and later:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFam...The following program panics on GHC 8.6 and later:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing :: forall k. k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
instance SingKind (a :~~: b) where
type Demote (a :~~: b) = a :~~: b
fromSing SHRefl = HRefl
toSing HRefl = SomeSing SHRefl
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)
(p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)
(r :: a :~~: b).
Sing r
-> Apply p HRefl
-> Apply p r
(~>:~~:) SHRefl pHRefl = pHRefl
type family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where
Why a (_ :: a :~~: y) = y :~~: a
data WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type
-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type
-- The version above does NOT panic
type instance Apply (WhySym a) e = Why a e
hsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).
a :~~: b -> b :~~: a
hsym eq = case toSing eq of
SomeSing (singEq :: Sing r) ->
(~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180627 for x86_64-unknown-linux):
coercionKind
Nth:3
(Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion
```
As noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.
This is a regression from GHC 8.4.3, in which the program simply errored:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:56:38: error:
• Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,
but ‘WhySym a’ has kind ‘forall (y :: z0).
TyFun (a1 :~~: y) * -> *’
• In the type ‘(WhySym a)’
In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
In a case alternative:
SomeSing (singEq :: Sing r)
-> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
• Relevant bindings include
singEq :: Sing a2 (bound at Bug.hs:55:23)
eq :: a1 :~~: b (bound at Bug.hs:54:6)
hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)
|
56 | (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl
| ^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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":"Implicitly quantifying a kind variable causes GHC 8.6 to panic (coercionKind)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC 8.6 and later:\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\nimport Data.Type.Equality\r\n\r\ndata family Sing :: forall k. k -> Type\r\ndata SomeSing :: Type -> Type where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k :: Type\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\ninstance SingKind (a :~~: b) where\r\n type Demote (a :~~: b) = a :~~: b\r\n fromSing SHRefl = HRefl\r\n toSing HRefl = SomeSing SHRefl\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\n(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k)\r\n (p :: forall (z :: Type) (y :: z). (a :~~: y) ~> Type)\r\n (r :: a :~~: b).\r\n Sing r\r\n -> Apply p HRefl\r\n -> Apply p r\r\n(~>:~~:) SHRefl pHRefl = pHRefl\r\n\r\ntype family Why (a :: j) (e :: a :~~: (y :: z)) :: Type where\r\n Why a (_ :: a :~~: y) = y :~~: a\r\n\r\ndata WhySym (a :: j) :: forall (y :: z). (a :~~: y) ~> Type\r\n-- data WhySym (a :: j) :: forall z (y :: z). (a :~~: y) ~> Type\r\n-- The version above does NOT panic\r\ntype instance Apply (WhySym a) e = Why a e\r\n\r\nhsym :: forall (j :: Type) (k :: Type) (a :: j) (b :: k).\r\n a :~~: b -> b :~~: a\r\nhsym eq = case toSing eq of\r\n SomeSing (singEq :: Sing r) ->\r\n (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n}}}\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: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180627 for x86_64-unknown-linux):\r\n coercionKind\r\n Nth:3\r\n (Inst {co_a1jI} (Coh <k_a1js[sk:1]>_N (Nth:0 (Sym {co_a1jI}))))\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:1887:9 in ghc:Coercion\r\n}}}\r\n\r\nAs noted in the comments, replacing `WhySym` with a version that explicitly quantifies `z` avoids the panic.\r\n\r\nThis is a regression from GHC 8.4.3, in which the program simply errored:\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:56:38: error:\r\n • Expected kind ‘forall z (y :: z). (a1 :~~: y) ~> *’,\r\n but ‘WhySym a’ has kind ‘forall (y :: z0).\r\n TyFun (a1 :~~: y) * -> *’\r\n • In the type ‘(WhySym a)’\r\n In the expression: (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n In a case alternative:\r\n SomeSing (singEq :: Sing r)\r\n -> (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n • Relevant bindings include\r\n singEq :: Sing a2 (bound at Bug.hs:55:23)\r\n eq :: a1 :~~: b (bound at Bug.hs:54:6)\r\n hsym :: (a1 :~~: b) -> b :~~: a1 (bound at Bug.hs:54:1)\r\n |\r\n56 | (~>:~~:) @j @k @a @b @(WhySym a) @r singEq HRefl\r\n | ^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15308Error message prints explicit kinds when it shouldn't2019-07-07T18:13:20ZRyan ScottError message prints explicit kinds when it shouldn'tWhen compiled, this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-print-explicit-kinds #-}
module Bug where
import Data.Kind
data Foo (a :: Type) :: forall ...When compiled, this program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-print-explicit-kinds #-}
module Bug where
import Data.Kind
data Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where
MkFoo :: Foo a f
f :: Foo a f -> String
f = show
```
Gives the following error:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show
|
13 | f = show
| ^^^^
```
This error message is slightly incorrect, however. In "`No instance for (Show (Foo a b f))`", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `-fno-print-explicit-kinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)
This is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:
```
$ /opt/ghc/8.0.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show
```
But it does not in GHC 8.2.1:
```
$ /opt/ghc/8.2.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:13:5: error:
• No instance for (Show (Foo a b f)) arising from a use of ‘show’
• In the expression: show
In an equation for ‘f’: f = show
|
13 | f = show
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Error message prints explicit kinds when it shouldn't","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When compiled, this program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# OPTIONS_GHC -fno-print-explicit-kinds #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (a :: Type) :: forall b. (a -> b -> Type) -> Type where\r\n MkFoo :: Foo a f\r\n\r\nf :: Foo a f -> String\r\nf = show\r\n}}}\r\n\r\nGives the following error:\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:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n |\r\n13 | f = show\r\n | ^^^^\r\n}}}\r\n\r\nThis error message is slightly incorrect, however. In \"`No instance for (Show (Foo a b f))`\", it claims that `Foo` has three visible type parameters, but it only has two. (I've even made sure to enable `-fno-print-explicit-kinds` at the type to ensure that the invisible `b` kind shouldn't get printed, but it was anyway.)\r\n\r\nThis is a regression that was apparently introduced between GHC 8.0 and 8.2, since in GHC 8.0.2, it prints the correct thing:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n}}}\r\n\r\nBut it does not in GHC 8.2.1:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:13:5: error:\r\n • No instance for (Show (Foo a b f)) arising from a use of ‘show’\r\n • In the expression: show\r\n In an equation for ‘f’: f = show\r\n |\r\n13 | f = show\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15282Document how equality-bearing constructors are promoted in Core2019-07-07T18:13:27ZRyan ScottDocument how equality-bearing constructors are promoted in CoreIn [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this work...In [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<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 | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Document how equality-bearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15245Data family promotion is possible2021-11-06T12:06:45ZVladislav ZavialovData family promotion is possibleThe User's Guide states that data families cannot be promoted, even with `-XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) rela...The User's Guide states that data families cannot be promoted, even with `-XTypeInType`:
> We promote data types and newtypes; type synonyms and type/data families are not promoted.
>
> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:
>
> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.
And yet the following code typechecks and runs:
```hs
{-# LANGUAGE TypeFamilies, TypeInType, TypeApplications #-}
import Type.Reflection
data family K
data instance K = MkK
main = print (typeRep @'MkK)
```
Is this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:
```
<int-index> The user guide states that data families aren't promoted even when -XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.
<int-index> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview "Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types."
<int-index> Is this info outdated?
<RyanGlScott> int-index: Is this in GHCi?
<RyanGlScott> It certainly fails in GHC
<RyanGlScott> But I think I understand why the former works
<int-index> RyanGlScott, yes, I'm checking this in GHCi
<RyanGlScott> int-index: So here's my understanding of how this works
<RyanGlScott> GHC kind-checks top-level declarations using a rather primitive SCC analysis
<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble
<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT
<RyanGlScott> As luck would have it, though, you were trying things out in GHCi
<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations
<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense
<RyanGlScott> *that sense
<int-index> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory
<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kind-checking sophisticated enough to handle this
<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.
<int-index> https://gist.github.com/int-index/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved
<int-index> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.
<RyanGlScott> Huh, now that's interesting
<int-index> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon' - and enabling -XTypeInType disables this check.
<RyanGlScott> int-index: Right, that's baffling me
<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)
<RyanGlScott> int-index: File a bug about that, I suppose
<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible
<int-index> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?
<int-index> Is it bad that -XDataKinds promotes data family constructors? Looks like I can just remove the "restrictions" part of the user guide and be done with it
<RyanGlScott> int-index: In theory, that shouldn't be possible
<int-index> OK, then what the check should be? No data families, any other restrictions?
<RyanGlScott> I might qualify that with "no data family instances defined in the same module"
<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)
<int-index> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...
<RyanGlScott> Oh, I thought you were only changing the users' guide :)
<int-index> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | --------------------- |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Documentation |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | RyanGlScott, goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Data family promotion is possible","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["RyanGlScott","goldfire"],"type":"Bug","description":"The User's Guide states that data families cannot be promoted, even with `-XTypeInType`:\r\n\r\n> We promote data types and newtypes; type synonyms and type/data families are not promoted.\r\n>\r\n> The flag TypeInType (which implies DataKinds) relaxes some of these restrictions, allowing:\r\n>\r\n> Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\r\n\r\nAnd yet the following code typechecks and runs:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeInType, TypeApplications #-}\r\n\r\nimport Type.Reflection\r\n\r\ndata family K\r\ndata instance K = MkK\r\n\r\nmain = print (typeRep @'MkK)\r\n}}}\r\n\r\nIs this a GHC bug or a documentation bug? I asked in IRC but I'm still confused:\r\n\r\n{{{\r\n<int-index> The user guide states that data families aren't promoted even when -XTypeInType is enabled. Where's the logic that ensures this? I checked with `data family K; data instance K = MkK` and I can use `'MkK` with no errors/warnings.\r\n<int-index> https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overview \"Promotion of type synonyms and type families, but not data families. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types.\"\r\n<int-index> Is this info outdated?\r\n<RyanGlScott> int-index: Is this in GHCi?\r\n<RyanGlScott> It certainly fails in GHC\r\n<RyanGlScott> But I think I understand why the former works\r\n<int-index> RyanGlScott, yes, I'm checking this in GHCi\r\n<RyanGlScott> int-index: So here's my understanding of how this works\r\n<RyanGlScott> GHC kind-checks top-level declarations using a rather primitive SCC analysis\r\n<RyanGlScott> In particular, it's primitive in the sense that data family instances give it a lot of trouble\r\n<RyanGlScott> If you tried taking your code and putting it into a standalone .hs file and compiling that, then it would definitely complain about a promoted use of MkT\r\n<RyanGlScott> As luck would have it, though, you were trying things out in GHCi\r\n<RyanGlScott> Which essentially checks each line of input as its own strongly connected group of declarations\r\n<RyanGlScott> So you can define MkT on one line and promote it in subsequent lines, since they're separate in the sense\r\n<RyanGlScott> *that sense\r\n<int-index> this sounds related to Trac #12088, and then I could work around it in GHC by using `$(return [])`, so data families are actually promoted anyway and this has nothing to do with GHC needing more powerful type theory\r\n<RyanGlScott> Well, it does need more powerful type theory in the sense that that's a prerequisite for making the SCC analysis for kind-checking sophisticated enough to handle this\r\n<RyanGlScott> But yes, it's quite simple to work around by using Template Haskell to explicitly split up groups.\r\n<int-index> https://gist.github.com/int-index/c6cc1e20c4b9b5c99af40ee4e23ecb61 this works and no template haskell involved\r\n<int-index> The reason I'm asking is that I'm touching this part of the User's Guide and I don't know what to write there.\r\n<RyanGlScott> Huh, now that's interesting\r\n<int-index> RyanGlScott, the only check I could find that controls what's promoted and what's not is 'isLegacyPromotableDataCon' - and enabling -XTypeInType disables this check.\r\n<RyanGlScott> int-index: Right, that's baffling me\r\n<RyanGlScott> Since that's supposed to be checked every time you promote a data constructor (I think)\r\n<RyanGlScott> int-index: File a bug about that, I suppose\r\n<RyanGlScott> Richard (who's sitting next to me right now) seems to think that that shouldn't be possible\r\n<int-index> RyanGlScott, the thing is, I happily removed this check completely in D4748. Does this mean I have to restore a weaker version of it that only checks for data families? Why?\r\n<int-index> Is it bad that -XDataKinds promotes data family constructors? Looks like I can just remove the \"restrictions\" part of the user guide and be done with it\r\n<RyanGlScott> int-index: In theory, that shouldn't be possible\r\n<int-index> OK, then what the check should be? No data families, any other restrictions?\r\n<RyanGlScott> I might qualify that with \"no data family instances defined in the same module\"\r\n<RyanGlScott> (Or to be precise, in the same SCC, but that's probably too technical for the users' guide)\r\n<int-index> Well, this sounds hard to check. I was thinking along the lines of keeping the 'not (isFamInstTyCon (dataConTyCon dc))' part of the check...\r\n<RyanGlScott> Oh, I thought you were only changing the users' guide :)\r\n<int-index> Well, at this point I'm confused if I should change only the user guide or the check as well. If data families shouldn't be promoted ever, then I'll change GHC. If the limitation is about the current SCC group, I can just mention Trac #12088 as a known infelicity in the User's Guide\r\n}}}\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15195Merge -XPolyKinds with -XTypeInType2019-07-07T18:13:50ZRichard Eisenbergrae@richarde.devMerge -XPolyKinds with -XTypeInTypeAs described in [this accepted proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ------------...As described in [this accepted proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst).
<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":"Merge -XPolyKinds with -XTypeInType","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As described in [https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst this accepted proposal].","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc/-/issues/15170GHC HEAD panic (dischargeFmv)2019-07-07T18:13:56ZRyan ScottGHC HEAD panic (dischargeFmv)The following program panics on GHC HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariable...The following program panics on GHC HEAD:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Proxy
data family Sing (a :: k)
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k = (r :: Type) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
withSomeSing :: forall k r
. SingKind k
=> Demote k
-> (forall (a :: k). Sing a -> r)
-> r
withSomeSing x f =
case toSing x of
SomeSing x' -> f x'
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing sFun x = withSomeSing x (fromSing . applySing sFun)
toSing = undefined
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type f @@ x = Apply f x
infixl 9 @@
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
=> (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))
-> Sing g
-> Sing a
-> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))
dcomp _sf _ _ = undefined
```
```
$ /opt/ghc/head/bin/ghc Bug2.hs
[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.5.20180501 for x86_64-unknown-linux):
dischargeFmv
[D] _ {0}:: (Apply
(f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] |> Sym ((TyFun
<Proxy xx_a1iA[tau:3]>_N
((TyFun
(Proxy
(Sym {co_a1jm})
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N
(Sym {co_a1jB} ; (Apply
(Sym {co_a1jm})
<*>_N
(Coh ((Coh <s_a1jn[fmv:0]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
->_N <*>_N) ; Sym {co_a1jA}) ; (Apply
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
->_N <*>_N)
(Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N
(Sym ((TyFun
<Proxy
xx_a1iA[tau:3]>_N
((TyFun
(Sym {co_a1jm})
<*>_N)_N
->_N <*>_N))_N
->_N <*>_N)))
<'Proxy>_N)_N)
(Sym ((TyFun
(Sym {co_a1jm})
<*>_N)_N
->_N <*>_N)))
(Coh <yy_a1iB[tau:3]>_N
{co_a1jm}))_N))_N
->_N <*>_N))_N
->_N <*>_N))
'Proxy :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm}) ~> s_a1jp[fmv:0]))
~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm})
~> s_a1jp[fmv:0]))
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad
```
On GHC 8.4.2, it simply throws an error:
```
$ /opt/ghc/8.4.2/bin/ghci Bug2.hs
GHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug2.hs, interpreted )
Bug2.hs:53:71: error:
• Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’
• In the first argument of ‘Proxy’, namely ‘y’
In the first argument of ‘(~>)’, namely ‘Proxy y’
In the second argument of ‘(~>)’, namely
‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’
|
53 | (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD panic (dischargeFmv)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics on GHC HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilyDependencies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\ndata family Sing (a :: k)\r\ndata SomeSing :: Type -> Type where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\nclass SingKind k where\r\n type Demote k = (r :: Type) | r -> k\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\nwithSomeSing :: forall k r\r\n . SingKind k\r\n => Demote k\r\n -> (forall (a :: k). Sing a -> r)\r\n -> r\r\nwithSomeSing x f =\r\n case toSing x of\r\n SomeSing x' -> f x'\r\n\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }\r\n\r\ninstance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where\r\n type Demote (k1 ~> k2) = Demote k1 -> Demote k2\r\n fromSing sFun x = withSomeSing x (fromSing . applySing sFun)\r\n toSing = undefined\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype f @@ x = Apply f x\r\ninfixl 9 @@\r\n\r\ndcomp :: forall (a :: Type)\r\n (b :: a ~> Type)\r\n (c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)\r\n (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n (g :: forall (x :: a). Proxy x ~> b @@ x)\r\n (x :: a).\r\n SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\n => (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy)))\r\n -> Sing g\r\n -> Sing a\r\n -> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)))\r\ndcomp _sf _ _ = undefined\r\n}}}\r\n{{{\r\n$ /opt/ghc/head/bin/ghc Bug2.hs\r\n[1 of 1] Compiling Bug ( Bug2.hs, Bug2.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180501 for x86_64-unknown-linux):\r\n dischargeFmv\r\n [D] _ {0}:: (Apply\r\n (f_a1ih[sk:2] xx_a1iA[tau:3] yy_a1iB[tau:3] |> Sym ((TyFun\r\n <Proxy xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Proxy\r\n (Sym {co_a1jm})\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N\r\n (Sym {co_a1jB} ; (Apply\r\n (Sym {co_a1jm})\r\n <*>_N\r\n (Coh ((Coh <s_a1jn[fmv:0]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n ->_N <*>_N) ; Sym {co_a1jA}) ; (Apply\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n ->_N <*>_N)\r\n (Coh <c_a1ig[sk:2] xx_a1iA[tau:3]>_N\r\n (Sym ((TyFun\r\n <Proxy\r\n xx_a1iA[tau:3]>_N\r\n ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n ->_N <*>_N))_N\r\n ->_N <*>_N)))\r\n <'Proxy>_N)_N)\r\n (Sym ((TyFun\r\n (Sym {co_a1jm})\r\n <*>_N)_N\r\n ->_N <*>_N)))\r\n (Coh <yy_a1iB[tau:3]>_N\r\n {co_a1jm}))_N))_N\r\n ->_N <*>_N))_N\r\n ->_N <*>_N))\r\n 'Proxy :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm}) ~> s_a1jp[fmv:0]))\r\n ~# (s_a1jQ[fmv:0] :: (Proxy (yy_a1iB[tau:3] |> {co_a1jm})\r\n ~> s_a1jp[fmv:0]))\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcSMonad.hs:3047:25 in ghc:TcSMonad\r\n}}}\r\n\r\nOn GHC 8.4.2, it simply throws an error:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghci Bug2.hs\r\nGHCi, version 8.4.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug2.hs, interpreted )\r\n\r\nBug2.hs:53:71: error:\r\n • Expected kind ‘Apply b xx’, but ‘y’ has kind ‘b @@ x’\r\n • In the first argument of ‘Proxy’, namely ‘y’\r\n In the first argument of ‘(~>)’, namely ‘Proxy y’\r\n In the second argument of ‘(~>)’, namely\r\n ‘Proxy y ~> c @@ ( 'Proxy :: Proxy x) @@ y’\r\n |\r\n53 | (f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15142GHC HEAD regression: tcTyVarDetails2019-07-07T18:14:05ZRyan ScottGHC HEAD regression: tcTyVarDetailsThis regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
...This regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
```
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
```
$ ~/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.5.20180511 for x86_64-unknown-linux):
tcTyVarDetails
co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
<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 regression: tcTyVarDetails","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This regression prevents the `generic-lens` library from building. Here is a minimized test case:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass ListTuple (tuple :: Type) (as :: [(k, Type)]) where\r\n type ListToTuple as :: Type\r\n}}}\r\n\r\nOn GHC 8.4.2, this compiles, but on GHC HEAD, it panics:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180511 for x86_64-unknown-linux):\r\n tcTyVarDetails\r\n co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15122GHC HEAD typechecker regression2019-07-07T18:14:10ZfmixingGHC HEAD typechecker regressionThis code, distilled from the `type-level-sets` library:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeO...This code, distilled from the `type-level-sets` library:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
data Proxy (p :: k) = Proxy
data Set (n :: [k]) where
Empty :: Set '[]
Ext :: e -> Set s -> Set (e ': s)
type family (m :: [k]) :\ (x :: k) :: [k] where
'[] :\ x = '[]
(x ': xs) :\ x = xs
(y ': xs) :\ x = y ': (xs :\ x)
class Remove s t where
remove :: Set s -> Proxy t -> Set (s :\ t)
instance Remove '[] t where
remove Empty Proxy = Empty
instance {-# OVERLAPS #-} Remove (x ': xs) x where
remove (Ext _ xs) Proxy = xs
instance {-# OVERLAPPABLE #-} (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
=> Remove (y ': xs) x where
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
```
Typechecks in GHC 8.4.2, but not in GHC HEAD:
```
$ /opt/ghc/head/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:31:33: error:
• Could not deduce: ((e : s) :\ x) ~ (e : (s :\ x))
from the context: (((y : xs) :\ x) ~ (y : (xs :\ x)), Remove xs x)
bound by the instance declaration at Bug.hs:(29,31)-(30,27)
or from: (k ~ *, (y : xs :: [k]) ~~ (e : s :: [*]))
bound by a pattern with constructor:
Ext :: forall e (s :: [*]). e -> Set s -> Set (e : s),
in an equation for ‘remove’
at Bug.hs:31:11-18
Expected type: Set ((y : xs) :\ x)
Actual type: Set (e : (s :\ x))
• In the expression: Ext y (remove xs x)
In an equation for ‘remove’:
remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
In the instance declaration for ‘Remove (y : xs) x’
• Relevant bindings include
x :: Proxy x (bound at Bug.hs:31:22)
xs :: Set s (bound at Bug.hs:31:17)
y :: e (bound at Bug.hs:31:15)
remove :: Set (y : xs) -> Proxy x -> Set ((y : xs) :\ x)
(bound at Bug.hs:31:3)
|
31 | remove (Ext y xs) (x@Proxy) = Ext y (remove xs x)
| ^^^^^^^^^^^^^^^^^^^
```
This regression was introduced in commit e3dbb44f53b2f9403d20d84e27f187062755a089 (Fix #12919 by making the flattener homegeneous.).8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15116GHC internal error when GADT return type mentions its own constructor name2019-07-07T18:14:11ZRyan ScottGHC internal error when GADT return type mentions its own constructor nameTake the following program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc...Take the following program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data A (a :: k) where
MkA :: A MkA
```
On GHC 8.4.2, this is rejected with a sensible error message:
```
$ /opt/ghc/8.4.2/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• Data constructor ‘MkA’ cannot be used here
(it is defined and used in the same recursive group)
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’
|
6 | MkA :: A MkA
| ^^^
```
On GHC HEAD, however, this causes a GHC internal error:
```
$ ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:6:12: error:
• GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [asv :-> Type variable ‘k’ = k :: *,
asw :-> Type variable ‘a’ = a :: k,
rqs :-> ATcTyCon A :: forall k. k -> *]
• In the first argument of ‘A’, namely ‘MkA’
In the type ‘A MkA’
In the definition of data constructor ‘MkA’
|
6 | MkA :: A MkA
| ^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC internal error when GADT return type mentions its own constructor name","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Take the following program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata A (a :: k) where\r\n MkA :: A MkA\r\n}}}\r\n\r\nOn GHC 8.4.2, this is rejected with a sensible error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.2/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • Data constructor ‘MkA’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n |\r\n6 | MkA :: A MkA\r\n | ^^^\r\n}}}\r\n\r\nOn GHC HEAD, however, this causes a GHC internal error:\r\n\r\n{{{\r\n$ ghc2/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:6:12: error:\r\n • GHC internal error: ‘MkA’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [asv :-> Type variable ‘k’ = k :: *,\r\n asw :-> Type variable ‘a’ = a :: k,\r\n rqs :-> ATcTyCon A :: forall k. k -> *]\r\n • In the first argument of ‘A’, namely ‘MkA’\r\n In the type ‘A MkA’\r\n In the definition of data constructor ‘MkA’\r\n |\r\n6 | MkA :: A MkA\r\n | ^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15079GHC HEAD regression: cannot instantiate higher-rank kind2020-10-31T11:08:22ZRyan ScottGHC HEAD regression: cannot instantiate higher-rank kindThe following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Void
inf...The following program typechecks on GHC 8.2.2 and 8.4.2:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Void
infixl 4 :==
-- | Heterogeneous Leibnizian equality.
newtype (a :: j) :== (b :: k)
= HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
newtype Coerce a = Coerce { uncoerce :: Starify a }
type family Starify (a :: k) :: Type where
Starify (a :: Type) = a
Starify _ = Void
coerce :: a :== b -> a -> b
coerce f = uncoerce . hsubst f . Coerce
```
But GHC HEAD rejects it:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:21:34: error:
• Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:
Coerce :: forall k. k -> *
Their kinds differ.
Expected type: a -> c0 * a
Actual type: Starify a -> Coerce a
• In the second argument of ‘(.)’, namely ‘Coerce’
In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’
In the expression: uncoerce . hsubst f . Coerce
|
21 | coerce f = uncoerce . hsubst f . Coerce
| ^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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 HEAD regression: cannot instantiate higher-rank kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.2.2 and 8.4.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Void\r\n\r\ninfixl 4 :==\r\n-- | Heterogeneous Leibnizian equality.\r\nnewtype (a :: j) :== (b :: k)\r\n = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }\r\n\r\nnewtype Coerce a = Coerce { uncoerce :: Starify a }\r\ntype family Starify (a :: k) :: Type where\r\n Starify (a :: Type) = a\r\n Starify _ = Void\r\n\r\ncoerce :: a :== b -> a -> b\r\ncoerce f = uncoerce . hsubst f . Coerce\r\n}}}\r\n\r\nBut GHC HEAD rejects it:\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:21:34: error:\r\n • Kind mismatch: cannot unify (c0 :: forall i. i -> *) with:\r\n Coerce :: forall k. k -> *\r\n Their kinds differ.\r\n Expected type: a -> c0 * a\r\n Actual type: Starify a -> Coerce a\r\n • In the second argument of ‘(.)’, namely ‘Coerce’\r\n In the second argument of ‘(.)’, namely ‘hsubst f . Coerce’\r\n In the expression: uncoerce . hsubst f . Coerce\r\n |\r\n21 | coerce f = uncoerce . hsubst f . Coerce\r\n | ^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15039Bizarre pretty-printing of inferred Coercible constraint in partial type sign...2019-07-07T18:14:36ZRyan ScottBizarre pretty-printing of inferred Coercible constraint in partial type signatureConsider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<...Consider the following GHCi session:
```
$ ghci
GHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> import Data.Type.Coercion
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:2:8: error:
• Found type wildcard ‘_’
standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of foo :: Coercible a b => Coercion a b
at <interactive>:2:27-40
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
λ> :set -fprint-explicit-kinds
λ> foo :: _ => Coercion a b; foo = Coercion
<interactive>:4:8: error:
• Found type wildcard ‘_’
standing for ‘(a :: *) ~~ (b :: *) :: TYPE
('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of
foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b
at <interactive>:4:27-40
To use the inferred type, enable PartialTypeSignatures
• In the type signature: foo :: _ => Coercion a b
```
There are two things quite strange about this:
1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.
1. For some reason, enabling `-fprint-explicit-kinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Bizarre pretty-printing of inferred Coercible constraint in partial type signature","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1","keywords":["PartialTypeSignatures"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Consider the following GHCi session:\r\n\r\n{{{\r\n$ ghci\r\nGHCi, version 8.4.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> import Data.Type.Coercion\r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:2:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘Coercible a b :: TYPE ('GHC.Types.TupleRep '[])’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of foo :: Coercible a b => Coercion a b\r\n at <interactive>:2:27-40\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\nλ> :set -fprint-explicit-kinds \r\nλ> foo :: _ => Coercion a b; foo = Coercion\r\n\r\n<interactive>:4:8: error:\r\n • Found type wildcard ‘_’\r\n standing for ‘(a :: *) ~~ (b :: *) :: TYPE\r\n ('GHC.Types.TupleRep ('[] GHC.Types.RuntimeRep))’\r\n Where: ‘a’, ‘b’ are rigid type variables bound by\r\n the inferred type of\r\n foo :: ((a :: *) ~~ (b :: *)) => Coercion * a b\r\n at <interactive>:4:27-40\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature: foo :: _ => Coercion a b\r\n}}}\r\n\r\nThere are two things quite strange about this:\r\n\r\n1. In both error messages, GHC claims that `Coercible a b`/`a ~~ b` has kind `TYPE (TupleRep '[])`. This is wrong, and should be `Coercible`.\r\n2. For some reason, enabling `-fprint-explicit-kinds` causes the inferred constraint to be `(~~)` instead of `Coercible`, which is just plain wrong.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14991GHC HEAD regression involving TYPEs in type families2019-07-07T18:14:46ZRyan ScottGHC HEAD regression involving TYPEs in type familiesThis program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type family Promote...This program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
-----
-- Type
-----
type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a
-----
-- Arrows
-----
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
```
However, it fails to typecheck on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:34:34: error:
• Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’
• In the first argument of ‘(~>)’, namely ‘PromoteX a’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
Bug.hs:34:48: error:
• Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’
• In the second argument of ‘(~>)’, namely ‘PromoteX b’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression involving TYPEs in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program typechecks on GHC 8.2.2 and 8.4.1:\r\n\r\n{{{#!hs\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\n\r\ntype family Promote (k :: Type) :: Type\r\ntype family PromoteX (a :: k) :: Promote k\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\n-----\r\n-- Type\r\n-----\r\n\r\ntype instance Demote Type = Type\r\ntype instance Promote Type = Type\r\n\r\ntype instance DemoteX (a :: Type) = Demote a\r\ntype instance PromoteX (a :: Type) = Promote a\r\n\r\n-----\r\n-- Arrows\r\n-----\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype instance Demote (a ~> b) = DemoteX a -> DemoteX b\r\ntype instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n}}}\r\n\r\nHowever, it fails to typecheck on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:34:34: error:\r\n • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’\r\n • In the first argument of ‘(~>)’, namely ‘PromoteX a’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n |\r\n34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n | ^^^^^^^^^^\r\n\r\nBug.hs:34:48: error:\r\n • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’\r\n • In the second argument of ‘(~>)’, namely ‘PromoteX b’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n |\r\n34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n | ^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev