GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2023-01-26T04:02:51Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/19690Bottom dictionaries can be derived with QuantifiedConstraints, UndecidableIns...2023-01-26T04:02:51Zaadaa-fgtaaBottom dictionaries can be derived with QuantifiedConstraints, UndecidableInstances and UndecidableSuperClasses[I'm not sure if this is a bug or documentation issue. I'd prefer the former so I applied "bug" template]
## Summary
With `QuantifiedConstraints`, `UndecidableInstances` and `UndecidableSuperClasses` it is possible to
produce bottom di...[I'm not sure if this is a bug or documentation issue. I'd prefer the former so I applied "bug" template]
## Summary
With `QuantifiedConstraints`, `UndecidableInstances` and `UndecidableSuperClasses` it is possible to
produce bottom dictionary, which isn't mentioned in docs as far as I can see.
## Steps to reproduce
```haskell
{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, ConstraintKinds, FlexibleInstances,
GADTs, QuantifiedConstraints, TypeApplications, ScopedTypeVariables #-}
module QCLoop where
class c => Hold c
instance c => Hold c
data Dict c = c => Dict
anythingDict :: Dict c
anythingDict = go
where
go :: (Hold c => c) => Dict c
go = Dict
```
Produces bottom dictionary
```haskell
Rec {
$dHold_rxi :: forall {c :: Constraint}. Hold c
$dHold_rxi = $dHold_rxi
end Rec }
anythingDict :: forall (c :: Constraint). Dict c
anythingDict = \ (@c) -> Dict ($dHold_rxi `cast` <Co:2>)
```
## Expected behavior
Either the program is rejected with "could not deduce c" or "too many iterations", or documentation for
`UndecidableInstances` and/or `UndecidableSuperClasses` mentions that they may result in
non-termination not only in typechecker but also at runtime.
I would really prefer the former as the ability to "prove" anything with such code scares me a bit.
## Environment
* GHC version used: 8.10.4, 9.0.1 and 9.1.20210409
* Operating System: Linux (NixOS)
* System Architecture: x86-64https://gitlab.haskell.org/ghc/ghc/-/issues/19682Constraint solver regression in 9.22021-07-28T16:20:14ZAndres LöhConstraint solver regression in 9.2## Summary
While trying to make the `generics-sop` and `sop-core` packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GH...## Summary
While trying to make the `generics-sop` and `sop-core` packages compatible with GHC 9.2, I discovered a regression in the constraint solver. The included program compiles at with GHC 9.0.1, GHC 8.8.4, GHC 8.6.5, GHC 8.4.4, GHC 8.2.2, but it fails with GHC 9.2 with the following error message:
```
AllEq.hs:19:21: error:
• Couldn't match type ‘ys0’ with ‘Head ys0 : Tail ys0’
arising from a use of ‘convert’
• In the second argument of ‘const’, namely ‘(convert xs)’
In the expression: const () (convert xs)
In an equation for ‘test’: test xs = const () (convert xs)
|
19 | test xs = const () (convert xs)
| ^^^^^^^
```
## Steps to reproduce
Run `ghc` or `ghci` on the following file:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module AllEq where
import Data.Kind
import Data.Proxy
convert :: (AllEq xs ys) => Proxy xs -> Proxy ys
convert p = Proxy
-- Works with ghc up to 9.0. Fails with ghc 9.2.
test :: Proxy '[Char, Bool] -> ()
test xs = const () (convert xs)
class (AllEqF xs ys, SameShapeAs xs ys) => AllEq (xs :: [a]) (ys :: [a])
instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
type family SameShapeAs (xs :: [a]) (ys :: [a]) :: Constraint where
SameShapeAs '[] ys = (ys ~ '[])
SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
type family AllEqF (xs :: [a]) (ys :: [a]) :: Constraint where
AllEqF '[] '[] = ()
AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
type family Head (xs :: [a]) :: a where
Head (x : xs) = x
type family Tail (xs :: [a]) :: [a] where
Tail (x : xs) = xs
```
## Expected behavior
I would expect the program to be accepted.
## Environment
* GHC version used: 9.2.0.20210406, built locally on my machine from the `ghc-9.2` branch at commit d197fb3d5c053cfb526272c29a443c33d1af0980
Optional:
* Operating System: Linux (NixOS)
* System Architecture: x86_649.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19677GHC does not rewrite in FunTy2022-02-21T17:09:27ZRichard Eisenbergrae@richarde.devGHC does not rewrite in FunTyConsider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
...Consider
```hs
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies, GADTs #-}
module Bug where
import GHC.Exts
class C x where
meth :: x -> ()
instance C (a -> b) where
meth _ = ()
type family Lifty throttle where
Lifty Int = LiftedRep
data G a where
MkG :: G Int
foo :: forall i (a :: TYPE (Lifty i)) (b :: TYPE (Lifty i)). G i -> (a -> b) -> ()
foo MkG = meth
```
GHC rejects, saying it cannot find an instance for `C (a -> b)`. But it should accept.
The problem is that the kinds of `a` and `b` are `TYPE (Lifty i)`. Even if we know `i ~ Int`, and therefore that `Lifty i ~ LiftedRep`, GHC does not rewrite these kinds internally, allowing instance matching to succeed.
!2477, when complete, should address this.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc/-/issues/19668Exponential blowup in T9198 (regresssion from 8.10 and 9.0)2021-10-11T08:17:53ZvdukhovniExponential blowup in T9198 (regresssion from 8.10 and 9.0)## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head t...## Summary
The T9198 test is showing rather unstable metrics in head, but the real issue is not the wobbly numbers but the scale. In GHC 8.10.4 and 9.0.1, adding more continuation terms results in linear cost increases, but with head the cost doubles with every term, as reported in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4890#note_343948
## Steps to reproduce
Compile `testsuite/tests/perf/compiler/T9198.hs` with `+RTS -s` with varying numbers of additional `a` continuation terms. The GHC runtime and memory allocation grow exponentially. The same is not observed with GHC 8.10.4 for example.
## Expected behavior
Linear cost. With 8.10.4 and the continuation count unmodified I get:
```
$ ghc -O -fasm testsuite/tests/perf/compiler/T9198.hs +RTS -s
116,102,480 bytes allocated in the heap
...
MUT time 0.069s ( 0.572s elapsed)
GC time 0.111s ( 0.111s elapsed)
Total time 0.181s ( 0.689s elapsed)
```
With head I get:
```
514,989,696 bytes allocated in the heap
...
MUT time 0.212s ( 0.604s elapsed)
GC time 0.366s ( 0.366s elapsed)
Total time 0.581s ( 0.979s elapsed)
```
## Environment
* GHC version used: head (9.1.20210402)9.2.1Matthew PickeringMatthew Pickeringhttps://gitlab.haskell.org/ghc/ghc/-/issues/19565`plots` fails to typechecking in 9.22021-03-19T23:36:40ZBen Gamari`plots` fails to typechecking in 9.2When updating `head.hackage` for 9.2, I noticed that `plots` now fails to typecheck,
```
src/Plots/Types.hs:697:17: error:
• Reduction stack overflow; size = 201
When simplifyin...When updating `head.hackage` for 9.2, I noticed that `plots` now fails to typecheck,
```
src/Plots/Types.hs:697:17: error:
• Reduction stack overflow; size = 201
When simplifying the following type: V p1
Use -freduction-depth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the pattern: StyledPlot p opts sty
In an equation for ‘styledPlot’:
styledPlot f s@(StyledPlot p opts sty)
= case eq p of
Just Refl -> f p <&> \ p' -> StyledPlot p' opts sty
Nothing -> pure s
where
eq :: Typeable a => a -> Maybe (a :~: p)
eq _ = eqT
|
697 | styledPlot f s@(StyledPlot p opts sty) =
| ^^^^^^^^^^^^^^^^^^^^^
```
I haven't tried lifting the reduction depth yet.9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19548Kind generalisation without -XPolyKinds leading to breakage2021-03-17T08:07:24ZSebastian GrafKind generalisation without -XPolyKinds leading to breakageThe following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal...The following program is reduced from `libraries/Cabal/Cabal/src/Distribution/Utils/Path.hs`, which I didn't manage to compile with @bgamari's [build-cabal.sh script](https://gitlab.haskell.org/bgamari/ghc-utils/-/blob/master/build-cabal.sh) today:
```hs
{-# LANGUAGE DeriveDataTypeable #-}
module Path where
import Data.Typeable
class Typeable a => C a where
data T a = T deriving Typeable
instance Typeable a => C (T a)
```
If compiled with HEAD (and `-fprint-explicit-kinds`, this errors
```
Path.hs:9:10: error:
• Could not deduce (Typeable @(*) k)
arising from the superclasses of an instance declaration
from the context: Typeable @k a
bound by the instance declaration at Path.hs:9:10-30
• In the instance declaration for ‘C @{*} (T @{k} a)’
|
9 | instance Typeable a => C (T a)
| ^^^^^^^^^^^^^^^^^^^^^
```
Apparently, `T`'s type parameter has been kind generalised. Why? I don't think `-XDeriveDataTypeable` implies `-XPolyKinds`.
Yet the error message mentions an implicit kind `k` that appears nowhere else in the program.https://gitlab.haskell.org/ghc/ghc/-/issues/19522Levity monomorphic instantiation of unsafeCoerce# is rejected as being levity...2021-10-11T08:15:50ZRyan ScottLevity monomorphic instantiation of unsafeCoerce# is rejected as being levity polymorphic in 9.0+While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> ...While experimenting with `unsafeCoerce#` recently, I tried the following:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
module Bug where
import GHC.Exts
import Unsafe.Coerce
f :: Int -> Int
f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
```
Surprisingly, GHC 9.0 and later reject this:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:10:7: error:
Cannot use function with levity-polymorphic arguments:
unsafeCoerce# :: forall (q :: RuntimeRep) (r :: RuntimeRep)
(a :: TYPE q) (b :: TYPE r).
a -> b
(Note that levity-polymorphic primops such as 'coerce' and unboxed tuples
are eta-expanded internally because they must occur fully saturated.
Use -fprint-typechecker-elaboration to display the full expression.)
Levity-polymorphic arguments: a :: TYPE q
|
10 | f x = unsafeCoerce# @LiftedRep @LiftedRep @Int @Int x
| ^^^^^^^^^^^^^
```
The error message confuses me, since nothing about this is levity polymorphic.
Note that this only occurs if visible type applications are used. If I remove them:
```hs
f :: Int -> Int
f x = unsafeCoerce# x
```
Then GHC accepts it.9.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/19503Dead suggestion for -XUnliftedNewtypes in checkNewDataCon2023-09-27T09:55:06ZSebastian GrafDead suggestion for -XUnliftedNewtypes in checkNewDataConNote [Implementation of UnliftedNewtypes], point <Error Messages> says:
```
<Error Messages>: It's tempting to think that the expected kind for a newtype
constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type....Note [Implementation of UnliftedNewtypes], point <Error Messages> says:
```
<Error Messages>: It's tempting to think that the expected kind for a newtype
constructor argument when -XUnliftedNewtypes is *not* enabled should just be Type.
But this leads to difficulty in suggesting to enable UnliftedNewtypes. Here is
an example:
newtype A = MkA Int#
If we expect the argument to MkA to have kind Type, then we get a kind-mismatch
error. The problem is that there is no way to connect this mismatch error to
-XUnliftedNewtypes, and suggest enabling the extension. So, instead, we allow
the A to type-check, but then find the problem when doing validity checking (and
where we get make a suitable error message).
```
I think that Note refers to the code in `GHC.Tc.TyCl.checkNewDataCon` (which is transitively called from `checkValidTyCon`). There we have
```hs
; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes
; let allowedArgType =
unlifted_newtypes || isLiftedType_maybe (scaledThing arg_ty1) == Just True
; checkTc allowedArgType $ vcat
[ text "A newtype cannot have an unlifted argument type"
, text "Perhaps you intended to use UnliftedNewtypes"
]
```
But that error emssage doesn't occur anywhere in the testsuite. If you try the example `A` from the Note, you instead get
```
test.hs:20:1: error:
• Newtype has non-* return kind ‘TYPE 'IntRep’
Perhaps you intended to use UnliftedNewtypes
• In the newtype declaration for ‘A’
|
20 | newtype A = MkA Int#
| ^^^^^^^^^^^^^^^^^^^^
```
(Side note: It's a bit surprising that the emission of that error suppresses any following errors, for example of a following decl `newtype B = MkB Int#`. Perhaps this has to do with the next paragraph.)
That message (which I actually prefer) is emitted by `GHC.Tc.Gen.HsType.checkDataKindSig`.
It seems we can just get rid of the code in `checkNewDataCon`. Either way, we should update Note [Implementation of UnliftedNewtypes]. Maybe Split if off into its own Sub-Note? That Note is awfully long and has many many sub items.https://gitlab.haskell.org/ghc/ghc/-/issues/19498Typeclass fails to compile with StandaloneKindSignatures; only compiles with ...2021-03-15T11:00:27ZdanidiazTypeclass fails to compile with StandaloneKindSignatures; only compiles with conventional kind annotations## Summary
A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.
## Steps to reproduce
Try to compile this module:
```
{-# LANGUAGE Allo...## Summary
A typeclass compiles correctly with conventional kind annotations, but when the kinds are given with a standalone kind signature it ceases to compile.
## Steps to reproduce
Try to compile this module:
```
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Main where
import Data.Kind
import Data.Proxy
import GHC.TypeLits
data Color
= R
| B
deriving (Show, Eq)
data Map symbol q
= E
| N Color (Map symbol q) symbol q (Map symbol q)
deriving (Show, Eq)
type Record :: (q -> Type) -> Map Symbol q -> Type
data Record f t where
Empty :: Record f E
Node :: Record f left -> f v -> Record f right -> Record f (N color left k v right)
type CanMakeBlack :: Map Symbol q -> Constraint
class CanMakeBlack t where
type MakeBlack t :: Map Symbol q
makeBlackR :: Record f t -> Record f (MakeBlack t)
instance CanMakeBlack (N color left k v right) where
type MakeBlack (N color left k v right) = N B left k v right
makeBlackR (Node left fv right) = Node left fv right
instance CanMakeBlack E where
type MakeBlack E = E
makeBlackR Empty = Empty
type Delable :: Symbol -> q -> Map Symbol q -> Constraint
class Delable k v t where
-- Using conventional kind annotations, it compiles correctly
--class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Del k v t :: Map Symbol q
del :: Record f t -> Record f (Del k v t)
type Deletable :: Symbol -> q -> Map Symbol q -> Constraint
class Deletable (k :: Symbol) (v :: q) (t :: Map Symbol q) where
type Delete k v t :: Map Symbol q
_delete :: Record f t -> Record f (Delete k v t)
instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
type Delete k v t = MakeBlack (Del k v t)
_delete r = makeBlackR (del @_ @k @v r)
main :: IO ()
main = pure ()
```
The compilation will fail with the error:
```
Main.hs:70:15: error:
* Could not deduce: MakeBlack (Del k v t) ~ MakeBlack (Del k v t)
from the context: (Delable k v t, Del k v t ~ deleted,
CanMakeBlack deleted)
bound by the instance declaration at Main.hs:68:10-86
Expected: Record f (Delete k v t)
Actual: Record f (MakeBlack (Del k v t))
NB: `MakeBlack' is a non-injective type family
```
However, if instead of the line
`class Delable k v t where`
We use the line
`class Delable (k :: Symbol) (v :: q) (t :: Map Symbol q) where`
The code compiles correctly, even if the standalone kind signature remains.
## Expected behavior
The code should compile correctly with the standalone kind signature, without need of explicit kind annotations on the variables.
## Environment
* GHC version used: 9.0.1
Optional:
* Operating System: Windows 10https://gitlab.haskell.org/ghc/ghc/-/issues/19495Tc trace of checkValidType panics in tcTypeKind for T16391b2022-01-10T23:57:14ZSebastian GrafTc trace of checkValidType panics in tcTypeKind for T16391bIn https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2218#note_335959, I triggered a panic in `tcTypeKind`. I thought that my branch was responsible, but then figured out that without `-ddump-tc-trace`, there was no panic. Then I tried...In https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2218#note_335959, I triggered a panic in `tcTypeKind`. I thought that my branch was responsible, but then figured out that without `-ddump-tc-trace`, there was no panic. Then I tried `-ddump-tc-trace` on `T16391b`:
```hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
module T16391b where
import GHC.Exts
type family T (r :: RuntimeRep) :: TYPE r
foo :: T r
foo = foo
```
And sure enough, that panics on HEAD:
```
checkValidTypeghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210305:
tcTypeKind
forall (r :: RuntimeRep). T r
[r_aw2[sk:2]]
T r_aw2[sk:2] :: TYPE r_aw2[sk:2]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:2660:18 in ghc:GHC.Core.Type
```
... when `checkValidType` (I think) ultimately would have printed the following expected error:
```
T16391b.hs:10:8: error:
• Quantified type's kind mentions quantified type variable
type: ‘T 'LiftedRep’
where the body of the forall has this kind: ‘TYPE r’
• In the type signature: foo :: T r
|
10 | foo :: T r
| ^^^
```
It's a matter of printing the error message *before* calling `tcTypeKind`:
```hs
checkValidType ctxt ty
= do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
; rankn_flag <- xoptM LangExt.RankNTypes
...
; checkNoErrs $
do { check_type ve ty
; checkUserTypeError ty
; traceTc "done ct" (ppr ty) }
...
; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) }
```
I suggest we simply delete the ` <+> text "::" <+> ppr (tcTypeKind ty)` of the first `traceTc`.https://gitlab.haskell.org/ghc/ghc/-/issues/19482"No skolem info" with the infinite kind2022-01-29T16:06:57ZRinat Striungislazybonesxp@gmail.com"No skolem info" with the infinite kind## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from H...## Summary
Today I get a crash with the following message:
```src/Bug.hs:12:25: error:ghc: panic! (the 'impossible' happened)
(GHC version 9.1.20210210:
No skolem info:
[r_axQl[ssk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Errors.hs:2847:17 in ghc:GHC.Tc.Errors
Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug
```
## Steps to reproduce
Here is my minimal example to reproduce:
```{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Bug where
instance BugClass ((s : sx) :: [r]) where
bugList = testF @r @s
class BugClass k where
bugList :: ()
testF :: forall a (b :: [a]). ()
testF = ()
```
Also, GHC-8.10 works well with a proper error message.
So, it looks like a regression.
## Expected behavior
I should get a compilation error message about the infinite kind construction ( `r ~ [r]`).
## Environment
* GHC version used:
GHC HEAD: [40983d2331fe34c0af6925db7588d5ac6a19ae36](https://gitlab.haskell.org/ghc/ghc/-/tree/40983d2331fe34c0af6925db7588d5ac6a19ae36)9.4.1https://gitlab.haskell.org/ghc/ghc/-/issues/19457conduit-1.3.4 builds with 9.0.1, but not HEAD, due to regression in typecheck...2021-03-09T09:59:21ZRyan Scottconduit-1.3.4 builds with 9.0.1, but not HEAD, due to regression in typechecking sectionsWhile patching `head.hackage` recently, I discovered recently that the `conduit-1.3.4` library fails to build on HEAD, despite compiling with 9.0.1. This is due to a typechecker regression introduced in commit 4196969c53c55191e644d9eb258...While patching `head.hackage` recently, I discovered recently that the `conduit-1.3.4` library fails to build on HEAD, despite compiling with 9.0.1. This is due to a typechecker regression introduced in commit 4196969c53c55191e644d9eb258c14c2bc8467da (`Improve handling of overloaded labels, literals, lists etc`). The issue concerns the way that GHC typechecks left and right sections. Here is a minimized example that illustrates the issue with a right section:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug where
f :: a -> forall b. b -> a
f x _ = x
g :: a -> a
g = (`f` "hello")
```
This compiles on 9.0.1, but fails on HEAD with the following error:
```
$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2 ( Bug2.hs, Bug2.o )
Bug2.hs:8:6: error:
• Couldn't match type: forall c1. c1 -> String
with: c -> String
Expected: b -> c -> String
Actual: b -> forall c. c -> String
• In the expression: "hello" `j`
In an equation for ‘k’: k = ("hello" `j`)
• Relevant bindings include
k :: b -> c -> String (bound at Bug2.hs:8:1)
|
8 | k = ("hello" `j`)
| ^^^^^^^^^^^
```
It's tempting to say that this should be rejected because of simplified subsumption, but that's not the full story. For one thing, 9.0.1 introduced simplified subsumption, but the code above typechecks under 9.0.1, so this is a HEAD-specific phenomenon. Moreover, [Section 3.5 of the Haskell 2010 Report](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-300003.5) specifically requires that the following identities hold for sections:
> Translation: The following identities hold:
>
> ```hs
> (op e) = \ x -> x op e
> (e op) = \ x -> e op x
> ```
>
> where `op` is a binary operator, `e` is an expression, and `x` is a variable that does not occur free in `e`.
Therefore, the definition of `g` should be equivalent to:
```hs
g :: a -> a
g = \x -> x `f` "hello"
```
And indeed, that typechecks on both 9.0.1 and HEAD. Therefore, I'm going to deem this a regression, since the Haskell 2010 Report seems to indicate that this ought to work.
The example above uses a right section, but the same issue applies to left sections as well, as shown by this example:
```hs
{-# LANGUAGE RankNTypes #-}
module Bug2 where
j :: a -> b -> forall c. c -> a
j x _ _ = x
k :: b -> c -> String
k = ("hello" `j`)
```
Again, this typechecks on 9.0.1 but not on HEAD:
```
$ ~/Software/ghc-9.1.20210227/bin/ghc Bug2.hs
[1 of 1] Compiling Bug2 ( Bug2.hs, Bug2.o )
Bug2.hs:8:6: error:
• Couldn't match type: forall c1. c1 -> String
with: c -> String
Expected: b -> c -> String
Actual: b -> forall c. c -> String
• In the expression: "hello" `j`
In an equation for ‘k’: k = ("hello" `j`)
• Relevant bindings include
k :: b -> c -> String (bound at Bug2.hs:8:1)
|
8 | k = ("hello" `j`)
| ^^^^^^^^^^^
```
However, the equivalent eta-expanded version of `k` typechecks on both 9.0.1 and HEAD:
```hs
k :: b -> c -> String
k = \x -> "hello" `j` x
```
cc @simonpj9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19432GHC 9.0 rejects default signature that 8.10 accepts2021-03-03T18:29:53ZRyan ScottGHC 9.0 rejects default signature that 8.10 acceptsI originally noticed this issue in the `barbies-2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{-# LANGUAGE Co...I originally noticed this issue in the `barbies-2.0.2.0` library on Hackage, which compiles with GHC 8.10.4 but fails to compile on GHC 9.0.1. Here is a minimized version of the code that fails to compile on 9.0.1:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
import Data.Coerce
import Data.Kind
import Data.Proxy
import GHC.Generics
import GHC.TypeNats
class FunctorT (t :: (k -> Type) -> k' -> Type) where
tmap :: forall f g
. (forall a . f a -> g a)
-> (forall x . t f x -> t g x)
-- Default implementation of 'tmap' based on 'Generic'.
default tmap
:: forall f g
. (forall a . f a -> g a)
-> (forall x. CanDeriveFunctorT t f g x => t f x -> t g x)
tmap f = toP (Proxy @1) . gmap (Proxy @1) f . fromP (Proxy @1)
type CanDeriveFunctorT t f g x
= ( GenericP 1 (t f x)
, GenericP 1 (t g x)
, GFunctor 1 f g (RepP 1 (t f x)) (RepP 1 (t g x))
)
-----
class GFunctor (n :: Nat) f g repbf repbg where
gmap :: Proxy n -> (forall a . f a -> g a) -> repbf x -> repbg x
class
( Coercible (Rep a) (RepP n a)
, Generic a
) => GenericP (n :: Nat) (a :: Type) where
type family RepP n a :: Type -> Type
toP :: Proxy n -> RepP n a x -> a
fromP :: Proxy n -> a -> RepP n a x
```
The important bit is the default signature for `tmap`. With GHC 9.0.1, this is rejected thusly:
```
$ /opt/ghc/9.0.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:24:11: error:
• The default type signature for tmap:
forall (f :: k -> *) (g :: k -> *).
(forall (a :: k). f a -> g a)
-> forall (x :: k'). CanDeriveFunctorT t f g x => t f x -> t g x
does not match its corresponding non-default type signature
• When checking the class method:
tmap :: forall k k' (t :: (k -> *) -> k' -> *) (f :: k -> *)
(g :: k -> *).
FunctorT t =>
(forall (a :: k). f a -> g a) -> forall (x :: k'). t f x -> t g x
In the class declaration for ‘FunctorT’
|
24 | default tmap
| ^^^^
```
Why does GHC 9.0.1 reject this? According to the [GHC User's Guide section on `DefaultSignatures`](https://downloads.haskell.org/ghc/9.0.1/docs/html/users_guide/exts/default_signatures.html#default-method-signatures):
> The type signature for a default method of a type class must take on the same form as the corresponding main method’s type signature. Otherwise, the typechecker will reject that class’s definition. By “take on the same form”, we mean that the default type signature should differ from the main type signature only in their contexts.
As far as I can tell, `tmap` meets this criterion, as the only difference between the two signatures is the presence of `CanDeriveFunctorT t f g x =>` in the default signature.https://gitlab.haskell.org/ghc/ghc/-/issues/19419GHC 9.0 unable to deduce that instance signature is at least as general as cl...2021-02-25T03:14:03Zsheafsam.derbyshire@gmail.comGHC 9.0 unable to deduce that instance signature is at least as general as class signatureThe following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module B...The following program compiles OK on GHC 8.10 but not on GHC 9.0:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where
-- base
import Data.Kind
( Constraint )
--------------------------------------------------------------------------------
data SplineType = Open | Closed
data Curve ( clo :: SplineType ) = Curve {- ... -}
data Spline ( clo :: SplineType ) = Spline {- ... -}
class KnownSplineType ( clo :: SplineType ) where
type TraversalCt clo ( clo' :: SplineType ) :: Constraint
biwitherSpline
:: ( forall clo'. ( TraversalCt clo clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline clo
-> Maybe ( Spline clo )
instance KnownSplineType Open where
type TraversalCt Open clo' = clo' ~ Open
biwitherSpline
:: ( Curve Open -> Maybe ( Curve Open ) )
-> Spline Open
-> Maybe ( Spline Open )
biwitherSpline _ _ = undefined
```
With GHC 9.0, I get the following error:
```
Bug.hs:37:8: error:
* Couldn't match type: Curve 'Open -> Maybe (Curve 'Open)
with: forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo')
Expected: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
Actual: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
* When checking that instance signature for `biwitherSpline'
is more general than its signature in the class
Instance sig: (Curve 'Open -> Maybe (Curve 'Open))
-> Spline 'Open -> Maybe (Spline 'Open)
Class sig: (forall (clo' :: SplineType).
TraversalCt 'Open clo' =>
Curve clo' -> Maybe (Curve clo'))
-> Spline 'Open -> Maybe (Spline 'Open)
In the instance declaration for `KnownSplineType 'Open'
|
37 | :: ( Curve Open -> Maybe ( Curve Open ) )
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
```
It seems that GHC 9.0 is unable to use the associated type family instance `TraversalCt Open clo' = clo' ~ Open` in checking that the instance signature is at least as general as the class signature. Is this expected, or an oversight?
Of course, changing the instance signature to the obviously correct
```haskell
biwitherSpline
:: ( forall clo'. ( TraversalCt Open clo' )
=> Curve clo' -> Maybe ( Curve clo' )
)
-> Spline Open
-> Maybe ( Spline Open )
```
makes the program compile again, but I think the other instance signature should also be accepted.https://gitlab.haskell.org/ghc/ghc/-/issues/19364oversized source range in type error message2021-03-04T10:42:13Zjwaldmannoversized source range in type error messageFor this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:7-21: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Ba...For this code
```
type Foo = Bool
type Bar = String
data Pair a b = Pair a b
baz :: Pair Foo Bar
baz = Pair "yes" "no"
```
ghc says
```
B.hs:7:7-21: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] [Char]
• In the expression: Pair "yes" "no"
In an equation for ‘baz’: baz = Pair "yes" "no"
|
7 | baz = Pair "yes" "no"
| ^^^^^^^^^^^^^^^
```
So, which argument is wrong?
In fact, how many are?
```
baz :: Pair Foo Bar
baz = Pair "yes" ()
B.hs:7:7-19: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Pair Foo Bar
Actual type: Pair [Char] ()
• In the expression: Pair "yes" ()
In an equation for ‘baz’: baz = Pair "yes" ()
|
7 | baz = Pair "yes" ()
| ^^^^^^^^^^^^^
```
The following case works better (it shows that the first argument is the problem). What's the difference?
```
foo :: (Foo,Bar)
foo = ("yes", "no")
B.hs:11:8-12: error:
• Couldn't match type ‘[Char]’ with ‘Bool’
Expected type: Foo
Actual type: [Char]
• In the expression: "yes"
In the expression: ("yes", "no")
In an equation for ‘foo’: foo = ("yes", "no")
|
11 | foo = ("yes", "no")
| ^^^^^
```https://gitlab.haskell.org/ghc/ghc/-/issues/19315GHC 9.0 regression: plots-0.1.1.2 fails to build due to ambiguous type variable2021-02-10T21:11:55ZRyan ScottGHC 9.0 regression: plots-0.1.1.2 fails to build due to ambiguous type variable_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/568397#L5617)_.
The `plots-0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc-9..._Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage/-/jobs/568397#L5617)_.
The `plots-0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc-9.0` branch. Here is a self-contained example with no external dependencies:
```hs
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Control.Monad.Reader
import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid (Any(..))
import Data.Typeable
type TypeableFloat n = (Typeable n, RealFloat n)
type Lens' s a = Lens s s a a
type Lens s t a b = forall f. Functor f => (a -> f b) -> s -> f t
type LensLike' f s a = LensLike f s s a a
type LensLike f s t a b = (a -> f b) -> s -> f t
type Getting r s a = (a -> Const r a) -> s -> Const r s
type ASetter s t a b = (a -> Identity b) -> s -> Identity t
data V2 a = V2 !a !a
flipX_Y :: Num n => V2 n -> V2 n
flipX_Y (V2 x y) = V2 (-y) (-x)
class R1 t where
_x :: Lens' (t a) a
class R1 t => R2 t where
_y :: Lens' (t a) a
instance R1 V2 where
_x f (V2 a b) = (`V2` b) <$> f a
instance R2 V2 where
_y f (V2 a b) = V2 a <$> f b
infixl 8 #
(#) :: a -> (a -> b) -> b
(#) = flip ($)
infixr 4 %~
(%~) :: ASetter s t a b -> (a -> b) -> s -> t
(%~) = over
(^.) :: s -> Getting a s a -> a
s ^. l = getConst (l Const s)
over :: ASetter s t a b -> (a -> b) -> s -> t
over l f = runIdentity . l (Identity . f)
view :: MonadReader s m => Getting a s a -> m a
view l = asks (getConst . l Const)
lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b
lens sa sbt afb s = sbt s <$> afb (sa s)
type family V a :: * -> *
type family N a :: *
type Vn a = V a (N a)
data Style (v :: * -> *) n = Style
class HasStyle a where
applyStyle :: Style (V a) (N a) -> a -> a
type TextFunction b v n = TextAlignment n -> String -> QDiagram b v n Any
data TickLabels b (v :: * -> *) n = TickLabels
{ tlFun :: [n] -> (n,n) -> [(n, String)]
, tlTextFun :: TextFunction b v n
, tlStyle :: Style v n
, tlGap :: n
}
type instance V (TickLabels b v n) = v
type instance N (TickLabels b v n) = n
class HasTickLabels f a b | a -> b where
tickLabel :: LensLike' f a (TickLabels b (V a) (N a))
tickLabelTextFunction :: Functor f => LensLike' f a (TextFunction b (V a) (N a))
tickLabelTextFunction = tickLabel . lens tlTextFun (\tl f -> tl {tlTextFun = f})
tickLabelFunction :: Functor f => LensLike' f a ([N a] -> (N a, N a) -> [(N a, String)])
tickLabelFunction = tickLabel . lens tlFun (\tl f -> tl {tlFun = f})
tickLabelStyle :: Functor f => LensLike' f a (Style (V a) (N a))
tickLabelStyle = tickLabel . lens tlStyle (\tl sty -> tl {tlStyle = sty})
tickLabelGap :: Functor f => LensLike' f a (N a)
tickLabelGap = tickLabel . lens tlGap (\tl n -> tl {tlGap = n})
instance HasTickLabels f (TickLabels b v n) b where
tickLabel = id
data ColourBar b n = ColourBar
{ cbTickLabels :: TickLabels b V2 n
, cbTicks :: MajorTicks V2 n
, cbWidth :: n
}
type instance V (ColourBar b n) = V2
type instance N (ColourBar b n) = n
data MajorTicks (v :: * -> *) n = MajorTicks
{ matFunction :: (n,n) -> [n]
}
type instance V (MajorTicks v n) = v
type instance N (MajorTicks v n) = n
class HasMajorTicks f a where
majorTicks :: LensLike' f a (MajorTicks (V a) (N a))
majorTicksFunction :: Functor f => LensLike' f a ((N a, N a) -> [N a])
majorTicksFunction = majorTicks . lens matFunction (\mat a -> mat {matFunction = a})
instance HasMajorTicks f (MajorTicks v n) where
majorTicks = id
data Path (v :: * -> *) n = Path
data (:-:) u v = (u -> v) :-: (v -> u)
infixr 7 :-:
instance Semigroup (a :-: a) where
(f :-: f') <> (g :-: g') = f . g :-: g' . f'
instance Monoid (v :-: v) where
mempty = id :-: id
data Transformation v n = Transformation (v n :-: v n) (v n :-: v n) (v n)
class Transformable t where
transform :: Transformation (V t) (N t) -> t -> t
translation :: v n -> Transformation v n
translation = Transformation mempty mempty
translate :: (Transformable t) => Vn t -> t -> t
translate = transform . translation
class Transformable t => Renderable t b where
orient :: HasOrientation o => o -> a -> a -> a
orient o h v =
case view orientation o of
Horizontal -> h
Vertical -> v
data Orientation = Horizontal | Vertical
class HasOrientation a where
orientation :: Lens' a Orientation
instance HasPlacement (ColourBar b n) where
placement = undefined
instance HasOrientation (ColourBar b n) where
orientation = undefined
instance Functor f => HasMajorTicks f (ColourBar b n) where
majorTicks = lens cbTicks (\c a -> c {cbTicks = a})
data ColourMap = ColourMap
data QDiagram b (v :: * -> *) n m = QD
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> HasStyle (QDiagram b v n m) where
applyStyle = undefined
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> Monoid (QDiagram b v n m) where
mempty = undefined
instance Semigroup m -- (Metric v, OrderedField n, Semigroup m)
=> Semigroup (QDiagram b v n m) where
(<>) = undefined
instance Semigroup m -- (OrderedField n, Metric v, Semigroup m)
=> Transformable (QDiagram b v n m) where
transform = undefined
type instance V (QDiagram b v n m) = v
type instance N (QDiagram b v n m) = n
data TextAlignment n = BaselineText | BoxAlignedText n n
data Placement = Placement
{ pAt :: V2 Rational
}
class HasPlacement a where
placement :: Lens' a Placement
placementAt :: Lens' a (V2 Rational)
placementAt = placement . lens pAt (\p a -> p {pAt = a})
renderColourBar
:: forall n b. (TypeableFloat n, Renderable (Path V2 n) b)
=> ColourBar b n
-> ColourMap
-> (n,n)
-> n
-> QDiagram b V2 n Any
renderColourBar cb@ColourBar {..} _cm bnds@(lb,ub) l
= tLbs
where
o, xy :: a -> a -> a
o = orient cb
xy a b = if let V2 x y = cb^.placementAt in x > y
then a else b
w = cbWidth
f x = (x - (ub + lb)/2) / (ub - lb) * l
inRange x = x >= lb && x <= ub
tickXs = view majorTicksFunction cbTicks bnds
tickXs' :: [n]
tickXs' = filter inRange tickXs
tickLabelXs :: [(n, String)]
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
tLbs :: QDiagram b V2 n Any
tLbs = foldMap drawTickLabel tickLabelXs
drawTickLabel :: (n, String) -> QDiagram b (V (TickLabels b V2 n)) (N (TickLabels b V2 n)) Any
drawTickLabel (x,label) =
view tickLabelTextFunction cbTickLabels tAlign label
# translate v
# applyStyle (cbTickLabels ^. tickLabelStyle)
where v = V2 (f x) (- w/2 - view tickLabelGap cbTickLabels)
# xy id (_y %~ negate)
# o id ((_y %~ negate) . flipX_Y)
tAlign = o (xy (BoxAlignedText 0.5 1) (BoxAlignedText 0.5 0))
(xy (BoxAlignedText 0 0.5) (BoxAlignedText 1 0.5))
```
This compiles with GHC 8.10.3 and earlier, but fails to compile with `ghc-9.0`:
```
$ ~/Software/ghc-9.0.0.20210130/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:229:22: error:
• Could not deduce (HasTickLabels
(Const ([n] -> (n, n) -> [(n, String)])) (TickLabels b V2 n) b0)
arising from a use of ‘tickLabelFunction’
from the context: (TypeableFloat n, Renderable (Path V2 n) b)
bound by the type signature for:
renderColourBar :: forall n b.
(TypeableFloat n, Renderable (Path V2 n) b) =>
ColourBar b n
-> ColourMap -> (n, n) -> n -> QDiagram b V2 n Any
at Bug.hs:(204,1)-(210,24)
The type variable ‘b0’ is ambiguous
Relevant bindings include
tickLabelXs :: [(n, String)] (bound at Bug.hs:229:3)
tickXs' :: [n] (bound at Bug.hs:226:3)
inRange :: n -> Bool (bound at Bug.hs:222:3)
tickXs :: [n] (bound at Bug.hs:224:3)
l :: n (bound at Bug.hs:211:52)
ub :: n (bound at Bug.hs:211:48)
cbTickLabels :: TickLabels b V2 n (bound at Bug.hs:211:31)
(Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-relevant-binds)
These potential instance exist:
instance HasTickLabels f (TickLabels b v n) b
-- Defined at Bug.hs:100:10
• In the first argument of ‘view’, namely ‘tickLabelFunction’
In the expression: view tickLabelFunction cbTickLabels tickXs' bnds
In an equation for ‘tickLabelXs’:
tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
|
229 | tickLabelXs = view tickLabelFunction cbTickLabels tickXs' bnds
| ^^^^^^^^^^^^^^^^^
```
Moreover, this compiles with GHC 9.0.1-rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlab-ci: Don't run LLVM tests on Debian 9`). This commit has an artifact associated with it, and I can confirm that the bug is not present here.
* 0789f7a18a78920f50647e2b4aa8082a14ca9e90 (`Hadrian: show default ghc-bignum backend (fix #18912)`)9.0.2https://gitlab.haskell.org/ghc/ghc/-/issues/19197‘:kind () :: '()’ doesn't give any output2021-01-18T17:11:59ZIcelandjack‘:kind () :: '()’ doesn't give any output```
$ ./ghc/_build/stage1/bin/ghc -ignore-dot-ghci --interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set -XKindSignatures -XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set -XPartialTypeSignatures ...```
$ ./ghc/_build/stage1/bin/ghc -ignore-dot-ghci --interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set -XKindSignatures -XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set -XPartialTypeSignatures -Wno-partial-type-signatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an errorhttps://gitlab.haskell.org/ghc/ghc/-/issues/19196TypeInType prevents Typeable from being resolved from a given2021-01-11T03:19:52ZSerge KosyrevTypeInType prevents Typeable from being resolved from a givenThe following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}...The following program is accepted without `TypeInType` by GHC 8.10.2:
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import Data.Dynamic
import Type.Reflection
data Liveness
= forall t. Live t
data IOA (l :: Liveness) where
IOE :: IOA (Live t)
data LTag (l :: Liveness) where
LLive :: Typeable t => TypeRep t -> LTag (Live t)
reconstruct :: Dynamic -> LTag l -> ()
reconstruct dyn l@LLive{} =
case l of
(LLive tr :: LTag (Live t)) ->
undefined $ withTypeable tr $
(fromDynamic dyn :: Maybe (IOA (Live t)))
main :: IO ()
main = undefined
```
It is, however, rejected with `TypeInType`, as follows:
```haskell
common/src/Dom/Pipe/IOA.hs:26:17: error:
• Could not deduce (Typeable t) arising from a use of ‘fromDynamic’
from the context: (l ~ 'Live t1, Typeable t1)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in an equation for ‘reconstruct’
at common/src/Dom/Pipe/IOA.hs:22:19-25
or from: ('Live t1 ~ 'Live t3, Typeable t3)
bound by a pattern with constructor:
LLive :: forall t1 (t2 :: t1).
Typeable t2 =>
TypeRep t2 -> LTag ('Live t2),
in a case alternative
at common/src/Dom/Pipe/IOA.hs:24:10-17
or from: Typeable t3
bound by a type expected by the context:
Typeable t3 => Maybe (IOA ('Live t1))
at common/src/Dom/Pipe/IOA.hs:26:16-56
• In the second argument of ‘($)’, namely
‘(fromDynamic dyn :: Maybe (IOA (Live t)))’
In the second argument of ‘($)’, namely
‘withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))’
In the expression:
undefined
$ withTypeable tr $ (fromDynamic dyn :: Maybe (IOA (Live t)))
|
26 | (fromDynamic dyn :: Maybe (IOA (Live t)))
| ^^^^^^^^^^^^^^^
```
Potentially related to #16627https://gitlab.haskell.org/ghc/ghc/-/issues/19167Regression around overloaded literals and type applications2021-02-21T16:41:22ZRichard Eisenbergrae@richarde.devRegression around overloaded literals and type applicationsThe new eager instantiation approach (adopted as a part of Quick Look) does not treat overloaded literals as "heads". This causes trouble when using them with type applications, which can be useful when using `-XRebindableSyntax`. Specif...The new eager instantiation approach (adopted as a part of Quick Look) does not treat overloaded literals as "heads". This causes trouble when using them with type applications, which can be useful when using `-XRebindableSyntax`. Specifically, the following module compiles with released GHCs:
```hs
{-# LANGUAGE RebindableSyntax, RankNTypes, TypeApplications, OverloadedStrings,
OverloadedLists, TypeFamilies #-}
module Bug where
import qualified Prelude as P
import qualified GHC.Exts as P
import Data.List.NonEmpty ( NonEmpty )
fromInteger :: P.Integer -> forall a. P.Num a => a
fromInteger n = P.fromInteger n
shouldBeAnInt = 3 @P.Int
newtype RevString = RevString P.String
deriving P.Show
instance P.IsString RevString where
fromString str = RevString (P.reverse str)
fromString :: P.String -> forall a. P.IsString a => a
fromString str = P.fromString str
shouldBeARevString = "hello" @RevString
fromListN :: P.Int -> [elt] -> forall list. (P.IsList list, elt ~ P.Item list) => list
fromListN n l = P.fromListN n l
shouldBeANonEmpty = ['x', 'y', 'z'] @(NonEmpty P.Char)
```
All three `shouldBe` definitions are rejected with HEAD. But accepted by 8.x9.2.1https://gitlab.haskell.org/ghc/ghc/-/issues/19154GHC 9.0 no longer typechecks a program involving overloaded labels and type a...2022-05-30T20:09:58Zsheafsam.derbyshire@gmail.comGHC 9.0 no longer typechecks a program involving overloaded labels and type applicationsIn the program that follows, I specify the type of a label by using a visible type application.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGU...In the program that follows, I specify the type of a label by using a visible type application.
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Labels where
-- base
import Prelude
import Data.Kind
( Type )
import GHC.TypeLits
( Symbol, KnownSymbol )
--------------------------------------------------------------------------
data Label (k :: Symbol) (a :: Type) = Label
class IsLabel k a v | v -> a, v -> k where
fromLabel :: v
instance KnownSymbol k => IsLabel k a (Label k a) where
fromLabel = Label @k @a
foo :: Label k a -> ()
foo _ = ()
test :: ()
test = foo ( #label @Bool )
```
The point of this program is that the label `#label` is polymorphic:
```haskell
#label :: forall (a :: Type). Label "label" a
```
and I am able to instantiate the type variable `a` with a type application.
<p>
<details>
<summary> Show/hide further context.</summary>
This was boiled down from the overloaded label syntax I provide in my shader library, see [here](https://gitlab.com/sheaf/fir/-/blob/master/src/FIR/Syntax/Labels.hs).
This added bit of syntax allows users of the library to write shaders in an imperative style, see [here](https://gitlab.com/sheaf/fir/-/blob/master/fir-examples/examples/shaders/FIR/Examples/JuliaSet/Shaders.hs#L117) for an example.
</details>
</p>
This program compiles fine on GHC 8.10 (and previous GHC versions), but fails to compile on GHC 9.0 (rc1) with the following error:
```
Labels.hs:35:14: error:
* Cannot apply expression of type `v0'
to a visible type argument `Bool'
* In the first argument of `foo', namely `(#label @Bool)'
In the expression: foo (#label @Bool)
In an equation for `test': test = foo (#label @Bool)
|
35 | test = foo ( #label @Bool )
| ^^^^^
```
Can someone enlighten me about what's going on? I found it quite useful to be able to pass further arguments to an overloaded label in this way, whereas I now have to write something like
```haskell
test :: ()
test = foo ( #label :: Label _ Bool )
```
to specify `a`, which defeats the purpose of the overloaded labels syntax. At that point I might as well just write:
```haskell
foo ( Label @"label" @Bool )
```9.2.1