GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:17:49Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14238`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.12019-07-07T18:17:49ZRyan Scott`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it w...Load this program into GHCi on 8.2.1 or later:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
data Foo (k :: Type) :: k -> Type where
MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)
```
And ask it what the kind of `Foo` is:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, 1 module loaded.
λ> :k Foo
Foo :: k -> *
```
This is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.
A workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:
```
λ> :set -fprint-explicit-foralls
λ> :k Foo
Foo :: forall k -> k -> *
```
This is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Bug.hs, interpreted )
Ok, modules loaded: Main.
λ> :k Foo
Foo :: forall k -> k -> Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"`:kind` suppresses visible dependent quantifiers by default in GHCi 8.2.1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Load this program into GHCi on 8.2.1 or later:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Foo (k :: Type) :: k -> Type where\r\n MkFoo :: Foo (k1 -> k2) f -> Foo k1 a -> Foo k2 (f a)\r\n}}}\r\n\r\nAnd ask it what the kind of `Foo` is:\r\n\r\n{{{\r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, 1 module loaded.\r\nλ> :k Foo\r\nFoo :: k -> *\r\n}}}\r\n\r\nThis is just plain wrong: the actual kind of `Foo` should be `forall k -> k -> *`. Normally, one can omit `forall`s from a kind signature, but this is a special case where we're using a //visible// forall. In other words, `forall k -> k -> *` is not the same as `k -> *`, as the former takes two arguments, whereas the latter takes one.\r\n\r\nA workaround is to force GHCi to come to its senses by explicitly enabling `-fprint-explicit-foralls`:\r\n\r\n{{{\r\nλ> :set -fprint-explicit-foralls \r\nλ> :k Foo\r\nFoo :: forall k -> k -> *\r\n}}}\r\n\r\nThis is actually a regression since GHC 8.0.2, since GHCi did the right thing by default then:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Main ( Bug.hs, interpreted )\r\nOk, modules loaded: Main.\r\nλ> :k Foo\r\nFoo :: forall k -> k -> Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/14203GHC-inferred type signature doesn't actually typecheck2019-07-07T18:17:58ZRyan ScottGHC-inferred type signature doesn't actually typecheckThis code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * ->...This code typechecks:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)
```
I was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:
```
λ> :i SMkSigma
data instance Sing z where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing
x) (px :: Apply p x).
(Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)
```
I attempted to incorporate this newfound knowledge into the program:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data family Sing :: k -> *
data Sigma (a :: *) :: (a ~> *) -> * where
MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).
Sing x -> Apply p x -> Sigma a p
data instance Sing (z :: Sigma a p) where
SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).
Sing sx -> Sing px -> Sing (MkSigma sx px)
```
But to my surprise, adding this inferred type signature causes the program to no longer typecheck!
```
GHCi, version 8.3.20170907: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:23:31: error:
• Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’
• In the first argument of ‘Sing’, namely ‘px’
In the type ‘Sing px’
In the definition of data constructor ‘SMkSigma’
|
23 | Sing sx -> Sing px -> Sing (MkSigma sx px)
| ^^
```
I'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC-inferred type signature doesn't actually typecheck","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\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\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nI was curious to know what the full type signature of `SMkSigma` was, so I asked GHCi what the inferred type is:\r\n\r\n{{{\r\nλ> :i SMkSigma\r\ndata instance Sing z where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing\r\n x) (px :: Apply p x).\r\n (Sing sx) -> (Sing px) -> Sing ('MkSigma sx px)\r\n}}}\r\n\r\nI attempted to incorporate this newfound knowledge into the program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\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\n\r\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ndata family Sing :: k -> *\r\n\r\ndata Sigma (a :: *) :: (a ~> *) -> * where\r\n MkSigma :: forall (a :: *) (p :: a ~> *) (x :: a).\r\n Sing x -> Apply p x -> Sigma a p\r\n\r\ndata instance Sing (z :: Sigma a p) where\r\n SMkSigma :: forall a (p :: a ~> *) (x :: a) (sx :: Sing x) (px :: Apply p x).\r\n Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n}}}\r\n\r\nBut to my surprise, adding this inferred type signature causes the program to no longer typecheck!\r\n\r\n{{{\r\nGHCi, version 8.3.20170907: 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:23:31: error:\r\n • Expected kind ‘Apply p0 x’, but ‘px’ has kind ‘Apply p1 x’\r\n • In the first argument of ‘Sing’, namely ‘px’\r\n In the type ‘Sing px’\r\n In the definition of data constructor ‘SMkSigma’\r\n |\r\n23 | Sing sx -> Sing px -> Sing (MkSigma sx px)\r\n | ^^\r\n}}}\r\n\r\nI'm showing the output of GHC HEAD here, but this bug can be reproduced all the way back to GHC 8.0.1.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/14175Panic repSplitTyConApp_maybe2019-07-07T18:18:08ZDavid FeuerPanic repSplitTyConApp_maybeThis definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3....This definition panics!
```hs
{-# LANGUAGE TypeFamilies, TypeInType #-}
module Whoops where
import Data.Kind
type family PComp (k :: j -> Type) (x :: k) :: ()
```
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
repSplitTyConApp_maybe
j_aon[sk:1]
*
*
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type
```
If I make it a type synonym instead, I get a proper error as expected.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Panic repSplitTyConApp_maybe","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This definition panics!\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeInType #-}\r\n\r\nmodule Whoops where\r\nimport Data.Kind\r\n\r\ntype family PComp (k :: j -> Type) (x :: k) :: ()\r\n}}}\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n repSplitTyConApp_maybe\r\n j_aon[sk:1]\r\n *\r\n *\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1123:5 in ghc:Type\r\n}}}\r\n\r\nIf I make it a type synonym instead, I get a proper error as expected.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14174GHC panic with TypeInType and type family2019-07-07T18:18:09ZDavid FeuerGHC panic with TypeInType and type familyThis rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y...This rather simple type family,
```hs
{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}
module GenWhoops where
import GHC.Generics
type family GenComp k (x :: k) (y :: k) :: Ordering where
GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y
```
produces the following panic:
```
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.3.20170828 for x86_64-unknown-linux):
piResultTy
k_a1LK[tau:1]
p_a1Lz[sk:1]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type
```
This happens with both GHC 8.2.1 and something very close to HEAD.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC panic with TypeInType and type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.2","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"This rather simple type family,\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies, TypeOperators, TypeInType #-}\r\n\r\nmodule GenWhoops where\r\nimport GHC.Generics\r\n\r\ntype family GenComp k (x :: k) (y :: k) :: Ordering where\r\n GenComp ((x :+: y) p) ('L1 x) ('L1 y) = GenComp (x p) x y\r\n}}}\r\n\r\nproduces the following panic:\r\n\r\n{{{\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.3.20170828 for x86_64-unknown-linux):\r\n piResultTy\r\n k_a1LK[tau:1]\r\n p_a1Lz[sk:1]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1138:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:949:35 in ghc:Type\r\n}}}\r\n\r\nThis happens with both GHC 8.2.1 and something very close to HEAD.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.3https://gitlab.haskell.org/ghc/ghc/-/issues/14162Core Lint error2019-07-07T18:18:12ZIcelandjackCore Lint error```hs
{-# Options_GHC -dcore-lint #-}
{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}
import Data.Kind
data family Sing (a :: k)
data
SubList :: [a] -> [a] -> Type where
SubN...```hs
{-# Options_GHC -dcore-lint #-}
{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds, TypeFamilies, GADTs, TypeInType #-}
import Data.Kind
data family Sing (a :: k)
data
SubList :: [a] -> [a] -> Type where
SubNil :: SubList '[] '[]
Keep :: SubList xs ys -> SubList (x ': xs) (x ': ys)
Drop :: SubList xs ys -> SubList xs (x ': ys)
data instance
Sing (x :: SubList ys xs) where
SSubNil :: Sing SubNil
SKeep :: Sing x -> Sing (Keep x)
SDrop :: Sing x -> Sing (Drop x)
```
running it gives a massive core lint error, attached as `lint.log`.8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/14042Datatypes cannot use a type family in their return kind2019-10-07T17:13:51ZRyan ScottDatatypes cannot use a type family in their return kindThis typechecks:
```hs
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Id (a :: Type) = a
data Foo :: Id Type
```
But changing the type synonym to a type family causes it to fail:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ...This typechecks:
```hs
{-# LANGUAGE TypeInType #-}
import Data.Kind
type Id (a :: Type) = a
data Foo :: Id Type
```
But changing the type synonym to a type family causes it to fail:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
type family Id (a :: Type) :: Type where
Id a = a
data Foo :: Id Type
```
```
$ ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Foo.hs:9:1: error:
• Kind signature on data type declaration has non-* return kind
Id *
• In the data declaration for ‘Foo’
|
9 | data Foo :: Id Type
| ^^^^^^^^
```
That error message is wrong, since `Id * = *`. And, besides, the definition should be accepted.
EDIT: This was originally about the error message. But #14042 changes the goal of the bug to fix the behavior.https://gitlab.haskell.org/ghc/ghc/-/issues/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]2022-03-22T09:23:50ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-...(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type -> Type where
WeirdNil :: WeirdList a
WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs
-> p _ (WeirdCons x xs))
-> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
-> (forall y. p x0 t3 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs
-> p (WeirdList z) t2 xs
-> p z t1 ('WeirdCons x xs))
-> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
-> (forall y. p x0 t0 'WeirdNil)
-> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
-> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))
-> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x -> WeirdList x -> Type).
Sing wl
-> (forall (y :: Type). p _ WeirdNil)
-> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))
-> p _ wl
|
24 | -> (forall (y :: Type). p _ WeirdNil)
| ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64-unknown-linux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #13877 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\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\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type -> Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs\r\n -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n -> (forall y. p x0 t3 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs\r\n -> p (WeirdList z) t2 xs\r\n -> p z t1 ('WeirdCons x xs))\r\n -> p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n -> (forall y. p x0 t0 'WeirdNil)\r\n -> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n -> Sing xs -> p (WeirdList z) t1 xs -> p z t2 ('WeirdCons x xs))\r\n -> p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64-unknown-linux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n21 | elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x -> WeirdList x -> Type).\r\n Sing wl\r\n -> (forall (y :: Type). p _ WeirdNil)\r\n -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x -> Sing xs -> p _ xs -> p _ (WeirdCons x xs))\r\n -> p _ wl\r\n |\r\n24 | -> (forall (y :: Type). p _ WeirdNil)\r\n | ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64-unknown-linux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13988GADT constructor with kind equality constraint quantifies unused existential ...2019-07-07T18:18:58ZRyan ScottGADT constructor with kind equality constraint quantifies unused existential type variablesReproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):
```
$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configurati...Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):
```
$ /opt/ghc/8.2.1/bin/ghci
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
λ> :set -XTypeInType -XGADTs -fprint-explicit-foralls
λ> import Data.Kind
λ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a
```
Note that `MkFoo` quantifies two extra existential type variables, `k2` and `k3` which are completely unused!
Note that this does not occur if the `MkFoo` constructor uses an explicit `forall`:
```
λ> :set -XScopedTypeVariables
λ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)
λ> :type +v MkFoo
MkFoo :: forall k (a :: k). k ~ * => Foo a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"GADT constructor with kind equality constraint quantifies unused existential type variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Reproducible with GHC 8.0.1., 8.0.2, 8.2.1, or HEAD (but I'll use GHC 8.2.1 to show the results of `:type +v`):\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\nλ> :set -XTypeInType -XGADTs -fprint-explicit-foralls \r\nλ> import Data.Kind\r\nλ> data Foo (a :: k) where MkFoo :: (k ~ Type) => Foo (a :: k)\r\nλ> :type +v MkFoo\r\nMkFoo :: forall k1 (a :: k1) k2 (k3 :: k2). k1 ~ * => Foo a\r\n}}}\r\n\r\nNote that `MkFoo` quantifies two extra existential type variables, `k2` and `k3` which are completely unused!\r\n\r\nNote that this does not occur if the `MkFoo` constructor uses an explicit `forall`:\r\n\r\n{{{\r\nλ> :set -XScopedTypeVariables \r\nλ> data Foo (a :: k) where MkFoo :: forall k (a :: k). (k ~ Type) => Foo (a :: k)\r\nλ> :type +v MkFoo\r\nMkFoo :: forall k (a :: k). k ~ * => Foo a\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13972GHC 8.2 error message around indexes for associated type instances is baffling2019-07-07T18:19:06ZRyan ScottGHC 8.2 error message around indexes for associated type instances is bafflingThis program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instan...This program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C Left where
type T (a -> Either a b) = Int
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:8: error:
• Type indexes must match class instance head
Expected: T (a -> Either a b)
Actual: T (a -> Either a b)
• In the type instance declaration for ‘T’
In the instance declaration for ‘C Left’
|
12 | type T (a -> Either a b) = Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```
Well those expected and actual types look pretty darn similar to me!
Note that the problem can be worked around by giving an explicit kind annotation for `Left`:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C (Left :: a -> Either a b) where
type T (a -> Either a b) = Int
```
I see two things we could do here:
1. Relax the "Type indexes must match class instance head" check so that it doesn't apply to invisible kind variables like `a` and `b`.
1. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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 8.2 error message around indexes for associated type instances is baffling","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program doesn't typecheck (only in GHC 8.2 and later):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C Left where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170704: 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:12:8: error:\r\n • Type indexes must match class instance head\r\n Expected: T (a -> Either a b)\r\n Actual: T (a -> Either a b)\r\n • In the type instance declaration for ‘T’\r\n In the instance declaration for ‘C Left’\r\n |\r\n12 | type T (a -> Either a b) = Int\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nWell those expected and actual types look pretty darn similar to me!\r\n\r\nNote that the problem can be worked around by giving an explicit kind annotation for `Left`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C (Left :: a -> Either a b) where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\nI see two things we could do here:\r\n\r\n1. Relax the \"Type indexes must match class instance head\" check so that it doesn't apply to invisible kind variables like `a` and `b`.\r\n2. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13938Iface type variable out of scope: k12019-07-07T18:19:20ZRyan ScottIface type variable out of scope: k1I managed to make GHC spit out an unusual warning when doing some dependent Haskell recently. This issue is reproducible on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD. You'll need these two files:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# L...I managed to make GHC spit out an unusual warning when doing some dependent Haskell recently. This issue is reproducible on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD. You'll need these two files:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Eliminator where
import Data.Kind (Type)
data family Sing (a :: k)
data instance Sing (z :: [a]) where
SNil :: Sing '[]
SCons :: Sing x -> Sing xs -> Sing (x:xs)
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
data FunArrow = (:->) -- ^ '(->)'
| (:~>) -- ^ '(~>)'
class FunType (arr :: FunArrow) where
type Fun (k1 :: Type) arr (k2 :: Type) :: Type
class FunType arr => AppType (arr :: FunArrow) where
type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
type FunApp arr = (FunType arr, AppType arr)
instance FunType (:->) where
type Fun k1 (:->) k2 = k1 -> k2
$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
$(return [])
instance AppType (:~>) where
type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
Sing l
-> p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
-> p l
elimList = elimListPoly @(:->)
elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
Sing l
-> p @@ '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-> p @@ l
elimListTyFun = elimListPoly @(:~>) @_ @p
elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
FunApp arr
=> Sing l
-> App [a] arr Type p '[]
-> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
-> App [a] arr Type p l
elimListPoly SNil pNil _ = pNil
elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
```
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module ListSpec where
import Eliminator
import Data.Kind
import Data.Type.Equality
import GHC.TypeLits
type family Length (l :: [a]) :: Nat where {}
type family Map (f :: a ~> b) (l :: [a]) :: [b] where {}
type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
= Length l :~: Length (Map f l)
data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type
type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l
mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
Length l :~: Length (Map f l)
mapPreservesLength
= elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined
```
You'll need to compile the files like this:
```
$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c Eliminator.hs
$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c ListSpec.hs
./Eliminator.hi
Declaration for elimListTyFun
Unfolding of elimListTyFun:
Iface type variable out of scope: k2
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Iface type variable out of scope: k1","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeApplications","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I managed to make GHC spit out an unusual warning when doing some dependent Haskell recently. This issue is reproducible on GHC 8.0.1, 8.0.2, 8.2.1, and HEAD. You'll need these two files:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeApplications #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Eliminator where\r\n\r\nimport Data.Kind (Type)\r\n\r\ndata family Sing (a :: k)\r\ndata instance Sing (z :: [a]) where\r\n SNil :: Sing '[]\r\n SCons :: Sing x -> Sing xs -> Sing (x:xs)\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 a @@ b = Apply a b\r\ninfixl 9 @@\r\n\r\ndata FunArrow = (:->) -- ^ '(->)'\r\n | (:~>) -- ^ '(~>)'\r\n\r\nclass FunType (arr :: FunArrow) where\r\n type Fun (k1 :: Type) arr (k2 :: Type) :: Type\r\n\r\nclass FunType arr => AppType (arr :: FunArrow) where\r\n type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2\r\n\r\ntype FunApp arr = (FunType arr, AppType arr)\r\n\r\ninstance FunType (:->) where\r\n type Fun k1 (:->) k2 = k1 -> k2\r\n\r\n$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter\r\n\r\ninstance AppType (:->) where\r\n type App k1 (:->) k2 (f :: k1 -> k2) x = f x\r\n\r\ninstance FunType (:~>) where\r\n type Fun k1 (:~>) k2 = k1 ~> k2\r\n\r\n$(return [])\r\n\r\ninstance AppType (:~>) where\r\n type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x\r\n\r\ninfixr 0 -?>\r\ntype (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2\r\n\r\nelimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).\r\n Sing l\r\n -> p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))\r\n -> p l\r\nelimList = elimListPoly @(:->)\r\n\r\nelimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).\r\n Sing l\r\n -> p @@ '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))\r\n -> p @@ l\r\nelimListTyFun = elimListPoly @(:~>) @_ @p\r\n\r\nelimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).\r\n FunApp arr\r\n => Sing l\r\n -> App [a] arr Type p '[]\r\n -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))\r\n -> App [a] arr Type p l\r\nelimListPoly SNil pNil _ = pNil\r\nelimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)\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\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule ListSpec where\r\n\r\nimport Eliminator\r\nimport Data.Kind\r\nimport Data.Type.Equality\r\nimport GHC.TypeLits\r\n\r\ntype family Length (l :: [a]) :: Nat where {}\r\ntype family Map (f :: a ~> b) (l :: [a]) :: [b] where {}\r\n\r\ntype WhyMapPreservesLength (f :: x ~> y) (l :: [x])\r\n = Length l :~: Length (Map f l)\r\ndata WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type\r\ntype instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l\r\n\r\nmapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).\r\n Length l :~: Length (Map f l)\r\nmapPreservesLength\r\n = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined\r\n}}}\r\n\r\nYou'll need to compile the files like this:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c Eliminator.hs \r\n$ /opt/ghc/8.0.2/bin/ghc -fforce-recomp -O2 -c ListSpec.hs \r\n./Eliminator.hi\r\nDeclaration for elimListTyFun\r\nUnfolding of elimListTyFun:\r\n Iface type variable out of scope: k2\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13913Can't apply higher-ranked kind in type family2019-07-07T18:19:30ZRyan ScottCan't apply higher-ranked kind in type familyThis code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g ...This code doesn't typecheck due to `F2`:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
f :: (forall (a :: Type). a -> a) -> Bool
f g = g True
type F1 (g :: forall (a :: Type). a -> a) = g True
type family F2 (g :: forall (a :: Type). a -> a) :: Bool where
F2 g = g True
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:14:6: error:
• Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’
• In the first argument of ‘F2’, namely ‘g’
In the type family declaration for ‘F2’
|
14 | F2 g = g True
| ^
```
This is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Can't apply higher-ranked kind in type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This code doesn't typecheck due to `F2`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nf :: (forall (a :: Type). a -> a) -> Bool\r\nf g = g True\r\n\r\ntype F1 (g :: forall (a :: Type). a -> a) = g True\r\n\r\ntype family F2 (g :: forall (a :: Type). a -> a) :: Bool where\r\n F2 g = g True\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: 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:14:6: error:\r\n • Expected kind ‘forall a. a -> a’, but ‘g’ has kind ‘Bool -> Bool’\r\n • In the first argument of ‘F2’, namely ‘g’\r\n In the type family declaration for ‘F2’\r\n |\r\n14 | F2 g = g True\r\n | ^\r\n}}}\r\n\r\nThis is surprising to me, since `F2` seems like the type family counterpart to `f` and `F1`, both of which typecheck.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13910Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)2019-07-07T18:19:31ZRyan ScottInlining a definition causes GHC to panic (repSplitTyConApp_maybe)Here is a program which I believe //should// typecheck:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-} ...Here is a program which I believe //should// typecheck:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
data family Sing (a :: k)
class SingKind k where
type Demote k = (r :: *) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data SomeSing k where
SomeSing :: Sing (a :: 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'
data TyFun :: * -> * -> *
type a ~> b = TyFun a b -> *
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
type a @@ b = Apply a b
infixl 9 @@
data FunArrow = (:->) | (:~>)
class FunType (arr :: FunArrow) where
type Fun (k1 :: Type) arr (k2 :: Type) :: Type
class FunType arr => AppType (arr :: FunArrow) where
type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
type FunApp arr = (FunType arr, AppType arr)
instance FunType (:->) where
type Fun k1 (:->) k2 = k1 -> k2
$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
instance AppType (:->) where
type App k1 (:->) k2 (f :: k1 -> k2) x = f x
instance FunType (:~>) where
type Fun k1 (:~>) k2 = k1 ~> k2
$(return [])
instance AppType (:~>) where
type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
infixr 0 -?>
type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
data instance Sing (z :: a :~: b) where
SRefl :: Sing Refl
instance SingKind (a :~: b) where
type Demote (a :~: b) = a :~: b
fromSing SRefl = Refl
toSing Refl = SomeSing SRefl
(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
Sing r
-> p @@ Refl
-> p @@ r
(~>:~:) SRefl pRefl = pRefl
type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
(y :: t) (e :: from :~: y) = App t arr Type p y
data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
:: forall (y :: t). from :~: y ~> Type
type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
= WhyReplacePoly arr from p y x
replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
p from
-> from :~: to
-> p to
replace = replacePoly @(:->)
replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
p @@ from
-> from :~: to
-> p @@ to
replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
(p :: (t -?> Type) arr).
FunApp arr
=> App t arr Type p from
-> from :~: to
-> App t arr Type p to
replacePoly from eq =
withSomeSing eq $ \(singEq :: Sing r) ->
(~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
= App t arr Type f a -> App t arr Type f z
data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
:: t ~> Type
type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
(a :: t) (b :: t).
FunApp arr
=> a :~: b
-> App t arr Type f a
-> App t arr Type f b
leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
a :~: b
-> f a
-> f b
leibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id
-- The line above is what you get if you inline the definition of leibnizPoly.
-- It causes a panic, however.
--
-- An equivalent implementation is commented out below, which does *not*
-- cause GHC to panic.
--
-- leibniz = leibnizPoly @(:->)
leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
a :~: b
-> f @@ a
-> f @@ b
leibnizTyFun = leibnizPoly @(:~>) @_ @f
```
GHC 8.2.1 and HEAD panic on the definition of `leibniz`, however:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
ghc: panic! (the 'impossible' happened)
(GHC version 8.2.0.20170623 for x86_64-unknown-linux):
repSplitTyConApp_maybe
(f_a5vT[sk:2] |> Sym (Trans
(Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
(D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
(f_a5vT[sk:2] |> Sym (Trans
(Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))
(D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]
k2_a5l0
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
Interestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:
```
$ /opt/ghc/8.0.2/bin/ghci Bug.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:134:64: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64-unknown-linux):
No skolem info: k2_a4KV
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | #13877 |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Inlining a definition causes GHC to panic (repSplitTyConApp_maybe)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here is a program which I believe //should// typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-} \r\n{-# LANGUAGE ConstraintKinds #-} \r\n{-# LANGUAGE GADTs #-} \r\n{-# LANGUAGE RankNTypes #-} \r\n{-# LANGUAGE ScopedTypeVariables #-} \r\n{-# LANGUAGE TemplateHaskell #-} \r\n{-# LANGUAGE Trustworthy #-} \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.Type.Equality \r\n \r\ndata family Sing (a :: k)\r\n\r\nclass SingKind k where\r\n type Demote k = (r :: *) | r -> k\r\n fromSing :: Sing (a :: k) -> Demote k\r\n toSing :: Demote k -> SomeSing k\r\n\r\ndata SomeSing k where\r\n SomeSing :: Sing (a :: 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\ndata TyFun :: * -> * -> *\r\ntype a ~> b = TyFun a b -> *\r\ninfixr 0 ~>\r\n\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\ntype a @@ b = Apply a b\r\ninfixl 9 @@\r\n\r\ndata FunArrow = (:->) | (:~>)\r\n\r\nclass FunType (arr :: FunArrow) where\r\n type Fun (k1 :: Type) arr (k2 :: Type) :: Type\r\n\r\nclass FunType arr => AppType (arr :: FunArrow) where\r\n type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2\r\n\r\ntype FunApp arr = (FunType arr, AppType arr)\r\n\r\ninstance FunType (:->) where\r\n type Fun k1 (:->) k2 = k1 -> k2\r\n\r\n$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter\r\n\r\ninstance AppType (:->) where\r\n type App k1 (:->) k2 (f :: k1 -> k2) x = f x\r\n\r\ninstance FunType (:~>) where\r\n type Fun k1 (:~>) k2 = k1 ~> k2\r\n\r\n$(return [])\r\n\r\ninstance AppType (:~>) where\r\n type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x\r\n\r\ninfixr 0 -?>\r\ntype (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2\r\n\r\ndata instance Sing (z :: a :~: b) where\r\n SRefl :: Sing Refl\r\n\r\ninstance SingKind (a :~: b) where\r\n type Demote (a :~: b) = a :~: b\r\n fromSing SRefl = Refl\r\n toSing Refl = SomeSing SRefl\r\n\r\n(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).\r\n Sing r\r\n -> p @@ Refl\r\n -> p @@ r\r\n(~>:~:) SRefl pRefl = pRefl\r\n\r\ntype WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)\r\n (y :: t) (e :: from :~: y) = App t arr Type p y\r\ndata WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)\r\n :: forall (y :: t). from :~: y ~> Type\r\ntype instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x\r\n = WhyReplacePoly arr from p y x\r\n\r\nreplace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).\r\n p from\r\n -> from :~: to\r\n -> p to\r\nreplace = replacePoly @(:->)\r\n\r\nreplaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).\r\n p @@ from\r\n -> from :~: to\r\n -> p @@ to\r\nreplaceTyFun = replacePoly @(:~>) @_ @_ @_ @p\r\n\r\nreplacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)\r\n (p :: (t -?> Type) arr).\r\n FunApp arr\r\n => App t arr Type p from\r\n -> from :~: to\r\n -> App t arr Type p to\r\nreplacePoly from eq =\r\n withSomeSing eq $ \\(singEq :: Sing r) ->\r\n (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from\r\n\r\ntype WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)\r\n = App t arr Type f a -> App t arr Type f z\r\ndata WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)\r\n :: t ~> Type\r\ntype instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z\r\n\r\nleibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)\r\n (a :: t) (b :: t).\r\n FunApp arr\r\n => a :~: b\r\n -> App t arr Type f a\r\n -> App t arr Type f b\r\nleibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id\r\n\r\nleibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).\r\n a :~: b\r\n -> f a\r\n -> f b\r\nleibniz = replaceTyFun @t @a @b @(WhyLeibnizPolySym (:->) f a) id\r\n-- The line above is what you get if you inline the definition of leibnizPoly.\r\n-- It causes a panic, however.\r\n--\r\n-- An equivalent implementation is commented out below, which does *not*\r\n-- cause GHC to panic.\r\n--\r\n-- leibniz = leibnizPoly @(:->)\r\n\r\nleibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).\r\n a :~: b\r\n -> f @@ a\r\n -> f @@ b\r\nleibnizTyFun = leibnizPoly @(:~>) @_ @f\r\n}}}\r\n\r\nGHC 8.2.1 and HEAD panic on the definition of `leibniz`, however:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: 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\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.0.20170623 for x86_64-unknown-linux):\r\n repSplitTyConApp_maybe\r\n (f_a5vT[sk:2] |> Sym (Trans\r\n (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))\r\n (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]\r\n (f_a5vT[sk:2] |> Sym (Trans\r\n (Sym (D:R:Funk1:->k2[0] <k1>_N <k2>_N))\r\n (D:R:Funk1:->k2[0] <t>_N <*>_N))) a_a5vU[sk:2]\r\n k2_a5l0\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1122:5 in ghc:Type\r\n\r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}\r\n\r\nInterestingly, GHC 8.0.1 and 8.0.2 do not give the same panic—they give the panic from #13877:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Bug.hs\r\nGHCi, version 8.0.2: 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:134:64: error:ghc: panic! (the 'impossible' happened) \r\n (GHC version 8.0.2 for x86_64-unknown-linux): \r\n No skolem info: k2_a4KV \r\n \r\nPlease report this as a GHC bug: http://www.haskell.org/ghc/reportabug\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13909Misleading error message when partially applying a data type with a visible q...2019-07-07T18:19:32ZRyan ScottMisleading error message when partially applying a data type with a visible quantifier in its kindI'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) ...I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) where
getName :: proxy a -> String
instance HasName Hm where
getName _ = "Hm"
```
This is rejected, however:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:18: error:
• Expecting two more arguments to ‘Hm’
Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
• In the first argument of ‘HasName’, namely ‘Hm’
In the instance declaration for ‘HasName Hm’
|
11 | instance HasName Hm where
| ^^
```
The culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Can't partially apply a data type with a visible quantifier in its kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Hm (k :: Type) (a :: k) :: Type\r\n\r\nclass HasName (a :: k) where\r\n getName :: proxy a -> String\r\n\r\ninstance HasName Hm where\r\n getName _ = \"Hm\"\r\n}}}\r\n\r\nThis is rejected, however:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:18: error:\r\n • Expecting two more arguments to ‘Hm’\r\n Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’\r\n • In the first argument of ‘HasName’, namely ‘Hm’\r\n In the instance declaration for ‘HasName Hm’\r\n |\r\n11 | instance HasName Hm where\r\n | ^^\r\n}}}\r\n\r\nThe culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13895"Illegal constraint in a type" error - is it fixable?2019-07-07T18:19:36ZRyan Scott"Illegal constraint in a type" error - is it fixable?I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d ...I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this doesn't typecheck:
```
• Could not deduce (Typeable (t k0))
from the context: (Data a, Typeable (t k))
bound by the type signature for:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
at NewData.hs:(170,3)-(173,26)
The type variable ‘k0’ is ambiguous
• In the ambiguity check for ‘dataCast1’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the class method:
dataCast1 :: forall a.
Data a =>
forall k (c :: * -> *) (t :: forall k1. k1 -> *).
Typeable (t k) =>
(forall d. Data d => c (t * d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
This makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:
```hs
dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t
=> (forall d. Data d => c (t d))
-> Maybe (c a)
```
But this also doesn't work:
```
NewData.hs:171:25: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘Typeable’, namely ‘t’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
171 | Typeable t
| ^
NewData.hs:172:40: error:
• Illegal constraint in a type: Typeable k0
• In the first argument of ‘c’, namely ‘(t d)’
In the type signature:
dataCast1 :: forall (c :: Type -> Type)
(t :: forall (k :: Type). Typeable k => k -> Type).
Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
In the class declaration for ‘Data’
|
172 | => (forall d. Data d => c (t d))
| ^^^
```
At this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [test case](http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs) checking for this behavior.
But is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"\"Illegal constraint in a type\" error - is it fixable?","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I recently sketched out a solution to #13327. Here is the type signature that I wanted to write:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this doesn't typecheck:\r\n\r\n{{{\r\n • Could not deduce (Typeable (t k0))\r\n from the context: (Data a, Typeable (t k))\r\n bound by the type signature for:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n at NewData.hs:(170,3)-(173,26)\r\n The type variable ‘k0’ is ambiguous\r\n • In the ambiguity check for ‘dataCast1’\r\n To defer the ambiguity check to use sites, enable AllowAmbiguousTypes\r\n When checking the class method:\r\n dataCast1 :: forall a.\r\n Data a =>\r\n forall k (c :: * -> *) (t :: forall k1. k1 -> *).\r\n Typeable (t k) =>\r\n (forall d. Data d => c (t * d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n170 | dataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). k -> Type).\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nThis makes sense, since GHC has no way to conclude that the `k` in `t`'s kind is also `Typeable`. I tried to convince GHC of that fact:\r\n\r\n{{{#!hs\r\ndataCast1 :: forall (c :: Type -> Type) (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t\r\n => (forall d. Data d => c (t d))\r\n -> Maybe (c a)\r\n}}}\r\n\r\nBut this also doesn't work:\r\n\r\n{{{\r\nNewData.hs:171:25: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘Typeable’, namely ‘t’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n171 | Typeable t\r\n | ^\r\n\r\nNewData.hs:172:40: error:\r\n • Illegal constraint in a type: Typeable k0\r\n • In the first argument of ‘c’, namely ‘(t d)’\r\n In the type signature:\r\n dataCast1 :: forall (c :: Type -> Type)\r\n (t :: forall (k :: Type). Typeable k => k -> Type).\r\n Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)\r\n In the class declaration for ‘Data’\r\n |\r\n172 | => (forall d. Data d => c (t d))\r\n | ^^^\r\n}}}\r\n\r\nAt this point, I'm stuck, since I have no idea how to work around this `Illegal constraint in a type` error. This error message appears to have originated as a part of the `TypeInType` patch, since there's even a [http://git.haskell.org/ghc.git/blob/58c781da4861faab11e4c5804e07e6892908ef72:/testsuite/tests/dependent/should_fail/PromotedClass.hs test case] checking for this behavior.\r\n\r\nBut is this a fundamental limitation of kind equalities? Or would it be possible to lift this restriction?","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/13879Strange interaction between higher-rank kinds and type synonyms2019-07-07T18:19:41ZRyan ScottStrange interaction between higher-rank kinds and type synonymsHere's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAG...Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data (a :: j) :~~: (b :: k) where
HRefl :: a :~~: a
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> p HRefl
-> p r
(%:~~:->) SHRefl pHRefl = pHRefl
type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x
```
Now I want to refactor this so that I use `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> App p HRefl
-> App p r
```
However, GHC doesn't like that:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘(:~~:) j z a a’,
but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’
• In the second argument of ‘App’, namely ‘HRefl’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
21 | -> App p HRefl
| ^^^^^
Bug.hs:22:20: error:
• Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’
• In the second argument of ‘App’, namely ‘r’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
22 | -> App p r
| ^
```
These errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.
Out of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> HRApp p HRefl
-> HRApp p r
```
But now I get an even stranger error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:22:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
22 | -> HRApp p r
| ^
```
That's right, it can't match the kinds:
- `forall z (y :: z). (:~~:) j z a y -> *`, and
- `forall z (y :: z). (:~~:) j z a y -> *`
Uh... what? Those are the same kind!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Strange interaction between higher-rank kinds and type synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\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\n\r\ndata family Sing (a :: k)\r\n\r\ndata (a :: j) :~~: (b :: k) where\r\n HRefl :: a :~~: a\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> p HRefl\r\n -> p r\r\n(%:~~:->) SHRefl pHRefl = pHRefl\r\n\r\ntype App f x = f x\r\ntype HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x\r\n}}}\r\n\r\nNow I want to refactor this so that I use `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> App p HRefl\r\n -> App p r\r\n}}}\r\n\r\nHowever, GHC doesn't like that:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: 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:21:20: error:\r\n • Expected kind ‘(:~~:) j z a a’,\r\n but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’\r\n • In the second argument of ‘App’, namely ‘HRefl’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n21 | -> App p HRefl\r\n | ^^^^^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’\r\n • In the second argument of ‘App’, namely ‘r’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n22 | -> App p r\r\n | ^\r\n}}}\r\n\r\nThese errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.\r\n\r\nOut of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> HRApp p HRefl\r\n -> HRApp p r\r\n}}}\r\n\r\nBut now I get an even stranger error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: 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:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n22 | -> HRApp p r\r\n | ^\r\n}}}\r\n\r\nThat's right, it can't match the kinds:\r\n\r\n* `forall z (y :: z). (:~~:) j z a y -> *`, and\r\n* `forall z (y :: z). (:~~:) j z a y -> *`\r\n\r\nUh... what? Those are the same kind!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13872Strange Typeable error message involving TypeInType2019-07-07T18:19:44ZRyan ScottStrange Typeable error message involving TypeInTypeI originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo whe...I originally discovered this when tinkering with #13871. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind
import Data.Typeable
data Foo (a :: Type) (b :: Type) where
MkFoo :: (a ~ Int, b ~ Char) => Foo a b
data family Sing (a :: k)
data SFoo (z :: Foo a b) where
SMkFoo :: SFoo MkFoo
f :: String
f = show $ typeOf SMkFoo
```
Fails in GHC 8.0.1, 8.0.2, and 8.2 (after applying [D3671](https://phabricator.haskell.org/D3671)) with a rather unsightly error message:
```
GHCi, version 8.3.20170624: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Foo.hs, interpreted )
Foo.hs:19:12: error:
• No instance for (Typeable <>) arising from a use of ‘typeOf’
• In the second argument of ‘($)’, namely ‘typeOf SMkFoo’
In the expression: show $ typeOf SMkFoo
In an equation for ‘f’: f = show $ typeOf SMkFoo
|
19 | f = show $ typeOf SMkFoo
| ^^^^^^^^^^^^^
```
I'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.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":"Strange Typeable error message involving TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally discovered this when tinkering with #13871. This program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind\r\nimport Data.Typeable\r\n\r\ndata Foo (a :: Type) (b :: Type) where\r\n MkFoo :: (a ~ Int, b ~ Char) => Foo a b\r\n\r\ndata family Sing (a :: k)\r\ndata SFoo (z :: Foo a b) where\r\n SMkFoo :: SFoo MkFoo\r\n\r\nf :: String\r\nf = show $ typeOf SMkFoo\r\n}}}\r\n\r\nFails in GHC 8.0.1, 8.0.2, and 8.2 (after applying Phab:D3671) with a rather unsightly error message:\r\n\r\n{{{\r\nGHCi, version 8.3.20170624: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:19:12: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeOf’\r\n • In the second argument of ‘($)’, namely ‘typeOf SMkFoo’\r\n In the expression: show $ typeOf SMkFoo\r\n In an equation for ‘f’: f = show $ typeOf SMkFoo\r\n |\r\n19 | f = show $ typeOf SMkFoo\r\n | ^^^^^^^^^^^^^\r\n}}}\r\n\r\nI'm not sure what this mysterious `<>` is, but I'm pretty sure it shouldn't be making an appearance here. (See also #13780, where `<>` also makes a surprise guest appearance.)","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13822GHC not using injectivity?2019-07-07T18:19:56ZIcelandjackGHC not using injectivity?This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds...This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TInt :: Ty STAR
TBool :: Ty STAR
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family
IK (k :: KIND) = (res :: Type) | res -> k where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family
I (t :: Ty k) = (res :: IK k) | res -> t where
I TInt = Int
I TBool = Bool
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyInt :: TyRep STAR TInt
TyBool :: TyRep STAR TBool
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
zero :: TyRep STAR a -> I a
zero = \case
TyInt -> 0
TyBool -> False
TyApp TyMaybe _ -> Nothing
```
When I ask it to infer the representation for `Int` and `Bool` it does so with no surprises
```hs
-- Inferred type:
--
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int
-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool
```
but inferring the representation for `Maybe Int` fails
```hs
-- v.hs:43:16: error:
-- • Couldn't match kind ‘k’ with ‘'STAR’
-- ‘k’ is a rigid type variable bound by
-- the inferred type of
-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- at v.hs:25:3
-- When matching the kind of ‘'TMaybe’
-- Expected type: Maybe Int
-- Actual type: I ('TApp 'TMaybe 'TInt)
-- • In the expression: zero rep :: Maybe Int
-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
-- • Relevant bindings include
-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int
```
even though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`
```
>>> :kind! I (TMaybe `TApp` TInt)
I (TMaybe `TApp` TInt) :: IK 'STAR
= Maybe Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC not using injectivity?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be normal behavior but.. (Example from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality])\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}\r\n\r\nimport Data.Kind\r\n\r\ndata KIND = STAR | KIND :> KIND\r\n\r\ndata Ty :: KIND -> Type where\r\n TInt :: Ty STAR\r\n TBool :: Ty STAR\r\n TMaybe :: Ty (STAR :> STAR)\r\n TApp :: Ty (a :> b) -> (Ty a -> Ty b)\r\n\r\ntype family\r\n IK (k :: KIND) = (res :: Type) | res -> k where\r\n IK STAR = Type\r\n IK (a:>b) = IK a -> IK b\r\n\r\ntype family\r\n I (t :: Ty k) = (res :: IK k) | res -> t where\r\n I TInt = Int\r\n I TBool = Bool\r\n I TMaybe = Maybe\r\n I (TApp f a) = (I f) (I a)\r\n\r\ndata TyRep (k :: KIND) (t :: Ty k) where\r\n TyInt :: TyRep STAR TInt\r\n TyBool :: TyRep STAR TBool\r\n TyMaybe :: TyRep (STAR:>STAR) TMaybe\r\n TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)\r\n\r\nzero :: TyRep STAR a -> I a\r\nzero = \\case\r\n TyInt -> 0\r\n TyBool -> False\r\n TyApp TyMaybe _ -> Nothing\r\n}}}\r\n\r\nWhen I ask it to infer the representation for `Int` and `Bool` it does so with no surprises\r\n\r\n{{{#!hs\r\n-- Inferred type: \r\n-- \r\n-- int :: TyRep STAR TInt -> Int\r\nint rep = zero rep :: Int\r\n\r\n\r\n-- bool:: TyRep STAR TBool -> Bool\r\nbool rep = zero rep :: Bool\r\n}}}\r\n\r\nbut inferring the representation for `Maybe Int` fails\r\n\r\n{{{#!hs\r\n-- v.hs:43:16: error:\r\n-- • Couldn't match kind ‘k’ with ‘'STAR’\r\n-- ‘k’ is a rigid type variable bound by\r\n-- the inferred type of\r\n-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>\r\n-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- at v.hs:25:3\r\n-- When matching the kind of ‘'TMaybe’\r\n-- Expected type: Maybe Int\r\n-- Actual type: I ('TApp 'TMaybe 'TInt)\r\n-- • In the expression: zero rep :: Maybe Int\r\n-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int\r\n-- • Relevant bindings include\r\n-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)\r\n-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- (bound at v.hs:43:1)\r\n-- Failed, modules loaded: none.\r\nmaybeInt rep = zero rep :: Maybe Int\r\n}}}\r\n\r\neven though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`\r\n\r\n{{{\r\n>>> :kind! I (TMaybe `TApp` TInt)\r\nI (TMaybe `TApp` TInt) :: IK 'STAR\r\n= Maybe Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13790GHC doesn't reduce type family in kind signature unless its arm is twisted2019-07-07T18:20:04ZRyan ScottGHC doesn't reduce type family in kind signature unless its arm is twistedHere's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}...Here's some code (inspired by Richard's musings [here](https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297)) which typechecks with GHC 8.2.1 or HEAD:
```hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data SomeSing (k :: Type) where
SomeSing :: Sing (a :: k) -> SomeSing k
type family Promote k :: Type
class (Promote (Demote k) ~ k) => SingKind (k :: Type) where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
type family DemoteX (a :: k) :: Demote k
type instance DemoteX (a :: Type) = Demote a
type instance Promote Type = Type
instance SingKind Type where
type Demote Type = Type
fromSing = error "fromSing Type"
toSing = error "toSing Type"
-----
data N = Z | S N
data instance Sing (z :: N) where
SZ :: Sing Z
SS :: Sing n -> Sing (S n)
type instance Promote N = N
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
```
Things get more interesting if you try to add this type instance at the end of this file:
```hs
type instance DemoteX (n :: N) = n
```
Now GHC will complain:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:49:34: error:
• Expected kind ‘Demote N’, but ‘n’ has kind ‘N’
• In the type ‘n’
In the type instance declaration for ‘DemoteX’
|
49 | type instance DemoteX (n :: N) = n
| ^
```
That error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:
```hs
...
instance SingKind N where
type Demote N = N
fromSing SZ = Z
fromSing (SS n) = S (fromSing n)
toSing Z = SomeSing SZ
toSing (S n) = case toSing n of
SomeSing sn -> SomeSing (SS sn)
$(return [])
type instance DemoteX (n :: N) = n
```
Then the file typechecks without issue.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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 doesn't reduce type family in kind signature unless its arm is twisted","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code (inspired by Richard's musings [https://github.com/goldfirere/singletons/issues/150#issuecomment-306088297 here]) which typechecks with GHC 8.2.1 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleInstances #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata SomeSing (k :: Type) where\r\n SomeSing :: Sing (a :: k) -> SomeSing k\r\n\r\ntype family Promote k :: Type\r\n\r\nclass (Promote (Demote k) ~ k) => SingKind (k :: Type) 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\ntype family DemoteX (a :: k) :: Demote k\r\ntype instance DemoteX (a :: Type) = Demote a\r\n\r\ntype instance Promote Type = Type\r\n\r\ninstance SingKind Type where\r\n type Demote Type = Type\r\n fromSing = error \"fromSing Type\"\r\n toSing = error \"toSing Type\"\r\n\r\n-----\r\n\r\ndata N = Z | S N\r\n\r\ndata instance Sing (z :: N) where\r\n SZ :: Sing Z\r\n SS :: Sing n -> Sing (S n)\r\ntype instance Promote N = N\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n}}}\r\n\r\nThings get more interesting if you try to add this type instance at the end of this file:\r\n\r\n{{{#!hs\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nNow GHC will complain:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: 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:49:34: error:\r\n • Expected kind ‘Demote N’, but ‘n’ has kind ‘N’\r\n • In the type ‘n’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n49 | type instance DemoteX (n :: N) = n\r\n | ^\r\n}}}\r\n\r\nThat error message smells funny, since we do have a type family instance that says `Demote N = N`! In fact, if you use Template Haskell to split up the declarations manually:\r\n\r\n{{{#!hs\r\n...\r\n\r\ninstance SingKind N where\r\n type Demote N = N\r\n fromSing SZ = Z\r\n fromSing (SS n) = S (fromSing n)\r\n toSing Z = SomeSing SZ\r\n toSing (S n) = case toSing n of\r\n SomeSing sn -> SomeSing (SS sn)\r\n$(return [])\r\ntype instance DemoteX (n :: N) = n\r\n}}}\r\n\r\nThen the file typechecks without issue.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13781(a :: (k :: Type)) is too exotic for Template Haskell2019-07-07T18:20:06ZRyan Scott(a :: (k :: Type)) is too exotic for Template HaskellOn GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```...On GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:8:3: error:
Exotic form of kind not (yet) handled by Template Haskell
(k :: Type)
|
8 | $([d| f :: Proxy (a :: (k :: Type))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
I don't think this would be too hard to support, though. I'll take a shot at fixing this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"(a :: (k :: Type)) is too exotic for Template Haskell","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"On GHC 8.0.1 or later, GHC will choke on this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\n$([d| f :: Proxy (a :: (k :: Type))\r\n f = Proxy\r\n |])\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: 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:8:3: error:\r\n Exotic form of kind not (yet) handled by Template Haskell\r\n (k :: Type)\r\n |\r\n8 | $([d| f :: Proxy (a :: (k :: Type))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nI don't think this would be too hard to support, though. I'll take a shot at fixing this.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/13780Nightmarish pretty-printing of equality type in GHC 8.2 error message2019-07-07T18:20:06ZRyan ScottNightmarish pretty-printing of equality type in GHC 8.2 error messageI originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuanti...I originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where
data family Sing (a :: k)
data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
```
In GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
```
But in GHC 8.2.1 and HEAD, it's hair-raisingly bad:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’,
but ‘'MkFoo
('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
|
9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
| ^^^^^
```
- \*WAT.\*\*
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| 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":"Nightmarish pretty-printing of equality type in GHC 8.2 error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally spotted this in https://ghc.haskell.org/trac/ghc/ticket/12102#comment:1, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Foo where\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata Foo a = a ~ Bool => MkFoo\r\ndata instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n}}}\r\n\r\nIn GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n}}}\r\n\r\nBut in GHC 8.2.1 and HEAD, it's hair-raisingly bad:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’,\r\n but ‘'MkFoo\r\n ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n |\r\n9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n | ^^^^^\r\n}}}\r\n\r\n**WAT.**","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev