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/13549GHC 8.2.1's typechecker rejects code generated by singletons that 8.0 accepts2019-07-07T18:21:23ZRyan ScottGHC 8.2.1's typechecker rejects code generated by singletons that 8.0 acceptsI recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but...I recently attempted to upgrade `singletons` to use GHC 8.2.1, but was thwarted when GHC's typechecker rejected code that was generated by Template Haskell. I was able to put all of this code in a single module (which I've attached), but sadly, it's 1367 lines long. What's important is that GHC 8.0.1 and 8.0.2 accept this code, but neither 8.2.1-rc1 nor HEAD do. Here is the error message you get, in its full glory:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs -fprint-explicit-kinds
GHCi, version 8.2.0.20170403: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:1328:59: error:
• Couldn't match type ‘c69895866216793215480’ with ‘[a_a337f]’
‘c69895866216793215480’ is untouchable
inside the constraints: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
Bug.hs:1328:59: error:
• Could not deduce: (Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
~~
(Let6989586621679736980Interleave'
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
t
t1
t2 :: ([a_a337f], [c69895866216793215480]))
from the context: t_a33gX ~ xs0_a33a0
bound by the type signature for:
lambda_a33gY :: forall (xs0_a33a0 :: [a_a337f]).
t_a33gX ~ xs0_a33a0 =>
Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply
[a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
at Bug.hs:(1122,11)-(1126,67)
or from: arg_a33h0 ~ (':) a_a337f n_a1kQc n_a1kQd
bound by a pattern with constructor:
SCons :: forall a_11 (z_a1kQb :: [a_11]) (n_a1kQc :: a_11) (n_a1kQd :: [a_11]).
z_a1kQb ~ (':) a_11 n_a1kQc n_a1kQd =>
Sing a_11 n_a1kQc -> Sing [a_11] n_a1kQd -> Sing [a_11] z_a1kQb,
in an equation for ‘sPerms’
at Bug.hs:1143:25-36
or from: (arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f (TyFun [a_a337f] [a_a337f] -> *) ((:$) a_a337f) t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO)
bound by the type signature for:
lambda_a33ha :: forall (t_a33aL :: a_a337f) (ts_a33aM :: [a_a337f]) (is_a33aO :: [a_a337f]).
(arg_a33h0
~
Apply
[a_a337f]
[a_a337f]
(Apply
a_a337f
(TyFun [a_a337f] [a_a337f] -> *)
((:$) a_a337f)
t_a33aL)
ts_a33aM,
arg_a33h1 ~ is_a33aO) =>
Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
at Bug.hs:(1145,23)-(1152,117)
or from: (arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq)
bound by the type signature for:
lambda_a33iH :: forall (xs_a33fp :: [a_a337f]) (r_a33fq :: [[a_a337f]]).
(arg_a33hh ~ xs_a33fp, arg_a33hi ~ r_a33fq) =>
Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
at Bug.hs:(1289,35)-(1294,157)
Expected type: Sing (TyFun [a_a337f] [a_a337f] -> *) t
-> Sing [a_a337f] t1
-> Sing [[a_a337f]] t2
-> Sing
([a_a337f], [[a_a337f]])
((@@)
[[a_a337f]]
([a_a337f], [[a_a337f]])
((@@)
[a_a337f]
([[a_a337f]] ~> ([a_a337f], [[a_a337f]]))
((@@)
(TyFun [a_a337f] [a_a337f] -> *)
([a_a337f] ~> ([[a_a337f]] ~> ([a_a337f], [[a_a337f]])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
[a_a337f]
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
Actual type: Sing (TyFun [a_a337f] c69895866216793215480 -> *) t
-> Sing [a_a337f] t1
-> Sing [c69895866216793215480] t2
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
t)
t1)
t2)
The type variable ‘c69895866216793215480’ is ambiguous
• In the second argument of ‘singFun3’, namely ‘sInterleave'’
In the first argument of ‘applySing’, namely
‘((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave')’
In the first argument of ‘applySing’, namely
‘((applySing
((singFun3
(Proxy ::
Proxy (Let6989586621679736980Interleave'Sym4 xs0_a33a0 t_a33aL ts_a33aM is_a33aO)))
sInterleave'))
((singFun1 (Proxy :: Proxy IdSym0)) sId))’
• Relevant bindings include
sX_6989586621679737266 :: Sing
([a_a337f], [[a_a337f]])
(Let6989586621679737265X_6989586621679737266Sym6
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO
xs_a33fp
r_a33fq)
(bound at Bug.hs:1321:41)
r_a33iK :: Sing [[a_a337f]] r_a33fq (bound at Bug.hs:1295:57)
xs_a33iJ :: Sing [a_a337f] xs_a33fp (bound at Bug.hs:1295:48)
lambda_a33iH :: Sing [a_a337f] xs_a33fp
-> Sing [[a_a337f]] r_a33fq
-> Sing
[[a_a337f]]
(Apply
[[a_a337f]]
[[a_a337f]]
(Apply
[a_a337f]
(TyFun [[a_a337f]] [[a_a337f]] -> *)
(Let6989586621679736980InterleaveSym4
[a_a337f]
[a_a337f]
a_a337f
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33hh)
arg_a33hi)
(bound at Bug.hs:1295:35)
sR :: Sing [[a_a337f]] arg_a33hi (bound at Bug.hs:1287:45)
sXs :: Sing [a_a337f] arg_a33hh (bound at Bug.hs:1287:41)
sInterleave' :: forall (arg_a33he :: TyFun
[a_a337f] c69895866216793215480
-> *) (arg_a33hf :: [a_a337f]) (arg_a33hg :: [c69895866216793215480]).
Sing (TyFun [a_a337f] c69895866216793215480 -> *) arg_a33he
-> Sing [a_a337f] arg_a33hf
-> Sing [c69895866216793215480] arg_a33hg
-> Sing
([a_a337f], [c69895866216793215480])
(Apply
[c69895866216793215480]
([a_a337f], [c69895866216793215480])
(Apply
[a_a337f]
([c69895866216793215480] ~> ([a_a337f], [c69895866216793215480]))
(Apply
(TyFun [a_a337f] c69895866216793215480 -> *)
([a_a337f]
~> ([c69895866216793215480]
~> ([a_a337f], [c69895866216793215480])))
(Let6989586621679736980Interleave'Sym4
[a_a337f]
[a_a337f]
a_a337f
c69895866216793215480
xs0_a33a0
t_a33aL
ts_a33aM
is_a33aO)
arg_a33he)
arg_a33hf)
arg_a33hg)
(bound at Bug.hs:1166:29)
lambda_a33ha :: Sing a_a337f t_a33aL
-> Sing [a_a337f] ts_a33aM
-> Sing [a_a337f] is_a33aO
-> Sing
[[a_a337f]]
(Apply
[a_a337f]
[[a_a337f]]
(Apply
[a_a337f]
([a_a337f] ~> [[a_a337f]])
(Let6989586621679736931PermsSym1 a_a337f xs0_a33a0)
arg_a33h0)
arg_a33h1)
(bound at Bug.hs:1153:23)
sTs :: Sing [a_a337f] n_a1kQd (bound at Bug.hs:1143:34)
sT :: Sing a_a337f n_a1kQc (bound at Bug.hs:1143:31)
lambda_a33gY :: Sing [a_a337f] xs0_a33a0
-> Sing
[[a_a337f]]
(Apply [a_a337f] [[a_a337f]] (PermutationsSym0 a_a337f) t_a33gX)
(bound at Bug.hs:1127:11)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
|
1328 | sInterleave'))
| ^^^^^^^^^^^^
```8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13546Kind error with type equality2019-07-07T18:21:24ZVladislav ZavialovKind error with type equalityThis code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T ...This code
```hs
{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}
import Data.Kind
data Dict c where
Dict :: c => Dict c
data T (t :: k)
type family UnT (a :: Type) :: k where
UnT (T t) = t
untt :: Dict (UnT (T "a") ~ "a")
untt = Dict
tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict
```
fails with this error:
```
tunt.hs:17:8: error:
• Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
‘k’ is a rigid type variable bound by
the type signature for:
tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
at tunt.hs:16:1-38
When matching types
UnT (T "a") :: k
"a" :: GHC.Types.Symbol
• In the expression: Dict
In an equation for ‘tunt’: tunt = Dict
• Relevant bindings include
tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)
|
17 | tunt = Dict
|
```
Instead I would expect these reductions to take place:
```
1. T (UnT (T "a")) ~ T "a"
2. T "a" ~ T "a"
3. constraint satisfied (refl)
```
<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 | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kind error with type equality","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":["goldfire"],"type":"Bug","description":"This code\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}\r\n\r\nimport Data.Kind\r\n\r\ndata Dict c where\r\n Dict :: c => Dict c\r\n\r\ndata T (t :: k)\r\n\r\ntype family UnT (a :: Type) :: k where\r\n UnT (T t) = t\r\n\r\nuntt :: Dict (UnT (T \"a\") ~ \"a\")\r\nuntt = Dict\r\n\r\ntunt :: Dict (T (UnT (T \"a\")) ~ T \"a\")\r\ntunt = Dict\r\n}}}\r\n\r\nfails with this error:\r\n\r\n{{{\r\ntunt.hs:17:8: error:\r\n • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’\r\n ‘k’ is a rigid type variable bound by\r\n the type signature for:\r\n tunt :: forall k. Dict T (UnT (T \"a\")) ~ T \"a\"\r\n at tunt.hs:16:1-38\r\n When matching types\r\n UnT (T \"a\") :: k\r\n \"a\" :: GHC.Types.Symbol\r\n • In the expression: Dict\r\n In an equation for ‘tunt’: tunt = Dict\r\n • Relevant bindings include\r\n tunt :: Dict T (UnT (T \"a\")) ~ T \"a\" (bound at tunt.hs:17:1)\r\n |\r\n17 | tunt = Dict\r\n | \r\n}}}\r\n\r\nInstead I would expect these reductions to take place:\r\n\r\n{{{\r\n 1. T (UnT (T \"a\")) ~ T \"a\"\r\n 2. T \"a\" ~ T \"a\"\r\n 3. constraint satisfied (refl)\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13530Horrible error message due to TypeInType2019-07-07T18:21:28ZSimon Peyton JonesHorrible error message due to TypeInTypeConsider this
```
{-# LANGUAGE MagicHash, UnboxedTuples #-}
module Foo where
import GHC.Exts
g :: Int -> (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int -> (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: err...Consider this
```
{-# LANGUAGE MagicHash, UnboxedTuples #-}
module Foo where
import GHC.Exts
g :: Int -> (# Int#, a #)
g (I# y) = (# y, undefined #)
f :: Int -> (# Int#, Int# #)
f x = g x
```
With GHC 8 we get
```
Foo.hs:11:7: error:
• Couldn't match a lifted type with an unlifted type
Expected type: (# Int#, Int# #)
Actual type: (# Int#, Int# #)
```
What a terrible error message!! It was much better in GHC 7.10:
```
Foo.hs:11:7:
Couldn't match kind ‘*’ with ‘#’
When matching types
a0 :: *
Int# :: #
Expected type: (# Int#, Int# #)
Actual type: (# Int#, a0 #)
```
What's going on?
The constraint solver sees
```
[W] alpha::TYPE LiftedRep ~ Int#::TYPE IntRep
```
So it homogenises the kinds, *and unifies alpha* (this did not happen in GHC 7.10), thus
```
alpha := Int# |> TYPE co
[W] co :: LiftedRep ~ IntRep
```
Of course the new constraint fails. But since we have unified alpha, when we print out the types are are unifying they both look like `(# Int#, Int# #)` (there's a suppressed cast in the second component).
I'm not sure what to do here.
(I tripped over this when debugging #13509.)https://gitlab.haskell.org/ghc/ghc/-/issues/13409Data types with higher-rank kinds are pretty-printed strangely2019-07-07T18:22:00ZRyan ScottData types with higher-rank kinds are pretty-printed strangelyFirst observed in #13399\##13409. If you define this:
```hs
data Foo :: (* -> *) -> (forall k. k -> *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
```...First observed in #13399\##13409. If you define this:
```hs
data Foo :: (* -> *) -> (forall k. k -> *)
```
and type `:i Foo` into GHCi, you get this back:
```
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
```
This seems to imply that Foo has three visible type parameters, which isn't true at all!
<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 | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Data types with higher-rank kinds are pretty-printed strangely","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"First observed in https://ghc.haskell.org/trac/ghc/ticket/13399#comment:5. If you define this:\r\n\r\n{{{#!hs\r\ndata Foo :: (* -> *) -> (forall k. k -> *)\r\n}}}\r\n\r\nand type `:i Foo` into GHCi, you get this back:\r\n\r\n{{{\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * -> *) k (c :: k)\r\n}}}\r\n\r\nThis seems to imply that Foo has three visible type parameters, which isn't true at all!","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13408Consider inferring a higher-rank kind for type synonyms2020-09-25T17:22:29ZRichard Eisenbergrae@richarde.devConsider inferring a higher-rank kind for type synonymsIn terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:
```hs
f :: (forall a. a -> a -> a) -> Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fa...In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:
```hs
f :: (forall a. a -> a -> a) -> Int
f z = z 0 1
g = f
```
`g` gets an inferred type equal to `f`'s. However, this fails at the type level:
```hs
type F (z :: forall a. a -> a -> a) = z 0 1
type G = F
```
If anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non-recursive equation.
This ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.
This is spun off from #13399, but is not tightly coupled to that ticket.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | -------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Consider inferring a higher-rank kind for type synonyms","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"In terms, a definition comprising one non-recursive equation may have a higher-rank type inferred. For example:\r\n\r\n{{{#!hs\r\nf :: (forall a. a -> a -> a) -> Int\r\nf z = z 0 1\r\n\r\ng = f\r\n}}}\r\n\r\n`g` gets an inferred type equal to `f`'s. However, this fails at the type level:\r\n\r\n{{{#!hs\r\ntype F (z :: forall a. a -> a -> a) = z 0 1\r\n\r\ntype G = F\r\n}}}\r\n\r\nIf anything is strange here, it's that the term-level definition is accepted. GHC should not be in the business of inferring higher-rank types. But there is an exception for definitions comprising one non-recursive equation.\r\n\r\nThis ticket proposes expanding this behavior to the type level, allowing `G` to be accepted.\r\n\r\nThis is spun off from #13399, but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13407Fix printing of higher-rank kinds2019-07-07T18:22:01ZRichard Eisenbergrae@richarde.devFix printing of higher-rank kindsWitness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeInType -XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: ...Witness this GHCi session:
```
rae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTypeInType -XRankNTypes
Prelude> import Data.Kind
Prelude Data.Kind> data Foo :: (* -> *) -> (forall k. k -> *)
Prelude Data.Kind> :info Foo
type role Foo phantom nominal phantom
data Foo (a :: * -> *) k (c :: k)
-- Defined at <interactive>:3:1
```
The output from `:info` is terrible, treating `k` as a visible parameter when it isn't.
This is spun off from #13399 but is not tightly coupled to that ticket.
<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":"Fix printing of higher-rank kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"Witness this GHCi session:\r\n\r\n{{{\r\nrae:09:18:37 ~/ghc/ghc> ghci -ignore-dot-ghci\r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XTypeInType -XRankNTypes\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data Foo :: (* -> *) -> (forall k. k -> *)\r\nPrelude Data.Kind> :info Foo\r\ntype role Foo phantom nominal phantom\r\ndata Foo (a :: * -> *) k (c :: k)\r\n \t-- Defined at <interactive>:3:1\r\n}}}\r\n\r\nThe output from `:info` is terrible, treating `k` as a visible parameter when it isn't.\r\n\r\nThis is spun off from #13399 but is not tightly coupled to that ticket.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13399Location of `forall` matters with higher-rank kind polymorphism2020-05-21T22:48:30ZEric CrockettLocation of `forall` matters with higher-rank kind polymorphismThe following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- erro...The following code fails to compile, but probably should:
```hs
{-# LANGUAGE RankNTypes, TypeInType #-}
import Data.Kind
data Foo :: forall k . (* -> *) -> k -> * -- Decl 1
class C (a :: forall k . k -> *)
instance C (Foo a) -- error on this line
```
with the error
```
• Expected kind ‘forall k. k -> *’, but ‘Foo a’ has kind ‘k0 -> *’
• In the first argument of ‘C’, namely ‘Foo a’
In the instance declaration for ‘C (Foo a)’
```
Similarly, the following declarations of `Foo` also cause a similar error at the instance declaration:
Decl 2: `data Foo :: (* -> *) -> k -> *`
Decl 3: `data Foo (a :: * -> *) (b :: k)`
However, if I move the `forall` to a point *after* the first type parameter (which is where the instance is partially applied) thusly:
Decl 4: `data Foo :: (* -> *) -> forall k . k -> *`
then GHC happily accepts the instance of `C`.
From my (admittedly negligible) knowledge of type theory, the signatures for Decls 1 and 4 (and 2) are identical, since the `forall` can be floated to the front of Decl 4. GHC should accept any of the four versions of `Foo`, since they are all equivalent.8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13391PolyKinds is more permissive in GHC 82019-07-07T18:22:06ZEric CrockettPolyKinds is more permissive in GHC 8The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
``...The docs claim that the definition in section 9.11.10
```
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
"requires that `-XTypeInType` be in effect", but this isn't the case.
The following compiles with GHC-8.0.2:
```
{-# LANGUAGE PolyKinds, GADTs #-}
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
```
The example does \*not\* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"PolyKinds is more permissive in GHC 8","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The docs claim that the definition in section 9.11.10\r\n\r\n{{{\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\n\"requires that `-XTypeInType` be in effect\", but this isn't the case.\r\n\r\nThe following compiles with GHC-8.0.2:\r\n\r\n{{{\r\n\r\n{-# LANGUAGE PolyKinds, GADTs #-}\r\n\r\ndata G (a :: k) where\r\n GInt :: G Int\r\n GMaybe :: G Maybe\r\n}}}\r\n\r\nThe example does *not* compile with 7.10.3, so this seems to be a case where `-XPolyKinds` has become more permissive in GHC 8 (as outlined in section 9.11.1). ","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/13364Remove checkValidTelescope2019-07-07T18:22:16ZRichard Eisenbergrae@richarde.devRemove checkValidTelescopeAll of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b ...All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have
```
data SameKind :: k -> k -> Type
```
and then here are three subtly ill-scoped kinds:
```
forall a (b :: a) (c :: Proxy d). SameKind b d
forall a. forall (b :: a). forall (c :: Proxy d). SameKind b d
forall d. forall a (b :: a). SameKind b d
```
Despite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.
While I am unaware of a concrete bug this all causes, it's a mess.
Better would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for *every* new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)
It might all just work! And then we can delete gobs of hairy code. Hooray!
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Remove checkValidTelescope","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"All of this new `TypeInType` nonsense has provided a number of ways that we can arrive at ill-scoped kinds. Let's assume we have\r\n\r\n{{{\r\ndata SameKind :: k -> k -> Type\r\n}}}\r\n\r\nand then here are three subtly ill-scoped kinds:\r\n\r\n{{{\r\nforall a (b :: a) (c :: Proxy d). SameKind b d\r\nforall a. forall (b :: a). forall (c :: Proxy d). SameKind b d\r\nforall d. forall a (b :: a). SameKind b d\r\n}}}\r\n\r\nDespite the close similarity between these cases, they are all handled separately. See `Note [Bad telescopes]` in !TcValidity for an overview, but these are spread between `tcImplicitTKBndrsX`, `tcExplicitTKBndrsX`, and those functions' calls to `checkValidTelescope`, `checkZonkValidTelescope`, and `checkValidInferredKinds`.\r\n\r\nWhile I am unaware of a concrete bug this all causes, it's a mess.\r\n\r\nBetter would be to use the existing machinery to prevent skolem-escape: `TcLevel`s and implication constraints. Specifically, it's quite plausible that all this can be avoided by a simple rule: bump the `TcLevel` (and create an implication constraint) for ''every'' new type variable brought into scope (including implicitly). (Actually, implicit variables have an implicit ordering that GHC is free to decide, so all implicitly bound variables should be brought into scope at once, with just one bump in the `TcLevel`.)\r\n\r\nIt might all just work! And then we can delete gobs of hairy code. Hooray!","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/13333Typeable regression in GHC HEAD2019-07-07T18:22:24ZRyan ScottTypeable regression in GHC HEADI recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGU...I recently wrote some code while exploring a fix for #13327 that heavily uses poly-kinded `Typeable`. This compiles without issue on GHC 8.0.1 and 8.0.2:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module DataCast where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k -> Constraint) (x :: j) where
D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
-> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
```
But on GHC HEAD, it barfs this error:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.1.20170223: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling DataCast ( Bug.hs, interpreted )
Bug.hs:28:29: error:
• Could not deduce (Typeable T) arising from a use of ‘gcast1’
GHC can't yet do polykinded Typeable (T :: * -> *)
from the context: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom)
bound by the type signature for:
dataCast1T :: (Typeable k, Typeable t, Typeable phantom,
Possibly Data phantom) =>
(forall d. Data d => c (t d)) -> Maybe (c (T phantom))
at Bug.hs:(22,1)-(25,35)
or from: (k ~ *, (phantom :: k) ~~ (x :: *), Data x)
bound by a pattern with constructor:
D :: forall k (p :: k -> Constraint) (x :: k). p x => D p x,
in a case alternative
at Bug.hs:28:23
• In the expression: gcast1 f
In a case alternative: Just D -> gcast1 f
In the expression:
case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
|
28 | Just D -> gcast1 f
| ^^^^^^^^
```
That error message itself is hilariously strange, since GHC certainly has the power to do polykinded `Typeable` nowadays.
Marking as high priority since this is a regression—feel free to lower the priority if you disagree.8.2.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12938Polykinded associated type family rejected on false pretenses2019-07-07T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to...If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<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":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12933Wrong class instance selection with Data.Kind.Type2022-08-04T22:32:56ZjulmWrong class instance selection with Data.Kind.TypeIf you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: S...If you consider the following code:
```hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
import GHC.Exts (Constraint)
import Data.Kind
-- | Partial singleton for a kind type.
data SKind k where
SKiTy :: SKind Type
SKiCo :: SKind Constraint
instance Show (SKind k) where
show SKiTy = "*"
show SKiCo = "Constraint"
class IKind k where
kind :: SKind k
instance IKind Constraint where
kind = SKiCo
```
Then, the main below will compile even though there is no (IKind Type) instance, and it will print "Constraint" two times,
instead of an expected "Constraint" then "\*":
```hs
main :: IO ()
main = do
print (kind::SKind Constraint)
print (kind::SKind Type)
```
And, the main below will print "\*" two times,
instead of an expected "\*" then "Constraint":
```hs
instance IKind Type where
kind = SKiTy
main :: IO ()
main = do
print (kind::SKind Type)
print (kind::SKind Constraint)
```
This can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.
Sorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Wrong class instance selection with Data.Kind.Type","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If you consider the following code:\r\n{{{#!hs\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE FlexibleInstances #-}\r\nmodule Bug where\r\n\r\nimport GHC.Exts (Constraint)\r\nimport Data.Kind\r\n\r\n-- | Partial singleton for a kind type.\r\ndata SKind k where\r\n SKiTy :: SKind Type\r\n SKiCo :: SKind Constraint\r\n\r\ninstance Show (SKind k) where\r\n show SKiTy = \"*\"\r\n show SKiCo = \"Constraint\"\r\n\r\nclass IKind k where\r\n kind :: SKind k\r\ninstance IKind Constraint where\r\n kind = SKiCo\r\n}}}\r\n\r\nThen, the main below will compile even though there is no (IKind Type) instance, and it will print \"Constraint\" two times,\r\ninstead of an expected \"Constraint\" then \"*\":\r\n{{{#!hs\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Constraint)\r\n print (kind::SKind Type)\r\n}}}\r\n\r\nAnd, the main below will print \"*\" two times,\r\ninstead of an expected \"*\" then \"Constraint\":\r\n{{{#!hs\r\ninstance IKind Type where\r\n kind = SKiTy\r\n\r\nmain :: IO ()\r\nmain = do\r\n print (kind::SKind Type)\r\n print (kind::SKind Constraint)\r\n}}}\r\n\r\nThis can be worked around by replacing Type with a new data type Ty to select the right class instances, using two type families Ty_of_Type and Type_of_Ty, as done in the attached Workaround.hs.\r\n\r\nSorry if this bug has already been fixed in HEAD: I was unable to find neither a bug report similar, nor a Linux x86_64 build of HEAD for me to test.","type_of_failure":"OtherFailure","blocking":[]} -->https://gitlab.haskell.org/ghc/ghc/-/issues/12931tc_infer_args does not set in-scope set correctly2023-07-16T13:20:59Zjohnleotc_infer_args does not set in-scope set correctlyAs noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnche...As noted in #12785\##12931, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line
```
kind = substTyUnchecked subst (tyVarKind tv)
```
This is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.
Note that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.
<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":"tc_infer_args does not set in-scope set correctly","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"As noted in https://ghc.haskell.org/trac/ghc/ticket/12785#comment:6, `TcHsType.tc_infer_args` does not set its in-scope set correctly, which means the call to `TcMType.new_meta_tv_x` will fail if `substTyUnchecked` is replaced by `substTy` in the line\r\n{{{\r\nkind = substTyUnchecked subst (tyVarKind tv)\r\n}}}\r\n\r\nThis is the only known caller of `new_meta_tv_x` to not set the in-scope set, now that #12549 has been fixed. Once this bug is fixed, change `substTyUnchecked` back to `substTy` in the line noted above.\r\n\r\nNote that other calls to `substTyUnchecked` that need to be converted to `substTy` are covered in the general ticket #11371.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12922Kind classes compile with PolyKinds2019-07-07T18:24:37ZMatthías Páll GissurarsonKind classes compile with PolyKindsI was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeO...I was asking around on \#haskell to better understand the new language extension, -XTypeInType, and how it is different from -XPolyKinds.
To study it, I was working with the following small example:
```
{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds #-}
module Main where
-- Define a Type for the natural numbers, zero and a successor
data Nat = Z | S Nat
class Addable k where
type (a :: k) + (b :: k) :: k
instance Addable Nat where
type (Z + a) = a
type (S a) + b = S (a + b)
main :: IO ()
main = putStrLn "Shouldn't this need TypeInType?"
```
(for more context, see https://gist.github.com/Tritlo/ce5510e80935ac398a33934ee47c7930)
Since according to a responder on \#haskell, the ability to have kind classes required TypeInType, and should not work with PolyKinds.
As the documentation mentions that there could be leakage between PolyKinds and TypeInType and to report such leaks, I felt that I should report it.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/12766Allow runtime-representation polymorphic data families2019-07-07T18:25:14ZIcelandjackAllow runtime-representation polymorphic data familiesThis is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```This is an offshoot of #12369 (‘data families shouldn't be required to have return kind \*, data instances should’), allowing family declarations something like:
```hs
data family Array a :: TYPE rep
```8.10.1https://gitlab.haskell.org/ghc/ghc/-/issues/12742Instantiation of invisible type family arguments is too eager2019-07-07T18:25:20ZRichard Eisenbergrae@richarde.devInstantiation of invisible type family arguments is too eagerThis module looks, to me, like it should be accepted:
```
{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
module Bug where
import Data.Kind
type family F :: forall k2. (k1, k2)
data T :: (forall k2. (Bool, k2)) -> Type
type S...This module looks, to me, like it should be accepted:
```
{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}
module Bug where
import Data.Kind
type family F :: forall k2. (k1, k2)
data T :: (forall k2. (Bool, k2)) -> Type
type S = T F
```
But it's not. The problem is that `TcHsType.handle_tyfams` eagerly instantiates *all* invisible arguments to a type family at every occurrence. Instead, it should instantiate only those that are counted in the TF's arity -- that is, those "before the colon".
Will fix.
<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":"Instantiation of invisible type family arguments is too eager","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This module looks, to me, like it should be accepted:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType, RankNTypes, TypeFamilies #-}\r\n\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family F :: forall k2. (k1, k2)\r\n\r\ndata T :: (forall k2. (Bool, k2)) -> Type\r\n\r\ntype S = T F\r\n}}}\r\n\r\nBut it's not. The problem is that `TcHsType.handle_tyfams` eagerly instantiates ''all'' invisible arguments to a type family at every occurrence. Instead, it should instantiate only those that are counted in the TF's arity -- that is, those \"before the colon\".\r\n\r\nWill fix.","type_of_failure":"OtherFailure","blocking":[]} -->Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12612Allow kinds of associated types to depend on earlier associated types2023-12-22T08:53:22ZdavemenendezAllow kinds of associated types to depend on earlier associated typesGHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t -> Type
m :: t -> T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used...GHC rejects the following code:
```hs
class C t where
type K t :: Type
type T t :: K t -> Type
m :: t -> T t a
```
with this error message
```
• Type constructor ‘K’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘K t -> Type’
```
See [e-mail discussion](https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-September/026402.html). This is connected to #12088, at least as far as defining instances of C.
<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":"Allow kinds of associated types to depend on earlier associated types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC rejects the following code:\r\n\r\n{{{#!hs\r\nclass C t where\r\n type K t :: Type\r\n type T t :: K t -> Type\r\n\r\n m :: t -> T t a\r\n}}}\r\n\r\nwith this error message\r\n\r\n{{{\r\n • Type constructor ‘K’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘K t -> Type’\r\n}}}\r\n\r\nSee [https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-September/026402.html e-mail discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} -->