GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210304T17:27:14Zhttps://gitlab.haskell.org/ghc/ghc//issues/19487Relax Note [Phantom type variables in kinds] to allow for phantom levity vars20210304T17:27:14ZSebastian GrafRelax Note [Phantom type variables in kinds] to allow for phantom levity varsWhile implementing the unlifted datatypes proposal (!2218), I realised that an edge case violates the kinding rules (`Note [Phantom type variables in kinds]`, in particular). Specifically
```hs
type T :: forall (l :: Levity). TYPE (BoxedRep l)
data T = MkT
```
Note that
1. `T` has a nullary data con `MkT`
2. `T` is levitypolymorphic
That means the type of `MkT`, `forall {l::Levity}. T @l`, is illkinded! We have `T @l :: TYPE (BoxedRep l)` and the `forall` is supposed to bind the `l`. But the kind rule for `forall a. TYPE rep` demands that `a` is not free in `rep`:
```
ty : TYPE rep
`a` is not free in rep
(FORALL1) 
forall a. ty : TYPE rep
```
I argue that there is no harm in allowing `TYPE (BoxedRep l)` here, because `l` does not affect the *representation* of `T`. I'm unaware of any other implications this might have.
We have to be a bit careful with evaluation semantics, but we have better means (https://gitlab.haskell.org/ghc/ghc//issues/15532#note_239845, #17521) to decide whether levity polymorphism is OK at the term level. In any instance, `MkT` is a data constructor and thus is a value under both callbyneed and callbyvalue semantics. I'm reasonably positive that allowing `MkT` to be wellkinded is OK. You can't do anything with it at the term level unless you apply it to a `Levity` anyway.While implementing the unlifted datatypes proposal (!2218), I realised that an edge case violates the kinding rules (`Note [Phantom type variables in kinds]`, in particular). Specifically
```hs
type T :: forall (l :: Levity). TYPE (BoxedRep l)
data T = MkT
```
Note that
1. `T` has a nullary data con `MkT`
2. `T` is levitypolymorphic
That means the type of `MkT`, `forall {l::Levity}. T @l`, is illkinded! We have `T @l :: TYPE (BoxedRep l)` and the `forall` is supposed to bind the `l`. But the kind rule for `forall a. TYPE rep` demands that `a` is not free in `rep`:
```
ty : TYPE rep
`a` is not free in rep
(FORALL1) 
forall a. ty : TYPE rep
```
I argue that there is no harm in allowing `TYPE (BoxedRep l)` here, because `l` does not affect the *representation* of `T`. I'm unaware of any other implications this might have.
We have to be a bit careful with evaluation semantics, but we have better means (https://gitlab.haskell.org/ghc/ghc//issues/15532#note_239845, #17521) to decide whether levity polymorphism is OK at the term level. In any instance, `MkT` is a data constructor and thus is a value under both callbyneed and callbyvalue semantics. I'm reasonably positive that allowing `MkT` to be wellkinded is OK. You can't do anything with it at the term level unless you apply it to a `Levity` anyway.https://gitlab.haskell.org/ghc/ghc//issues/19482"No skolem info" with the infinite kind20210304T01:11:45ZRinat Striungis"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 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, GHC8.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)## 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, GHC8.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.2.1https://gitlab.haskell.org/ghc/ghc//issues/19457conduit1.3.4 builds with 9.0.1, but not HEAD, due to regression in typecheck...20210301T11:40:36ZRyan Scottconduit1.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 `conduit1.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/ghc9.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 HEADspecific phenomenon. Moreover, [Section 3.5 of the Haskell 2010 Report](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8300003.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/ghc9.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 etaexpanded version of `k` typechecks on both 9.0.1 and HEAD:
```hs
k :: b > c > String
k = \x > "hello" `j` x
```
cc @simonpjWhile patching `head.hackage` recently, I discovered recently that the `conduit1.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/ghc9.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 HEADspecific phenomenon. Moreover, [Section 3.5 of the Haskell 2010 Report](https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8300003.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/ghc9.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 etaexpanded 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 accepts20210303T18:29:53ZRyan ScottGHC 9.0 rejects default signature that 8.10 acceptsI originally noticed this issue in the `barbies2.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 nondefault 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#defaultmethodsignatures):
> 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.I originally noticed this issue in the `barbies2.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 nondefault 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#defaultmethodsignatures):
> 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/19428Deprecate `Winaccessiblecode`20210302T01:19:11ZSebastian GrafDeprecate `Winaccessiblecode`In https://gitlab.haskell.org/ghc/ghc//merge_requests/5100#note_333682, the special role of `Winaccessiblecode` came up. In particular, how it's not integrated well with the rest of how the patternmatch checker works today. For one, it's implemented somewhere in the typechecker, I think. But I also think its purpose is subsumed by `Woverlappingpatterns` (which will warn for *any* inaccessible RHS, not just those caused by contradictory type constraints) noawadays.
I propose to deprecate the flag.In https://gitlab.haskell.org/ghc/ghc//merge_requests/5100#note_333682, the special role of `Winaccessiblecode` came up. In particular, how it's not integrated well with the rest of how the patternmatch checker works today. For one, it's implemented somewhere in the typechecker, I think. But I also think its purpose is subsumed by `Woverlappingpatterns` (which will warn for *any* inaccessible RHS, not just those caused by contradictory type constraints) noawadays.
I propose to deprecate the flag.https://gitlab.haskell.org/ghc/ghc//issues/19419GHC 9.0 unable to deduce that instance signature is at least as general as cl...20210225T03:14:03ZsheafGHC 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 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.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/19396Surprising lack of generalisation using MonoLocalBinds20210226T21:25:06ZTom EllisSurprising lack of generalisation using MonoLocalBinds## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on HaskellCafe](https://mail.haskell.org/pipermail/haskellcafe/2021February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE ScopedTypeVariables #}
 This code came up in the context of writing a parser, but that's
 not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
 DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
 Does not type check
pFG1 :: Parser B > Parser (D B)
pFG1 pBArg = pBD GF AP <> pBD DF AM
where pBD f p = f p <$> pBArg
 Does type check
pFG2 :: Parser B > Parser (D B)
pFG2 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 Does not type check
pFG3 :: forall b. Parser b > Parser (D b)
pFG3 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 The specifics of the parser don't matter
data Parser a = Parser
(<>) :: Parser a > Parser a > Parser a
(<>) _ _ = Parser
(<$>) :: (a > b) > Parser a > Parser b
(<$>) _ _ = Parser
```## Motivation
It seems to me that `MonoLocalBinds` is too aggressive in avoiding generalisation. Please observe the example below. In `pFG1`, `pBD` is not generalised. The reason is roughly because `pBArg` does not have a monomorphic type signature, and indeed providing one, as in `pFG2`, leads to a generalised definition.
But this seems too aggressive to me. In `pFG1` the type of `pBArg` *is* known and monomorphic. Its type occurs in the type signature of `pFG1`! Could we generalise `pBD` in this case?
This is a simplified and anonymised version of real word code. This really does happen. The cause puzzled me and I'm an experienced Haskell user. I feel bad for a less experienced colleague who might try something similar but would receive a type error for code which seems like it really ought to type check.
## Proposal
Extend [the definition of "closed"](https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/let_generalisation.html) to encompass lambda bound variables whose type, from the explicit type signature of the lambda, is known and contains no free type variables.
## Notes
This issue was [discussed between @tomjaguarpaw1 and @rae on HaskellCafe](https://mail.haskell.org/pipermail/haskellcafe/2021February/133381.html).
I have included `pFG3` for *information only* in case anyone is curious what happens in the polymorphic case. They don't work even with an explicit type signature.
## Example
```haskell
{# LANGUAGE MonoLocalBinds #}
{# LANGUAGE ScopedTypeVariables #}
 This code came up in the context of writing a parser, but that's
 not terribly important
import Prelude hiding ((<$>))
data B = B
data D f = GF AP f
 DF AM f
data AM = AM
data AP = AP
pB :: Parser B
pB = Parser
 Does not type check
pFG1 :: Parser B > Parser (D B)
pFG1 pBArg = pBD GF AP <> pBD DF AM
where pBD f p = f p <$> pBArg
 Does type check
pFG2 :: Parser B > Parser (D B)
pFG2 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser B
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 Does not type check
pFG3 :: forall b. Parser b > Parser (D b)
pFG3 pBArg = pBD GF AP <> pBD DF AM
where pBArg' :: Parser b
pBArg' = pBArg
pBD f p = f p <$> pBArg'
 The specifics of the parser don't matter
data Parser a = Parser
(<>) :: Parser a > Parser a > Parser a
(<>) _ _ = Parser
(<$>) :: (a > b) > Parser a > Parser b
(<$>) _ _ = Parser
```https://gitlab.haskell.org/ghc/ghc//issues/19364oversized source range in type error message20210304T10: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:721: 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:719: 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:812: 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")
 ^^^^^
```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:721: 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:719: 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:812: 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: plots0.1.1.2 fails to build due to ambiguous type variable20210210T21:11:55ZRyan ScottGHC 9.0 regression: plots0.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 `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained 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 `ghc9.0`:
```
$ ~/Software/ghc9.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 fmaxrelevantbinds=N or fnomaxrelevantbinds)
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.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: 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 ghcbignum backend (fix #18912)`)_Originally observed in a `head.hackage` CI build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/568397#L5617)_.
The `plots0.1.1.2` library fails to compile using commit 0789f7a18a78920f50647e2b4aa8082a14ca9e90 of the `ghc9.0` branch. Here is a selfcontained 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 `ghc9.0`:
```
$ ~/Software/ghc9.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 fmaxrelevantbinds=N or fnomaxrelevantbinds)
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.1rc1. This regression was introduced at some point between the following commits:
* 9183f5a537df159e37c26d9d385cf497bcfaae30 (`gitlabci: 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 ghcbignum backend (fix #18912)`)9.0.2https://gitlab.haskell.org/ghc/ghc//issues/19272EGraphs for representation of normalised refinement types in the patternmat...20210129T23:14:50ZSebastian GrafEGraphs for representation of normalised refinement types in the patternmatch checkerI realised today that the quite complicated data structure+invariants (`Nabla`'s [`TmState`](https://gitlab.haskell.org/ghc/ghc//blob/0249974e7622e35927060da21f9231cb1e6357b9/compiler/GHC/HsToCore/Pmc/Solver/Types.hs#L125142)) we use while patternmatch coverage checking fits "egraphs" quite well.
I realised so while reading the POPL 2021 paper [*`egg`: Fast and Extensible Equality Saturation*](https://arxiv.org/abs/2004.03082). The similarity is striking. I think the inhabitation test could probably be expressed as an egraph analysis.
To be a bit more concrete, an egraph is basically a unionfind data structure on terms. If we start with the disjoint equality classes `{Just x}, {Just y}, {x}, {y}` and later find out that `x ~ y`, we'd `merge` the equality classes `{x}` and `{y}`. The egraph data structure then restores congruence, putting `Just x` and `Just y` into the same equality class as well: `{Just x, Just y}, {x, y}`. Note how this also puts the "CSE" pass envisioned in #17208 on firm ground. There we have
```hs
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```
To see that the match is exhaustive, we have to see that `reverse xs ~ reverse xs'` from `xs ~ xs'`. This is exactly the kind of congruence that egraphs maintain: Replace `Just` by `reverse` in the example above. (It does so via a technique called "upward merge" that we'd have to implement in an adhoc manner to fix #17208).
The egraph representation is quite compact and trivially supports the ∆(x) lookup from the paper (it's just the `find` operation), and extends it to expressions, ∆(e), via `canonicalize`.
While I think this is an important and useful observation, I'm not so keen about implementing it; it's a bit unclear to me if we can retain the same (mostly sufficient) efficiency that our checker has today, and #17208 alone is not compelling enough of a use case for me to pursue.
Maybe that data structure would be useful in other parts of GHC as well. I imagine that Type Family rewrites fit into the same framework. It was conceived for theorem provers, after all. Maybe it's also a useful representation for the Simplifier, although implementing it would be a huge change with possibly daunting repercussions. Still, a good data structure to have up one's sleeve.I realised today that the quite complicated data structure+invariants (`Nabla`'s [`TmState`](https://gitlab.haskell.org/ghc/ghc//blob/0249974e7622e35927060da21f9231cb1e6357b9/compiler/GHC/HsToCore/Pmc/Solver/Types.hs#L125142)) we use while patternmatch coverage checking fits "egraphs" quite well.
I realised so while reading the POPL 2021 paper [*`egg`: Fast and Extensible Equality Saturation*](https://arxiv.org/abs/2004.03082). The similarity is striking. I think the inhabitation test could probably be expressed as an egraph analysis.
To be a bit more concrete, an egraph is basically a unionfind data structure on terms. If we start with the disjoint equality classes `{Just x}, {Just y}, {x}, {y}` and later find out that `x ~ y`, we'd `merge` the equality classes `{x}` and `{y}`. The egraph data structure then restores congruence, putting `Just x` and `Just y` into the same equality class as well: `{Just x, Just y}, {x, y}`. Note how this also puts the "CSE" pass envisioned in #17208 on firm ground. There we have
```hs
safeLast3 :: [a] > Maybe a
safeLast3 xs
 [] < reverse xs = Nothing
safeLast3 xs'
 (x:_) < reverse xs' = Just x
```
To see that the match is exhaustive, we have to see that `reverse xs ~ reverse xs'` from `xs ~ xs'`. This is exactly the kind of congruence that egraphs maintain: Replace `Just` by `reverse` in the example above. (It does so via a technique called "upward merge" that we'd have to implement in an adhoc manner to fix #17208).
The egraph representation is quite compact and trivially supports the ∆(x) lookup from the paper (it's just the `find` operation), and extends it to expressions, ∆(e), via `canonicalize`.
While I think this is an important and useful observation, I'm not so keen about implementing it; it's a bit unclear to me if we can retain the same (mostly sufficient) efficiency that our checker has today, and #17208 alone is not compelling enough of a use case for me to pursue.
Maybe that data structure would be useful in other parts of GHC as well. I imagine that Type Family rewrites fit into the same framework. It was conceived for theorem provers, after all. Maybe it's also a useful representation for the Simplifier, although implementing it would be a huge change with possibly daunting repercussions. Still, a good data structure to have up one's sleeve.https://gitlab.haskell.org/ghc/ghc//issues/19197‘:kind () :: '()’ doesn't give any output20210118T17:11:59ZIcelandjack‘:kind () :: '()’ doesn't give any output```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
ghci> :k (_, _) :: '(_, _)
ghci>
ghci> import Data.Functor.Identity
ghci> :k Identity _ :: 'Identity _
ghci>
```
It should give an error```
$ ./ghc/_build/stage1/bin/ghc ignoredotghci interactive
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/ :? for help
ghci> :set XKindSignatures XDataKinds
ghci> :k () :: '()
ghci>
ghci> :set XPartialTypeSignatures Wnopartialtypesignatures
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 given20210111T03: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 #}
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:1925
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:1017
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:1656
• 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 #16627The 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:1925
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:1017
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:1656
• 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 applications20210221T16: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`. 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.xThe 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...20210222T09:40:05ZsheafGHC 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 #}
{# 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/firexamples/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 )
```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/firexamples/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.1https://gitlab.haskell.org/ghc/ghc//issues/19142panic lookup_final_id with fdefertypeerrors and kind error in instance def...20210122T21:09:33ZJakob Brünkerpanic lookup_final_id with fdefertypeerrors and kind error in instance definition## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64## Summary
This file
```haskell
{# OPTIONS_GHC fdefertypeerrors #}
{# LANGUAGE ExplicitForAll
, TypeApplications
, KindSignatures
, FlexibleInstances
#}
foo :: forall (f :: * > *) . String
foo = ""
instance Show a where
show _ = foo @Int
```
produces the following error:
```
Bug.hs:12:17: warning: [Wdeferredtypeerrors]
• Expected kind ‘* > *’, but ‘Int’ has kind ‘*’
• In the type ‘Int’
In the expression: foo @Int
In an equation for ‘show’: show _ = foo @Int

12  show _ = foo @Int
 ^^^
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
lookup_final_id
$fShowa
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Iface/Tidy.hs:200:12 in ghc:GHC.Iface.Tidy
```
Without `fdefertypeerrors`, only the kind error would be shown, not the panic.
## Expected behavior
GHC shouldn't panic
## Environment
* GHC version used: 9.0.0.20201227 as well as 8.10.2
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/19140panic: No skolem info when trying to use variable with polymorphic kind as Ty...20201231T13:44:07ZJakob Brünkerpanic: No skolem info when trying to use variable with polymorphic kind as Type/Constraint## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the following three instances trigger the error
```haskell
{# LANGUAGE ExplicitForAll , PolyKinds #}
instance (forall (a :: k) . a) => Show b
instance (forall (a :: k) . Show a) => Show b
instance (forall (a :: k) . a > a) => Show b
```
Error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
No skolem info:
[k_aEZ[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
8.10 has the expected behavior: show the following type error
```
Bug.hs:3:29: error:
• Expected a constraint, but ‘a’ has kind ‘k’
• In the instance declaration for ‘Show b’

3  instance (forall (a :: k) . a) => Show b
 ^
Bug.hs:4:34: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the first argument of ‘Show’, namely ‘a’
In the instance declaration for ‘Show b’

4  instance (forall (a :: k) . Show a) => Show b
 ^
Bug.hs:5:29: error:
• Expected a constraint, but ‘a > a’ has kind ‘*’
• In the instance declaration for ‘Show b’

5  instance (forall (a :: k) . a > a) => Show b
 ^^^^^^
Failed, no modules loaded.
```
## Environment
* GHC version used: 9.0.0.20201227
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_64## Summary
In a quantified constraint in the context for an instance declaration, when trying to use a type variable with a polymorphic kind as either a `Type` or a `Constraint`, ghc will panic.
## Steps to reproduce
Each of the following three instances trigger the error
```haskell
{# LANGUAGE ExplicitForAll , PolyKinds #}
instance (forall (a :: k) . a) => Show b
instance (forall (a :: k) . Show a) => Show b
instance (forall (a :: k) . a > a) => Show b
```
Error:
```
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20201227:
No skolem info:
[k_aEZ[sk:1]]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Outputable.hs:1230:37 in ghc:GHC.Utils.Outputable
pprPanic, called at compiler/GHC/Tc/Errors.hs:2810:17 in ghc:GHC.Tc.Errors
```
## Expected behavior
8.10 has the expected behavior: show the following type error
```
Bug.hs:3:29: error:
• Expected a constraint, but ‘a’ has kind ‘k’
• In the instance declaration for ‘Show b’

3  instance (forall (a :: k) . a) => Show b
 ^
Bug.hs:4:34: error:
• Expected a type, but ‘a’ has kind ‘k’
• In the first argument of ‘Show’, namely ‘a’
In the instance declaration for ‘Show b’

4  instance (forall (a :: k) . Show a) => Show b
 ^
Bug.hs:5:29: error:
• Expected a constraint, but ‘a > a’ has kind ‘*’
• In the instance declaration for ‘Show b’

5  instance (forall (a :: k) . a > a) => Show b
 ^^^^^^
Failed, no modules loaded.
```
## Environment
* GHC version used: 9.0.0.20201227
Optional:
* Operating System: Ubuntu inside WSL2 inside Windows 10
* System Architecture: x86_649.2.1https://gitlab.haskell.org/ghc/ghc//issues/19137Incorrect documentation around EqualCtList20201230T19:59:58ZRichard Eisenbergrae@richarde.devIncorrect documentation around EqualCtListThe solver maintains a structure `EqualCtList`, with this Note:
```
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* All are equalities
* All these equalities have the same LHS
* The list is never empty
* No element of the list can rewrite any other
* Derived before Wanted
From the fourth invariant it follows that the list is
 A single [G], or
 Zero or one [D] or [WD], followed by any number of [W]
The Wanteds can't rewrite anything which is why we put them last
```
Yet this isn't quite accurate. If we have a `[G] a ~R Bool` and a `[D] a ~ Int`, neither can rewrite the other. Both can live in the `EqualCtList` quite peacefully. Thus, the "it follows that" is wrong. Worse, the rewriter contains the code
```hs
; case lookupDVarEnv ieqs tv of
Just (EqualCtList (ct : _))  If the first doesn't work,
 the subsequent ones won't either
 CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } < ct
```
but the comment there isn't true: the first might not work, but maybe a later one will.
I tried quite hard to come up with some misbehavior that this misunderstanding caused, but it's quite hard. An example with a Given that contains a touchable metavariable wouldn't be convincing (#18929), and all other examples seem to lead to program rejection. And because the prioritization of some errors over others, it's hard to see the bad error.
Yet I still think there is a problem here, and that we should search through the list looking for a valid inert.The solver maintains a structure `EqualCtList`, with this Note:
```
Note [EqualCtList invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* All are equalities
* All these equalities have the same LHS
* The list is never empty
* No element of the list can rewrite any other
* Derived before Wanted
From the fourth invariant it follows that the list is
 A single [G], or
 Zero or one [D] or [WD], followed by any number of [W]
The Wanteds can't rewrite anything which is why we put them last
```
Yet this isn't quite accurate. If we have a `[G] a ~R Bool` and a `[D] a ~ Int`, neither can rewrite the other. Both can live in the `EqualCtList` quite peacefully. Thus, the "it follows that" is wrong. Worse, the rewriter contains the code
```hs
; case lookupDVarEnv ieqs tv of
Just (EqualCtList (ct : _))  If the first doesn't work,
 the subsequent ones won't either
 CEqCan { cc_ev = ctev, cc_lhs = TyVarLHS tv
, cc_rhs = rhs_ty, cc_eq_rel = ct_eq_rel } < ct
```
but the comment there isn't true: the first might not work, but maybe a later one will.
I tried quite hard to come up with some misbehavior that this misunderstanding caused, but it's quite hard. An example with a Given that contains a touchable metavariable wouldn't be convincing (#18929), and all other examples seem to lead to program rejection. And because the prioritization of some errors over others, it's hard to see the bad error.
Yet I still think there is a problem here, and that we should search through the list looking for a valid inert.https://gitlab.haskell.org/ghc/ghc//issues/19131Does the subtype check in Note [Impedance matching] ever fail?20210217T13:00:27ZRichard Eisenbergrae@richarde.devDoes the subtype check in Note [Impedance matching] ever fail?`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a > Bool > Bool
g_mono_ty :: [b] > Bool > Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a > Bool > Bool
g :: forall b. [b] > Bool > Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a > Bool > Bool, [b] > Bool > Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) > f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) > g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a > F a
where F is a noninjective type function.
```
This describes a subtype check. That subtype check is performed with the context returned from this function:
```hs
mk_impedance_match_msg :: MonoBindInfo
> TcType > TcType
> TidyEnv > TcM (TidyEnv, SDoc)
 This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) < zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) < zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing > text "inferred"
Just sig  isPartialSig sig > text "(partial)"
 otherwise > empty
```
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this subtype check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.`GHC.Tc.Gen.Bind` tells us
```
Note [Impedance matching]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f 0 x = x
f n x = g [] (not x)
g [] y = f 10 y
g _ y = f 9 y
After typechecking we'll get
f_mono_ty :: a > Bool > Bool
g_mono_ty :: [b] > Bool > Bool
with constraints
(Eq a, Num a)
Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
The types we really want for f and g are
f :: forall a. (Eq a, Num a) => a > Bool > Bool
g :: forall b. [b] > Bool > Bool
We can get these by "impedance matching":
tuple :: forall a b. (Eq a, Num a) => (a > Bool > Bool, [b] > Bool > Bool)
tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
f a d1 d2 = case tuple a Any d1 d2 of (f, g) > f
g b = case tuple Integer b dEqInteger dNumInteger of (f,g) > g
Suppose the shared quantified tyvars are qtvs and constraints theta.
Then we want to check that
forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype
and the proof is the impedance matcher.
Notice that the impedance matcher may do defaulting. See #7173.
It also cleverly does an ambiguity check; for example, rejecting
f :: F a > F a
where F is a noninjective type function.
```
This describes a subtype check. That subtype check is performed with the context returned from this function:
```hs
mk_impedance_match_msg :: MonoBindInfo
> TcType > TcType
> TidyEnv > TcM (TidyEnv, SDoc)
 This is a rare but rather awkward error messages
mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
inf_ty sig_ty tidy_env
= do { (tidy_env1, inf_ty) < zonkTidyTcType tidy_env inf_ty
; (tidy_env2, sig_ty) < zonkTidyTcType tidy_env1 sig_ty
; let msg = vcat [ text "When checking that the inferred type"
, nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
, text "is as general as its" <+> what <+> text "signature"
, nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
; return (tidy_env2, msg) }
where
what = case mb_sig of
Nothing > text "inferred"
Just sig  isPartialSig sig > text "(partial)"
 otherwise > empty
```
A search in the testsuite shows no occurrence of "When checking that the inferred type".
So: Does this subtype check ever fail? If so, we should have a test case in the testsuite for this message. If not, we should explain why failure is impossible and then remove the above function.https://gitlab.haskell.org/ghc/ghc//issues/19107GADT pattern match defeats instance solving20210125T22:41:18ZRichard Eisenbergrae@richarde.devGADT pattern match defeats instance solvingWhen I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.When I say
```hs
{# LANGUAGE GADTs #}
 NB: NO FlexibleContexts
module Bug where
data T a where
MkT :: Show a => [a] > T a
f (MkT x) = show x
```
GHC says
```
Bug.hs:8:1: error:
• Non typevariable argument in the constraint: Show [a]
(Use FlexibleContexts to permit this)
• When checking the inferred type
f :: forall {a}. Show [a] => T a > String
```
The problem is that GHC wants to infer `f :: Show [a] => T a > String`. Yet the correct type is `f :: Show a => T a > String`, with the simplified `Show a` constraint.
The reason this happens is that the solver ends up in this scenario:
```
at level 2
[G] Show alpha[tau:1]
[W] Show [alpha[tau:1]]
```
Before committing to the toplevel `Show a => Show [a]` instance, GHC checks whether any Givens might fire later. It worries `Show alpha` might apply later. But this would be impossible unless `alpha` becomes an infinitely nested list. There is already logic in `lookupInstEnv'` to usefully ignore such absurdities in instance lookup (see `Note [Infinitary substitution in lookup]` in GHC.Core.InstEnv), and we should extend this logic to `matchableGivens`.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19106Partial type signature variable confuses instance solving20210125T22:40:41ZRichard Eisenbergrae@richarde.devPartial type signature variable confuses instance solvingWhen I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.When I say
```hs
{# LANGUAGE TypeFamilies, GADTs #}
module Bug where
f :: (a ~ [b]) => T a > _ > String
f (MkT x) _ = show x
data T a where
MkT :: G a => a > T a
type family G a where
G [b] = Show b
```
I get
```
Bug.hs:6:1: error:
• Could not deduce (Show b)
from the context: a ~ [b]
bound by the inferred type for ‘f’:
forall a b {w}. (a ~ [b]) => T a > w > String
at Bug.hs:6:120
• When checking that the inferred type
f :: forall {a} {b} {w}. (a ~ [b], Show [b]) => T a > w > String
is as general as its (partial) signature
f :: forall a b {w}. (a ~ [b]) => T a > w > String
```
We end up with
```
[G] Show b[tyv:1]
[W] Show [b[tyv:1]]
```
The check in `matchableGivens` considers `b` a metavariable. This isn't entirely wrong, but `b` is a `TyVarTv`, and should not be considered unifiable in `matchableGivens`. The solution is very easy: just change `matchableGivens` to treat `TyVarTv`s like skolems.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.dev