GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:19:06Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13972GHC 8.2 error message around indexes for associated type instances is baffling2019-07-07T18:19:06ZRyan ScottGHC 8.2 error message around indexes for associated type instances is bafflingThis program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instan...This program doesn't typecheck (only in GHC 8.2 and later):
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C Left where
type T (a -> Either a b) = Int
```
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:12:8: error:
• Type indexes must match class instance head
Expected: T (a -> Either a b)
Actual: T (a -> Either a b)
• In the type instance declaration for ‘T’
In the instance declaration for ‘C Left’
|
12 | type T (a -> Either a b) = Int
| ^^^^^^^^^^^^^^^^^^^^^^^^^
```
Well those expected and actual types look pretty darn similar to me!
Note that the problem can be worked around by giving an explicit kind annotation for `Left`:
```hs
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class C (a :: k) where
type T k :: Type
instance C (Left :: a -> Either a b) where
type T (a -> Either a b) = Int
```
I see two things we could do here:
1. Relax the "Type indexes must match class instance head" check so that it doesn't apply to invisible kind variables like `a` and `b`.
1. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.2 error message around indexes for associated type instances is baffling","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeFamilies,","TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program doesn't typecheck (only in GHC 8.2 and later):\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C Left where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:12:8: error:\r\n • Type indexes must match class instance head\r\n Expected: T (a -> Either a b)\r\n Actual: T (a -> Either a b)\r\n • In the type instance declaration for ‘T’\r\n In the instance declaration for ‘C Left’\r\n |\r\n12 | type T (a -> Either a b) = Int\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}\r\n\r\nWell those expected and actual types look pretty darn similar to me!\r\n\r\nNote that the problem can be worked around by giving an explicit kind annotation for `Left`:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE PolyKinds #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass C (a :: k) where\r\n type T k :: Type\r\n\r\ninstance C (Left :: a -> Either a b) where\r\n type T (a -> Either a b) = Int\r\n}}}\r\n\r\nI see two things we could do here:\r\n\r\n1. Relax the \"Type indexes must match class instance head\" check so that it doesn't apply to invisible kind variables like `a` and `b`.\r\n2. Clarify the error message. At the very least, we could say `Expected: T (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type variables as `a1` and `b1`. In an ideal world, we'd even indicate where `a1` and `b1` should be coming from (the kind of `Left`).","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13909Misleading error message when partially applying a data type with a visible q...2019-07-07T18:19:32ZRyan ScottMisleading error message when partially applying a data type with a visible quantifier in its kindI'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) ...I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:
```hs
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
data Hm (k :: Type) (a :: k) :: Type
class HasName (a :: k) where
getName :: proxy a -> String
instance HasName Hm where
getName _ = "Hm"
```
This is rejected, however:
```
$ /opt/ghc/8.2.1/bin/ghci Bug.hs
GHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/ryanglscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:11:18: error:
• Expecting two more arguments to ‘Hm’
Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’
• In the first argument of ‘HasName’, namely ‘Hm’
In the instance declaration for ‘HasName Hm’
|
11 | instance HasName Hm where
| ^^
```
The culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Can't partially apply a data type with a visible quantifier in its kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I'm not sure if this is a bug or an intended design, so I'll ask here. I want this program to typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata Hm (k :: Type) (a :: k) :: Type\r\n\r\nclass HasName (a :: k) where\r\n getName :: proxy a -> String\r\n\r\ninstance HasName Hm where\r\n getName _ = \"Hm\"\r\n}}}\r\n\r\nThis is rejected, however:\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Bug.hs\r\nGHCi, version 8.2.0.20170623: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/ryanglscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:11:18: error:\r\n • Expecting two more arguments to ‘Hm’\r\n Expected kind ‘k0’, but ‘Hm’ has kind ‘forall k -> k -> *’\r\n • In the first argument of ‘HasName’, namely ‘Hm’\r\n In the instance declaration for ‘HasName Hm’\r\n |\r\n11 | instance HasName Hm where\r\n | ^^\r\n}}}\r\n\r\nThe culprit appears to be the fact that `Hm` has kind `forall k -> k -> *`, which uses a visible quantifier. Does this prevent partial applications of `Hm`? Or is this simply a GHC bug?","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/13781(a :: (k :: Type)) is too exotic for Template Haskell2019-07-07T18:20:06ZRyan Scott(a :: (k :: Type)) is too exotic for Template HaskellOn GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```...On GHC 8.0.1 or later, GHC will choke on this code:
```hs
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
import Data.Proxy
$([d| f :: Proxy (a :: (k :: Type))
f = Proxy
|])
```
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:8:3: error:
Exotic form of kind not (yet) handled by Template Haskell
(k :: Type)
|
8 | $([d| f :: Proxy (a :: (k :: Type))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
I don't think this would be too hard to support, though. I'll take a shot at fixing this.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"(a :: (k :: Type)) is too exotic for Template Haskell","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"On GHC 8.0.1 or later, GHC will choke on this code:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TemplateHaskell #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\n\r\n$([d| f :: Proxy (a :: (k :: Type))\r\n f = Proxy\r\n |])\r\n}}}\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Bug.hs, interpreted )\r\n\r\nBug.hs:8:3: error:\r\n Exotic form of kind not (yet) handled by Template Haskell\r\n (k :: Type)\r\n |\r\n8 | $([d| f :: Proxy (a :: (k :: Type))\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n}}}\r\n\r\nI don't think this would be too hard to support, though. I'll take a shot at fixing this.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Ryan ScottRyan Scotthttps://gitlab.haskell.org/ghc/ghc/-/issues/13780Nightmarish pretty-printing of equality type in GHC 8.2 error message2019-07-07T18:20:06ZRyan ScottNightmarish pretty-printing of equality type in GHC 8.2 error messageI originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuanti...I originally spotted this in #12102\##13780, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:
```hs
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Foo where
data family Sing (a :: k)
data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
```
In GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:
```
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
```
But in GHC 8.2.1 and HEAD, it's hair-raisingly bad:
```
GHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( Bug.hs, interpreted )
Bug.hs:9:40: error:
• Expected kind ‘Foo a’,
but ‘'MkFoo
('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’
• In the second argument of ‘~’, namely ‘MkFoo’
In the definition of data constructor ‘SMkFoo’
In the data instance declaration for ‘Sing’
|
9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
| ^^^^^
```
- \*WAT.\*\*
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.2.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Nightmarish pretty-printing of equality type in GHC 8.2 error message","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1-rc2","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I originally spotted this in https://ghc.haskell.org/trac/ghc/ticket/12102#comment:1, but I happened to stumble upon it again recently in a separate context, so I though it deserved its own ticket. Here's some code which does not typecheck:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ExistentialQuantification #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Foo where\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata Foo a = a ~ Bool => MkFoo\r\ndata instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n}}}\r\n\r\nIn GHC 8.0.1 and 8.0.2, the error message you'd get from this program was reasonable enough:\r\n\r\n{{{\r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’, but ‘'MkFoo’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n}}}\r\n\r\nBut in GHC 8.2.1 and HEAD, it's hair-raisingly bad:\r\n\r\n{{{\r\nGHCi, version 8.2.0.20170522: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Foo ( Bug.hs, interpreted )\r\n\r\nBug.hs:9:40: error:\r\n • Expected kind ‘Foo a’,\r\n but ‘'MkFoo\r\n ('Data.Type.Equality.C:~ ('GHC.Types.Eq# <>))’ has kind ‘Foo Bool’\r\n • In the second argument of ‘~’, namely ‘MkFoo’\r\n In the definition of data constructor ‘SMkFoo’\r\n In the data instance declaration for ‘Sing’\r\n |\r\n9 | data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo\r\n | ^^^^^\r\n}}}\r\n\r\n**WAT.**","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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/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/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/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/12369data families shouldn't be required to have return kind *, data instances should2021-09-09T23:17:59ZEdward Kmettdata families shouldn't be required to have return kind *, data instances shouldI'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1...I'd like to be able to define
```hs
{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}
data family Fix :: (k -> *) -> k
newtype instance Fix f = In { out :: f (Fix f) }
```
But currently this is disallowed:
```
Fix.hs:2:1: error:
• Kind signature on data type declaration has non-* return kind
(k -> *) -> k
• In the data family declaration for ‘Fix’
```
Ultimately I think the issue here is that data __instances__ should be required to end in kind \*, not the families, but this generalization didn't mean anything until we had `PolyKinds`.
As an example of a usecase, with the above, I could define a bifunctor fixed point such as
```hs
newtype instance Fix f a = In2 { out2 :: f (Fix f a) a }
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1 |
| Type | FeatureRequest |
| 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 families shouldn't be required to have return kind *, data instances should","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"I'd like to be able to define\r\n\r\n{{{#!hs\r\n{-# language PolyKinds, KindSignatures, GADTs, TypeFamilies #-}\r\ndata family Fix :: (k -> *) -> k\r\nnewtype instance Fix f = In { out :: f (Fix f) }\r\n}}}\r\n\r\nBut currently this is disallowed:\r\n\r\n{{{\r\nFix.hs:2:1: error:\r\n • Kind signature on data type declaration has non-* return kind\r\n (k -> *) -> k\r\n • In the data family declaration for ‘Fix’\r\n}}}\r\n\r\nUltimately I think the issue here is that data __instances__ should be required to end in kind *, not the families, but this generalization didn't mean anything until we had `PolyKinds`.\r\n\r\nAs an example of a usecase, with the above, I could define a bifunctor fixed point such as\r\n\r\n{{{#!hs\r\nnewtype instance Fix f a = In2 { out2 :: f (Fix f a) a }\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/12176Failure of bidirectional type inference at the kind level2019-07-07T18:27:19ZRichard Eisenbergrae@richarde.devFailure of bidirectional type inference at the kind levelI'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k...I'm feeling particularly sadistic towards GHC at the moment, and so I fed it this:
```hs
import Data.Kind
data Proxy :: forall k. k -> Type where
MkProxy :: forall k (a :: k). Proxy a
data X where
MkX :: forall (k :: Type) (a :: k). Proxy a -> X
type Expr = (MkX :: forall (a :: Bool). Proxy a -> X)
type family Foo (x :: forall (a :: k). Proxy a -> X) where
Foo (MkX :: forall (a :: k). Proxy a -> X) = (MkProxy :: Proxy k)
```
Incredibly, GHC accepts it! And it even means what I wish it to, with GHCi telling me the following (with `-fprint-explicit-kinds`):
```
λ> :i Foo
type family Foo k (x :: forall (a :: k). Proxy k a -> X)
:: Proxy * k
where [k] Foo k ('MkX k) = 'MkProxy * k
```
That is, I wished to extract the kind parameter to `MkK`, matching against a partially-applied `MkX`, and GHC understood that intention.
However, sadly, writing `Foo Expr` produces
```
• Expected kind ‘forall (a :: k0). Proxy k0 a -> X’,
but ‘Expr a0’ has kind ‘Proxy Bool a0 -> X’
• In the first argument of ‘Foo’, namely ‘Expr’
In the type ‘Foo Expr’
In the type family declaration for ‘XXX’
```
For some reason, `Expr` is getting instantiated when it shouldn't be.
Perhaps there's a simpler test case demonstrating the bug, but I feel so gleeful that this chicanery is accepted at all that I wanted to post.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11963GHC introduces kind equality without TypeInType2019-07-07T18:28:14ZEdward Z. YangGHC introduces kind equality without TypeInTypeThe following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a ...The following program is accepted by GHC 8.0 rc2
```
{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
data Typ k t where
Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t
```
This probably shouldn't be accepted, because this is a circuitous way of saying:
```
{-# LANGUAGE TypeInType #-}
data Typ k (t :: k) = Typ
```
which does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?
Printing with explicit kinds makes it clear why the obvious check didn't fire:
```
ezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds
GHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
Ok, modules loaded: Main.
*Main> :info Typ
type role Typ nominal nominal nominal
data Typ k k1 (t :: k) where
Typ :: forall k (t :: k).
(forall (a :: k -> *). a t -> a t) -> Typ k k t
-- Defined at B.hs:2:1
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.0.1-rc2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC introduces kind equality without TypeInType","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1-rc2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program is accepted by GHC 8.0 rc2\r\n\r\n{{{\r\n{-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}\r\ndata Typ k t where\r\n Typ :: (forall (a :: k -> *). a t -> a t) -> Typ k t\r\n}}}\r\n\r\nThis probably shouldn't be accepted, because this is a circuitous way of saying:\r\n\r\n{{{\r\n{-# LANGUAGE TypeInType #-}\r\ndata Typ k (t :: k) = Typ\r\n}}}\r\n\r\nwhich does not work without `TypeInType`. Or perhaps both should be accepted without `TypeInType`?\r\n\r\nPrinting with explicit kinds makes it clear why the obvious check didn't fire:\r\n\r\n{{{\r\nezyang@sabre:~$ ghc-8.0 --interactive B.hs -fprint-explicit-kinds\r\nGHCi, version 8.0.0.20160204: http://www.haskell.org/ghc/ :? for help\r\n[1 of 1] Compiling Main ( B.hs, interpreted )\r\nOk, modules loaded: Main.\r\n*Main> :info Typ\r\ntype role Typ nominal nominal nominal\r\ndata Typ k k1 (t :: k) where\r\n Typ :: forall k (t :: k).\r\n (forall (a :: k -> *). a t -> a t) -> Typ k k t\r\n \t-- Defined at B.hs:2:1\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1johnleojohnleohttps://gitlab.haskell.org/ghc/ghc/-/issues/11785Merge types and kinds in Template Haskell2019-07-07T18:28:33ZRichard Eisenbergrae@richarde.devMerge types and kinds in Template Haskell!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---...!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ---------------- |
| Version | 8.1 |
| Type | Task |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Template Haskell |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Kinds should be treated like types in TcSplice","status":"New","operating_system":"","component":"Template Haskell","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"!TcSplice handles kinds differently than types. Now that they are the same, it's probably best to rewrite this code.","type_of_failure":"OtherFailure","blocking":[]} -->8.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/11196TypeInType performance regressions2021-03-31T16:11:18ZRichard Eisenbergrae@richarde.devTypeInType performance regressionsThis ticket is to track the handful of performance regressions seen with the addition of `TypeInType`. It is quite possibly a good idea to break these out into separate tickets, but until we investigate, they're all bundled here.
The re...This ticket is to track the handful of performance regressions seen with the addition of `TypeInType`. It is quite possibly a good idea to break these out into separate tickets, but until we investigate, they're all bundled here.
The regressions are (all in bytes allocated, unless otherwise noted):
- T3064, up by 14.9%
- T5030, up by 61.8%
- T5837, up by 13%
- T5321Fun, up by 11%
- T5631, up by 39%
- T9872d, **down** by 22% (see below)
- T9872a, up by 33.6%
- T9872c, up by 59.4%
- T9872b, up by 49.4%
- T9675, up by 29.7%, and peak megabytes allocated up by 28.4%
- haddock.base, up by 12.4%
- haddock.Cabal, up by 9.5%
I did add an optimization around type family reduction (the function `zonk_eq_types` in !TcCanonical) that could cause such a drastic reduction.8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14846Renamer hangs (because of -XInstanceSigs?)2019-07-07T18:15:20ZIcelandjackRenamer hangs (because of -XInstanceSigs?)```hs
{-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
type Cat ob = ob -> ob...```hs
{-# Language RankNTypes, TypeInType, EmptyCase, GADTs, FlexibleInstances, ConstraintKinds, UndecidableInstances, AllowAmbiguousTypes, InstanceSigs, ScopedTypeVariables #-}
import Data.Kind
import Data.Proxy
type Cat ob = ob -> ob -> Type
data Struct :: (k -> Constraint) -> Type where
S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
data AStruct :: Struct cls -> Type where
AStruct :: cls a => AStruct (Structured a cls)
class StructI (structured::Struct (cls :: k -> Constraint)) where
struct :: AStruct structured
instance (Structured xx cls ~ structured, cls xx) => StructI structured where
struct :: AStruct (Structured xx cls)
struct = AStruct
data Hom :: Cat k -> Cat (Struct cls) where
class Category (cat::Cat ob) where
i :: StructI a => ríki a a
instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
-- Commenting out this instance signature makes the issue go away
i :: forall a. StructI a => Hom ríki a a
i = case struct :: AStruct (Structured a cls) of
```
Running on 8.2.1 and 8.5.20180105 both loop until interrupted
```
$ ghci -ignore-dot-ghci 199.hs
GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 199.hs, interpreted )
^CInterrupted.
>
>
```8.4.2Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15664Core Lint error2019-07-07T18:03:32ZIcelandjackCore Lint errorFrom [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
import Data.K...From [Generic Programming of All Kinds](https://dl.acm.org/citation.cfm?id=3242745),
```hs
{-# Language RankNTypes, TypeOperators, DataKinds, PolyKinds, GADTs, TypeInType, TypeFamilies #-}
{-# Options_GHC -dcore-lint #-}
import Data.Kind
import GHC.Exts
import Data.Function
data Ctx :: Type -> Type where
E :: Ctx(Type)
(:&:) :: a -> Ctx(as) -> Ctx(a -> as)
type family
Apply(kind) (f :: kind) (ctx :: Ctx kind) :: Type where
Apply(Type) a E = a
Apply(k -> ks) f (a:&:as) = Apply(ks) (f a) as
data ApplyT kind :: kind -> Ctx(kind) -> Type where
A0 :: a
-> ApplyT(Type) a E
AS :: ApplyT(ks) (f a) as
-> ApplyT(k -> ks) f (a:&:as)
type f ~> g = (forall xx. f xx -> g xx)
unravel :: ApplyT(k) f ~> Apply(k) f
unravel (A0 a) = a
unravel (AS fa) = unravel fa
```
gives a core lint error
```
$ ghci -ignore-dot-ghci hs/443.hs > /tmp/bug.log
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15583Treating Constraint as Type when using (type C = Constraint)2019-07-07T18:04:02ZIcelandjackTreating Constraint as Type when using (type C = Constraint)This may be similar/same as #15412? I can't get to the latest GHC right now. Again the "culprit" is using `type C = Constraint`.
The code example should not compile, but the error it gives is unexpected. If we define the associated type...This may be similar/same as #15412? I can't get to the latest GHC right now. Again the "culprit" is using `type C = Constraint`.
The code example should not compile, but the error it gives is unexpected. If we define the associated type family `Ob_ (cat :: Cat ob) :: ob -> C` using `C`
```hs
{-# Language KindSignatures, PolyKinds, DataKinds, TypeInType, TypeFamilies, FlexibleInstances #-}
import Data.Kind
type T = Type
type C = Constraint
type Cat ob = ob -> ob -> T
class Category_ (cat :: Cat ob) where
type Ob_ (cat :: Cat ob) :: ob -> C
id_ :: Ob_ cat a => cat a a
class NoCls (a::k)
instance NoCls (a::k)
instance Category_ (->) where
type Ob_ (->) = NoCls
-- id_ :: NoCls a => (a -> a) -XInstanceSigs
id_ = ()
```
the definition of `id_` fails (as we expect), but the expected type (`Ob_ (->) a -> a -> a`) is wrong:
```
$ ghci -ignore-dot-ghci 348.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( 348.hs, interpreted )
348.hs:22:9: error:
• Couldn't match expected type ‘Ob_ (->) a -> a -> a’
with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (->)’
• Relevant bindings include
id_ :: Ob_ (->) a -> a -> a (bound at 348.hs:22:3)
|
22 | id_ = ()
| ^^
Failed, no modules loaded.
Prelude>
```
If we simply replace `Ob_` with `type Ob_ (cat :: Cat ob) :: ob -> Constraint`, the expected type (`a -> a`) matches my intuition:
```
348.hs:22:9: error:
• Couldn't match expected type ‘a -> a’ with actual type ‘()’
• In the expression: ()
In an equation for ‘id_’: id_ = ()
In the instance declaration for ‘Category_ (->)’
• Relevant bindings include id_ :: a -> a (bound at 348.hs:22:3)
|
22 | id_ = ()
| ^^
```8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15545Forced to enable TypeInType because of (i ~ i)2019-07-07T18:04:13ZIcelandjackForced to enable TypeInType because of (i ~ i)I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XPoly...I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`
```
$ ghci -ignore-dot-ghci
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XPolyKinds -XGADTs
Prelude> import Data.Kind
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
<interactive>:3:45: error:
• Data constructor ‘NP’ constrains the choice of kind parameter:
i ~ i
Use TypeInType to allow this
• In the definition of data constructor ‘NP’
In the data type declaration for ‘NP’
Prelude Data.Kind>
```
I would rather expect the warning I get after enabling `TypeInType`
```
Prelude Data.Kind> :set -XTypeInType
Prelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
<interactive>:8:28: error:
• Couldn't match ‘k’ with ‘i’
• In the data declaration for ‘NP’
```
----
**ps** making sure this is OK as well; it works after enabling `-XTypeInType` and quantifying with `-XRankNTypes` (is this using polymorphic recursion?)
```
Prelude Data.Kind> :set -XTypeInType -XRankNTypes
Prelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
Prelude Data.Kind> :t NP
NP :: forall i (f :: i -> *) (a :: i). f a -> NP f a
```
it also works for
```hs
data NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a
data NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Forced to enable TypeInType because of (i ~ i)","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"I don't know if this is a bug but `i ~ i` holds by reflexivity so I would not have expected it to require `TypeInType`\r\n\r\n{{{\r\n$ ghci -ignore-dot-ghci\r\nGHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help\r\nPrelude> :set -XPolyKinds -XGADTs\r\nPrelude> import Data.Kind\r\nPrelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\n\r\n<interactive>:3:45: error:\r\n • Data constructor ‘NP’ constrains the choice of kind parameter:\r\n i ~ i\r\n Use TypeInType to allow this\r\n • In the definition of data constructor ‘NP’\r\n In the data type declaration for ‘NP’\r\nPrelude Data.Kind> \r\n}}}\r\n\r\nI would rather expect the warning I get after enabling `TypeInType`\r\n\r\n{{{\r\nPrelude Data.Kind> :set -XTypeInType\r\nPrelude Data.Kind> data NP :: (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\n\r\n<interactive>:8:28: error:\r\n • Couldn't match ‘k’ with ‘i’\r\n • In the data declaration for ‘NP’\r\n}}}\r\n\r\n----\r\n\r\n'''ps''' making sure this is OK as well; it works after enabling `-XTypeInType` and quantifying with `-XRankNTypes` (is this using polymorphic recursion?)\r\n\r\n{{{\r\nPrelude Data.Kind> :set -XTypeInType -XRankNTypes\r\nPrelude Data.Kind> data NP :: forall i k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\nPrelude Data.Kind> :t NP\r\nNP :: forall i (f :: i -> *) (a :: i). f a -> NP f a\r\n}}}\r\n\r\nit also works for\r\n\r\n{{{#!hs\r\ndata NP :: forall k. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\ndata NP :: forall i. (k -> Type) -> (i -> Type) where NP :: f a -> NP f a\r\ndata NP :: (k -> Type) -> forall i. (i -> Type) where NP :: f a -> NP f a\r\n}}}\r\n\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15428Oversaturated type family application panicks GHC (piResultTys2)2019-07-07T18:04:56ZRyan ScottOversaturated type family application panicks GHC (piResultTys2)The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
im...The following program panics when compiled with GHC 8.6.1 or HEAD:
```hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family Flurmp :: k
type family Pure (x :: a) :: f a
wat :: forall (f :: Type -> Type) (p :: Type).
Proxy (f p) -> ()
wat _ =
let s :: (Flurmp :: f p)
:~: Pure (Flurmp :: p -> p) (Flurmp :: p)
s = undefined
in ()
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64-unknown-linux):
piResultTys2
f_aAT a_aAU
[(->) p_a1uI[sk:1], p_a1uI[sk:1] -> p_a1uI[sk:1], Flurmp, Flurmp]
[Flurmp]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type
```
On GHC 8.4 and earlier, this simply gives an error message:
```
$ /opt/ghc/8.4.3/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:18:16: error:
• Expecting one more argument to ‘Pure (Flurmp :: p -> p)’
Expected kind ‘p -> f p’,
but ‘Pure (Flurmp :: p -> p)’ has kind ‘p -> p -> p’
• In the second argument of ‘(:~:)’, namely
‘Pure (Flurmp :: p -> p) (Flurmp :: p)’
In the type signature:
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
In the expression:
let
s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
s = undefined
in ()
• Relevant bindings include
wat :: Proxy (f p) -> () (bound at Bug.hs:16:1)
|
18 | :~: Pure (Flurmp :: p -> p) (Flurmp :: p)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | high |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.6+ panics (piResultTys2), older GHCs don't","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program panics when compiled with GHC 8.6.1 or HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ScopedTypeVariables #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\nimport Data.Proxy\r\nimport Data.Type.Equality\r\n\r\ntype family Flurmp :: k\r\ntype family Pure (x :: a) :: f a\r\n\r\nwat :: forall (f :: Type -> Type) (p :: Type).\r\n Proxy (f p) -> ()\r\nwat _ =\r\n let s :: (Flurmp :: f p)\r\n :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64-unknown-linux):\r\n piResultTys2\r\n f_aAT a_aAU\r\n [(->) p_a1uI[sk:1], p_a1uI[sk:1] -> p_a1uI[sk:1], Flurmp, Flurmp]\r\n [Flurmp]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Type.hs:1041:9 in ghc:Type\r\n}}}\r\n\r\nOn GHC 8.4 and earlier, this simply gives an error message:\r\n\r\n{{{\r\n$ /opt/ghc/8.4.3/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:18:16: error:\r\n • Expecting one more argument to ‘Pure (Flurmp :: p -> p)’\r\n Expected kind ‘p -> f p’,\r\n but ‘Pure (Flurmp :: p -> p)’ has kind ‘p -> p -> p’\r\n • In the second argument of ‘(:~:)’, namely\r\n ‘Pure (Flurmp :: p -> p) (Flurmp :: p)’\r\n In the type signature:\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n In the expression:\r\n let\r\n s :: (Flurmp :: f p) :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n s = undefined\r\n in ()\r\n • Relevant bindings include\r\n wat :: Proxy (f p) -> () (bound at Bug.hs:16:1)\r\n |\r\n18 | :~: Pure (Flurmp :: p -> p) (Flurmp :: p)\r\n | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1https://gitlab.haskell.org/ghc/ghc/-/issues/15419GHC 8.6.1 regression (buildKindCoercion)2019-07-07T18:04:59ZRyan ScottGHC 8.6.1 regression (buildKindCoercion)The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes ...The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
data family Sing :: forall k. k -> Type
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
data instance Sing :: forall a b. (a, b) -> Type where
STuple2 :: Sing x -> Sing y -> Sing '(x, y)
newtype instance Sing (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }
-----
newtype Par1 p = Par1 p
newtype K1 c p = K1 c
data (f :*: g) p = f p :*: g p
data instance Sing :: forall p. Par1 p -> Type where
SPar1 :: Sing x -> Sing ('Par1 x)
data instance Sing :: forall k c (p :: k). K1 c p -> Type where
SK1 :: Sing x -> Sing ('K1 x)
data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
(f :*: g) p -> Type where
(:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)
class Generic1 (f :: k -> Type) where
type Rep1 f :: k -> Type
from1 :: f a -> Rep1 f a
to1 :: Rep1 f a -> f a
class PGeneric1 (f :: k -> Type) where
type From1 (z :: f a) :: Rep1 f a
type To1 (z :: Rep1 f a) :: f a
class SGeneric1 (f :: k -> Type) where
sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)
sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
instance Generic1 ((,) a) where
type Rep1 ((,) a) = K1 a :*: Par1
from1 (x, y) = K1 x :*: Par1 y
to1 (K1 x :*: Par1 y) = (x, y)
instance PGeneric1 ((,) a) where
type From1 '(x, y) = 'K1 x ':*: 'Par1 y
type To1 ('K1 x ':*: 'Par1 y) = '(x, y)
instance SGeneric1 ((,) a) where
sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y
sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y
-----
type family GenericFmap (g :: a ~> b) (x :: f a) :: f b where
GenericFmap g x = To1 (Fmap g (From1 x))
class PFunctor (f :: Type -> Type) where
type Fmap (g :: a ~> b) (x :: f a) :: f b
type Fmap g x = GenericFmap g x
class SFunctor (f :: Type -> Type) where
sFmap :: forall a b (g :: a ~> b) (x :: f a).
Sing g -> Sing x -> Sing (Fmap g x)
default sFmap :: forall a b (g :: a ~> b) (x :: f a).
( SGeneric1 f, SFunctor (Rep1 f)
, Fmap g x ~ GenericFmap g x )
=> Sing g -> Sing x -> Sing (Fmap g x)
sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))
-----
instance PFunctor Par1 where
type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)
instance PFunctor (K1 c) where
type Fmap _ ('K1 x) = 'K1 x
instance PFunctor (f :*: g) where
type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y
instance SFunctor Par1 where
sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)
instance SFunctor (K1 c) where
sFmap _ (SK1 sx) = SK1 sx
instance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where
sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy
-----
instance PFunctor ((,) a)
-- The line below causes the panic
instance SFunctor ((,) a)
```
```
$ /opt/ghc/8.6.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 8.6.0.20180714 for x86_64-unknown-linux):
buildKindCoercion
K1 a_a1Nj :*: Par1
Rep1 ((,) a_a1Nj)
*
a_a1Nj
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable
pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | highest |
| Resolution | Unresolved |
| Component | Compiler (Type checker) |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC 8.6.1 regression (buildKindCoercion)","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"The following program typechecks on GHC 8.4.1, but panics on GHC 8.6.1 and HEAD:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE DefaultSignatures #-}\r\n{-# LANGUAGE FlexibleContexts #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE RankNTypes #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing :: forall k. k -> Type\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\ntype family Apply (f :: k1 ~> k2) (x :: k1) :: k2\r\n\r\ndata instance Sing :: forall a b. (a, b) -> Type where\r\n STuple2 :: Sing x -> Sing y -> Sing '(x, y)\r\nnewtype instance Sing (f :: k1 ~> k2) =\r\n SLambda { applySing :: forall t. Sing t -> Sing (f `Apply` t) }\r\n\r\n-----\r\n\r\nnewtype Par1 p = Par1 p\r\nnewtype K1 c p = K1 c\r\ndata (f :*: g) p = f p :*: g p\r\n\r\ndata instance Sing :: forall p. Par1 p -> Type where\r\n SPar1 :: Sing x -> Sing ('Par1 x)\r\ndata instance Sing :: forall k c (p :: k). K1 c p -> Type where\r\n SK1 :: Sing x -> Sing ('K1 x)\r\ndata instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).\r\n (f :*: g) p -> Type where\r\n (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)\r\n\r\nclass Generic1 (f :: k -> Type) where\r\n type Rep1 f :: k -> Type\r\n from1 :: f a -> Rep1 f a\r\n to1 :: Rep1 f a -> f a\r\n\r\nclass PGeneric1 (f :: k -> Type) where\r\n type From1 (z :: f a) :: Rep1 f a\r\n type To1 (z :: Rep1 f a) :: f a\r\n\r\nclass SGeneric1 (f :: k -> Type) where\r\n sFrom1 :: forall (a :: k) (z :: f a). Sing z -> Sing (From1 z)\r\n sTo1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)\r\n\r\ninstance Generic1 ((,) a) where\r\n type Rep1 ((,) a) = K1 a :*: Par1\r\n from1 (x, y) = K1 x :*: Par1 y\r\n to1 (K1 x :*: Par1 y) = (x, y)\r\n\r\ninstance PGeneric1 ((,) a) where\r\n type From1 '(x, y) = 'K1 x ':*: 'Par1 y\r\n type To1 ('K1 x ':*: 'Par1 y) = '(x, y)\r\n\r\ninstance SGeneric1 ((,) a) where\r\n sFrom1 (STuple2 x y) = SK1 x :%*: SPar1 y\r\n sTo1 (SK1 x :%*: SPar1 y) = STuple2 x y\r\n\r\n-----\r\n\r\ntype family GenericFmap (g :: a ~> b) (x :: f a) :: f b where\r\n GenericFmap g x = To1 (Fmap g (From1 x))\r\n\r\nclass PFunctor (f :: Type -> Type) where\r\n type Fmap (g :: a ~> b) (x :: f a) :: f b\r\n type Fmap g x = GenericFmap g x\r\n\r\nclass SFunctor (f :: Type -> Type) where\r\n sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n Sing g -> Sing x -> Sing (Fmap g x)\r\n default sFmap :: forall a b (g :: a ~> b) (x :: f a).\r\n ( SGeneric1 f, SFunctor (Rep1 f)\r\n , Fmap g x ~ GenericFmap g x )\r\n => Sing g -> Sing x -> Sing (Fmap g x)\r\n sFmap sg sx = sTo1 (sFmap sg (sFrom1 sx))\r\n\r\n-----\r\n\r\ninstance PFunctor Par1 where\r\n type Fmap f ('Par1 x) = 'Par1 (f `Apply` x)\r\ninstance PFunctor (K1 c) where\r\n type Fmap _ ('K1 x) = 'K1 x\r\ninstance PFunctor (f :*: g) where\r\n type Fmap h (x ':*: y) = Fmap h x ':*: Fmap h y\r\n\r\ninstance SFunctor Par1 where\r\n sFmap sf (SPar1 sx) = SPar1 (sf `applySing` sx)\r\ninstance SFunctor (K1 c) where\r\n sFmap _ (SK1 sx) = SK1 sx\r\ninstance (SFunctor f, SFunctor g) => SFunctor (f :*: g) where\r\n sFmap sh (sx :%*: sy) = sFmap sh sx :%*: sFmap sh sy\r\n\r\n-----\r\n\r\ninstance PFunctor ((,) a)\r\n-- The line below causes the panic\r\ninstance SFunctor ((,) a)\r\n}}}\r\n{{{\r\n$ /opt/ghc/8.6.1/bin/ghc Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc: panic! (the 'impossible' happened)\r\n (GHC version 8.6.0.20180714 for x86_64-unknown-linux):\r\n buildKindCoercion\r\n K1 a_a1Nj :*: Par1\r\n Rep1 ((,) a_a1Nj)\r\n *\r\n a_a1Nj\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1164:37 in ghc:Outputable\r\n pprPanic, called at compiler/types/Coercion.hs:2069:9 in ghc:Coercion\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev