GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-07-07T18:37:21Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/10141CUSK mysteries2019-07-07T18:37:21ZRichard Eisenbergrae@richarde.devCUSK mysteriesTake the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)Take the following definition:
```hs
type family G (a :: k) where
G Int = Bool
G Bool = Int
G a = a
```
It compiles in 7.8.3, but not in 7.10.1 RC2. This makes me sad. I will fix.
(Found by Jan Stolarek.)8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/11715Constraint vs *2022-12-08T17:29:35ZBen GamariConstraint vs *I first noticed something was a bit odd with `Constraint` when chasing #11334. Consider this testcase (`-O0` is sufficient),
```hs
import Data.Typeable
main = do
print $ typeRep (Proxy :: Proxy Eq)
print $ typeOf (Proxy :: Prox...I first noticed something was a bit odd with `Constraint` when chasing #11334. Consider this testcase (`-O0` is sufficient),
```hs
import Data.Typeable
main = do
print $ typeRep (Proxy :: Proxy Eq)
print $ typeOf (Proxy :: Proxy Eq)
```
With `ghc-8.0` this will produce,
```
Eq
Proxy (* -> *) Eq
```
Notice the second line; GHC seems to be claiming that `Eq :: * -> *`, which is clearly nonsense.
I believe this issue may be the cause of some of the testsuite failures that I'm seeing on #11011. Unfortunately I haven't the foggiest where this issue might originate.
See also
- #11621
- #12933
- #9547
- #13931
- #15918 (about `mkCastTy`)
- #21530 (ultimately also about `mkCastTy`)8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/12938Polykinded associated type family rejected on false pretenses2019-07-07T18:24:33ZRichard Eisenbergrae@richarde.devPolykinded associated type family rejected on false pretensesIf I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to...If I say
```
class HasRep a where
type Rep a :: TYPE r
```
I get
```
• Kind variable ‘r’ is implicitly bound in datatype
‘Rep’, but does not appear as the kind of any
of its type variables. Perhaps you meant
to bind it (with TypeInType) explicitly somewhere?
Type variables with inferred kinds: a
• In the class declaration for ‘HasRep’
```
This definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how *useful* this is, but it's not bogus.)
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.0.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Polykinded associated type family rejected on false pretenses","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.2.1","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"If I say\r\n\r\n{{{\r\nclass HasRep a where\r\n type Rep a :: TYPE r\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\n • Kind variable ‘r’ is implicitly bound in datatype\r\n ‘Rep’, but does not appear as the kind of any\r\n of its type variables. Perhaps you meant\r\n to bind it (with TypeInType) explicitly somewhere?\r\n Type variables with inferred kinds: a\r\n • In the class declaration for ‘HasRep’\r\n}}}\r\n\r\nThis definition should be accepted, though, as `r` is just an invisible parameter to the associated type family. (I don't know how ''useful'' this is, but it's not bogus.)","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13075Top-level bang pattern accepted2019-07-07T18:23:49ZRichard Eisenbergrae@richarde.devTop-level bang pattern acceptedWhen I compile/link
```hs
{-# LANGUAGE BangPatterns #-}
module Main where
!(Just x) = Nothing
main = putStrLn "hi there!"
```
I get
```
rae:09:50:49 ~/temp> ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking B...When I compile/link
```hs
{-# LANGUAGE BangPatterns #-}
module Main where
!(Just x) = Nothing
main = putStrLn "hi there!"
```
I get
```
rae:09:50:49 ~/temp> ghc Bug.hs
[1 of 1] Compiling Main ( Bug.hs, Bug.o )
Linking Bug ...
ld: can't open output file for writing: Bug, errno=21 for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
`gcc' failed in phase `Linker'. (Exit code: 1)
```
This bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.
Will fix while I'm in the area.
<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":"Top-level bang pattern accepted","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"OwnedBy","contents":"goldfire"},"version":"8.0.1","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"When I compile/link\r\n\r\n{{{#!hs\r\n{-# LANGUAGE BangPatterns #-}\r\n\r\nmodule Main where\r\n\r\n!(Just x) = Nothing\r\n\r\nmain = putStrLn \"hi there!\"\r\n}}}\r\n\r\nI get\r\n\r\n{{{\r\nrae:09:50:49 ~/temp> ghc Bug.hs\r\n[1 of 1] Compiling Main ( Bug.hs, Bug.o )\r\nLinking Bug ...\r\nld: can't open output file for writing: Bug, errno=21 for architecture x86_64\r\nclang: error: linker command failed with exit code 1 (use -v to see invocation)\r\n`gcc' failed in phase `Linker'. (Exit code: 1)\r\n}}}\r\n\r\nThis bogus code should be rejected more gracefully (and earlier). It actually also loads into GHCi, but shouldn't.\r\n\r\nWill fix while I'm in the area.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/13650Implement KPush in types2021-10-04T14:41:09ZRichard Eisenbergrae@richarde.devImplement KPush in typesA recent commit contributed a Note (https://gitlab.haskell.org/ghc/ghc/-/commit/ef0ff34d462e3780210567a13d58b868ec3399e0#07ce9a046fb8ea6659690020b0a8551d94cfdf1c_1175_1163) that explains why we need the dreaded KPush rule to be implement...A recent commit contributed a Note (https://gitlab.haskell.org/ghc/ghc/-/commit/ef0ff34d462e3780210567a13d58b868ec3399e0#07ce9a046fb8ea6659690020b0a8551d94cfdf1c_1175_1163) 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 well-kinded 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 well-kinded 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/14737Improve performance of Simplify.simplCast2019-09-23T07:37:55ZTobias Dammerstdammers@gmail.comImprove performance of Simplify.simplCastSplitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs](https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs), `simplCast` eats up more execution time than we ...Splitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs](https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs), `simplCast` eats up more execution time than we think it should.
From [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:10](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10):
> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given
>
> ```
> (fun |> co) @t1 @t2 ... @tn
> ```
>
> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.
>
> Solution: gather up those type arguments (easy) and define
>
> ```
> pushCoTyArgs :: Coercion -> [Type] -> Maybe ([Type], Coercion)
> ```
And [https://ghc.haskell.org/trac/ghc/ticket/11735\#comment:41](https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41):
> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.
>
> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.
>
> This should be an easy win all around.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | --------------------------- |
| Version | 8.2.2 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire, simonpj, tdammers |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Improve performance of Simplify.simplCast","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.2.2","keywords":[],"differentials":[],"test_case":"","architecture":"","cc":["goldfire","simonpj","tdammers"],"type":"Bug","description":"Splitting off task 3 from #11735. When compiling [https://ghc.haskell.org/trac/ghc/attachment/ticket/14683/Grammar.hs], `simplCast` eats up more execution time than we think it should.\r\n\r\nFrom [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:10]:\r\n\r\n> Something is clearly wrong with `Simplify.simplCast`. I think I know what it is. Given\r\n> {{{\r\n> (fun |> co) @t1 @t2 ... @tn\r\n> }}}\r\n> we will call `pushCoTyArg` `n` times, and hence does `n` singleton substitutions, via the `n` calls to `piResultTy`.\r\n> \r\n> Solution: gather up those type arguments (easy) and define\r\n> {{{\r\n> pushCoTyArgs :: Coercion -> [Type] -> Maybe ([Type], Coercion)\r\n> }}}\r\n\r\nAnd [https://ghc.haskell.org/trac/ghc/ticket/11735#comment:41]:\r\n\r\n> OK. I looked at `pushCoTyArg` and friends, and I have a very simple solution: just move the `isReflexiveCo` case in `addCoerce` (a local function within `Simplify.simplCast`) to the top. That should do it. Then `pushCoTyArg` is never called with a reflexive coercion, and so the `piResultTy` case won't happen.\r\n> \r\n> Now, `pushCoArgs` might still call `pushCoTyArg` with a reflexive coercion, but it can be taught not to as well: Have `pushCoArgs` return a `Maybe ([CoreArg], Maybe Coercion)` and `pushCoArg` return a `Maybe (CoreArg, Maybe Coercion)`. If the second return values are `Nothing`, that means that there is no cast (i.e., that the cast would have been reflexive). The only client of `pushCoArg(s)` is `exprIsConApp_maybe`, which simply omits a cast if `pushCoArgs` returns `Nothing`. Then, we never have to bother creating the reflexive coercions.\r\n> \r\n> This should be an easy win all around.\r\n","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14808GHC HEAD regression: GADT constructors no longer quantify tyvars in topologic...2019-07-07T18:15:30ZRyan ScottGHC HEAD regression: GADT constructors no longer quantify tyvars in topological orderOriginally noticed in #14796. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
f...Originally noticed in #14796. This program:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import Data.Kind
data ECC ctx f a where
ECC :: ctx => f a -> ECC ctx f a
f :: [()] -> ECC () [] ()
f = ECC @() @[] @()
```
Typechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:12:5: error:
• Couldn't match type ‘()’ with ‘[]’
Expected type: [()] -> ECC (() :: Constraint) [] ()
Actual type: () [] -> ECC (() :: Constraint) () []
• In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^^^^^^^^^^^^^^
Bug.hs:12:10: error:
• Expected kind ‘* -> *’, but ‘()’ has kind ‘*’
• In the type ‘()’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^
Bug.hs:12:14: error:
• Expecting one more argument to ‘[]’
Expected a type, but ‘[]’ has kind ‘* -> *’
• In the type ‘[]’
In the expression: ECC @() @[] @()
In an equation for ‘f’: f = ECC @() @[] @()
|
12 | f = ECC @() @[] @()
| ^^
```
This is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's
```
$ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.4.0.20180209: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (ctx :: Constraint) (f :: * -> *) a.
ctx =>
f a -> ECC ctx f a
```
In GHC HEAD, however, it's:
```
$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -XTypeApplications -fprint-explicit-foralls
GHCi, version 8.5.20180213: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :type +v ECC
ECC
:: forall (f :: * -> *) a (ctx :: Constraint).
ctx =>
f a -> ECC ctx f a
```
This regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).
<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 | simonpj |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"GHC HEAD regression: GADT constructors no longer quantify tyvars in topological order","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["GADTs"],"differentials":[],"test_case":"","architecture":"","cc":["simonpj"],"type":"Bug","description":"Originally noticed in #14796. This program:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE ConstraintKinds #-}\r\n{-# LANGUAGE GADTs #-}\r\n{-# LANGUAGE TypeApplications #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ndata ECC ctx f a where\r\n ECC :: ctx => f a -> ECC ctx f a\r\n\r\nf :: [()] -> ECC () [] ()\r\nf = ECC @() @[] @()\r\n}}}\r\n\r\nTypechecks in GHC 8.2.2 and 8.4.1, but not in GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 Bug.hs\r\n[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\n\r\nBug.hs:12:5: error:\r\n • Couldn't match type ‘()’ with ‘[]’\r\n Expected type: [()] -> ECC (() :: Constraint) [] ()\r\n Actual type: () [] -> ECC (() :: Constraint) () []\r\n • In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^^^^^^^^^^^^^^\r\n\r\nBug.hs:12:10: error:\r\n • Expected kind ‘* -> *’, but ‘()’ has kind ‘*’\r\n • In the type ‘()’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^\r\n\r\nBug.hs:12:14: error:\r\n • Expecting one more argument to ‘[]’\r\n Expected a type, but ‘[]’ has kind ‘* -> *’\r\n • In the type ‘[]’\r\n In the expression: ECC @() @[] @()\r\n In an equation for ‘f’: f = ECC @() @[] @()\r\n |\r\n12 | f = ECC @() @[] @()\r\n | ^^\r\n}}}\r\n\r\nThis is because the order of type variables for `ECC` has changed between GHC 8.4.1 and HEAD. In 8.4.1, it's\r\n\r\n{{{\r\n$ /opt/ghc/8.4.1/bin/ghci Bug.hs -XTypeApplications -fprint-explicit-foralls\r\nGHCi, version 8.4.0.20180209: 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\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (ctx :: Constraint) (f :: * -> *) a.\r\n ctx =>\r\n f a -> ECC ctx f a\r\n}}}\r\n\r\nIn GHC HEAD, however, it's:\r\n\r\n{{{\r\n$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -XTypeApplications -fprint-explicit-foralls\r\nGHCi, version 8.5.20180213: 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\nOk, one module loaded.\r\nλ> :type +v ECC\r\nECC\r\n :: forall (f :: * -> *) a (ctx :: Constraint).\r\n ctx =>\r\n f a -> ECC ctx f a\r\n}}}\r\n\r\nThis regression was introduced in fa29df02a1b0b926afb2525a258172dcbf0ea460 (Refactor ConDecl: Trac #14529).","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/14991GHC HEAD regression involving TYPEs in type families2019-07-07T18:14:46ZRyan ScottGHC HEAD regression involving TYPEs in type familiesThis program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type family Promote...This program typechecks on GHC 8.2.2 and 8.4.1:
```hs
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
type family Promote (k :: Type) :: Type
type family PromoteX (a :: k) :: Promote k
type family Demote (k :: Type) :: Type
type family DemoteX (a :: k) :: Demote k
-----
-- Type
-----
type instance Demote Type = Type
type instance Promote Type = Type
type instance DemoteX (a :: Type) = Demote a
type instance PromoteX (a :: Type) = Promote a
-----
-- Arrows
-----
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type instance Demote (a ~> b) = DemoteX a -> DemoteX b
type instance Promote (a -> b) = PromoteX a ~> PromoteX b
```
However, it fails to typecheck on GHC HEAD:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs
GHCi, version 8.5.20180401: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug ( Bug.hs, interpreted )
Bug.hs:34:34: error:
• Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’
• In the first argument of ‘(~>)’, namely ‘PromoteX a’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
Bug.hs:34:48: error:
• Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’
• In the second argument of ‘(~>)’, namely ‘PromoteX b’
In the type ‘PromoteX a ~> PromoteX b’
In the type instance declaration for ‘Promote’
|
34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b
| ^^^^^^^^^^
```
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ----------------------- |
| Version | 8.5 |
| 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 HEAD regression involving TYPEs in type families","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This program typechecks on GHC 8.2.2 and 8.4.1:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\n{-# LANGUAGE TypeOperators #-}\r\n{-# LANGUAGE UndecidableInstances #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\ntype family Promote (k :: Type) :: Type\r\ntype family PromoteX (a :: k) :: Promote k\r\n\r\ntype family Demote (k :: Type) :: Type\r\ntype family DemoteX (a :: k) :: Demote k\r\n\r\n-----\r\n-- Type\r\n-----\r\n\r\ntype instance Demote Type = Type\r\ntype instance Promote Type = Type\r\n\r\ntype instance DemoteX (a :: Type) = Demote a\r\ntype instance PromoteX (a :: Type) = Promote a\r\n\r\n-----\r\n-- Arrows\r\n-----\r\n\r\ndata TyFun :: Type -> Type -> Type\r\ntype a ~> b = TyFun a b -> Type\r\ninfixr 0 ~>\r\n\r\ntype instance Demote (a ~> b) = DemoteX a -> DemoteX b\r\ntype instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n}}}\r\n\r\nHowever, it fails to typecheck on GHC HEAD:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 --interactive Bug.hs\r\nGHCi, version 8.5.20180401: 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:34:34: error:\r\n • Expected a type, but ‘PromoteX a’ has kind ‘Promote (TYPE t0)’\r\n • In the first argument of ‘(~>)’, namely ‘PromoteX a’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n |\r\n34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n | ^^^^^^^^^^\r\n\r\nBug.hs:34:48: error:\r\n • Expected a type, but ‘PromoteX b’ has kind ‘Promote (TYPE t1)’\r\n • In the second argument of ‘(~>)’, namely ‘PromoteX b’\r\n In the type ‘PromoteX a ~> PromoteX b’\r\n In the type instance declaration for ‘Promote’\r\n |\r\n34 | type instance Promote (a -> b) = PromoteX a ~> PromoteX b\r\n | ^^^^^^^^^^\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15142GHC HEAD regression: tcTyVarDetails2019-07-07T18:14:05ZRyan ScottGHC HEAD regression: tcTyVarDetailsThis regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
...This regression prevents the `generic-lens` library from building. Here is a minimized test case:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
class ListTuple (tuple :: Type) (as :: [(k, Type)]) where
type ListToTuple as :: Type
```
On GHC 8.4.2, this compiles, but on GHC HEAD, it panics:
```
$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180511 for x86_64-unknown-linux):
tcTyVarDetails
co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable
pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var
```
<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 HEAD regression: tcTyVarDetails","status":"New","operating_system":"","component":"Compiler (Type checker)","related":[],"milestone":"8.6.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.5","keywords":["TypeFamilies","TypeInType,"],"differentials":[],"test_case":"","architecture":"","cc":[""],"type":"Bug","description":"This regression prevents the `generic-lens` library from building. Here is a minimized test case:\r\n\r\n{{{#!hs\r\n{-# LANGUAGE MultiParamTypeClasses #-}\r\n{-# LANGUAGE TypeFamilies #-}\r\n{-# LANGUAGE TypeInType #-}\r\nmodule Bug where\r\n\r\nimport Data.Kind\r\n\r\nclass ListTuple (tuple :: Type) (as :: [(k, Type)]) where\r\n type ListToTuple as :: Type\r\n}}}\r\n\r\nOn GHC 8.4.2, this compiles, but on GHC HEAD, it panics:\r\n\r\n{{{\r\n$ ~/Software/ghc/inplace/bin/ghc-stage2 Bug.hs[1 of 1] Compiling Bug ( Bug.hs, Bug.o )\r\nghc-stage2: panic! (the 'impossible' happened)\r\n (GHC version 8.5.20180511 for x86_64-unknown-linux):\r\n tcTyVarDetails\r\n co_aWx :: (k_aWt[tau:2] :: *) ~# (* :: *)\r\n Call stack:\r\n CallStack (from HasCallStack):\r\n callStackDoc, called at compiler/utils/Outputable.hs:1162:37 in ghc:Outputable\r\n pprPanic, called at compiler/basicTypes/Var.hs:497:22 in ghc:Var\r\n}}}","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15282Document how equality-bearing constructors are promoted in Core2019-07-07T18:13:27ZRyan ScottDocument how equality-bearing constructors are promoted in CoreIn [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this work...In [D4728](https://phabricator.haskell.org/D4728), Simon was utterly baffled as to how one could promote the `MkT` constructor in:
```hs
data T a where
MkT :: (a ~ Int) => T a
```
Richard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.
<details><summary>Trac metadata</summary>
| Trac field | Value |
| ---------------------- | ------------ |
| Version | 8.4.3 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | goldfire |
| Operating system | |
| Architecture | |
</details>
<!-- {"blocked_by":[],"summary":"Document how equality-bearing constructors are promoted in Core","status":"New","operating_system":"","component":"Compiler","related":[],"milestone":"8.8.1","resolution":"Unresolved","owner":{"tag":"Unowned"},"version":"8.4.3","keywords":["TypeInType"],"differentials":[],"test_case":"","architecture":"","cc":["goldfire"],"type":"Bug","description":"In Phab:D4728, Simon was utterly baffled as to how one could promote the `MkT` constructor in:\r\n\r\n{{{#!hs\r\ndata T a where\r\n MkT :: (a ~ Int) => T a\r\n}}}\r\n\r\nRichard knows the inner machinations of how this works (including what coercions are used in the Core that `'MkT` desugars to), but not many others do. Simon requested that Richard document this knowledge in a Note somewhere. This ticket exists to keep track of this request.","type_of_failure":"OtherFailure","blocking":[]} -->8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://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.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/15579topNormaliseType is wrong2019-07-07T18:04:02ZSimon Peyton JonestopNormaliseType is wrongI’m very puzzled about topNormaliseTYpe_maybe. Here it is:
```haskell
topNormaliseType_maybe env ty
= topNormaliseTypeX stepper mkTransCo ty
where
stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
tyFamStepper r...I’m very puzzled about topNormaliseTYpe_maybe. Here it is:
```haskell
topNormaliseType_maybe env ty
= topNormaliseTypeX stepper mkTransCo ty
where
stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
tyFamStepper rec_nts tc tys -- Try to step a type/data family
= let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
-- NB: It's OK to use normaliseTcArgs here instead of
-- normalise_tc_args (which takes the LiftingContext described
-- in Note [Normalising types]) because the reduceTyFamApp below
-- works only at top level. We'll never recur in this function
-- after reducing the kind of a bound tyvar.
case reduceTyFamApp_maybe env Representational tc ntys of
Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co)
_ -> NS_Done
```
I have two puzzlements
1. First, it seems utterly wrong to normalise the arguments using Representational. Consider
```haskell
F (N Int)
where newtype N x = [x]
```
> We don’t want to reduce `(N Int)` to `[Int]`, and then try reducing `(F [Int])`!! That is totally bogus. Surely we should use (the role-aware) `normalise_tc_args` here?
1. I have literally no clue what `Note [Normalising types]` is all about. Moreover there is no Lifting Context passed to `normalise_tc_args`, so I don’t know what this stuff about `LiftingContext` is about. Is this historical baggage?
Richard and I discussed this. (1) is a bug; for (2) the comment is misleading and should be deleted.
Richard will do these things -- and will add examples to the mysterious `Note [Normalising types]`8.6.1Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev