GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:21:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13555Typechecker regression when combining PolyKinds and MonoLocalBinds2019-07-07T18:21:21ZRyan ScottTypechecker regression when combining PolyKinds and MonoLocalBinds`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUA...`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:
```hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
module Crypto.Lol.Types.FiniteField (GF(..)) where
import Data.Functor.Identity (Identity(..))
data T a
type Polynomial a = T a
newtype GF fp d = GF (Polynomial fp)
type CRTInfo r = (Int -> r, r)
type Tagged s b = TaggedT s Identity b
newtype TaggedT s m b = TagT { untagT :: m b }
class Reflects a i where
value :: Tagged a i
class CRTrans mon r where
crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)
instance CRTrans Maybe (GF fp d) where
crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
crtInfo = undefined
```
This typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )
Bug.hs:25:14: error:
• Couldn't match type ‘k0’ with ‘k2’
because type variable ‘k2’ would escape its scope
This (rigid, skolem) type variable is bound by
the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
Expected type: TaggedT m Maybe (CRTInfo (GF fp d))
Actual type: TaggedT m Maybe (CRTInfo (GF fp d))
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Bug.hs:25:14: error:
• Could not deduce (Reflects m Int)
from the context: Reflects m Int
bound by the type signature for:
crtInfo :: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
at Bug.hs:25:14-79
The type variable ‘k0’ is ambiguous
• When checking that instance signature for ‘crtInfo’
is more general than its signature in the class
Instance sig: forall (m :: k0).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
Class sig: forall k2 (m :: k2).
Reflects m Int =>
TaggedT m Maybe (CRTInfo (GF fp d))
In the instance declaration for ‘CRTrans Maybe (GF fp d)’
|
25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Notably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Typechecker regression when combining PolyKinds and MonoLocalBinds","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"`lol-0.6.0.0` from Hackage currently fails to build with GHC 8.2.1 because of this regression. Here is a minimized example:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE InstanceSigs #-}\r\n{-# LANGUAGE MonoLocalBinds #-}\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\nmodule Crypto.Lol.Types.FiniteField (GF(..)) where\r\n\r\nimport Data.Functor.Identity (Identity(..))\r\n\r\ndata T a\r\ntype Polynomial a = T a\r\nnewtype GF fp d = GF (Polynomial fp)\r\ntype CRTInfo r = (Int -> r, r)\r\ntype Tagged s b = TaggedT s Identity b\r\nnewtype TaggedT s m b = TagT { untagT :: m b }\r\n\r\nclass Reflects a i where\r\n value :: Tagged a i\r\n\r\nclass CRTrans mon r where\r\n crtInfo :: Reflects m Int => TaggedT m mon (CRTInfo r)\r\n\r\ninstance CRTrans Maybe (GF fp d) where\r\n crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n crtInfo = undefined\r\n}}}\r\n\r\nThis typechecks OK with GHC 8.0.2, but with 8.2.1, it complains:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Crypto.Lol.Types.FiniteField ( Bug.hs, interpreted )\r\n\r\nBug.hs:25:14: error:\r\n • Couldn't match type ‘k0’ with ‘k2’\r\n because type variable ‘k2’ would escape its scope\r\n This (rigid, skolem) type variable is bound by\r\n the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n Expected type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n Actual type: TaggedT m Maybe (CRTInfo (GF fp d))\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n\r\nBug.hs:25:14: error:\r\n • Could not deduce (Reflects m Int)\r\n from the context: Reflects m Int\r\n bound by the type signature for:\r\n crtInfo :: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n at Bug.hs:25:14-79\r\n The type variable ‘k0’ is ambiguous\r\n • When checking that instance signature for ‘crtInfo’\r\n is more general than its signature in the class\r\n Instance sig: forall (m :: k0).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n Class sig: forall k2 (m :: k2).\r\n Reflects m Int =>\r\n TaggedT m Maybe (CRTInfo (GF fp d))\r\n In the instance declaration for ‘CRTrans Maybe (GF fp d)’\r\n |\r\n25 | crtInfo :: forall m . (Reflects m Int) => TaggedT m Maybe (CRTInfo (GF fp d))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nNotably, both `PolyKinds` and `MonoLocalBinds` are required to trigger this bug.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/12503Template Haskell regression: GHC erroneously thinks a type variable is also a...2019-07-07T18:26:20ZRyan ScottTemplate Haskell regression: GHC erroneously thinks a type variable is also a kindThe following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)
```hs
{-# LANGUAGE ...The following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)
```hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -ddump-splices #-}
module Regression where
import Language.Haskell.TH
data T k
class C a
$(do TyConI (DataD [] tName [ KindedTV kName kKind]
#if __GLASGOW_HASKELL__ >= 800
_
#endif
_ _) <- reify ''T
d <- instanceD (cxt []) (conT ''C `appT` (conT tName `appT` sigT (varT kName) kKind)) []
return [d])
```
```
$ /opt/ghc/8.0.1/bin/ghc Regression.hs
[1 of 1] Compiling Regression ( Regression.hs, Regression.o )
Regression.hs:(13,3)-(19,15): Splicing declarations
do { TyConI (DataD []
tName_a2RT
[KindedTV kName_a2RU kKind_a2RV]
_
_
_) <- reify ''T;
d_a31Y <- instanceD
(cxt [])
(conT ''C
`appT` (conT tName_a2RT `appT` sigT (varT kName_a2RU) kKind_a2RV))
[];
return [d_a31Y] }
======>
instance C (T (k_avB :: k_avC))
Regression.hs:13:3: error:
Variable ‘k_avB’ used as both a kind and a type
Did you intend to use TypeInType?
```
Somewhat confusingly, you can use `instance C (T (k_avB :: k_avC))` on its own, and it will compile without issue. Also, quoting it doesn't seem to trip up this bug, as this also compiles without issue:
```hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -ddump-splices #-}
module WorksSomehow where
import Language.Haskell.TH
data T k
class C a
$([d| instance C (T k) |])
```
The original program has several workarounds:
1. Turn off `PolyKinds` (OK, this isn't a very good workaround...)
1. Add an explicit kind signature to `T`, e.g., `data T (k :: k1)`
1. Change the type variable of `T` to some other letter, e.g., `data T p` or `data T k1`
Given that (3) is a successful workaround, I strongly suspect that GHC is confusing the type variable `k` (which gets `ddump-splice`d as `k_avB`) with the kind variable `k` (which gets `ddump-splice`d as `k_avC`) due to their common prefix `k`.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Template Haskell regression: GHC erroneously thinks a type variable is also a kind","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The following program compiles without issue on GHC 7.6.3 through GHC 7.10.3, but fails to compile on GHC 8.0.1 and GHC HEAD. (I added a CPP guard simply because the `DataD` constructor changed between 7.10 and 8.0.)\r\n\r\n{{{#!hs\r\n{-# LANGUAGE CPP #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule Regression where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata T k\r\nclass C a\r\n\r\n$(do TyConI (DataD [] tName [ KindedTV kName kKind]\r\n#if __GLASGOW_HASKELL__ >= 800\r\n _\r\n#endif\r\n _ _) <- reify ''T\r\n d <- instanceD (cxt []) (conT ''C `appT` (conT tName `appT` sigT (varT kName) kKind)) []\r\n return [d])\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghc Regression.hs \r\n[1 of 1] Compiling Regression ( Regression.hs, Regression.o )\r\nRegression.hs:(13,3)-(19,15): Splicing declarations\r\n do { TyConI (DataD []\r\n tName_a2RT\r\n [KindedTV kName_a2RU kKind_a2RV]\r\n _\r\n _\r\n _) <- reify ''T;\r\n d_a31Y <- instanceD\r\n (cxt [])\r\n (conT ''C\r\n `appT` (conT tName_a2RT `appT` sigT (varT kName_a2RU) kKind_a2RV))\r\n [];\r\n return [d_a31Y] }\r\n ======>\r\n instance C (T (k_avB :: k_avC))\r\n\r\nRegression.hs:13:3: error:\r\n Variable ‘k_avB’ used as both a kind and a type\r\n Did you intend to use TypeInType?\r\n}}}\r\n\r\nSomewhat confusingly, you can use `instance C (T (k_avB :: k_avC))` on its own, and it will compile without issue. Also, quoting it doesn't seem to trip up this bug, as this also compiles without issue:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE CPP #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# OPTIONS_GHC -ddump-splices #-}\r\nmodule WorksSomehow where\r\n\r\nimport Language.Haskell.TH\r\n\r\ndata T k\r\nclass C a\r\n\r\n$([d| instance C (T k) |])\r\n}}}\r\n\r\nThe original program has several workarounds:\r\n\r\n1. Turn off `PolyKinds` (OK, this isn't a very good workaround...)\r\n2. Add an explicit kind signature to `T`, e.g., `data T (k :: k1)`\r\n3. Change the type variable of `T` to some other letter, e.g., `data T p` or `data T k1`\r\n\r\nGiven that (3) is a successful workaround, I strongly suspect that GHC is confusing the type variable `k` (which gets `ddump-splice`d as `k_avB`) with the kind variable `k` (which gets `ddump-splice`d as `k_avC`) due to their common prefix `k`.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13879Strange interaction between higher-rank kinds and type synonyms2019-07-07T18:19:41ZRyan ScottStrange interaction between higher-rank kinds and type synonymsHere's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAG...Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
data family Sing (a :: k)
data (a :: j) :~~: (b :: k) where
HRefl :: a :~~: a
data instance Sing (z :: a :~~: b) where
SHRefl :: Sing HRefl
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> p HRefl
-> p r
(%:~~:->) SHRefl pHRefl = pHRefl
type App f x = f x
type HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x
```
Now I want to refactor this so that I use `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> App p HRefl
-> App p r
```
However, GHC doesn't like that:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘(:~~:) j z a a’,
but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’
• In the second argument of ‘App’, namely ‘HRefl’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
21 | -> App p HRefl
| ^^^^^
Bug.hs:22:20: error:
• Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’
• In the second argument of ‘App’, namely ‘r’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> App p HRefl -> App p r
|
22 | -> App p r
| ^
```
These errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.
Out of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:
```hs
(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r
-> HRApp p HRefl
-> HRApp p r
```
But now I get an even stranger error message:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:21:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
21 | -> HRApp p HRefl
| ^
Bug.hs:22:20: error:
• Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,
but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’
• In the first argument of ‘HRApp’, namely ‘p’
In the type signature:
(%:~~:->) :: forall (j :: Type)
(k :: Type)
(a :: j)
(b :: k)
(r :: a :~~: b)
(p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
Sing r -> HRApp p HRefl -> HRApp p r
|
22 | -> HRApp p r
| ^
```
That's right, it can't match the kinds:
- `forall z (y :: z). (:~~:) j z a y -> *`, and
- `forall z (y :: z). (:~~:) j z a y -> *`
Uh... what? Those are the same kind!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Strange interaction between higher-rank kinds and type synonyms","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Here's some code with typechecks with GHC 8.0.1, 8.0.2, 8.2.1, and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata (a :: j) :~~: (b :: k) where\r\n HRefl :: a :~~: a\r\n\r\ndata instance Sing (z :: a :~~: b) where\r\n SHRefl :: Sing HRefl\r\n\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> p HRefl\r\n -> p r\r\n(%:~~:->) SHRefl pHRefl = pHRefl\r\n\r\ntype App f x = f x\r\ntype HRApp (f :: forall (z :: Type) (y :: z). a :~~: y -> Type) (x :: a :~~: b) = f x\r\n}}}\r\n\r\nNow I want to refactor this so that I use `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> App p HRefl\r\n -> App p r\r\n}}}\r\n\r\nHowever, GHC doesn't like that:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘(:~~:) j z a a’,\r\n but ‘'HRefl j a’ has kind ‘(:~~:) j j a a’\r\n • In the second argument of ‘App’, namely ‘HRefl’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n21 | -> App p HRefl\r\n | ^^^^^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘(:~~:) j z a b’, but ‘r’ has kind ‘(:~~:) j k a b’\r\n • In the second argument of ‘App’, namely ‘r’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> App p HRefl -> App p r\r\n |\r\n22 | -> App p r\r\n | ^\r\n}}}\r\n\r\nThese errors are surprising to me, since it appears that the two higher-rank types, `z` and `y`, are behaving differently here: `y` appears to be willing to unify with other types in applications of `p`, but `z` isn't! I would expect //both// to be willing to unify in applications of `p`.\r\n\r\nOut of desperation, I tried this other formulation of `(%:~~:->)` which uses `HRApp` instead of `App`:\r\n\r\n{{{#!hs\r\n(%:~~:->) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r\r\n -> HRApp p HRefl\r\n -> HRApp p r\r\n}}}\r\n\r\nBut now I get an even stranger error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds -fprint-explicit-foralls\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:21:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n21 | -> HRApp p HRefl\r\n | ^\r\n\r\nBug.hs:22:20: error:\r\n • Expected kind ‘forall z (y :: z). (:~~:) j z a y -> *’,\r\n but ‘p’ has kind ‘forall z (y :: z). (:~~:) j z a y -> *’\r\n • In the first argument of ‘HRApp’, namely ‘p’\r\n In the type signature:\r\n (%:~~:->) :: forall (j :: Type)\r\n (k :: Type)\r\n (a :: j)\r\n (b :: k)\r\n (r :: a :~~: b)\r\n (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).\r\n Sing r -> HRApp p HRefl -> HRApp p r\r\n |\r\n22 | -> HRApp p r\r\n | ^\r\n}}}\r\n\r\nThat's right, it can't match the kinds:\r\n\r\n* `forall z (y :: z). (:~~:) j z a y -> *`, and\r\n* `forall z (y :: z). (:~~:) j z a y -> *`\r\n\r\nUh... what? Those are the same kind!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13822GHC not using injectivity?2019-07-07T18:19:56ZIcelandjackGHC not using injectivity?This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds...This may be normal behavior but.. (Example from [System FC with Explicit Kind Equality](http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs))
```hs
{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}
import Data.Kind
data KIND = STAR | KIND :> KIND
data Ty :: KIND -> Type where
TInt :: Ty STAR
TBool :: Ty STAR
TMaybe :: Ty (STAR :> STAR)
TApp :: Ty (a :> b) -> (Ty a -> Ty b)
type family
IK (k :: KIND) = (res :: Type) | res -> k where
IK STAR = Type
IK (a:>b) = IK a -> IK b
type family
I (t :: Ty k) = (res :: IK k) | res -> t where
I TInt = Int
I TBool = Bool
I TMaybe = Maybe
I (TApp f a) = (I f) (I a)
data TyRep (k :: KIND) (t :: Ty k) where
TyInt :: TyRep STAR TInt
TyBool :: TyRep STAR TBool
TyMaybe :: TyRep (STAR:>STAR) TMaybe
TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
zero :: TyRep STAR a -> I a
zero = \case
TyInt -> 0
TyBool -> False
TyApp TyMaybe _ -> Nothing
```
When I ask it to infer the representation for `Int` and `Bool` it does so with no surprises
```hs
-- Inferred type:
--
-- int :: TyRep STAR TInt -> Int
int rep = zero rep :: Int
-- bool:: TyRep STAR TBool -> Bool
bool rep = zero rep :: Bool
```
but inferring the representation for `Maybe Int` fails
```hs
-- v.hs:43:16: error:
-- • Couldn't match kind ‘k’ with ‘'STAR’
-- ‘k’ is a rigid type variable bound by
-- the inferred type of
-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>
-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- at v.hs:25:3
-- When matching the kind of ‘'TMaybe’
-- Expected type: Maybe Int
-- Actual type: I ('TApp 'TMaybe 'TInt)
-- • In the expression: zero rep :: Maybe Int
-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int
-- • Relevant bindings include
-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)
-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int
-- (bound at v.hs:43:1)
-- Failed, modules loaded: none.
maybeInt rep = zero rep :: Maybe Int
```
even though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`
```
>>> :kind! I (TMaybe `TApp` TInt)
I (TMaybe `TApp` TInt) :: IK 'STAR
= Maybe Int
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC not using injectivity?","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["InjectiveFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This may be normal behavior but.. (Example from [http://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1014&context=compsci_pubs System FC with Explicit Kind Equality])\r\n\r\n{{{#!hs\r\n{-# LANGUAGE GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilyDependencies, TypeInType, RankNTypes, LambdaCase, EmptyCase #-}\r\n\r\nimport Data.Kind\r\n\r\ndata KIND = STAR | KIND :> KIND\r\n\r\ndata Ty :: KIND -> Type where\r\n TInt :: Ty STAR\r\n TBool :: Ty STAR\r\n TMaybe :: Ty (STAR :> STAR)\r\n TApp :: Ty (a :> b) -> (Ty a -> Ty b)\r\n\r\ntype family\r\n IK (k :: KIND) = (res :: Type) | res -> k where\r\n IK STAR = Type\r\n IK (a:>b) = IK a -> IK b\r\n\r\ntype family\r\n I (t :: Ty k) = (res :: IK k) | res -> t where\r\n I TInt = Int\r\n I TBool = Bool\r\n I TMaybe = Maybe\r\n I (TApp f a) = (I f) (I a)\r\n\r\ndata TyRep (k :: KIND) (t :: Ty k) where\r\n TyInt :: TyRep STAR TInt\r\n TyBool :: TyRep STAR TBool\r\n TyMaybe :: TyRep (STAR:>STAR) TMaybe\r\n TyApp :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)\r\n\r\nzero :: TyRep STAR a -> I a\r\nzero = \\case\r\n TyInt -> 0\r\n TyBool -> False\r\n TyApp TyMaybe _ -> Nothing\r\n}}}\r\n\r\nWhen I ask it to infer the representation for `Int` and `Bool` it does so with no surprises\r\n\r\n{{{#!hs\r\n-- Inferred type: \r\n-- \r\n-- int :: TyRep STAR TInt -> Int\r\nint rep = zero rep :: Int\r\n\r\n\r\n-- bool:: TyRep STAR TBool -> Bool\r\nbool rep = zero rep :: Bool\r\n}}}\r\n\r\nbut inferring the representation for `Maybe Int` fails\r\n\r\n{{{#!hs\r\n-- v.hs:43:16: error:\r\n-- • Couldn't match kind ‘k’ with ‘'STAR’\r\n-- ‘k’ is a rigid type variable bound by\r\n-- the inferred type of\r\n-- maybeInt :: (I 'TInt ~ Int, I 'TMaybe ~ Maybe) =>\r\n-- TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- at v.hs:25:3\r\n-- When matching the kind of ‘'TMaybe’\r\n-- Expected type: Maybe Int\r\n-- Actual type: I ('TApp 'TMaybe 'TInt)\r\n-- • In the expression: zero rep :: Maybe Int\r\n-- In an equation for ‘maybeInt’: maybeInt rep = zero rep :: Maybe Int\r\n-- • Relevant bindings include\r\n-- rep :: TyRep 'STAR ('TApp 'TMaybe 'TInt) (bound at v.hs:43:10)\r\n-- maybeInt :: TyRep 'STAR ('TApp 'TMaybe 'TInt) -> Maybe Int\r\n-- (bound at v.hs:43:1)\r\n-- Failed, modules loaded: none.\r\nmaybeInt rep = zero rep :: Maybe Int\r\n}}}\r\n\r\neven though `I` is injective and GHC knows that `I (TMaybe `TApp` TMaybe) = Maybe Int`\r\n\r\n{{{\r\n>>> :kind! I (TMaybe `TApp` TInt)\r\nI (TMaybe `TApp` TInt) :: IK 'STAR\r\n= Maybe Int\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13762TypeInType is not documented in the users' guide flag reference2019-07-07T18:20:12ZRyan ScottTypeInType is not documented in the users' guide flag referenceAt least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value...At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Documentation |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"TypeInType is not documented in the users' guide flag reference","status":"New","operating_system":"","component":"Documentation","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"At least, not as of http://git.haskell.org/ghc.git/blob/09d5c993aae208e3d34a9e715297922b6ea42b3f:/utils/mkUserGuidePart/Options/Language.hs. We should fix this.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13625GHC internal error: ‘Y’ is not in scope during type checking, but it passed t...2019-07-07T18:20:53ZMatthew PickeringGHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r...```
{-# LANGUAGE TypeInType #-}
data X :: Y where Y :: X
```
The error message is:
```
Bug.hs:2:11: error: …
• GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer
tcl_env of environment: [r1cR :-> APromotionErr TyConPE]
• In the kind ‘Y’
```
Originally reported by \@mietek in #11821
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | mietek |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["mietek"],"type":"Bug","description":"{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata X :: Y where Y :: X\r\n}}}\r\n\r\nThe error message is:\r\n\r\n{{{\r\nBug.hs:2:11: error: …\r\n • GHC internal error: ‘Y’ is not in scope during type checking, but it passed the renamer\r\n tcl_env of environment: [r1cR :-> APromotionErr TyConPE]\r\n • In the kind ‘Y’\r\n}}}\r\n\r\nOriginally reported by @mietek in #11821","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13603Can't resolve levity polymorphic superclass2019-07-07T18:21:04ZIcelandjackCan't resolve levity polymorphic superclassThis works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the...This works
```hs
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> b)
```
but the moment you add (`b :: TYPE rep`) to the last line it stops working
```hs
-- t3I7.hs:9:10-40: error: …
-- • Could not deduce (A b)
-- arising from the superclasses of an instance declaration
-- from the context: B b
-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40
-- • In the instance declaration for ‘B (a -> b)’
-- Compilation failed.
{-# Language PolyKinds, TypeInType #-}
import GHC.Exts (TYPE, RuntimeRep)
class A (a :: TYPE rep)
class A a => B (a :: TYPE rep)
instance A b => A (a -> (b :: TYPE rep))
instance B b => B (a -> (b :: TYPE rep))
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't resolve levity polymorphic superclass","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["LevityPolymorphism,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This works\r\n\r\n{{{#!hs\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> b)\r\n}}}\r\n\r\nbut the moment you add (`b :: TYPE rep`) to the last line it stops working\r\n\r\n\r\n{{{#!hs\r\n-- t3I7.hs:9:10-40: error: …\r\n-- • Could not deduce (A b)\r\n-- arising from the superclasses of an instance declaration\r\n-- from the context: B b\r\n-- bound by the instance declaration at /tmp/t3I7.hs:9:10-40\r\n-- • In the instance declaration for ‘B (a -> b)’\r\n-- Compilation failed.\r\n\r\n{-# Language PolyKinds, TypeInType #-}\r\n\r\nimport GHC.Exts (TYPE, RuntimeRep)\r\n\r\nclass A (a :: TYPE rep)\r\nclass A a => B (a :: TYPE rep)\r\n\r\ninstance A b => A (a -> (b :: TYPE rep))\r\ninstance B b => B (a -> (b :: TYPE rep))\r\n}}}\r\n\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/13337GHC doesn't think a type is of kind *, despite having evidence for it2019-07-07T18:22:23ZRyan ScottGHC doesn't think a type is of kind *, despite having evidence for itThe easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
b...The easiest way to illustrate this bug is this:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where
import Data.Kind (Type)
blah :: forall (a :: k). k ~ Type => a -> a
blah x = x
```
```
$ 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 Foo ( Foo.hs, interpreted )
Foo.hs:8:43: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the type signature:
blah :: forall (a :: k). k ~ Type => a -> a
```
I find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!
If the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:
```hs
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Foo where
import Data.Kind (Type)
import Data.Typeable
foo :: forall k (a :: k) proxy. (Typeable k, Typeable a)
=> proxy a -> String
foo _ =
case eqT :: Maybe (k :~: Type) of
Nothing -> "Non-Type kind"
Just Refl ->
case eqT :: Maybe (a :~: Int) of
Nothing -> "Non-Int type"
Just Refl -> "It's an Int!"
```
This exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!
<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 | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC doesn't think a type is of kind *, despite having evidence for it","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"The easiest way to illustrate this bug is this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\n\r\nblah :: forall (a :: k). k ~ Type => a -> a\r\nblah x = x\r\n}}}\r\n\r\n{{{\r\n$ 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 Foo ( Foo.hs, interpreted )\r\n\r\nFoo.hs:8:43: error:\r\n • Expected a type, but ‘a’ has kind ‘k’\r\n • In the type signature:\r\n blah :: forall (a :: k). k ~ Type => a -> a\r\n}}}\r\n\r\nI find this behavior quite surprising, especially since we have evidence that `k ~ Type` in scope!\r\n\r\nIf the program above looks too contrived, consider a similar program that uses `Typeable`. I want to write something like this:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Foo where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Typeable\r\n\r\nfoo :: forall k (a :: k) proxy. (Typeable k, Typeable a)\r\n => proxy a -> String\r\nfoo _ =\r\n case eqT :: Maybe (k :~: Type) of\r\n Nothing -> \"Non-Type kind\"\r\n Just Refl ->\r\n case eqT :: Maybe (a :~: Int) of\r\n Nothing -> \"Non-Int type\"\r\n Just Refl -> \"It's an Int!\"\r\n}}}\r\n\r\nThis exhibits the same problem. Despite the fact that we pattern-matched on a `Refl` of type `k :~: Type`, GHC refuses to consider the possibility that `a :~: Int` is well kinded, even though `(a :: k)`, and we learned from the first `Refl` that `k ~ Type`!","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11966Surprising behavior with higher-rank quantification of kind variables2019-07-07T18:28:13ZOllie CharlesSurprising behavior with higher-rank quantification of kind variablesSorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANG...Sorry about the rubbish title. I wrote the following code, which type checks:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Test where
import Data.Kind (Type)
-- Simplification
type family Col (f :: k -> j) (x :: k) :: Type
-- Base types
data PGBaseType = PGInteger | PGText
-- Transformations
data Column t = Column Symbol t
newtype Nullable t = Nullable t
newtype HasDefault t = HasDefault t
-- Interpretations
data Expr k
data Record (f :: forall k. k -> Type) =
Record {rX :: Col f ('Column "x" 'PGInteger)
,rY :: Col f ('Column "y" ('Nullable 'PGInteger))
,rZ :: Col f ('HasDefault 'PGText)}
```
However, if I play with this in GHCI, I can get the following error:
```
λ> let x = undefined :: Record Expr
<interactive>:136:29-32: error:
• Expected kind ‘forall k. k -> Type’,
but ‘Expr’ has kind ‘forall k. k -> *’
• In the first argument of ‘Record’, namely ‘Expr’
In an expression type signature: Record Expr
In the expression: undefined :: Record Expr
```
It seems that if I write
```hs
data Expr :: forall k. k -> Type
```
things work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc3 |
| 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":"Surprising behavior with higher-rank quantification of kind variables","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1-rc3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Sorry about the rubbish title. I wrote the following code, which type checks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE DataKinds #-}\r\n{-# LANGUAGE KindSignatures #-}\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n\r\nmodule Test where\r\n\r\nimport Data.Kind (Type)\r\n\r\n-- Simplification\r\ntype family Col (f :: k -> j) (x :: k) :: Type\r\n\r\n-- Base types\r\ndata PGBaseType = PGInteger | PGText\r\n\r\n-- Transformations\r\ndata Column t = Column Symbol t\r\nnewtype Nullable t = Nullable t\r\nnewtype HasDefault t = HasDefault t\r\n\r\n-- Interpretations\r\ndata Expr k\r\n\r\ndata Record (f :: forall k. k -> Type) =\r\n Record {rX :: Col f ('Column \"x\" 'PGInteger)\r\n ,rY :: Col f ('Column \"y\" ('Nullable 'PGInteger))\r\n ,rZ :: Col f ('HasDefault 'PGText)}\r\n\r\n}}}\r\n\r\nHowever, if I play with this in GHCI, I can get the following error:\r\n\r\n{{{\r\nλ> let x = undefined :: Record Expr\r\n\r\n<interactive>:136:29-32: error:\r\n • Expected kind ‘forall k. k -> Type’,\r\n but ‘Expr’ has kind ‘forall k. k -> *’\r\n • In the first argument of ‘Record’, namely ‘Expr’\r\n In an expression type signature: Record Expr\r\n In the expression: undefined :: Record Expr\r\n}}}\r\n\r\nIt seems that if I write\r\n\r\n{{{#!hs\r\ndata Expr :: forall k. k -> Type\r\n}}}\r\n\r\nthings work, but I'm unclear if/why that is necessary, and the error message certainly needs to be fixed.","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/11592Self-kinded type variable accepted2019-07-07T18:29:41ZSimon Peyton JonesSelf-kinded type variable acceptedFound when chasing #11407
```
data T (a::a) = Blah -- Accepted
data S (b :: a) a = ...
-- Rejected with: variable ‘a’ used as a kind variable before being bound
-- as a type variable. Perhaps reorder your variables?
...Found when chasing #11407
```
data T (a::a) = Blah -- Accepted
data S (b :: a) a = ...
-- Rejected with: variable ‘a’ used as a kind variable before being bound
-- as a type variable. Perhaps reorder your variables?
```
But `T` should be rejected too, for the same reason as `S`
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 7.10.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Self-kinded type varialbe accepted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.10.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Found when chasing #11407\r\n{{{\r\ndata T (a::a) = Blah -- Accepted\r\n\r\ndata S (b :: a) a = ...\r\n -- Rejected with: variable ‘a’ used as a kind variable before being bound\r\n -- as a type variable. Perhaps reorder your variables?\r\n}}}\r\nBut `T` should be rejected too, for the same reason as `S`","type_of_failure":"OtherFailure","blocking":[]} -->8.2.1johnleojohnleohttps://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/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/11995Can't infer type2019-07-07T18:28:05ZIcelandjackCan't infer type```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → N...```hs
{-# LANGUAGE RankNTypes, LambdaCase, TypeOperators,
TypeInType, UnicodeSyntax, GADTs #-}
module T11995 where
import Data.Kind
data NP :: forall k. (ĸ → Type) → ([k] → Type) where
Nil :: NP f '[]
(:*) :: f x → NP f xs → NP f (x:xs)
newtype K a b = K a deriving Show
unK (K a) = a
h'collapse :: NP (K a) xs -> [a]
h'collapse = \case
Nil -> []
K x:*xs -> x : h'collapse xs
```
if we replace `xs` by an underscore:
```
tJN0.hs:13:29-30: error: …
• Could not deduce: (xs :: [ĸ]) ~~ ((':) ĸ x xs :: [ĸ])
from the context: ((k :: *) ~~ (ĸ :: *),
(t :: [k]) ~~ ((':) ĸ x xs :: [ĸ]))
bound by a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3-9
‘xs’ is a rigid type variable bound by
a pattern with constructor:
:* :: forall k (f :: k -> *) (x :: k) (xs :: [k]).
f x -> NP k k f xs -> NP k k f ((':) k x xs),
in a case alternative
at /tmp/tJN0.hs:13:3
Expected type: NP ĸ k (K ĸ a) t
Actual type: NP ĸ ĸ (K ĸ a) xs
• In the first argument of ‘h'collapse’, namely ‘xs’
In the second argument of ‘(:)’, namely ‘h'collapse xs’
In the expression: x : h'collapse xs
• Relevant bindings include
xs :: NP ĸ ĸ (K ĸ a) xs (bound at /tmp/tJN0.hs:13:8)
h'collapse :: NP ĸ k (K ĸ a) t -> [a] (bound at /tmp/tJN0.hs:11:1)
Compilation failed.
```
Should it not be able to infer that?
The Glorious Glasgow Haskell Compilation System, version 8.1.201604198.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/11400* is not an indexed type family2019-07-07T18:30:35ZRyan Scott* is not an indexed type familyI can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help
λ>...I can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:
```
$ /opt/ghc/head/bin/ghci
GHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help
λ> :set -XTypeInType -XTypeFamilies
λ> import Data.Kind
λ> data family IdxProxy k (a :: k)
λ> data instance IdxProxy * a
<interactive>:5:1: error:
• Illegal family instance for ‘*’
(* is not an indexed type family)
• In the data instance declaration for ‘*’
λ> data instance IdxProxy Type a
λ> :kind! IdxProxy *
IdxProxy * :: * -> *
= IdxProxy *
λ> :kind! IdxProxy Type
IdxProxy Type :: Type -> *
= IdxProxy Type
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.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":"* is not an indexed type family","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"I can't seem to create an indexed data family using the kind `*` with `-XTypeInType` enabled. I have to work around it by using `Type`:\r\n\r\n{{{\r\n$ /opt/ghc/head/bin/ghci\r\nGHCi, version 8.1.20160108: http://www.haskell.org/ghc/ :? for help\r\nλ> :set -XTypeInType -XTypeFamilies \r\nλ> import Data.Kind\r\nλ> data family IdxProxy k (a :: k)\r\nλ> data instance IdxProxy * a\r\n\r\n<interactive>:5:1: error:\r\n • Illegal family instance for ‘*’\r\n (* is not an indexed type family)\r\n • In the data instance declaration for ‘*’\r\nλ> data instance IdxProxy Type a\r\nλ> :kind! IdxProxy *\r\nIdxProxy * :: * -> *\r\n= IdxProxy *\r\nλ> :kind! IdxProxy Type\r\nIdxProxy Type :: Type -> *\r\n= IdxProxy Type\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.2.2https://gitlab.haskell.org/ghc/ghc/-/issues/12919Equality not used for substitution2019-07-07T18:24:38ZVladislav ZavialovEquality not used for substitutionThis code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
module T12919 where
import Data.Kind
data N = Z
data V :: N -> Type where
VZ :: V Z
type family VC (n :: N) :: Type where
VC Z = Type
type famil...This code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
module T12919 where
import Data.Kind
data N = Z
data V :: N -> Type where
VZ :: V Z
type family VC (n :: N) :: Type where
VC Z = Type
type family VF (xs :: V n) (f :: VC n) :: Type where
VF VZ f = f
data Dict c where
Dict :: c => Dict c
prop :: xs ~ VZ => Dict (VF xs f ~ f)
prop = Dict
```
fails with this error:
```
T12919.hs:22:8: error:
• Couldn't match type ‘f’ with ‘VF 'VZ f’
arising from a use of ‘Dict’
‘f’ is a rigid type variable bound by
the type signature for:
prop :: forall (xs :: V 'Z) f. xs ~ 'VZ => Dict VF xs f ~ f
at T12919.hs:21:9
• In the expression: Dict
In an equation for ‘prop’: prop = Dict
• Relevant bindings include
prop :: Dict VF xs f ~ f (bound at T12919.hs:22:1)
```
However, if I substitute `xs` with `VZ` (by hand) in the type of `prop`, it compiles. Can be reproduced with GHC 8.0.1 but not HEAD.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14720GHC 8.4.1-alpha regression with TypeInType2019-07-07T18:15:53ZRyan ScottGHC 8.4.1-alpha regression with TypeInTypeGHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Ty...GHC 8.2.2 is able to typecheck this code:
```hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module SGenerics where
import Data.Kind (Type)
import Data.Type.Equality ((:~:)(..), sym, trans)
import Data.Void
data family Sing (z :: k)
class Generic (a :: Type) where
type Rep a :: Type
from :: a -> Rep a
to :: Rep a -> a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: Rep a
type PTo (x :: Rep a) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
class (PGeneric k, SGeneric k) => VGeneric k where
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a
data Decision a = Proved a
| Disproved (a -> Void)
class SDecide k where
(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))
=> Sing a -> Sing b -> Decision (a :~: b)
s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
Proved (Refl :: PFrom a :~: PFrom b) ->
case (sTof s1, sTof s2) of
(Refl, Refl) -> Proved Refl
Disproved contra -> Disproved (\Refl -> contra Refl)
```
But GHC 8.4.1-alpha2 cannot:
```
$ /opt/ghc/8.4.1/bin/ghc Bug.hs
[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )
Bug.hs:44:52: error:
• Could not deduce: PFrom a ~ PFrom a
from the context: b ~ a
bound by a pattern with constructor:
Refl :: forall k (a :: k). a :~: a,
in a lambda abstraction
at Bug.hs:44:37-40
Expected type: PFrom a :~: PFrom b
Actual type: PFrom a :~: PFrom a
NB: ‘PFrom’ is a non-injective type family
• In the first argument of ‘contra’, namely ‘Refl’
In the expression: contra Refl
In the first argument of ‘Disproved’, namely
‘(\ Refl -> contra Refl)’
• Relevant bindings include
contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)
s2 :: Sing b (bound at Bug.hs:40:9)
s1 :: Sing a (bound at Bug.hs:40:3)
(%~) :: Sing a -> Sing b -> Decision (a :~: b)
(bound at Bug.hs:40:3)
|
44 | Disproved contra -> Disproved (\Refl -> contra Refl)
| ^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.4.1-alpha1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.4.1-alpha regression with TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.1-alpha1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC 8.2.2 is able to typecheck this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE AllowAmbiguousTypes #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule SGenerics where\r\n\r\nimport Data.Kind (Type)\r\nimport Data.Type.Equality ((:~:)(..), sym, trans)\r\nimport Data.Void\r\n\r\ndata family Sing (z :: k)\r\n\r\nclass Generic (a :: Type) where\r\n type Rep a :: Type\r\n from :: a -> Rep a\r\n to :: Rep a -> a\r\n\r\nclass PGeneric (a :: Type) where\r\n type PFrom (x :: a) :: Rep a\r\n type PTo (x :: Rep a) :: a\r\n\r\nclass SGeneric k where\r\n sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)\r\n sTo :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)\r\n\r\nclass (PGeneric k, SGeneric k) => VGeneric k where\r\n sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a\r\n sFot :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a\r\n\r\ndata Decision a = Proved a\r\n | Disproved (a -> Void)\r\n\r\nclass SDecide k where\r\n (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)\r\n default (%~) :: forall (a :: k) (b :: k). (VGeneric k, SDecide (Rep k))\r\n => Sing a -> Sing b -> Decision (a :~: b)\r\n s1 %~ s2 = case sFrom s1 %~ sFrom s2 of\r\n Proved (Refl :: PFrom a :~: PFrom b) ->\r\n case (sTof s1, sTof s2) of\r\n (Refl, Refl) -> Proved Refl\r\n Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n}}}\r\n\r\nBut GHC 8.4.1-alpha2 cannot:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling SGenerics ( Bug.hs, Bug.o )\r\n\r\nBug.hs:44:52: error:\r\n • Could not deduce: PFrom a ~ PFrom a\r\n from the context: b ~ a\r\n bound by a pattern with constructor:\r\n Refl :: forall k (a :: k). a :~: a,\r\n in a lambda abstraction\r\n at Bug.hs:44:37-40\r\n Expected type: PFrom a :~: PFrom b\r\n Actual type: PFrom a :~: PFrom a\r\n NB: ‘PFrom’ is a non-injective type family\r\n • In the first argument of ‘contra’, namely ‘Refl’\r\n In the expression: contra Refl\r\n In the first argument of ‘Disproved’, namely\r\n ‘(\\ Refl -> contra Refl)’\r\n • Relevant bindings include\r\n contra :: (PFrom a :~: PFrom b) -> Void (bound at Bug.hs:44:15)\r\n s2 :: Sing b (bound at Bug.hs:40:9)\r\n s1 :: Sing a (bound at Bug.hs:40:3)\r\n (%~) :: Sing a -> Sing b -> Decision (a :~: b)\r\n (bound at Bug.hs:40:3)\r\n |\r\n44 | Disproved contra -> Disproved (\\Refl -> contra Refl)\r\n | ^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14450GHCi spins forever2019-07-07T18:16:59ZIcelandjackGHCi spins foreverThe following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import ...The following code compiles just fine (8.3.20170920)
```hs
{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
type Cat ob = ob -> ob -> Type
type SameKind (a :: k) (b :: k) = (() :: Constraint)
type family
Apply (f :: a ~> b) (x :: a) :: b where
Apply IddSym0 x = Idd x
class Varpi (f :: i ~> j) where
type Dom (f :: i ~> j) :: Cat i
type Cod (f :: i ~> j) :: Cat j
varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')
type family
Idd (a::k) :: k where
Idd (a::k) = a
data IddSym0 :: k ~> k where
IddSym0KindInference :: IddSym0 l
instance Varpi (IddSym0 :: Type ~> Type) where
type Dom (IddSym0 :: Type ~> Type) = (->)
type Cod (IddSym0 :: Type ~> Type) = (->)
varpa :: (a -> a') -> (a -> a')
varpa = id
```
But if you change the final instance to
```hs
instance Varpi (IddSym0 :: k ~> k) where
type Dom (IddSym0 :: Type ~> Type) = (->)
```
it sends GHC for a spin.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.2.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHCi spins forever","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["PolyKinds","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following code compiles just fine (8.3.20170920)\r\n\r\n{{{#!hs\r\n{-# Language KindSignatures, TypeOperators, PolyKinds, TypeOperators, ConstraintKinds, TypeFamilies, DataKinds, TypeInType, GADTs, AllowAmbiguousTypes, InstanceSigs #-}\r\n\r\nimport Data.Kind\r\n\r\ndata TyFun :: Type -> Type -> Type\r\n\r\ntype a ~> b = TyFun a b -> Type\r\n\r\ntype Cat ob = ob -> ob -> Type\r\n\r\ntype SameKind (a :: k) (b :: k) = (() :: Constraint)\r\n\r\ntype family \r\n Apply (f :: a ~> b) (x :: a) :: b where\r\n Apply IddSym0 x = Idd x\r\n\r\nclass Varpi (f :: i ~> j) where\r\n type Dom (f :: i ~> j) :: Cat i\r\n type Cod (f :: i ~> j) :: Cat j\r\n\r\n varpa :: Dom f a a' -> Cod f (Apply f a) (Apply f a')\r\n\r\ntype family \r\n Idd (a::k) :: k where\r\n Idd (a::k) = a\r\n\r\ndata IddSym0 :: k ~> k where\r\n IddSym0KindInference :: IddSym0 l\r\n\r\ninstance Varpi (IddSym0 :: Type ~> Type) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n type Cod (IddSym0 :: Type ~> Type) = (->)\r\n\r\n varpa :: (a -> a') -> (a -> a')\r\n varpa = id\r\n}}}\r\n\r\nBut if you change the final instance to\r\n\r\n{{{#!hs\r\ninstance Varpi (IddSym0 :: k ~> k) where\r\n type Dom (IddSym0 :: Type ~> Type) = (->)\r\n}}}\r\n\r\nit sends GHC for a spin.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/14441GHC HEAD regression involving type families in kinds2019-07-07T18:17:02ZRyan ScottGHC HEAD regression involving type families in kindsIn GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k)...In GHC 8.2.1, this file typechecks:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
data Prox (a :: k) = P
type instance Demote (Prox (a :: k)) = Prox (DemoteX a)
$(return [])
type instance DemoteX P = P
```
(Note that the `$(return [])` line is essential, as it works around #13790.)
However, on GHC HEAD, this now fails:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:15:27: error:
• Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’
• In the type ‘P’
In the type instance declaration for ‘DemoteX’
|
15 | type instance DemoteX P = P
| ^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression involving type families in kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"In GHC 8.2.1, this file typechecks:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\ndata Prox (a :: k) = P\r\n\r\ntype instance Demote (Prox (a :: k)) = Prox (DemoteX a)\r\n$(return [])\r\ntype instance DemoteX P = P\r\n}}}\r\n\r\n(Note that the `$(return [])` line is essential, as it works around #13790.)\r\n\r\nHowever, on GHC HEAD, this now fails:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:15:27: error:\r\n • Expected kind ‘Demote (Prox a0)’, but ‘P’ has kind ‘Prox a1’\r\n • In the type ‘P’\r\n In the type instance declaration for ‘DemoteX’\r\n |\r\n15 | type instance DemoteX P = P\r\n | ^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/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/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.1