GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2024-03-25T19:13:15Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/24559Lambda with invisible type pattern fails to splice with TemplateHaskell2024-03-25T19:13:15ZRyan ScottLambda with invisible type pattern fails to splice with TemplateHaskellI am using GHC 9.10.1-alpha1, which introduces `@`-binders in more places in pattern contexts (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11109). Here is an example of an expression one can write with this feature:
```hs
{-# LA...I am using GHC 9.10.1-alpha1, which introduces `@`-binders in more places in pattern contexts (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11109). Here is an example of an expression one can write with this feature:
```hs
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
module Foo where
import Data.Kind
import Data.Proxy
f :: (forall (a :: Type). Proxy a) -> Proxy Bool
f k = k @Bool
g1 :: Proxy Bool
g1 = f (\ @a -> Proxy @a)
```
So far, so good. Now let's introduce a variant of `g1` where the expression is spliced in via `TemplateHaskell`:
```hs
g2 :: Proxy Bool
g2 = f $([| \ @a -> Proxy @a |])
```
I would expect this to typecheck just like `g1` does. And yet, it doesn't:
```
$ ghc-9.10 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:16:9: error: [GHC-14964]
• Invisible type pattern a has no associated forall
• In the first argument of ‘f’, namely ‘(\ @a -> Proxy @a)’
In the expression: f (\ @a -> Proxy @a)
In an equation for ‘g2’: g2 = f (\ @a -> Proxy @a)
|
16 | g2 = f $([| \ @a -> Proxy @a |])
| ^^^^^^^^^^^^^^^^^^^^^^^^
```9.10.1Simon Peyton JonesSimon Peyton Joneshttps://gitlab.haskell.org/ghc/ghc/-/issues/24557TypeAbstractions doesn't parse with \case, but does parse with \cases2024-03-28T08:53:38ZRyan ScottTypeAbstractions doesn't parse with \case, but does parse with \casesI am using GHC 9.10.1-alpha1, which introduces `@`-binders in more places in pattern contexts (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11109). Based on one of the test cases added in that MR, I discovered that `TypeAbstractio...I am using GHC 9.10.1-alpha1, which introduces `@`-binders in more places in pattern contexts (https://gitlab.haskell.org/ghc/ghc/-/merge_requests/11109). Based on one of the test cases added in that MR, I discovered that `TypeAbstractions` could be combined with `LambdaCase`, e.g.,
```hs
{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE TypeAbstractions #-}
module Foo where
import Data.Kind
f :: (forall (a :: Type). ()) -> ()
f k = k @Bool
g :: ()
g = f (\cases
@a -> ())
```
Great. What is surprising, however, is that if I change `\cases` to be `\case`:
```hs
g :: ()
g = f (\case
@a -> ())
```
Then GHC fails to parse it:
```
$ ghc-9.10 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:11:8: error: [GHC-06074]
Unexpected \case expression in function application:
\case
Suggested fixes:
• Use parentheses.
• Perhaps you intended to use BlockArguments
|
11 | g = f (\case
| ^
Foo.hs:11:8: error: [GHC-66228]
View pattern in expression context: \case @a -> ()
|
11 | g = f (\case
| ^^^^^...
```
This feels inconsistent, as I would expect that if `\cases` works, then `\case` should also work. Is this intended?https://gitlab.haskell.org/ghc/ghc/-/issues/24202DataToTag instances in signature files don't work2023-11-21T23:06:40ZMatthew Cravenclyring@gmail.comDataToTag instances in signature files don't work## Summary
Since !8912 landed, signature files are allowed to contain/request instances for the special `DataToTag` class. But these are not actually usable, and fail with a very unhelpful error message.
In principle there is no reason...## Summary
Since !8912 landed, signature files are allowed to contain/request instances for the special `DataToTag` class. But these are not actually usable, and fail with a very unhelpful error message.
In principle there is no reason it shouldn't be possible to support `DataToTag` instances in signatures, but doing so doesn't appear completely trivial and there seems to be little or no demand for this feature.
See also the test case `T15379-DataToTag`.https://gitlab.haskell.org/ghc/ghc/-/issues/24173`-Wunused-packages` overreports with alternative Preludes2023-12-04T16:33:50ZLeo Zhang`-Wunused-packages` overreports with alternative Preludes## Summary
Using an alternative Prelude (in my case, Relude) through `mixins` will cause `-Wunused-packages` to report that a package is unused when it is actually used. I suspect this might be related to https://gitlab.haskell.org/ghc/...## Summary
Using an alternative Prelude (in my case, Relude) through `mixins` will cause `-Wunused-packages` to report that a package is unused when it is actually used. I suspect this might be related to https://gitlab.haskell.org/ghc/ghc/-/issues/18563, which is also related to `mixins`.
## Steps to reproduce
1. Clone https://github.com/elldritch/cabal-unused-packages-mixin-repro and make sure you're running GHC 9.4.7.
2. Run `cabal build`.
You should see this error message:
```
$ cabal build
Build profile: -w ghc-9.4.7 -O1
In order, the following will be built (use -v for more details):
- cabal-unused-packages-mixin-repro-0.1.0.0 (lib) (file src/Example.hs changed)
Preprocessing library for cabal-unused-packages-mixin-repro-0.1.0.0..
Building library for cabal-unused-packages-mixin-repro-0.1.0.0..
<no location info>: error: [-Wunused-packages, -Werror=unused-packages]
The following packages were specified via -package or -package-id flags,
but were not needed for compilation:
- relude-1.2.1.0 (exposed by flag -package-id relude-1.2.1.0-ea787ea216b250f63edab15a196f92bee0e612410323d35bd7a6caf35e8a006b)
Error: cabal: Failed to build cabal-unused-packages-mixin-repro-0.1.0.0.
```
## Expected behavior
This warning should not be triggered, since Relude is being imported as the implicit Prelude.
## Environment
* GHC version used: 9.4.7
Optional:
* Operating System: Arch Linux
* System Architecture: x86_64Ben GamariBen Gamarihttps://gitlab.haskell.org/ghc/ghc/-/issues/23763`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1:...2023-09-11T13:21:22ZMikolaj Konarski`Nat` (in)equality transitivity or congruence regression in GHC 9.8.1-alpha1: Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/):
* clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d
* `cabal build`
* you get
```
src/HordeAd/Core/As...Repro with GHC 9.8.1-alpha1 and head.hackage (http://ghc.gitlab.haskell.org/head.hackage/):
* clone https://github.com/Mikolaj/horde-ad/commit/e76ff6c2f2b1fc53a00c6b78f74cb1ab8b94790d
* `cabal build`
* you get
```
src/HordeAd/Core/AstSimplify.hs:1192:9: error: [GHC-64725]
• Cannot satisfy: OS.Rank sh2 <= 1 + OS.Rank sh1
• In the first argument of ‘($)’, namely ‘astTransposeS @zsuccPerm’
In the second argument of ‘($)’, namely
‘astTransposeS @zsuccPerm $ astReplicateS @n v’
In the second argument of ‘($)’, namely
‘trustMeThisIsAPermutation @zsuccPerm
$ astTransposeS @zsuccPerm $ astReplicateS @n v’
|
1192 | $ astTransposeS @zsuccPerm $ astReplicateS @n v
```
It works fine with GHC <= 9.6 and also after patching it in the following way:
https://github.com/Mikolaj/horde-ad/commit/0417f413051f1739fe32cfaf7869755276171449
My guess is that previously GHC could deduce:
OS.Rank zsuccPerm <= 1 + OS.Rank sh1
from (note that `sh2` that GHC invents here in just `zsuccPerm` -- this obfuscation in error messages is already reported in one of my older tickets)
OS.Rank zsuccPerm :~: 1 + OS.Rank perm
and
OS.Rank perm <= OS.Rank sh1
but now it can't.
The issue may be in GHC itself or in how plugin `GHC.TypeLits.Normalise` has been updated to 9.8.1-alpha1, but I doubt the latter, because it's been updated on head.hackage by people that know what they are doing.
I haven't tried with HEAD of the github repo of `GHC.TypeLits.Normalise` and GHC 9.6, but I don't think `GHC.TypeLits.Normalise` has been modified vs the version on Hackage (`GHC.TypeLits.KnownNat.Solver` has been, but it seem unrelated).
CC: @christiaanbhttps://gitlab.haskell.org/ghc/ghc/-/issues/23692ApplicativeDo breaks typechecking2023-07-25T14:22:12ZSergey VinokurovApplicativeDo breaks typechecking## Summary
When enabling the `ApplicativeDo` extension the provided program ceases to typecheck. It does work in 9.4.5 and does work if I move `putStrLn` around or remove it entirely, which is surprising. Removing `ApplicativeDo` extens...## Summary
When enabling the `ApplicativeDo` extension the provided program ceases to typecheck. It does work in 9.4.5 and does work if I move `putStrLn` around or remove it entirely, which is surprising. Removing `ApplicativeDo` extension also helps but I'd like to get its effects in `parseCommandLine` function (omitted here for brevity).
## Steps to reproduce
Compile the following program.
Original program:
```haskell
{-# LANGUAGE ApplicativeDo #-}
module Main (main) where
import Control.Monad
data Command
= PolyCmd
| VanillaCmd
data CommonConfig = CommonConfig
{ ccVerbose :: Bool
}
parseCommandline :: IO (CommonConfig, Command)
parseCommandline = undefined
locateHelper :: FilePath -> IO (Maybe FilePath)
locateHelper = undefined
complexWrapper :: IO a -> IO a
complexWrapper = undefined
vanillaRun :: IO ()
vanillaRun = pure ()
polyRun :: (forall a. IO a -> IO a) -> IO ()
polyRun f = f $ pure ()
main :: IO ()
main = do
(config, cmd) <- parseCommandline
when (ccVerbose config) $
putStrLn "OK"
let wrapper :: IO a -> IO a
wrapper act = do
complexWrapper act
case cmd of
VanillaCmd -> wrapper vanillaRun
PolyCmd -> polyRun wrapper
```
```
$ ghc -c Main.hs
Main.hs:42:27: error: [GHC-25897]
• Couldn't match type ‘a’ with ‘()’
Expected: IO a -> IO a
Actual: IO () -> IO ()
‘a’ is a rigid type variable bound by
a type expected by the context:
forall a. IO a -> IO a
at Main.hs:42:27-33
• In the first argument of ‘polyRun’, namely ‘wrapper’
In the expression: polyRun wrapper
In a case alternative: PolyCmd -> polyRun wrapper
|
42 | PolyCmd -> polyRun wrapper
| ^^^^^^^
```
However this one does typecheck
```haskell
{-# LANGUAGE ApplicativeDo #-}
module Main (main) where
import Control.Monad
data Command
= PolyCmd
| VanillaCmd
data CommonConfig = CommonConfig
{ ccVerbose :: Bool
}
parseCommandline :: IO (CommonConfig, Command)
parseCommandline = undefined
locateHelper :: FilePath -> IO (Maybe FilePath)
locateHelper = undefined
complexWrapper :: IO a -> IO a
complexWrapper = undefined
vanillaRun :: IO ()
vanillaRun = pure ()
polyRun :: (forall a. IO a -> IO a) -> IO ()
polyRun f = f $ pure ()
main :: IO ()
main = do
(config, cmd) <- parseCommandline
let wrapper :: IO a -> IO a
wrapper act = do
when (ccVerbose config) $
putStrLn "OK"
complexWrapper act
case cmd of
VanillaCmd -> wrapper vanillaRun
PolyCmd -> polyRun wrapper
```
Commenting out `ApplicativeDo` also makes the original program typecheck.
## Expected behavior
Original program typechecks successfully with `ApplicativeDo` extension enabled.
## Environment
* GHC version used: 9.6.2
Optional:
* Operating System: Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/23322Backpack: Import standalone modules from indefinite packages in instancing mo...2023-07-02T23:06:56ZRodrigo MesquitaBackpack: Import standalone modules from indefinite packages in instancing modules failsSay I have the following modules and signatures in a cabal project
```haskell
module A where
data SomeUsefulThing = SomeUsefulThing
```
```haskell
signature B where
import A
someUsefulFun :: SomeUsefulThing -> ()
```
```haskell
module...Say I have the following modules and signatures in a cabal project
```haskell
module A where
data SomeUsefulThing = SomeUsefulThing
```
```haskell
signature B where
import A
someUsefulFun :: SomeUsefulThing -> ()
```
```haskell
module B.Instance where
import A
someUsefulFun :: SomeUsefulThing -> ()
someUsefulFun SomeUsefulThing = ()
```
Note that in B's signature and instance, `someUsefulFun` share the same type `SomeUsefulThing` imported from `A`.
```haskell
import A
import B
main = pure (someUsefulFun SomeUsefulThing)
```
```cabal
cabal-version: 3.4
name: ex2
version: 0.1.0.0
build-type: Simple
library pa
build-depends: base
exposed-modules: A
signatures: B
hs-source-dirs: pa
library pb
build-depends: base, ex2:pa
exposed-modules: B.Instance
hs-source-dirs: pb
library
exposed-modules: Main
build-depends: base, ex2:pa, ex2:pb
mixins: ex2:pa requires (B as B.Instance),
hs-source-dirs: main
```
When compiling this project, it fails with
```
<no location info>: error:
• Identifier ‘someUsefulFun’ has conflicting definitions in the module
and its hsig file
Main module: someUsefulFun ::
ex2-0.1.0.0:pa[B=<B>]:A.SomeUsefulThing -> ()
Hsig file: someUsefulFun :: A.SomeUsefulThing -> ()
The two types are different
• while checking that B.Instance implements signature B in ex2-0.1.0.0:pa[B=B.Instance]
```
The cause is `SomeUsefulThing`, in the context of `pa` is imported from `A`, but in the context of `pb`, is imported from `ex2:pa[B=<B>]:A`.
I think it should be possible to use the shared definition of `SomeUsefulThing`, since `A` is a completely standalone module (doesn't depend on any indefinite signatures). Even if it did, it is reasonable to think it should also work.
Is this a fundamental limitation or something we can overcome?
Many thanks.sheafsam.derbyshire@gmail.comsheafsam.derbyshire@gmail.comhttps://gitlab.haskell.org/ghc/ghc/-/issues/23228Cmm lint error in GHC.Bits when compiled without optimisation2023-07-30T17:31:59ZMatthew PickeringCmm lint error in GHC.Bits when compiled without optimisation
Repro, add the `OPTIONS_GHC` pragma to the top of `GHC.Bits`
```
{-# OPTIONS_GHC -O0 -}
```
```
./hadrian/build --flavour=validate -o_validate -j4 _validate/stage1/libraries/base/build/GHC/Bits.o
```
Gives the following Cmm lint e...
Repro, add the `OPTIONS_GHC` pragma to the top of `GHC.Bits`
```
{-# OPTIONS_GHC -O0 -}
```
```
./hadrian/build --flavour=validate -o_validate -j4 _validate/stage1/libraries/base/build/GHC/Bits.o
```
Gives the following Cmm lint error:
```
Cmm lint error:
in basic block c2E2
Shift operation MO_U_Shr W64 has out-of-range offset 64. This will result in undefined behavior
Program was:
{offset
c2CU: // global
_s1YF::P64 = R3; // CmmAssign
_s1YE::P64 = R2; // CmmAssign
if ((old + 0) - <highSp> < SpLim) (likely: False) goto c2CY; else goto c2CZ; // CmmCondBranch
c2CY: // global
R3 = _s1YF::P64; // CmmAssign
R2 = _s1YE::P64; // CmmAssign
R1 = $crotate2_r1Hc_closure; // CmmAssign
call (stg_gc_fun)(R3, R2, R1) args: 8, res: 0, upd: 8; // CmmCall
c2CZ: // global
I64[(young<c2CR> + 8)] = c2CR; // CmmStore
R1 = _s1YE::P64; // CmmAssign
if (R1 & 7 != 0) goto c2CR; else goto c2CS; // CmmCondBranch
c2CS: // global
call (I64[R1])(R1) returns to c2CR, args: 8, res: 8, upd: 8; // CmmCall
c2CR: // global
_s1YG::P64 = R1; // CmmAssign
_s1YH::I64 = I64[_s1YG::P64 + 7]; // CmmAssign
I64[(young<c2CX> + 8)] = c2CX; // CmmStore
R1 = _s1YF::P64; // CmmAssign
if (R1 & 7 != 0) goto c2CX; else goto c2D1; // CmmCondBranch
c2D1: // global
call (I64[R1])(R1) returns to c2CX, args: 8, res: 8, upd: 8; // CmmCall
c2CX: // global
_s1YI::P64 = R1; // CmmAssign
_s1YJ::I64 = I64[_s1YI::P64 + 7]; // CmmAssign
_c2D6::I64 = _s1YJ::I64 & 63; // CmmAssign
_s1YK::I64 = _c2D6::I64; // CmmAssign
switch [-9223372036854775808 .. 9223372036854775807] _s1YK::I64 {
case 0 : goto c2DK;
default: {goto c2Db;}
} // CmmSwitch
c2DK: // global
// slowCall
I64[(young<c2DO> + 8)] = c2DO; // CmmStore
R2 = 1; // CmmAssign
R1 = isTrue#_closure; // CmmAssign
call stg_ap_n_fast(R2,
R1) returns to c2DO, args: 8, res: 8, upd: 8; // CmmCall
c2DO: // global
_s1YQ::P64 = R1; // CmmAssign
// slow_call for isTrue#_closure with pat stg_ap_n
_c2Ec::P64 = _s1YQ::P64 & 7; // CmmAssign
switch [1 .. 2] _c2Ec::P64 {
case 1 : goto c2E0;
case 2 : goto c2E7;
} // CmmSwitch
c2E7: // global
Hp = Hp + 16; // CmmAssign
if (Hp > HpLim) (likely: False) goto c2Ea; else goto c2E9; // CmmCondBranch
c2Ea: // global
HpAlloc = 16; // CmmAssign
R1 = _s1YQ::P64; // CmmAssign
call stg_gc_unpt_r1(R1) returns to c2DO, args: 8, res: 8, upd: 8; // CmmCall
c2E9: // global
// allocHeapClosure
I64[Hp - 8] = W#_con_info; // CmmStore
I64[Hp] = _s1YH::I64; // CmmStore
_c2E6::P64 = Hp - 7; // CmmAssign
R1 = _c2E6::P64; // CmmAssign
call (P64[(old + 8)])(R1) args: 8, res: 0, upd: 8; // CmmCall
c2E0: // global
Hp = Hp + 16; // CmmAssign
if (Hp > HpLim) (likely: False) goto c2E3; else goto c2E2; // CmmCondBranch
c2E3: // global
HpAlloc = 16; // CmmAssign
R1 = _s1YQ::P64; // CmmAssign
call stg_gc_unpt_r1(R1) returns to c2DO, args: 8, res: 8, upd: 8; // CmmCall
c2E2: // global
_c2DS::I64 = _s1YH::I64 >> 64; // CmmAssign
_s1YR::I64 = _c2DS::I64; // CmmAssign
_c2DV::I64 = _s1YH::I64 | _s1YR::I64; // CmmAssign
_s1YS::I64 = _c2DV::I64; // CmmAssign
// allocHeapClosure
I64[Hp - 8] = W#_con_info; // CmmStore
I64[Hp] = _s1YS::I64; // CmmStore
_c2DY::P64 = Hp - 7; // CmmAssign
R1 = _c2DY::P64; // CmmAssign
call (P64[(old + 8)])(R1) args: 8, res: 0, upd: 8; // CmmCall
c2Db: // global
// slowCall
I64[(young<c2Df> + 8)] = c2Df; // CmmStore
R2 = 0; // CmmAssign
R1 = isTrue#_closure; // CmmAssign
call stg_ap_n_fast(R2,
R1) returns to c2Df, args: 8, res: 8, upd: 8; // CmmCall
c2Df: // global
_s1YL::P64 = R1; // CmmAssign
// slow_call for isTrue#_closure with pat stg_ap_n
_c2Eb::P64 = _s1YL::P64 & 7; // CmmAssign
switch [1 .. 2] _c2Eb::P64 {
case 1 : goto c2Dx;
case 2 : goto c2DE;
} // CmmSwitch
c2DE: // global
Hp = Hp + 16; // CmmAssign
if (Hp > HpLim) (likely: False) goto c2DH; else goto c2DG; // CmmCondBranch
c2DH: // global
HpAlloc = 16; // CmmAssign
R1 = _s1YL::P64; // CmmAssign
call stg_gc_unpt_r1(R1) returns to c2Df, args: 8, res: 8, upd: 8; // CmmCall
c2DG: // global
// allocHeapClosure
I64[Hp - 8] = W#_con_info; // CmmStore
I64[Hp] = _s1YH::I64; // CmmStore
_c2DD::P64 = Hp - 7; // CmmAssign
R1 = _c2DD::P64; // CmmAssign
call (P64[(old + 8)])(R1) args: 8, res: 0, upd: 8; // CmmCall
c2Dx: // global
Hp = Hp + 16; // CmmAssign
if (Hp > HpLim) (likely: False) goto c2DA; else goto c2Dz; // CmmCondBranch
c2DA: // global
HpAlloc = 16; // CmmAssign
R1 = _s1YL::P64; // CmmAssign
call stg_gc_unpt_r1(R1) returns to c2Df, args: 8, res: 8, upd: 8; // CmmCall
c2Dz: // global
_c2Dj::I64 = 64 - _s1YK::I64; // CmmAssign
_s1YN::I64 = _c2Dj::I64; // CmmAssign
_c2Dm::I64 = _s1YH::I64 >> _s1YN::I64; // CmmAssign
_s1YO::I64 = _c2Dm::I64; // CmmAssign
_c2Dp::I64 = _s1YH::I64 << _s1YK::I64; // CmmAssign
_s1YM::I64 = _c2Dp::I64; // CmmAssign
_c2Ds::I64 = _s1YM::I64 | _s1YO::I64; // CmmAssign
_s1YP::I64 = _c2Ds::I64; // CmmAssign
// allocHeapClosure
I64[Hp - 8] = W#_con_info; // CmmStore
I64[Hp] = _s1YP::I64; // CmmStore
_c2Dv::P64 = Hp - 7; // CmmAssign
R1 = _c2Dv::P64; // CmmAssign
call (P64[(old + 8)])(R1) args: 8, res: 0, upd: 8; // CmmCall
}
<no location info>: error:
Compilation had errors
Command failed
Build failed.
```https://gitlab.haskell.org/ghc/ghc/-/issues/23040`OverloadedRecordDot` and `COLUMN`-pragmas don't play nice together2023-02-28T15:27:27ZSimon Hengelsol@typeful.net`OverloadedRecordDot` and `COLUMN`-pragmas don't play nice together## Summary
`foo.foo` is accepted while `foo{-# COLUMN 23 #-}.foo` results in a parse error.
This is surprising from a users perspective and can break `OverloadedRecordDot` with source-to-source transformations / pre-processors (as it d...## Summary
`foo.foo` is accepted while `foo{-# COLUMN 23 #-}.foo` results in a parse error.
This is surprising from a users perspective and can break `OverloadedRecordDot` with source-to-source transformations / pre-processors (as it does for me).
## Steps to reproduce
```
{-# LANGUAGE NoFieldSelectors #-}
{-# LANGUAGE OverloadedRecordDot #-}
data Foo = Foo { foo :: String }
foo :: Foo
foo = Foo "foo"
main :: IO ()
main = do
putStrLn foo.foo -- works
putStrLn foo{-# COLUMN 23 #-}.foo -- parse error
```
## Expected behavior
Both `foo.foo` and `foo{-# COLUMN 23 #-}.foo` should be accepted.
## Investigation
`foo.foo` is tokenized to:
[ITvarid "foo", ITproj False, ITvarid "bar"]
However, `foo{-# COLUMN 23 #-}.foo` is tokenized to:
[ITvarid "foo", ITproj True, ITvarid "bar"]
So from what I understand, even though this manifests as a parse error, the bug is actually in the lexer.
## Environment
* GHC version used: 9.6.0.20230111
Optional:
* Operating System: Linux
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc/-/issues/21376Type synonym with forall causes point-free code to not be equivalent2022-04-12T21:16:58ZpbrisbinType synonym with forall causes point-free code to not be equivalent## Summary
In GHC 9.0.2, it seems that using a point-free style doesn't
work when a certain kind of `type` is involved.
This fails to compile (full details below):
```hs
limitRetries :: Natural -> RetryPolicy
limitRetries = Retry.limi...## Summary
In GHC 9.0.2, it seems that using a point-free style doesn't
work when a certain kind of `type` is involved.
This fails to compile (full details below):
```hs
limitRetries :: Natural -> RetryPolicy
limitRetries = Retry.limitRetries . fromIntegral
-- Given,
-- Retry.limitRetries :: Int -> RetryPolicy
-- type RetryPolicy = forall m. RetryPolicyM m
```
While this works fine:
```hs
limitRetries :: Natural -> RetryPolicy
limitRetries x = Retry.limitRetries $ fromIntegral x
```
As a relatively compiler-naive Haskell user, I wouldn't expect code with
and without a point here to behave any differently, so I'm reporting this
as a bug.
Also, HLint will automatically eta-reduce away a point, so this is a new avenue by which
it can break your code.
## Steps to reproduce
This error first hit me when upgrading a project using the `retry` library,
so I've pared down my repro from there. I'm also using `stack` because it
makes it trivial to ensure someone can run this at all the exact versions
as I'm seeing.
**repro.hs**
```hs
{-# LANGUAGE RankNTypes #-}
module Control.Retry
( main
) where
import Prelude
import Numeric.Natural
newtype RetryPolicyM m = RetryPolicyM { getRetryPolicyM :: () -> m (Maybe Int) }
type RetryPolicy = forall m . Monad m => RetryPolicyM m
limitRetries :: Int -> RetryPolicy
limitRetries = undefined
limitRetries' :: Natural -> RetryPolicy
limitRetries' = limitRetries . fromIntegral
main :: IO ()
main = putStrLn "hi"
```
```console
% stack --resolver lts-19.3 runhaskell -- repro.hs
repro.hs:16:16: error:
• Couldn't match expected type ‘Int -> RetryPolicy’
with actual type ‘a0’
Cannot instantiate unification variable ‘a0’
with a type involving polytypes: Int -> RetryPolicy
• In the expression: undefined
In an equation for ‘limitRetries’: limitRetries = undefined
|
16 | limitRetries = undefined
| ^^^^^^^^^
repro.hs:19:17: error:
• Couldn't match type ‘c0’ with ‘RetryPolicy’
Expected: Int -> c0
Actual: Int -> RetryPolicy
Cannot instantiate unification variable ‘c0’
with a type involving polytypes: RetryPolicy
• In the first argument of ‘(.)’, namely ‘limitRetries’
In the expression: limitRetries . fromIntegral
In an equation for ‘limitRetries'’:
limitRetries' = limitRetries . fromIntegral
|
19 | limitRetries' = limitRetries . fromIntegral
```
## Expected behavior
The code should compile.
GHC 8.10 does not exhibit this behavior:
```console
% stack --resolver lts-18.28 runhaskell -- repro.hs
hi
```
With GHC 9, you have to add points to both of these:
```diff
- limitRetries = undefined
+ limitRetries x = undefined x
```
```diff
- limitRetries' = limitRetries . fromIntegral
+ limitRetries' x = limitRetries $ fromIntegral x
```
```console
% stack --resolver lts-19.3 runhaskell -- repro.hs
hi
```
## Environment
* GHC version used: 9.0.2 and 9.2.2
Optional:
* Operating System: Arch Linux
* System Architecture:
```console
% uname -a
Linux prince 5.16.14-arch1-1 #1 SMP PREEMPT Fri, 11 Mar 2022 17:40:36 +0000 x86_64 GNU/Linux
```https://gitlab.haskell.org/ghc/ghc/-/issues/21309Order dependence in type checking with the monomorphism restriction2022-04-25T01:39:53ZRichard Eisenbergrae@richarde.devOrder dependence in type checking with the monomorphism restrictionThe order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes...The order in which GHC type-checks definitions can change the outcome of type-checking when the monomorphism restriction is involved. This is because the monomorphism restriction affects all variables mentioned in a constraint; sometimes, though, a constraint can be eagerly solved, making it disappear (and thus not affecting any variables).
A nested example:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug where
class C a b where
method :: a -> b -> ()
instance C Char b where
method _ _ = ()
f1 x = let g = \y -> method x y in
(x : "hi", (g True, g Nothing))
f2 x = (x : "hi",
let g = \y -> method x y in
(g True, g Nothing))
```
`f1` is rejected, as `method x y` gives rise to `[W] C alpha beta`, which cannot be solved. Then, `g` is not generalised, so we get `g :: beta -> ()`, which is not general enough for its two usages.
`f2` is accepted, as `method x y` gives rise to `[W] C Char beta`, easily solved by the instance. No MR happens.
A top-level example:
```hs
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Bug2 where
x = 5
class C a b where
method :: a -> b -> ()
instance C Int b where
method _ _ = ()
x2 :: (Int, ((), ()))
x2 = (x + 1, (g True, g 'x')) -- remove references to 'g' to allow module to be accepted
g = \y -> method x y
x3 :: ((), ())
x3 = (g True, g 'x')
```
This is rejected. Note that `x2` depends on `g`, and thus `g` is type-checked first -- critically, before we know that `x :: Int`. So the MR kicks in and prevents generalisation. However if we change to `x2 = (x + 1, ((), ()))`, then the module is accepted: `x2` gets seen first, we learn that `x :: Int`, and then there is no constraint to prevent generalisation in `g`. The two different uses in `x3` are accepted.
I don't think this will be easy to fix: we would somehow need to delay the computation of whether or not to generalise, and that seems Very Hard. Maybe this just gets filed in the user manual under `FlexibleInstances` and how flexibility can sometimes cause trouble? Not sure. Note that "let should not be generalised" is not enough here, because the problem can manifest at top-level.
This is based on a conversation with @simonpj this morning; credit to him for outlining the problem.https://gitlab.haskell.org/ghc/ghc/-/issues/21210Quantified constraint should be accepted in RHS of type family equation2022-03-15T15:33:45ZRichard Eisenbergrae@richarde.devQuantified constraint should be accepted in RHS of type family equationThis is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Ch...This is rejected, but it shouldn't be:
```hs
{-# LANGUAGE QuantifiedConstraints, DataKinds, TypeFamilies #-}
module Bug4 where
import Data.Kind
newtype Phant p = MkPhant Int
deriving Eq
f1 :: forall p. (forall x. Eq (p x)) => p Char -> p Double -> Bool
f1 p1 p2 = p1 == p1 && p2 == p2
type ForallEq p = forall x. Eq (p x)
f2 :: ForallEq p => p Char -> p Double -> Bool
f2 p1 p2 = p1 == p1 && p2 == p2
type ForallEqs :: [Type -> Type] -> Constraint
type family ForallEqs ps where
ForallEqs '[] = ()
ForallEqs (p : ps) = (ForallEq p, ForallEqs ps)
```
The `forall` in a quantified constraint is really a different `forall` than the one used in normal types, and it should be acceptable in the RHS of a type family equation.https://gitlab.haskell.org/ghc/ghc/-/issues/20926Inconsistency between SAKs and inference2022-01-11T15:34:37ZSimon Peyton JonesInconsistency between SAKs and inferenceConsider
```
{-# LANGUAGE CUSKs, TypeFamilies, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}
module Foo where
import Data.Kind
class C f where
type S (f :: turtle)
type T f
```
This is accepted today. ...Consider
```
{-# LANGUAGE CUSKs, TypeFamilies, EmptyDataDecls, PolyKinds, KindSignatures, StandaloneKindSignatures #-}
module Foo where
import Data.Kind
class C f where
type S (f :: turtle)
type T f
```
This is accepted today. But try adding a stand-alone kind signature (with the correct kind!):
```
type C :: wombat -> Constraint
```
and the same program is rejected with
```
Foo.hs:10:4: error:
• Expected kind ‘wombat’, but ‘f’ has kind ‘turtle’
‘turtle’ is a rigid type variable bound by
the associated type family declaration for ‘S’
at Foo.hs:10:12-22
‘wombat’ is a rigid type variable bound by
the associated type family declaration for ‘S’
at Foo.hs:7:11-30
• In the associated type family declaration for ‘S’
|
10 | type S (f :: turtle)
| ^^^^^^^^^^^^^^^^^^^^
```
This seems inconsistent.
## Diagnosis
The reason this happens with a standalone kind signature
is because `kcCheckDeclHeader_sig` looks at
* the kind signature `C :: wombat -> Constraint`,
* the class header for C, namely `class C f where`,
and gives C the final skolem tyvars `[wombat, f::wombat]`.
Then `check_initial_kind_assoc` uses the CUSK strategy to kind-check S; and that in turn
uses a skolem for `turtle`, which doesn't unify with `wombat`.
On the other hand, without the standalone kind signature we accept it because we kind-check
the class and associated types together, rather than doing the class first and then the
associated types.
## Discussion
Consider a CUSK version of the same program:
```
class C (f :: turtle) where
type S (f :: wombat) :: Type
```
This is rejected today, with the same message as above, on the grounds that `wombat` is a local alias for `turtle`.
This treatment is inconsistent with the term level where we allow
```
f1 :: forall a. a -> blah
f1 (x :: b) = ... -- b is a local alias for a
```
On the other hand, we also reject
```
data T (a :: p) (b :: q) = MkT (SameKind a b)
```
where `SameKind :: k -> k -> Type`. You could argue that `p` and `q` are both aliases for the same
kind variable (`k`? `p`?); and that would be consistent with the term level where we allow
```
f2 :: forall a. a -> a -> blah
f2 (x :: b) (y :: c) = ... -- b and c are both local aliases for a.
```
But I hate the definition of `T` because it looks so outright misleading. (I hate `f2` as well, just not so much.)
The principle is, I think, that variables brought into scope simultaneously should not be aliases for each other.
Nested scopes are a different matter.
## Conclusion
I'm content with the treatment for
* inference (right at the top_)
* CUSKs (rejecting aliases)
but not with that for standalone kind signatures (as above). Given
```
type C :: wombat -> Constraint
class C f where
type S (f :: turtle)
type T f
```
I think we should accept this, with `turtle` as the name of the scoped variable.https://gitlab.haskell.org/ghc/ghc/-/issues/20805Take a Quick Look at lists2021-12-22T14:05:05ZRichard Eisenbergrae@richarde.devTake a Quick Look at listsI want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of usin...I want to make a video about Quick Look. But I also want it to have more content than just the venerable `head ids`. So I thought a bit about what would make a nice use case for impredicative polymorphism. I came up with the idea of using `forall a. Tree a -> Maybe a` as the type of indices into a tree structure. I could now search in one tree for a value that satisfies a predicate returning a `forall a. Tree a -> Maybe a` to then retrieve a corresponding value (if the tree has the right shape) in another tree. Here is the code:
```hs
data Tree a
= Leaf a
| Node (Tree a) a (Tree a)
deriving (Show, Functor)
type TreeIndex = forall a. Tree a -> Maybe a
lookupTree :: forall a. (a -> Bool) -> Tree a -> Maybe TreeIndex
lookupTree p = go
where
go :: Tree a -> Maybe TreeIndex
go (Leaf x)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = Nothing
go (Node left x right)
| p x = Just (\case Leaf y -> Just y
Node _ y _ -> Just y)
| otherwise = asum [go left, go right] -- (go left : go right : [])
```
(This doesn't work, as written, because the last line just returns the `TreeIndex` from the recursive call. But never mind this.)
(NB to GHC aficionados: `asum` is the same as GHC's `firstJusts`.)
What's sad is that the last line fails to type-check. However, if I remove the list argument and replace it with the commented-out cons-and-nil argument, all is well. This is because GHC doesn't take a Quick Look at lists. But it really should. And probably tuples, too.https://gitlab.haskell.org/ghc/ghc/-/issues/20318GHC complains about impredicativity in type synonym for a quantified constraint2021-09-07T14:37:54ZRichard Eisenbergrae@richarde.devGHC complains about impredicativity in type synonym for a quantified constraintIf I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps yo...If I say
```hs
{-# LANGUAGE ConstraintKinds, QuantifiedConstraints #-}
module Bug where
type T b = (Ord b, forall a. Eq a)
```
then GHC HEAD says
```
Bug.hs:5:1: error:
• Illegal polymorphic type: forall a. Eq a
Perhaps you intended to use ImpredicativeTypes
• In the type synonym declaration for ‘T’
|
5 | type T b = (Ord b, forall a. Eq a)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Note that `T` defines a *constraint* synonym, not a type synonym. Accordingly, `QuantifiedConstraints` should be enough to accept this definition.
Inspired by https://mail.haskell.org/pipermail/haskell-cafe/2021-August/134388.htmlhttps://gitlab.haskell.org/ghc/ghc/-/issues/20113Should we allow a newtype with a representation-polymorphic field with NoFiel...2022-06-11T06:47:37Zsheafsam.derbyshire@gmail.comShould we allow a newtype with a representation-polymorphic field with NoFieldSelectors?The following newtype declaration is accepted:
```haskell
{-# LANGUAGE PolyKinds, UnliftedNewtypes#-}
import GHC.Exts
newtype X (a :: TYPE rep) = MkX a
```
However, the following is rejected:
```haskell
{-# LANGUAGE PolyKinds, Unlift...The following newtype declaration is accepted:
```haskell
{-# LANGUAGE PolyKinds, UnliftedNewtypes#-}
import GHC.Exts
newtype X (a :: TYPE rep) = MkX a
```
However, the following is rejected:
```haskell
{-# LANGUAGE PolyKinds, UnliftedNewtypes, NoFieldSelectors #-}
import GHC.Exts
newtype Y (a :: TYPE rep) = MkY { y_fld :: a }
```
```
A representation-polymorphic type is not allowed here:
Type: a
Kind: TYPE rep
In the type of binder `$sel:y_fld:MkY'
|
4 | newtype Y (a :: TYPE rep) = MkY { y_fld :: a }
| ^^^^^
```
The problem is that the field selector is still generated internally (whence the mangled selector name `$sel:y_fld:MkY` leaking out into the error message), which runs into trouble with the representation polymorphism checks.
I'm not sure exactly what to do. We could continue to reject the program (possibly improving the error message); we could not generate the field selector at all; or we could somehow attempt to generate a representation polymorphic selector which must be representation-monomorphic at use-sites.
cc-ing @adamgundry and @simonpj for thoughts.https://gitlab.haskell.org/ghc/ghc/-/issues/19743Core Lint error (From-kind of Cast differs from kind of enclosed type) with T...2023-07-16T20:35:54ZRyan ScottCore Lint error (From-kind of Cast differs from kind of enclosed type) with TH-generated data typeThe following program will produce a Core Lint error when compiled:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE St...The following program will produce a Core Lint error when compiled:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind (Constraint, Type)
import Language.Haskell.TH hiding (Type)
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type SameKind :: k -> k -> Constraint
type SameKind a b = ()
type Const :: Type -> Type -> Type
type family Const x y where
Const x _ = x
type Wat :: forall (x :: Type) -> Const Type x -> Type -> Const Type x
type Wat x y z = Bool
{-
data WatSym2 (x :: Type) (y :: Const Type x) :: (~>) Type (Const Type x)
where
WatSym2KindInference :: forall x y z f.
SameKind (Apply (WatSym2 x y) z) (Wat x y z) =>
WatSym2 x y f
-}
$(do let watSym2 = mkName "WatSym2"
watSym2KindInference = mkName "WatSym2KindInference"
x <- newName "x"
y <- newName "y"
z <- newName "z"
f <- newName "f"
let d = DataD [] watSym2 [ kindedTV x (ConT ''Type), kindedTV y (ConT ''Const `AppT` ConT ''Type `AppT` VarT x) ]
(Just (InfixT (ConT ''Type) ''(~>) (ConT ''Const `AppT` ConT ''Type `AppT` VarT x)))
[ ForallC [ PlainTV x SpecifiedSpec
, PlainTV y SpecifiedSpec
-- , KindedTV y SpecifiedSpec (ConT ''Const `AppT` ConT ''Type `AppT` VarT x)
, PlainTV z SpecifiedSpec
, PlainTV f SpecifiedSpec
]
[ConT ''SameKind `AppT` (ConT ''Apply `AppT` (ConT watSym2 `AppT` VarT x `AppT` VarT y) `AppT` VarT z)
`AppT` (ConT ''Wat `AppT` VarT x `AppT` VarT y `AppT` VarT z)]
(GadtC [watSym2KindInference] [] (ConT watSym2 `AppT` VarT x `AppT` VarT y `AppT` VarT f))
]
[]
pure [d])
```
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs -dcore-lint -dno-typeable-binds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
*** Core Lint errors : in result of CorePrep ***
Bug.hs:43:2: warning:
From-kind of Cast differs from kind of enclosed type
From-kind: Const (*) x_a30I
Kind of enclosed type: *
Actual enclosed type: y_a30J
Coercion used in cast: Sym (D:R:Const[0] <*>_N <x_a30I>_N)
In the type of a binder: WatSym2KindInference
In the type ‘forall {x} {y :: Const (*) x}
{a :: TyFun (*) (Const (*) x)} {z} {f :: TyFun (*) (*)}.
(y ~# (y |> Sym (D:R:Const[0] <*>_N <x>_N)))
-> (a ~# (f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N))
-> SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N)
-> WatSym2 x y a’
Substitution: [TCvSubst
In scope: InScope {z_X0 f_X1 x_a30I y_a30J a_a31O}
Type env: [X0 :-> z_X0, X1 :-> f_X1, a30I :-> x_a30I,
a30J :-> y_a30J, a31O :-> a_a31O]
Co env: []]
*** Offending Program ***
$WWatSym2KindInference [InlPrag=INLINE[final] CONLIKE]
:: forall x y z (f :: TyFun (*) (*)).
SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N (D:R:Const[0] <*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N) =>
WatSym2
x
(y |> Sym (D:R:Const[0] <*>_N <x>_N))
(f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N)
[GblId[DataConWrapper],
Arity=1,
Caf=NoCafRefs,
Str=<L,U>,
Unf=OtherCon []]
$WWatSym2KindInference
= \ (@x_a30I)
(@y_a30J)
(@z_X0)
(@(f_X1 :: TyFun (*) (*)))
(dt_s325 [Occ=Once1]
:: SameKind
(Apply
(WatSym2
x_a30I (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N
<x_a30I>_N))_N
%<'Many>_N ->_N <*>_N)
z_X0)
(Wat
x_a30I
(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
z_X0 |> D:R:Const[0] <*>_N <x_a30I>_N)) ->
WatSym2KindInference
@x_a30I
@(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
@(f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)
@z_X0
@f_X1
@~(<(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))>_N
:: (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
@~(<(f_X1 |> (TyFun
<*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)>_N
:: (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N)
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
dt_s325
WatSym2KindInference [InlPrag=NOUSERINLINE CONLIKE]
:: forall {x} {y :: Const (*) x} {a :: TyFun (*) (Const (*) x)} {z}
{f :: TyFun (*) (*)}.
(y ~# (y |> Sym (D:R:Const[0] <*>_N <x>_N)))
-> (a ~# (f |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x>_N)))_N))
-> SameKind
(Apply
(WatSym2 x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) |> (TyFun
<*>_N
(D:R:Const[0] <*>_N <x>_N))_N
%<'Many>_N ->_N <*>_N)
z)
(Wat x (y |> Sym (D:R:Const[0] <*>_N <x>_N)) z |> D:R:Const[0]
<*>_N <x>_N)
-> WatSym2 x y a
[GblId[DataCon], Arity=3, Caf=NoCafRefs, Unf=OtherCon []]
WatSym2KindInference
= \ (@x_a30I)
(@(y_a30J :: Const (*) x_a30I))
(@(a_a31O :: TyFun (*) (Const (*) x_a30I)))
(@z_X0)
(@(f_X1 :: TyFun (*) (*)))
(eta_B0
:: y_a30J ~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
(eta_B1
:: a_a31O
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
(eta_B2 [Occ=Once1]
:: SameKind
(Apply
(WatSym2
x_a30I (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)) |> (TyFun
<*>_N
(D:R:Const[0]
<*>_N
<x_a30I>_N))_N
%<'Many>_N ->_N <*>_N)
z_X0)
(Wat
x_a30I
(y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N))
z_X0 |> D:R:Const[0] <*>_N <x_a30I>_N)) ->
WatSym2KindInference
@x_a30I
@y_a30J
@a_a31O
@z_X0
@f_X1
@~(eta_B0
:: y_a30J ~# (y_a30J |> Sym (D:R:Const[0] <*>_N <x_a30I>_N)))
@~(eta_B1
:: a_a31O
~# (f_X1 |> (TyFun <*>_N (Sym (D:R:Const[0] <*>_N <x_a30I>_N)))_N))
eta_B2
*** End of Offense ***
<no location info>: error:
Compilation had errors
```
Curiously, the Core Lint error goes away if you do either of the following:
1. Replace the Template Haskell–generated version of `WatSym2` with the hand-written version that is commented-out above.
2. Replace the `, PlainTV y SpecifiedSpec` line with the ``, KindedTV y SpecifiedSpec (ConT ''Const `AppT` ConT ''Type `AppT` VarT x)`` line below it that is commented out.
Because Template Haskell appears to be critical to triggering this bug, I suspect that this may be related to #11812 or #17537. The error here is different than what is seen in those issues, however, so to be on the safe side, I decided to open a dedicated issue for this.https://gitlab.haskell.org/ghc/ghc/-/issues/19726Unexpected type-checking behavior with let and DataKinds2021-05-10T12:28:34ZbenjaminUnexpected type-checking behavior with let and DataKinds## Motivation
When playing around with the code for known-length vectors from #19722, I noticed following behavior in the type-checker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a ...## Motivation
When playing around with the code for known-length vectors from #19722, I noticed following behavior in the type-checker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a -> a
last (x :> Nil) = x
last (_ :> xs) = case xs of x' :> xs' -> last xs
--last (_ :> xs) = let (x' :> xs') = xs in last xs
--last (_ :> xs) = let (x' :> xs') = xs in last (x' :> xs')
```
The main issue here is that we can't just write `last (_ :> xs) = last xs`, because then GHC can't verify that the type of `xs` is really `Vec (Succ n) a`.
So the workaround is to let GHC know that `xs` is really non-empty in this second case.
The first version of the case `_ :> xs` using a case-expression compiles fine, but the two version implemented using let-expressions don't type-check.
I lack an in-depth understanding of the type-checker or even the DataKinds extension, but I think the 3 versions are semantically identical.
## Proposal
Make all 3 versions type-check.https://gitlab.haskell.org/ghc/ghc/-/issues/19312Unbound record/field names in Template Haskell Quotes2021-04-07T19:55:24ZAdam GundryUnbound record/field names in Template Haskell QuotesIn a Template Haskell expression quotation, unbound variables and constructors are allowed, and are represented using `UnboundVarE`. However unbound names are not permitted in record construction (`RecConE`) or update (`RecUpdE`), and le...In a Template Haskell expression quotation, unbound variables and constructors are allowed, and are represented using `UnboundVarE`. However unbound names are not permitted in record construction (`RecConE`) or update (`RecUpdE`), and lead to scope errors in the quotation. This leads to strangely inconsistent behaviour:
```
GHCi, version 8.6.5: http://www.haskell.org/ghc/ :? for help
Prelude> :set -XTemplateHaskellQuotes
Prelude> import Language.Haskell.TH.Syntax as TH
Prelude TH> unQ [| foo |]
UnboundVarE foo
Prelude TH> unQ [| Foo |]
UnboundVarE Foo
Prelude TH> unQ [| Foo {} |]
<interactive>:5:8: error:
• Not in scope: data constructor ‘Foo’
• In the Template Haskell quotation [| Foo {} |]
Prelude TH> unQ [| Foo { foo = bar } |]
<interactive>:6:8: error:
• Not in scope: data constructor ‘Foo’
• In the Template Haskell quotation [| Foo {foo = bar} |]
<interactive>:6:14: error:
• Not in scope: ‘foo’
• In the Template Haskell quotation [| Foo {foo = bar} |]
Prelude TH> unQ [| Just { pi = bar } |]
RecConE GHC.Maybe.Just [(GHC.Float.pi,UnboundVarE bar)]
```
It seems odd that:
* `Foo` is accepted but `Foo {}` is not.
* `Foo { foo = bar }` leads to not-in-scope errors for `Foo` and `foo` but not `bar`.
* `Just { pi = bar }` is accepted even though it is complete nonsense, because `Just` is not a record constructor and `pi` is not a field.
I'm not sure what the right behaviour is here. One possibility would be to drop `UnboundVarE` and instead add a constructor to `Name` for unbound names, which would allow us to represent arbitrary expressions involving out-of-scope names.
Thanks to @edsko for highlighting this. I've tested that this behaviour occurs with 8.6.5, 8.10.2 and a relatively recent HEAD.https://gitlab.haskell.org/ghc/ghc/-/issues/19285Core lint error (with flags: -O2 -fobject-code -fstatic-argument-transformati...2022-05-24T19:06:23ZIcelandjackCore lint error (with flags: -O2 -fobject-code -fstatic-argument-transformation -dcore-lint)```haskell
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Options_GHC -O2 -fobject-code -fstatic-argument-transformation -dcore-lint #-}
import Control.Category
import Data.Kind
app...```haskell
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language RankNTypes #-}
{-# Options_GHC -O2 -fobject-code -fstatic-argument-transformation -dcore-lint #-}
import Control.Category
import Data.Kind
apply :: Int -> (forall (ob :: Type) (cat :: ob -> ob -> Type) (a :: ob). Category cat => cat a a -> cat a a)
apply n = apply n
```
Gets a core lint error, I'm using GHC 9.1.0.20201202 and it seems all these flags play together. If I remove any of them it compiles fine.
```
$ ./ghc -ignore-dot-ghci --interactive ./4091_bug.hs
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( /home/.., /home/.. )
*** Core Lint errors : in result of Static argument ***
/home/..:11:1: warning:
Mismatch in type between binder and occurrence
Binder: apply_rzf :: Int
-> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *} {a :: ob_aF9}.
Category cat_aFa =>
cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
Occurrence: apply :: Int
-> forall ob (cat :: ob -> ob -> *) (a :: ob).
Category cat =>
cat a a -> cat a a
Before subst: Int
-> forall ob (cat :: ob -> ob -> *) (a :: ob).
Category cat =>
cat a a -> cat a a
In the RHS of apply :: Int
-> forall ob (cat :: ob -> ob -> *) (a :: ob).
Category cat =>
cat a a -> cat a a
In the body of lambda with binder ds_dFA :: Int
In the body of lambda with binder ob_aF9 :: *
In the body of lambda with binder cat_aFa :: ob_aF9 -> ob_aF9 -> *
In the body of lambda with binder a_aFb :: ob_aF9
In the body of lambda with binder $dCategory_aFc :: Category
cat_aFa
In the RHS of sat_worker_sFM :: cat_aFa a_aFb a_aFb
-> cat_aFa a_aFb a_aFb
In the body of letrec with binders apply_rzf :: Int
-> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *}
{a :: ob_aF9}.
Category cat_aFa =>
cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
In an occurrence of apply :: Int
-> forall ob (cat :: ob -> ob -> *) (a :: ob).
Category cat =>
cat a a -> cat a a
Substitution: [TCvSubst
In scope: InScope {ob_aF9 cat_aFa a_aFb}
Type env: [aF9 :-> ob_aF9, aFa :-> cat_aFa, aFb :-> a_aFb]
Co env: []]
*** Offending Program ***
apply [Occ=LoopBreaker]
:: Int
-> forall ob (cat :: ob -> ob -> *) (a :: ob).
Category cat =>
cat a a -> cat a a
[LclIdX,
Arity=2,
Str=<U><U>b,
Cpr=b,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=True)}]
apply
= \ (ds_dFA :: Int)
(@ob_aF9)
(@(cat_aFa :: ob_aF9 -> ob_aF9 -> *))
(@(a_aFb :: ob_aF9))
($dCategory_aFc :: Category cat_aFa) ->
letrec {
sat_worker_sFM :: cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
[LclId]
sat_worker_sFM
= let {
apply_rzf
:: Int
-> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *} {a :: ob_aF9}.
Category cat_aFa =>
cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
[LclId]
apply_rzf
= \ (ds_sFH :: Int)
(@ob_sFI)
(@(cat_sFJ :: ob_aF9 -> ob_aF9 -> *))
(@(a_sFK :: ob_aF9))
($dCategory_sFL :: Category cat_aFa) ->
sat_worker_sFM } in
apply ds_dFA @ob_aF9 @cat_aFa @a_aFb $dCategory_aFc; } in
sat_worker_sFM
$trModule_sFC :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_sFC = "main"#
$trModule_sFD :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule_sFD = TrNameS $trModule_sFC
$trModule_sFE :: Addr#
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_sFE = "Main"#
$trModule_sFF :: TrName
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule_sFF = TrNameS $trModule_sFE
$trModule :: Module
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule = Module $trModule_sFD $trModule_sFF
*** End of Offense ***
<no location info>: error:
Compilation had errors
*** Exception: ExitFailure 1
ghci>
```