GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20190707T18:18:23Zhttps://gitlab.haskell.org/ghc/ghc//issues/14119Refactor type patterns20190707T18:18:23ZRichard Eisenbergrae@richarde.devRefactor type patternsType patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
 They must never mention a type family.
Types that appear as arguments on the LHS of a RULE should also be type patterns.
Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.
I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.
We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in [ticket:14038\#comment:140786](https://gitlab.haskell.org//ghc/ghc/issues/14038#note_140786). It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  #12564, #14038 
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Refactor type patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:\r\n\r\n * They must never mention a `forall`.\r\n * They must never mention a context. (The context in a class instance head is a different part of the instance construct.)\r\n * They must never mention a type family.\r\n\r\nTypes that appear as arguments on the LHS of a RULE should also be type patterns.\r\n\r\nType patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.\r\n\r\nI thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.\r\n\r\nWe could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like \"wobbly types\" than OutsideIn.","type_of_failure":"OtherFailure","blocking":[12564,14038]} >Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:
 They must never mention a `forall`.
 They must never mention a context. (The context in a class instance head is a different part of the instance construct.)
 They must never mention a type family.
Types that appear as arguments on the LHS of a RULE should also be type patterns.
Type patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.
I thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.
We could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in [ticket:14038\#comment:140786](https://gitlab.haskell.org//ghc/ghc/issues/14038#note_140786). It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like "wobbly types" than OutsideIn.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.2.1 
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  #12564, #14038 
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Refactor type patterns","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"Type patterns are used in instance heads: class instances, type instances, and data/newtype instances. These type patterns differ from ordinary types in several ways:\r\n\r\n * They must never mention a `forall`.\r\n * They must never mention a context. (The context in a class instance head is a different part of the instance construct.)\r\n * They must never mention a type family.\r\n\r\nTypes that appear as arguments on the LHS of a RULE should also be type patterns.\r\n\r\nType patterns are used in GHC differently than types as well: we should match only against patterns, never ordinary types.\r\n\r\nI thus propose that a new datatype within GHC to store type patterns. I'll call it `TyPat` here, but perhaps a longer name is better. The matcher (in the `Unify` module) would then take a `TyPat` parameter, making clear which type is the template and which is the concrete instantiation.\r\n\r\nWe could have a new algorithm to typecheck/desugar source syntax into patterns. This new algorithm could accommodate issues like those mentioned in comment:6:ticket:14038. It could also avoid ever putting a type family in a kind parameter, which would fix #12564. Separating out checking type patterns from proper types could also improve GADT pattern matching in types, which is currently more like \"wobbly types\" than OutsideIn.","type_of_failure":"OtherFailure","blocking":[12564,14038]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/14040Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]20200123T19:31:02ZRyan ScottTyped holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2](Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >(Originally spun off from #13877.)
The following program gives a somewhat decent error message in GHC 8.0.1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeInType #}
module Bug where
import Data.Kind
data family Sing (a :: k)
data WeirdList :: Type > Type where
WeirdNil :: WeirdList a
WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a
data instance Sing (z :: WeirdList a) where
SWeirdNil :: Sing WeirdNil
SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)
elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs
> p _ (WeirdCons x xs))
> p _ wl
elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
elimWeirdList (SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil pWeirdCons
= pWeirdCons @z @x @xs x xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
```
$ /opt/ghc/8.0.1/bin/ghci Foo.hs
GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:34:8: error:
• Cannot apply expression of type ‘Sing wl
> (forall y. p x0 t3 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs
> p (WeirdList z) t2 xs
> p z t1 ('WeirdCons x xs))
> p a t0 wl’
to a visible type argument ‘WeirdList z’
• In the sixth argument of ‘pWeirdCons’, namely
‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
In the expression:
pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
In an equation for ‘elimWeirdList’:
elimWeirdList
(SWeirdCons (x :: Sing (x :: z))
(xs :: Sing (xs :: WeirdList (WeirdList z))))
pWeirdNil
pWeirdCons
= pWeirdCons
@z
@x
@xs
x
xs
(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)
```
But in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:
```
$ /opt/ghc/8.0.2/bin/ghci Foo.hs
GHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘t0’
Where: ‘t0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl
• Relevant bindings include
elimWeirdList :: Sing wl
> (forall y. p x0 t0 'WeirdNil)
> (forall z (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x
> Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))
> p a t3 wl
(bound at Foo.hs:29:1)
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.0.2 for x86_64unknownlinux):
No skolem info: z_a13X[sk]
```
```
$ /opt/ghc/8.2.1/bin/ghci Foo.hs
GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Foo.hs, interpreted )
Foo.hs:21:18: error:
• The kind of variable ‘wl1’, namely ‘WeirdList a1’,
depends on variable ‘a1’ from an inner scope
Perhaps bind ‘wl1’ sometime after binding ‘a1’
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
Foo.hs:24:41: error:
• Found type wildcard ‘_’ standing for ‘w0’
Where: ‘w0’ is an ambiguous type variable
‘x0’ is an ambiguous type variable
To use the inferred type, enable PartialTypeSignatures
• In the type signature:
elimWeirdList :: forall (a :: Type)
(wl :: WeirdList a)
(p :: forall (x :: Type). x > WeirdList x > Type).
Sing wl
> (forall (y :: Type). p _ WeirdNil)
> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))
> p _ wl

24  > (forall (y :: Type). p _ WeirdNil)
 ^
Foo.hs:26:44: error:ghc: panic! (the 'impossible' happened)
(GHC version 8.2.1 for x86_64unknownlinux):
No skolem info:
z_a1sY[sk:2]
Call stack:
CallStack (from HasCallStack):
prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors
```
(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.0.2 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler (Type checker) 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  #13877 
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Typed holes regression in GHC 8.0.2: No skolem info: z_a1sY[sk:2]","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[13877],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.2","keywords":["PartialTypeSignatures","TypeFamilies,","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"(Originally spun off from #13877.)\r\n\r\nThe following program gives a somewhat decent error message in GHC 8.0.1:\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs #}\r\n{# LANGUAGE RankNTypes #}\r\n{# LANGUAGE ScopedTypeVariables #}\r\n{# LANGUAGE TypeApplications #}\r\n{# LANGUAGE TypeFamilies #}\r\n{# LANGUAGE TypeInType #}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)\r\n\r\ndata WeirdList :: Type > Type where\r\n WeirdNil :: WeirdList a\r\n WeirdCons :: a > WeirdList (WeirdList a) > WeirdList a\r\n\r\ndata instance Sing (z :: WeirdList a) where\r\n SWeirdNil :: Sing WeirdNil\r\n SWeirdCons :: Sing w > Sing wws > Sing (WeirdCons w wws)\r\n\r\nelimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs\r\n > p _ (WeirdCons x xs))\r\n > p _ wl\r\nelimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil\r\nelimWeirdList (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil pWeirdCons\r\n = pWeirdCons @z @x @xs x xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.0.1/bin/ghci Foo.hs \r\nGHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:34:8: error:\r\n • Cannot apply expression of type ‘Sing wl\r\n > (forall y. p x0 t3 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs\r\n > p (WeirdList z) t2 xs\r\n > p z t1 ('WeirdCons x xs))\r\n > p a t0 wl’\r\n to a visible type argument ‘WeirdList z’\r\n • In the sixth argument of ‘pWeirdCons’, namely\r\n ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’\r\n In the expression:\r\n pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n In an equation for ‘elimWeirdList’:\r\n elimWeirdList\r\n (SWeirdCons (x :: Sing (x :: z))\r\n (xs :: Sing (xs :: WeirdList (WeirdList z))))\r\n pWeirdNil\r\n pWeirdCons\r\n = pWeirdCons\r\n @z\r\n @x\r\n @xs\r\n x\r\n xs\r\n (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)\r\n}}}\r\n\r\nBut in GHC 8.0.2, 8.2.1, and HEAD, it panics to varying degrees:\r\n\r\n{{{\r\n$ /opt/ghc/8.0.2/bin/ghci Foo.hs \r\nGHCi, version 8.0.2: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘t0’\r\n Where: ‘t0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n • Relevant bindings include\r\n elimWeirdList :: Sing wl\r\n > (forall y. p x0 t0 'WeirdNil)\r\n > (forall z (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x\r\n > Sing xs > p (WeirdList z) t1 xs > p z t2 ('WeirdCons x xs))\r\n > p a t3 wl\r\n (bound at Foo.hs:29:1)\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.0.2 for x86_64unknownlinux):\r\n\tNo skolem info: z_a13X[sk]\r\n}}}\r\n\r\n{{{\r\n$ /opt/ghc/8.2.1/bin/ghci Foo.hs \r\nGHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help\r\nLoaded GHCi configuration from /home/rgscott/.ghci\r\n[1 of 1] Compiling Bug ( Foo.hs, interpreted )\r\n\r\nFoo.hs:21:18: error:\r\n • The kind of variable ‘wl1’, namely ‘WeirdList a1’,\r\n depends on variable ‘a1’ from an inner scope\r\n Perhaps bind ‘wl1’ sometime after binding ‘a1’\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n21  elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)\r\n  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...\r\n\r\nFoo.hs:24:41: error:\r\n • Found type wildcard ‘_’ standing for ‘w0’\r\n Where: ‘w0’ is an ambiguous type variable\r\n ‘x0’ is an ambiguous type variable\r\n To use the inferred type, enable PartialTypeSignatures\r\n • In the type signature:\r\n elimWeirdList :: forall (a :: Type)\r\n (wl :: WeirdList a)\r\n (p :: forall (x :: Type). x > WeirdList x > Type).\r\n Sing wl\r\n > (forall (y :: Type). p _ WeirdNil)\r\n > (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).\r\n Sing x > Sing xs > p _ xs > p _ (WeirdCons x xs))\r\n > p _ wl\r\n \r\n24  > (forall (y :: Type). p _ WeirdNil)\r\n  ^\r\n\r\nFoo.hs:26:44: error:ghc: panic! (the 'impossible' happened)\r\n (GHC version 8.2.1 for x86_64unknownlinux):\r\n\tNo skolem info:\r\n z_a1sY[sk:2]\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable\r\n callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable\r\n pprPanic, called at compiler/typecheck/TcErrors.hs:2653:5 in ghc:TcErrors\r\n}}}\r\n\r\n(The error messages from HEAD, at commit 791947db6db32ef7d4772a821a0823e558e3c05b, are the same as in GHC 8.2.1.)","type_of_failure":"OtherFailure","blocking":[]} >Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13933Support Typeable instances for types with coercions20190707T18:19:21ZRichard Eisenbergrae@richarde.devSupport Typeable instances for types with coercionsIf I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG

10  rep = typeRep @MkG

```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeApplications, TypeInType #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n \r\n10  rep = typeRep @MkG\r\n  \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} >If I say
```hs
{# LANGUAGE GADTs, TypeApplications, TypeInType #}
module Bug where
import Type.Reflection
data G a where
MkG :: a ~ Bool => G a
rep = typeRep @MkG
```
I get
```
Bug.hs:10:7: error:
• No instance for (Typeable <>) arising from a use of ‘typeRep’
• In the expression: typeRep @MkG
In an equation for ‘rep’: rep = typeRep @MkG

10  rep = typeRep @MkG

```
First off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Support Typeable instances for types with coercions","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":["TypeInType,","Typeable"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{#!hs\r\n{# LANGUAGE GADTs, TypeApplications, TypeInType #}\r\n\r\nmodule Bug where\r\n\r\nimport Type.Reflection\r\n\r\ndata G a where\r\n MkG :: a ~ Bool => G a\r\n\r\nrep = typeRep @MkG\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nBug.hs:10:7: error:\r\n • No instance for (Typeable <>) arising from a use of ‘typeRep’\r\n • In the expression: typeRep @MkG\r\n In an equation for ‘rep’: rep = typeRep @MkG\r\n \r\n10  rep = typeRep @MkG\r\n  \r\n}}}\r\n\r\nFirst off, the error message is confusing, mentioning the mysterious `<>`. But more importantly, it would be nice if the `Typeable` mechanism supported coercions.","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/13650Implement KPush in types20190707T18:20:47ZRichard Eisenbergrae@richarde.devImplement KPush in typesA recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >A recent commit contributed a [Note](https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191) that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that `t1 `eqType` t2` and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.
This ticket serves as a reminder to do so.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  
 Type  Task 
 TypeOfFailure  OtherFailure 
 Priority  high 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Implement KPush in types","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.4.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Task","description":"A recent commit contributed a [https://phabricator.haskell.org/diffusion/GHC/browse/master/compiler/types/Type.hs;a483e711da7834bc952367f554ac4e877b4e157a$1191 Note] that explains why we need the dreaded KPush rule to be implemented in `splitTyConApp`. Without KPush there, it's possible that we can have two types t1 and t2 such that {{{t1 `eqType` t2}}} and yet they respond differently to `splitTyConApp`: t1 = `(T > co1) (a > co2)` and t2 = `T a`. Both t1 and t2 are wellkinded and can have the same kind. But one is a `TyConApp` and one is an `AppTy`. (Actually, looking at this, perhaps the magic will be in `mkAppTy`, not `splitTyConApp`.) But I have to look closer.\r\n\r\nThis ticket serves as a reminder to do so.","type_of_failure":"OtherFailure","blocking":[]} >8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/13408Consider inferring a higherrank kind for type synonyms20200925T17:22:29ZRichard Eisenbergrae@richarde.devConsider inferring a higherrank kind for type synonymsIn terms, a definition comprising one nonrecursive equation may have a higherrank 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 termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive 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 higherrank 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 nonrecursive equation may have a higherrank 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 termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive 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":[]} >In terms, a definition comprising one nonrecursive equation may have a higherrank 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 termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive 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 higherrank 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 nonrecursive equation may have a higherrank 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 termlevel definition is accepted. GHC should not be in the business of inferring higherrank types. But there is an exception for definitions comprising one nonrecursive 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/12564Type family in type pattern kind20190824T18:45:27ZVladislav ZavialovType family in type pattern kindI want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:
```haskell
{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}
import Data.Kind
data N = Z  S N
type family Len (xs :: [a]) :: N where
Len '[] = Z
Len (_ ': xs) = S (Len xs)
data Fin :: N > Type where
FZ :: Fin (S n)
FS :: Fin n > Fin (S n)
type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
At (x ': _) FZ = x
At (_ ': xs) (FS i) = At xs i
```
It fails to compile with this error:
```
FinAt.hs:16:3: error:
• Illegal type synonym family application in instance: 'FZ
• In the equations for closed type family ‘At’
In the type family declaration for ‘At’
```
That's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.
I tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:
```haskell
x :: At '[Bool] FZ
x = True
```
results in
```
FinAt.hs:20:5: error:
• Couldn't match expected type ‘At
* ((':) * Bool ('[] *)) ('FZ 'Z)’
with actual type ‘Bool’
• In the expression: True
In an equation for ‘x’: x = True
```
<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, intindex 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family in type pattern kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","intindex"],"type":"Bug","description":"I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:\r\n\r\n{{{#!haskell\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}\r\n\r\nimport Data.Kind\r\n\r\ndata N = Z  S N\r\n\r\ntype family Len (xs :: [a]) :: N where\r\n Len '[] = Z\r\n Len (_ ': xs) = S (Len xs)\r\n\r\ndata Fin :: N > Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n > Fin (S n)\r\n\r\ntype family At (xs :: [a]) (i :: Fin (Len xs)) :: a where\r\n At (x ': _) FZ = x\r\n At (_ ': xs) (FS i) = At xs i\r\n}}}\r\n\r\nIt fails to compile with this error:\r\n\r\n{{{\r\nFinAt.hs:16:3: error:\r\n • Illegal type synonym family application in instance: 'FZ\r\n • In the equations for closed type family ‘At’\r\n In the type family declaration for ‘At’\r\n}}}\r\n\r\nThat's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.\r\n\r\nI tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:\r\n\r\n{{{#!haskell\r\nx :: At '[Bool] FZ\r\nx = True\r\n}}}\r\n\r\nresults in\r\n\r\n{{{\r\nFinAt.hs:20:5: error:\r\n • Couldn't match expected type ‘At\r\n * ((':) * Bool ('[] *)) ('FZ 'Z)’\r\n with actual type ‘Bool’\r\n • In the expression: True\r\n In an equation for ‘x’: x = True\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:
```haskell
{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}
import Data.Kind
data N = Z  S N
type family Len (xs :: [a]) :: N where
Len '[] = Z
Len (_ ': xs) = S (Len xs)
data Fin :: N > Type where
FZ :: Fin (S n)
FS :: Fin n > Fin (S n)
type family At (xs :: [a]) (i :: Fin (Len xs)) :: a where
At (x ': _) FZ = x
At (_ ': xs) (FS i) = At xs i
```
It fails to compile with this error:
```
FinAt.hs:16:3: error:
• Illegal type synonym family application in instance: 'FZ
• In the equations for closed type family ‘At’
In the type family declaration for ‘At’
```
That's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.
I tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:
```haskell
x :: At '[Bool] FZ
x = True
```
results in
```
FinAt.hs:20:5: error:
• Couldn't match expected type ‘At
* ((':) * Bool ('[] *)) ('FZ 'Z)’
with actual type ‘Bool’
• In the expression: True
In an equation for ‘x’: x = True
```
<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, intindex 
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Type family in type pattern kind","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.0.1","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","intindex"],"type":"Bug","description":"I want to write a type family that is analogous to `!!` for lists but requires the index to be no bigger than the length of the list. Usually, in dependently typed languages finite sets are used for this purpose, here's an attempt to do so in Haskell:\r\n\r\n{{{#!haskell\r\n{# LANGUAGE TypeInType, TypeFamilies, GADTs, TypeOperators #}\r\n\r\nimport Data.Kind\r\n\r\ndata N = Z  S N\r\n\r\ntype family Len (xs :: [a]) :: N where\r\n Len '[] = Z\r\n Len (_ ': xs) = S (Len xs)\r\n\r\ndata Fin :: N > Type where\r\n FZ :: Fin (S n)\r\n FS :: Fin n > Fin (S n)\r\n\r\ntype family At (xs :: [a]) (i :: Fin (Len xs)) :: a where\r\n At (x ': _) FZ = x\r\n At (_ ': xs) (FS i) = At xs i\r\n}}}\r\n\r\nIt fails to compile with this error:\r\n\r\n{{{\r\nFinAt.hs:16:3: error:\r\n • Illegal type synonym family application in instance: 'FZ\r\n • In the equations for closed type family ‘At’\r\n In the type family declaration for ‘At’\r\n}}}\r\n\r\nThat's because the kind of the `FZ` pattern (first clause of `At`) has the kind `Fin (Len xs)` and the application of `Len` cannot reduce completely. `checkValidTypePat` then disallows the pattern, as it contains a type family application.\r\n\r\nI tried to suppress `checkValidTypePat` and the definition of `At` has compiled; however, it's of little use, since `At` doesn't reduce:\r\n\r\n{{{#!haskell\r\nx :: At '[Bool] FZ\r\nx = True\r\n}}}\r\n\r\nresults in\r\n\r\n{{{\r\nFinAt.hs:20:5: error:\r\n • Couldn't match expected type ‘At\r\n * ((':) * Bool ('[] *)) ('FZ 'Z)’\r\n with actual type ‘Bool’\r\n • In the expression: True\r\n In an equation for ‘x’: x = True\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} >8.4.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/11962Support induction recursion20200106T11:26:23ZRichard Eisenbergrae@richarde.devSupport induction recursionNow that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
 Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
 A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k)  we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) > (El a > U) > U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x > El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/internal#separatingtypesignaturesfromdefinitions).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n  Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n  A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)  we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) > (El a > U) > U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x > El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} >Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:
```
mutual
 Codes for types.
data U : Set where
nat : U
pi : (a : U) → (El a → U) → U
 A function that interprets codes as actual types.
El : U → Set
El nat = ℕ
El (pi a b) = (x : El a) → El (b x)
```
Note that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.
Translation into Haskell:
```
import Data.Kind
data family Sing (a :: k)  we still require singletons
data U :: Type where
Nat :: U
Pi :: Sing (a :: U) > (El a > U) > U
type family El (u :: U) :: Type where
El 'Nat = Int
El (Pi a b) = forall (x :: El a). Sing x > El (b x)
```
This currently errors with
```
• Type constructor ‘U’ cannot be used here
(it is defined and used in the same recursive group)
• In the kind ‘U’
```
It needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)
I have some very sketchy notes on how we might do this [here](https://gitlab.haskell.org/ghc/ghc/wikis/dependenthaskell/internal#separatingtypesignaturesfromdefinitions).
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.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":"Support induction recursion","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"FeatureRequest","description":"Now that we have `XTypeInType`, let's take it a step further and allow induction recursion. This feature exists in Agda and Idris. Here is a short example of what can be done in Agda:\r\n\r\n{{{\r\n mutual\r\n  Codes for types.\r\n\r\n data U : Set where\r\n nat : U\r\n pi : (a : U) → (El a → U) → U\r\n\r\n  A function that interprets codes as actual types.\r\n\r\n El : U → Set\r\n El nat = ℕ\r\n El (pi a b) = (x : El a) → El (b x)\r\n}}}\r\n\r\nNote that the `U` datatype and the `El` function depend on each other. But if you look more closely, the header for `U` does not depend on `El`; only the constructors of `U` depend on `El`. So if we typecheck `U : Set` first, then `El : U → Set`, then the constructors of `U`, then the equations of `El`, we're OK.\r\n\r\nTranslation into Haskell:\r\n\r\n{{{\r\nimport Data.Kind\r\n\r\ndata family Sing (a :: k)  we still require singletons\r\n\r\ndata U :: Type where\r\n Nat :: U\r\n Pi :: Sing (a :: U) > (El a > U) > U\r\n\r\ntype family El (u :: U) :: Type where\r\n El 'Nat = Int\r\n El (Pi a b) = forall (x :: El a). Sing x > El (b x)\r\n}}}\r\n\r\nThis currently errors with\r\n\r\n{{{\r\n • Type constructor ‘U’ cannot be used here\r\n (it is defined and used in the same recursive group)\r\n • In the kind ‘U’\r\n}}}\r\n\r\nIt needn't error. (I'm cheating a bit here, because for unrelated reasons, we can't return a `forall` on the righthand side of a type family. But that's not the issue at hand.)\r\n\r\nI have some very sketchy notes on how we might do this [wiki:DependentHaskell/Internal#Separatingtypesignaturesfromdefinitions here].","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/11196TypeInType performance regressions20190707T18:31:30ZRichard 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 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.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/7503Bug with PolyKinds, type synonyms & GADTs20190707T18:49:28ZAshley YakeleyBug with PolyKinds, type synonyms & GADTsGHC incorrectly rejects this program:
```
{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapType a
data A :: WrappedType > * where
MkA :: forall (a :: *). AW a > A (WrapType a)
type AW (a :: k) = A (WrapType a)
type AW' (a :: k) = A (WrapType a)
class C (a :: k) where
aw :: AW a  workaround: AW'
instance C [] where
aw = aw
```
GHC accepts the program when AW is replaced with AW' on that line.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.6.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":"Bug with PolyKinds, type synonyms & GADTs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC incorrectly rejects this program:\r\n{{{\r\n{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}\r\nmodule TestConstraintKinds where\r\n import GHC.Exts hiding (Any)\r\n\r\n data WrappedType = forall a. WrapType a\r\n\r\n data A :: WrappedType > * where\r\n MkA :: forall (a :: *). AW a > A (WrapType a)\r\n\r\n type AW (a :: k) = A (WrapType a)\r\n type AW' (a :: k) = A (WrapType a)\r\n\r\n class C (a :: k) where\r\n aw :: AW a  workaround: AW'\r\n\r\n instance C [] where\r\n aw = aw\r\n}}}\r\n\r\nGHC accepts the program when AW is replaced with AW' on that line.","type_of_failure":"OtherFailure","blocking":[]} >GHC incorrectly rejects this program:
```
{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapType a
data A :: WrappedType > * where
MkA :: forall (a :: *). AW a > A (WrapType a)
type AW (a :: k) = A (WrapType a)
type AW' (a :: k) = A (WrapType a)
class C (a :: k) where
aw :: AW a  workaround: AW'
instance C [] where
aw = aw
```
GHC accepts the program when AW is replaced with AW' on that line.
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  7.6.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":"Bug with PolyKinds, type synonyms & GADTs","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"7.6.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"GHC incorrectly rejects this program:\r\n{{{\r\n{# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #}\r\nmodule TestConstraintKinds where\r\n import GHC.Exts hiding (Any)\r\n\r\n data WrappedType = forall a. WrapType a\r\n\r\n data A :: WrappedType > * where\r\n MkA :: forall (a :: *). AW a > A (WrapType a)\r\n\r\n type AW (a :: k) = A (WrapType a)\r\n type AW' (a :: k) = A (WrapType a)\r\n\r\n class C (a :: k) where\r\n aw :: AW a  workaround: AW'\r\n\r\n instance C [] where\r\n aw = aw\r\n}}}\r\n\r\nGHC accepts the program when AW is replaced with AW' on that line.","type_of_failure":"OtherFailure","blocking":[]} >8.0.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc//issues/14420Data families should not instantiate to nonType kinds20210201T10:19:24ZRichard Eisenbergrae@richarde.devData families should not instantiate to nonType kinds```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >```hs
data family Any :: k  allowable now due to fix for #12369
type family F (a :: Bool) :: Nat where
F True = 0
F False = 1
F Any = 2
```
```
ghci> :kind! F True
F True :: Nat
= 0
ghci> :kind! F False
F False :: Nat
= 1
ghci> :kind! F Any
F Any :: Nat
= 2
```
Oh dear.
We should require that any instantiation of a data family be to a kind that ends in `Type`.
Inspired by [ticket:9429\#comment:144757](https://gitlab.haskell.org//ghc/ghc/issues/9429#note_144757)
<details><summary>Trac metadata</summary>
 Trac field  Value 
    
 Version  8.3 
 Type  Bug 
 TypeOfFailure  OtherFailure 
 Priority  normal 
 Resolution  Unresolved 
 Component  Compiler 
 Test case  
 Differential revisions  
 BlockedBy  
 Related  
 Blocking  
 CC  
 Operating system  
 Architecture  
</details>
<! {"blocked_by":[],"summary":"Data families should not instantiate to nonType kinds","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.3","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"{{{#!hs\r\ndata family Any :: k  allowable now due to fix for #12369\r\n\r\ntype family F (a :: Bool) :: Nat where\r\n F True = 0\r\n F False = 1\r\n F Any = 2\r\n}}}\r\n\r\n{{{\r\nghci> :kind! F True\r\nF True :: Nat\r\n= 0\r\nghci> :kind! F False\r\nF False :: Nat\r\n= 1\r\nghci> :kind! F Any\r\nF Any :: Nat\r\n= 2\r\n}}}\r\n\r\nOh dear.\r\n\r\nWe should require that any instantiation of a data family be to a kind that ends in `Type`.\r\n\r\nInspired by comment:31:ticket:9429","type_of_failure":"OtherFailure","blocking":[]} >https://gitlab.haskell.org/ghc/ghc//issues/12612Allow kinds of associated types to depend on earlier associated types20190707T18:25:50ZdavemenendezAllow 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 in the same recursive group)
• In the kind ‘K t > Type’
```
See [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/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/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >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 [email discussion](https://mail.haskell.org/pipermail/glasgowhaskellusers/2016September/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/glasgowhaskellusers/2016September/026402.html email discussion]. This is connected to #12088, at least as far as defining instances of C.","type_of_failure":"OtherFailure","blocking":[]} >