GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:17:22Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/14350Infinite loop when typechecking incorrect implementation (GHC HEAD only)2019-07-07T18:17:22ZRyan ScottInfinite loop when typechecking incorrect implementation (GHC HEAD only)On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ...On GHC HEAD, typechecking this program loops infinitely:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data Proxy a = Proxy
data family Sing (a :: k)
data SomeSing k where
SomeSing :: Sing (a :: k) -> SomeSing k
class SingKind k where
type Demote k :: Type
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
data instance Sing (x :: Proxy k) where
SProxy :: Sing 'Proxy
instance SingKind (Proxy k) where
type Demote (Proxy k) = Proxy k
fromSing SProxy = Proxy
toSing Proxy = SomeSing SProxy
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 @@
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where
type Demote (k1 ~> k2) = Demote k1 -> Demote k2
fromSing sFun x = case toSing x of SomeSing y -> fromSing (applySing sFun y)
toSing = undefined
dcomp :: forall (a :: Type)
(b :: a ~> Type)
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type)
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y)
(g :: forall (x :: a). Proxy x ~> b @@ x)
(x :: a).
Sing f
-> Sing g
-> Sing x
-> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))
dcomp f g x = applySing f Proxy Proxy
```
This is a regression from GHC 8.2.1/8.2.2, where it gives a proper error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.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 ( Bug.hs, interpreted )
Bug.hs:59:15: error:
• Couldn't match expected type ‘Proxy a2
-> Apply (Apply (c x4) 'Proxy) (Apply (g x4) 'Proxy)’
with actual type ‘Sing (f x y @@ t0)’
• The function ‘applySing’ is applied to three arguments,
but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
has only two
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:59:27: error:
• Couldn't match expected type ‘Sing t0’
with actual type ‘Proxy a0’
• In the second argument of ‘applySing’, namely ‘Proxy’
In the expression: applySing f Proxy Proxy
In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
• Relevant bindings include
x :: Sing x4 (bound at Bug.hs:59:11)
g :: Sing (g x3) (bound at Bug.hs:59:9)
f :: Sing (f x2 y) (bound at Bug.hs:59:7)
dcomp :: Sing (f x2 y)
-> Sing (g x3) -> Sing x4 -> (c x4 @@ 'Proxy) @@ (g x4 @@ 'Proxy)
(bound at Bug.hs:59:1)
|
59 | dcomp f g x = applySing f Proxy Proxy
| ^^^^^
```8.4.1https://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/14230Gruesome kind mismatch errors for associated data family instances2019-07-07T18:17:51ZRyan ScottGruesome kind mismatch errors for associated data family instancesSpun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
...Spun off from #14175\##14230. This program, which can only really be compiled on GHC HEAD at the moment:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
class C k where
data CD :: k -> k -> *
instance C (Maybe a) where
data CD :: (k -> *) -> (k -> *) -> *
```
Gives a heinous error message:
```
Bug.hs:11:3: error:
• Expected kind ‘(k -> *) -> (k -> *) -> *’,
but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
-> Maybe a -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
11 | data CD :: (k -> *) -> (k -> *) -> *
| ^^^^^^^
```
- We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.
- The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.
Another program in a similar vein:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C a where
data CD k (a :: k) :: k -> *
instance C (Maybe a) where
data CD k (a :: k -> *) :: (k -> *) -> *
```
```
Bug.hs:13:3: error:
• Expected kind ‘(k -> *) -> *’,
but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
• In the data instance declaration for ‘CD’
In the instance declaration for ‘C (Maybe a)’
|
13 | data CD k (a :: k -> *) :: (k -> *) -> *
| ^^^^^^^^^^^^^^^^^^^^^^^
```
This error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Gruesome kind mismatch errors for associated data family instances","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9. This program, which can only really be compiled on GHC HEAD at the moment:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Bug where\r\n\r\nclass C k where\r\n data CD :: k -> k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD :: (k -> *) -> (k -> *) -> *\r\n}}}\r\n\r\nGives a heinous error message:\r\n\r\n{{{\r\nBug.hs:11:3: error:\r\n • Expected kind ‘(k -> *) -> (k -> *) -> *’,\r\n but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a\r\n -> Maybe a -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n11 | data CD :: (k -> *) -> (k -> *) -> *\r\n | ^^^^^^^\r\n}}}\r\n\r\n* We shouldn't be expecting kind `(k -> *) -> (k -> *) -> *`, but rather kind `Maybe a -> Maybe a -> *`, due to the instance head itself.\r\n* The phrase `‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’` is similarly confusing. This doesn't point out that the real issue is the use of `(k -> *)`.\r\n\r\nAnother program in a similar vein:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\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\nclass C a where\r\n data CD k (a :: k) :: k -> *\r\n\r\ninstance C (Maybe a) where\r\n data CD k (a :: k -> *) :: (k -> *) -> *\r\n}}}\r\n{{{\r\nBug.hs:13:3: error:\r\n • Expected kind ‘(k -> *) -> *’,\r\n but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’\r\n • In the data instance declaration for ‘CD’\r\n In the instance declaration for ‘C (Maybe a)’\r\n |\r\n13 | data CD k (a :: k -> *) :: (k -> *) -> *\r\n | ^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nThis error message is further muddled by the incorrect use of `k` as the first type pattern (instead of `k -> *`, as subsequent kind signatures would suggest).","type_of_failure":"OtherFailure","blocking":[]} -->8.8.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14209GHC 8.2.1 regression involving telescoping kind signature2019-07-07T18:17:56ZRyan ScottGHC 8.2.1 regression involving telescoping kind signatureThe following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejecte...The following program typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
module Bug where
data MyProxy k (a :: k) = MyProxy
data Foo (z :: MyProxy k (a :: k))
```
But in GHC 8.2.1, it's rejected:
```
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:6:1: error:
Kind variable ‘k’ is implicitly bound in datatype
‘Foo’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it explicitly somewhere?
Type variables with inferred kinds:
(k :: *) (a :: k) (z :: MyProxy k a)
|
6 | data Foo (z :: MyProxy k (a :: k))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2.1 regression involving telescoping kind signature","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":[""],"type":"Bug","description":"The following program typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\ndata MyProxy k (a :: k) = MyProxy\r\ndata Foo (z :: MyProxy k (a :: k))\r\n}}}\r\n\r\nBut in GHC 8.2.1, it's rejected:\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 Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:6:1: error:\r\n Kind variable ‘k’ is implicitly bound in datatype\r\n ‘Foo’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it explicitly somewhere?\r\n Type variables with inferred kinds:\r\n (k :: *) (a :: k) (z :: MyProxy k a)\r\n |\r\n6 | data Foo (z :: MyProxy k (a :: k))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.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/14086Empty case does not detect kinds2023-02-12T12:50:17ZDavid FeuerEmpty case does not detect kinds```hs
{-# language TypeInType, EmptyCase #-}
module Silly where
import Data.Kind
f :: Type -> Int
f x = case x of
```
GHC warns
```
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: *
```
...```hs
{-# language TypeInType, EmptyCase #-}
module Silly where
import Data.Kind
f :: Type -> Int
f x = case x of
```
GHC warns
```
Pattern match(es) are non-exhaustive
In a case alternative: Patterns not matched: _ :: *
```
In fact, `Type` is only a type because of `TypeInType`. It has no actual values, so the empty case is exhaustive.
To be honest, I kind of wish GHC would give me a warning for doing something so silly as to even give a function an argument of type `Type`, but I imagine that might be hard.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | low |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Empty case does not detect kinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\n{-# language TypeInType, EmptyCase #-}\r\nmodule Silly where\r\nimport Data.Kind\r\n\r\nf :: Type -> Int\r\nf x = case x of\r\n}}}\r\n\r\nGHC warns\r\n\r\n{{{\r\n Pattern match(es) are non-exhaustive\r\n In a case alternative: Patterns not matched: _ :: *\r\n}}}\r\n\r\nIn fact, `Type` is only a type because of `TypeInType`. It has no actual values, so the empty case is exhaustive.\r\n\r\nTo be honest, I kind of wish GHC would give me a warning for doing something so silly as to even give a function an argument of type `Type`, but I imagine that might be hard.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://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/13915GHC 8.2 regression: "Can't find interface-file declaration" for promoted data...2019-07-07T18:19:30ZRyan ScottGHC 8.2 regression: "Can't find interface-file declaration" for promoted data family instanceDue to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's...Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE TypeFamilies #-}
module Foo where
data family T a
data instance T Int = MkT
```
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Foo
data Proxy (a :: k)
data S = MkS (Proxy 'MkT)
```
However, this stopped typechecking in GHC 8.2:
```
$ /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 2] Compiling Foo ( Foo.hs, interpreted )
[2 of 2] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1:1: error:
Can't find interface-file declaration for variable Foo.$tc'MkT
Probable cause: bug in .hi-boot file, or inconsistent .hi file
Use -ddump-if-trace to get an idea of which file caused the error
|
1 | {-# LANGUAGE TypeInType #-}
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2 regression: \"Can't find interface-file declaration\" for promoted data family instance","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Due to #12088, you can't define a data family instance and promote it in the same module. One could, up until GHC 8.2, work around this using (somewhat obscure) wisdom: define the data family instance in a separate module from where it's promoted. For example, `Bug` typechecks in GHC 8.0.1 and 8.0.2:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\ndata family T a\r\ndata instance T Int = MkT\r\n}}}\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Foo\r\n\r\ndata Proxy (a :: k)\r\ndata S = MkS (Proxy 'MkT)\r\n}}}\r\n\r\nHowever, this stopped typechecking in GHC 8.2:\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 2] Compiling Foo ( Foo.hs, interpreted )\r\n[2 of 2] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:1:1: error:\r\n Can't find interface-file declaration for variable Foo.$tc'MkT\r\n Probable cause: bug in .hi-boot file, or inconsistent .hi file\r\n Use -ddump-if-trace to get an idea of which file caused the error\r\n |\r\n1 | {-# LANGUAGE TypeInType #-}\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.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.1