GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210511T03:26:51Zhttps://gitlab.haskell.org/ghc/ghc//issues/19815Use isReflexiveCo when building an MCo20210511T03:26:51ZSimon Peyton JonesUse isReflexiveCo when building an MCoIn other work I found that checking for reflexivity (using `isReflexiveCo` rather than `isReflCo`) when building an MCoercion had an astonishing impact on T18223. Compile time allocation reduced by a factor of four!
This tickets is to check whether it's a good idea generally.In other work I found that checking for reflexivity (using `isReflexiveCo` rather than `isReflCo`) when building an MCoercion had an astonishing impact on T18223. Compile time allocation reduced by a factor of four!
This tickets is to check whether it's a good idea generally.https://gitlab.haskell.org/ghc/ghc//issues/19787Weird behaviour with `tcIfaceExpr`20210503T17:41:43ZJosh MeredithWeird behaviour with `tcIfaceExpr`When recovering the Core AST of a class method in a plugin through multiple methods, the typecheck loaded (deserialised) AST appears to be using the wrong expression for certain methods. This occurs both using ASTs recovered from the preexisting unfoldings, as well as when using the `toIfaceBind` and `tcIfaceExpr` functions from GHC to (de)serialise the bindings via an extensible interface field.
As an example, using the following type class and instances:
```haskell
class TwoClass a where
twoA :: a > Integer
twoB :: a > Bool
instance TwoClass Integer where
twoA = id
twoB = (>1)
instance TwoClass Bool where
twoA True = 1
twoA False = 0
twoB = not
```
_Before_ serialisation, from the `CgGuts.cgBinds`, we have class methods that look like:
```
twoA :: forall a. TwoClass a => a > Integer
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(SL,A)>,
RULES: Built in rule for twoA: "Class op twoA"]
twoA
= \ (@a) (v_B1 :: TwoClass a) >
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 > v_B2 },
twoB :: forall a. TwoClass a => a > Bool
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(A,SL)>,
RULES: Built in rule for twoB: "Class op twoB"]
twoB
= \ (@a) (v_B1 :: TwoClass a) >
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 > v_B3 }
```
Each of the class methods is deconstructed as a data constructor and obviously uses the correct field of that constructor as the method. However, after roundtripping this through (de)serialisation, we're have:
```
twoA :: forall a. TwoClass a => a > Integer
[LclId]
twoA
= \ (@a) (v :: TwoClass a) > case v of v { C:TwoClass v v > v },
twoB :: forall a. TwoClass a => a > Bool
[LclId]
twoB
= \ (@a) (v :: TwoClass a) > case v of v { C:TwoClass v v > v }
```
Now, the reuse of the variable name `v` shouldn't be a problem on it's own  since these local variables are serialised as `FastStrings`, which have `Unique`s  but we find in the plugin that for `twoA`, it's the _wrong_ `Unique`, incorrectly giving `twoA` an expression of type `a > Bool`.
We're using GHC 8.10.4 for the Plutus plugin, but I've tested and found what seems to be the same behaviour in an uptodate version of master. I expect that there must be another explanation here, since unfoldings are used by GHC for inlining, and I don't believe those would go unnoticed if broken.When recovering the Core AST of a class method in a plugin through multiple methods, the typecheck loaded (deserialised) AST appears to be using the wrong expression for certain methods. This occurs both using ASTs recovered from the preexisting unfoldings, as well as when using the `toIfaceBind` and `tcIfaceExpr` functions from GHC to (de)serialise the bindings via an extensible interface field.
As an example, using the following type class and instances:
```haskell
class TwoClass a where
twoA :: a > Integer
twoB :: a > Bool
instance TwoClass Integer where
twoA = id
twoB = (>1)
instance TwoClass Bool where
twoA True = 1
twoA False = 0
twoB = not
```
_Before_ serialisation, from the `CgGuts.cgBinds`, we have class methods that look like:
```
twoA :: forall a. TwoClass a => a > Integer
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(SL,A)>,
RULES: Built in rule for twoA: "Class op twoA"]
twoA
= \ (@a) (v_B1 :: TwoClass a) >
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 > v_B2 },
twoB :: forall a. TwoClass a => a > Bool
[GblId[ClassOp],
Arity=1,
Caf=NoCafRefs,
Str=<SP(A,SL)>,
RULES: Built in rule for twoB: "Class op twoB"]
twoB
= \ (@a) (v_B1 :: TwoClass a) >
case v_B1 of v_B1 { C:TwoClass v_B2 v_B3 > v_B3 }
```
Each of the class methods is deconstructed as a data constructor and obviously uses the correct field of that constructor as the method. However, after roundtripping this through (de)serialisation, we're have:
```
twoA :: forall a. TwoClass a => a > Integer
[LclId]
twoA
= \ (@a) (v :: TwoClass a) > case v of v { C:TwoClass v v > v },
twoB :: forall a. TwoClass a => a > Bool
[LclId]
twoB
= \ (@a) (v :: TwoClass a) > case v of v { C:TwoClass v v > v }
```
Now, the reuse of the variable name `v` shouldn't be a problem on it's own  since these local variables are serialised as `FastStrings`, which have `Unique`s  but we find in the plugin that for `twoA`, it's the _wrong_ `Unique`, incorrectly giving `twoA` an expression of type `a > Bool`.
We're using GHC 8.10.4 for the Plutus plugin, but I've tested and found what seems to be the same behaviour in an uptodate version of master. I expect that there must be another explanation here, since unfoldings are used by GHC for inlining, and I don't believe those would go unnoticed if broken.https://gitlab.haskell.org/ghc/ghc//issues/19765Inscope check for type variables can be confusing in presence of runtime rep...20210429T12:41:33ZRichard Eisenbergrae@richarde.devInscope check for type variables can be confusing in presence of runtime representation polymorphismFrom #19764, thanks to @yaitskov:
```hs
{# LANGUAGE DeriveLift #}
{# LANGUAGE StandaloneDeriving #}
module Main where
import Language.Haskell.TH.Syntax (Lift (..))
newtype Ref = Ref { r :: ()} deriving (Lift)
deriving instance Lift ()
main :: IO ()
main = pure ()
```
This prints
```
/Users/rae/temp/Bug.hs:8:41: error:
• Overlapping instances for Lift ()
arising from the first field of ‘Ref’ (type ‘()’)
Matching instances:
two instances involving outofscope types
(use fprintpotentialinstances to see them all)
• When deriving the instance for (Lift Ref)

8  newtype Ref = Ref { r :: ()} deriving (Lift)

```
The "instances involving outofscope types" are both `Lift ()`. Note that `Lift` is in scope. So GHC must be confused about `()`, which is a shame.From #19764, thanks to @yaitskov:
```hs
{# LANGUAGE DeriveLift #}
{# LANGUAGE StandaloneDeriving #}
module Main where
import Language.Haskell.TH.Syntax (Lift (..))
newtype Ref = Ref { r :: ()} deriving (Lift)
deriving instance Lift ()
main :: IO ()
main = pure ()
```
This prints
```
/Users/rae/temp/Bug.hs:8:41: error:
• Overlapping instances for Lift ()
arising from the first field of ‘Ref’ (type ‘()’)
Matching instances:
two instances involving outofscope types
(use fprintpotentialinstances to see them all)
• When deriving the instance for (Lift Ref)

8  newtype Ref = Ref { r :: ()} deriving (Lift)

```
The "instances involving outofscope types" are both `Lift ()`. Note that `Lift` is in scope. So GHC must be confused about `()`, which is a shame.https://gitlab.haskell.org/ghc/ghc//issues/19726Unexpected typechecking behavior with let and DataKinds20210510T12:28:34ZbenjaminUnexpected typechecking behavior with let and DataKinds## Motivation
When playing around with the code for knownlength vectors from #19722, I noticed following behavior in the typechecker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a > a
last (x :> Nil) = x
last (_ :> xs) = case xs of x' :> xs' > last xs
last (_ :> xs) = let (x' :> xs') = xs in last xs
last (_ :> xs) = let (x' :> xs') = xs in last (x' :> xs')
```
The main issue here is that we can't just write `last (_ :> xs) = last xs`, because then GHC can't verify that the type of `xs` is really `Vec (Succ n) a`.
So the workaround is to let GHC know that `xs` is really nonempty in this second case.
The first version of the case `_ :> xs` using a caseexpression compiles fine, but the two version implemented using letexpressions don't typecheck.
I lack an indepth understanding of the typechecker or even the DataKinds extension, but I think the 3 versions are semantically identical.
## Proposal
Make all 3 versions typecheck.## Motivation
When playing around with the code for knownlength vectors from #19722, I noticed following behavior in the typechecker when trying to implement a function to get the last element of a vector.
```
last :: Vec (Succ n) a > a
last (x :> Nil) = x
last (_ :> xs) = case xs of x' :> xs' > last xs
last (_ :> xs) = let (x' :> xs') = xs in last xs
last (_ :> xs) = let (x' :> xs') = xs in last (x' :> xs')
```
The main issue here is that we can't just write `last (_ :> xs) = last xs`, because then GHC can't verify that the type of `xs` is really `Vec (Succ n) a`.
So the workaround is to let GHC know that `xs` is really nonempty in this second case.
The first version of the case `_ :> xs` using a caseexpression compiles fine, but the two version implemented using letexpressions don't typecheck.
I lack an indepth understanding of the typechecker or even the DataKinds extension, but I think the 3 versions are semantically identical.
## Proposal
Make all 3 versions typecheck.https://gitlab.haskell.org/ghc/ghc//issues/19690Bottom dictionaries can be derived with QuantifiedConstraints, UndecidableIns...20210416T00:27:00ZaadaafgtaaBottom 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 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
nontermination 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: x8664[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
nontermination 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: x8664https://gitlab.haskell.org/ghc/ghc//issues/19682Constraint solver regression in 9.220210506T20:41:18ZAndres LöhConstraint solver regression in 9.2## Summary
While trying to make the `genericssop` and `sopcore` 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 `ghc9.2` branch at commit d197fb3d5c053cfb526272c29a443c33d1af0980
Optional:
* Operating System: Linux (NixOS)
* System Architecture: x86_64## Summary
While trying to make the `genericssop` and `sopcore` 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 `ghc9.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 FunTy20210412T15:42:16ZRichard 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
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.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/19675runExists: a typelevel version of runRW20210409T20:55:20ZSimon Peyton JonesrunExists: a typelevel version of runRW(All this started in #16646.)
# Problem
In GHC.TypeLits we have
```
newtype SSymbol (s :: Symbol) = SSymbol String
```
The intent is that this type is very private to GHC.TypeLits, beucase
it is supposed to be a singleton type. If we have two values `x1, x2
:: SSymbol ty`, then the string inside `x1` should be the same as the
string inside `x2`.
How do we make a `SSymbol`? We want to provide
```
withSSymbol :: String > (forall s. SSymbol s > r) > r
```
Note the `forall s`, which plays a similar (existential) role to the `forall s` in
```
runST :: (forall s. ST s a) > a
```
But how can we *define* `withSSymbol`? Here is a try:
```
withSSymbol str cont = cont (SSymbol str)
```
But if we elaborate we find this means:
```
withSSymbol str cont = cont @(Any @Symbol) (SSymbol @(Any @Symbol) str)
```
What is that `Any`??? And consider
```
withSSymbol "foo" (\s1 > withSSymbol "bar2 (\s2 > blah)
```
If we allow `withSSymbol` to inline we can get
```
let s1 = SSymbol @(Any @Symbol) "foo"
s2 = SSymbol @(Any @Symbol) "bar"
in blah
```
Urk! `s1, s2 :: SSymbol (Any @Symbol)` but they carry different payloads.
In conjunction with `magicDict` this can give rise to subtle outright bugs:
see #16586 and `Note [NOINLINE someNatVal]` in GHC.TypeNats.
The hacky "solution" (adopted by the patch for #16586) is "don't
inline `withSSymbol`" but that is smelly  and inefficient!
# Solution
So what can we do? Here is one suggestion. Suppose we had
```
runExists :: forall k. (forall (a::k). Proxy# @k a > r) > r
```
Rather like `runST`, this gives you a type variable you can refer to, that is effectively existential.
Now we can write
```
withSSymbol str cont = runExists (\(_::Proxy# s) > cont (SSymbol @s str))
```
So `runExists` allows us to bring into scope a fresh skolem type variable.
**Note 1:** If we had biglambda in the source language, as Richard wants, maybe we could even get rid of the `Proxy#`
and write
```
runExists :: forall k. (forall (a::k). r) > r
withSSymbol str cont = runExists (\@s > cont (SSymbol @s str))
```
which would be quite a bit nicer. **End of note 1**
We already have something very like `runExists`, in the form of `runRW#`
```
runRW# :: forall (r :: RuntimeRep) (o :: TYPE r).
(State# RealWorld > o) > o
 See Note [runRW magic] in GHC.CoreToStg.Prep.
{# NOINLINE runRW# #}  runRW# is inlined manually in CorePrep
runRW# m = m realWorld#
```
where `Note [runRW magic]` in GHC.CoreToStg.Prep (reproduced below) describes various bit of magic are described that allow us to optimise around `runRW`. In particular:
* case expressions move inside the argument
* we inline `runRW#` in CorePrep, to eliminate the lambda.
We could do the same for `runExists`.
The advantage of this is that *we don't need any NOINLINE stuff for `withSSymbol` and friends*.
Only `runExists` is magic.
**Note 2.** Actually we'd want `runExists to have a levitypolymorphic result, thus:
```
runExists :: forall k (r :: RuntimeRep) (o :: TYPE r).
(forall (a::k). o) > o
```
**End of Note2**.
Question: can we somehow combine `runRW#` and `runExists`? I think they may be a bit different:
* `runExists` brings a new skolem type variable into scope
* `runRW` brings a valuelevel token into scope  it's a *value* lambda
## Note [runRW magic]
Reproduced from GHC.CoreToStg.Prep
```
{ Note [runRW magic]
~~~~~~~~~~~~~~~~~~~~~
Some definitions, for instance @runST@, must have careful control over float out
of the bindings in their body. Consider this use of @runST@,
f x = runST ( \ s > let (a, s') = newArray# 100 [] s
(_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s'' )
If we inline @runST@, we'll get:
f x = let (a, s') = newArray# 100 [] realWorld#{NB}
(_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s''
And now if we allow the @newArray#@ binding to float out to become a CAF,
we end up with a result that is totally and utterly wrong:
f = let (a, s') = newArray# 100 [] realWorld#{NB}  YIKES!!!
in \ x >
let (_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s''
All calls to @f@ will share a {\em single} array! Clearly this is nonsense and
must be prevented.
This is what @runRW#@ gives us: by being inlined extremely late in the
optimization (right before lowering to STG, in CorePrep), we can ensure that
no further floating will occur. This allows us to safely inline things like
@runST@, which are otherwise needlessly expensive (see #10678 and #5916).
'runRW' has a variety of quirks:
* 'runRW' is knownkey with a NOINLINE definition in
GHC.Magic. This definition is used in cases where runRW is curried.
* In addition to its normal Haskell definition in GHC.Magic, we give it
a special late inlining here in CorePrep and GHC.StgToByteCode, avoiding
the incorrect sharing due to floatout noted above.
* It is levitypolymorphic:
runRW# :: forall (r1 :: RuntimeRep). (o :: TYPE r)
=> (State# RealWorld > (# State# RealWorld, o #))
> (# State# RealWorld, o #)
* It has some special simplification logic to allow unboxing of results when
runRW# appears in a strict context. See Note [Simplification of runRW#]
below.
* Since its body is inlined, we allow runRW#'s argument to contain jumps to
join points. That is, the following is allowed:
join j x = ...
in runRW# @_ @_ (\s > ... jump j 42 ...)
The Core Linter knows about this. See Note [Linting of runRW#] in
GHC.Core.Lint for details.
The occurrence analyser and SetLevels also know about this, as described in
Note [Simplification of runRW#].
Other relevant Notes:
* Note [Simplification of runRW#] below, describing a transformation of runRW
applications in strict contexts performed by the simplifier.
* Note [Linting of runRW#] in GHC.Core.Lint
* Note [runRW arg] below, describing a nonobvious case where the
lateinlining could go wrong.
```(All this started in #16646.)
# Problem
In GHC.TypeLits we have
```
newtype SSymbol (s :: Symbol) = SSymbol String
```
The intent is that this type is very private to GHC.TypeLits, beucase
it is supposed to be a singleton type. If we have two values `x1, x2
:: SSymbol ty`, then the string inside `x1` should be the same as the
string inside `x2`.
How do we make a `SSymbol`? We want to provide
```
withSSymbol :: String > (forall s. SSymbol s > r) > r
```
Note the `forall s`, which plays a similar (existential) role to the `forall s` in
```
runST :: (forall s. ST s a) > a
```
But how can we *define* `withSSymbol`? Here is a try:
```
withSSymbol str cont = cont (SSymbol str)
```
But if we elaborate we find this means:
```
withSSymbol str cont = cont @(Any @Symbol) (SSymbol @(Any @Symbol) str)
```
What is that `Any`??? And consider
```
withSSymbol "foo" (\s1 > withSSymbol "bar2 (\s2 > blah)
```
If we allow `withSSymbol` to inline we can get
```
let s1 = SSymbol @(Any @Symbol) "foo"
s2 = SSymbol @(Any @Symbol) "bar"
in blah
```
Urk! `s1, s2 :: SSymbol (Any @Symbol)` but they carry different payloads.
In conjunction with `magicDict` this can give rise to subtle outright bugs:
see #16586 and `Note [NOINLINE someNatVal]` in GHC.TypeNats.
The hacky "solution" (adopted by the patch for #16586) is "don't
inline `withSSymbol`" but that is smelly  and inefficient!
# Solution
So what can we do? Here is one suggestion. Suppose we had
```
runExists :: forall k. (forall (a::k). Proxy# @k a > r) > r
```
Rather like `runST`, this gives you a type variable you can refer to, that is effectively existential.
Now we can write
```
withSSymbol str cont = runExists (\(_::Proxy# s) > cont (SSymbol @s str))
```
So `runExists` allows us to bring into scope a fresh skolem type variable.
**Note 1:** If we had biglambda in the source language, as Richard wants, maybe we could even get rid of the `Proxy#`
and write
```
runExists :: forall k. (forall (a::k). r) > r
withSSymbol str cont = runExists (\@s > cont (SSymbol @s str))
```
which would be quite a bit nicer. **End of note 1**
We already have something very like `runExists`, in the form of `runRW#`
```
runRW# :: forall (r :: RuntimeRep) (o :: TYPE r).
(State# RealWorld > o) > o
 See Note [runRW magic] in GHC.CoreToStg.Prep.
{# NOINLINE runRW# #}  runRW# is inlined manually in CorePrep
runRW# m = m realWorld#
```
where `Note [runRW magic]` in GHC.CoreToStg.Prep (reproduced below) describes various bit of magic are described that allow us to optimise around `runRW`. In particular:
* case expressions move inside the argument
* we inline `runRW#` in CorePrep, to eliminate the lambda.
We could do the same for `runExists`.
The advantage of this is that *we don't need any NOINLINE stuff for `withSSymbol` and friends*.
Only `runExists` is magic.
**Note 2.** Actually we'd want `runExists to have a levitypolymorphic result, thus:
```
runExists :: forall k (r :: RuntimeRep) (o :: TYPE r).
(forall (a::k). o) > o
```
**End of Note2**.
Question: can we somehow combine `runRW#` and `runExists`? I think they may be a bit different:
* `runExists` brings a new skolem type variable into scope
* `runRW` brings a valuelevel token into scope  it's a *value* lambda
## Note [runRW magic]
Reproduced from GHC.CoreToStg.Prep
```
{ Note [runRW magic]
~~~~~~~~~~~~~~~~~~~~~
Some definitions, for instance @runST@, must have careful control over float out
of the bindings in their body. Consider this use of @runST@,
f x = runST ( \ s > let (a, s') = newArray# 100 [] s
(_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s'' )
If we inline @runST@, we'll get:
f x = let (a, s') = newArray# 100 [] realWorld#{NB}
(_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s''
And now if we allow the @newArray#@ binding to float out to become a CAF,
we end up with a result that is totally and utterly wrong:
f = let (a, s') = newArray# 100 [] realWorld#{NB}  YIKES!!!
in \ x >
let (_, s'') = fill_in_array_or_something a x s'
in freezeArray# a s''
All calls to @f@ will share a {\em single} array! Clearly this is nonsense and
must be prevented.
This is what @runRW#@ gives us: by being inlined extremely late in the
optimization (right before lowering to STG, in CorePrep), we can ensure that
no further floating will occur. This allows us to safely inline things like
@runST@, which are otherwise needlessly expensive (see #10678 and #5916).
'runRW' has a variety of quirks:
* 'runRW' is knownkey with a NOINLINE definition in
GHC.Magic. This definition is used in cases where runRW is curried.
* In addition to its normal Haskell definition in GHC.Magic, we give it
a special late inlining here in CorePrep and GHC.StgToByteCode, avoiding
the incorrect sharing due to floatout noted above.
* It is levitypolymorphic:
runRW# :: forall (r1 :: RuntimeRep). (o :: TYPE r)
=> (State# RealWorld > (# State# RealWorld, o #))
> (# State# RealWorld, o #)
* It has some special simplification logic to allow unboxing of results when
runRW# appears in a strict context. See Note [Simplification of runRW#]
below.
* Since its body is inlined, we allow runRW#'s argument to contain jumps to
join points. That is, the following is allowed:
join j x = ...
in runRW# @_ @_ (\s > ... jump j 42 ...)
The Core Linter knows about this. See Note [Linting of runRW#] in
GHC.Core.Lint for details.
The occurrence analyser and SetLevels also know about this, as described in
Note [Simplification of runRW#].
Other relevant Notes:
* Note [Simplification of runRW#] below, describing a transformation of runRW
applications in strict contexts performed by the simplifier.
* Note [Linting of runRW#] in GHC.Core.Lint
* Note [runRW arg] below, describing a nonobvious case where the
lateinlining could go wrong.
```https://gitlab.haskell.org/ghc/ghc//issues/19652GHC's failure to rewrite in coercions & kinds leads to spurious occurscheck ...20210408T08:48:53ZRichard Eisenbergrae@richarde.devGHC's failure to rewrite in coercions & kinds leads to spurious occurscheck failureConsider this mess:
```hs
{# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () > k1 > k2 > k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 > k2 > Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () > Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u > a > Proxy b > Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```
GHC fails (in the RHS of `g`) with an occurscheck, but it should succeed.
The problem is that we end up with
```
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
```
where we have already unified `upsilon := '()`.
But GHC refuses to rewrite in kinds, so the `Const` never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type` and `beta := Any @Type > sym (AxConst Type (Any @Type))`.
Proposed solution:
The wanted above actually gets simplified to become
```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta > co) :: Type)
```
The `co` is easily solved. Then, when we get to `w2`, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha` is free in `co` and reorient, giving
```
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha > sym co :: Const '() Type alpha)
```
which can be solved by unifying `beta := alpha > sym co`. `alpha` will then remain unconstrained and will be zonked to `Any`.
The key new part is looking at the coercion when deciding whether to reorient.Consider this mess:
```hs
{# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () > k1 > k2 > k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 > k2 > Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () > Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u > a > Proxy b > Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```
GHC fails (in the RHS of `g`) with an occurscheck, but it should succeed.
The problem is that we end up with
```
[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)
```
where we have already unified `upsilon := '()`.
But GHC refuses to rewrite in kinds, so the `Const` never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type` and `beta := Any @Type > sym (AxConst Type (Any @Type))`.
Proposed solution:
The wanted above actually gets simplified to become
```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta > co) :: Type)
```
The `co` is easily solved. Then, when we get to `w2`, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha` is free in `co` and reorient, giving
```
[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha > sym co :: Const '() Type alpha)
```
which can be solved by unifying `beta := alpha > sym co`. `alpha` will then remain unconstrained and will be zonked to `Any`.
The key new part is looking at the coercion when deciding whether to reorient.Richard Eisenbergrae@richarde.devRichard Eisenbergrae@richarde.devhttps://gitlab.haskell.org/ghc/ghc//issues/19634Implement type family reduction via termlevel functions20210409T11:44:34ZRinat StriungisImplement type family reduction via termlevel functions## Motivation
Today I see two problems:
1. Type family reduction could be painfully slow.
In a complex case (typelevel parser) rewriter took \~ 50% compilation time.
[Example](https://gist.github.com/Haskellmouse/b05db12de9e9fdc8cfa9b02f436eccc0#file1profilingwopatchtxt).
2. Writing base type families could cause one of two unwanted consequences:
1. In the case of adding them as builtin type families code base of GHC could be terribly grown.
[First char kind MR for example](https://gitlab.haskell.org/ghc/ghc//merge_requests/3598).
This MR includes many useful type families, but it was decided to make a smaller MR with only a few TFs to
avoid increasing GHC codebase for \~ 2000 lines mostly because of TFs.
2. Adding them via plugins is a painful process for developers at least because they have to track all changes in unstable GHC plugin API.
In both cases, developers have to learn many implementation details and internals of GHC.
## Proposal
I want to add a new **TYPEFUN** pragma, which works in the following way:
```type IsAlphaNum :: Char > Bool
type family IsAlphaNum c
{# TYPEFUN IsAlphaNum = Data.Char.isAlphaNum #}
```
1. This pragma says which termlevel function use for reducing type family.
2. It reduces only when inputs contain no type variables.
3. It works only when all types (both arguments and result) are promotable in any way.
The main idea is to use precompiled to bytecode termlevel functions
in process of type checking which should solve both problems from the motivation part:
accelerate type family reduction and make writing TFs much easier.## Motivation
Today I see two problems:
1. Type family reduction could be painfully slow.
In a complex case (typelevel parser) rewriter took \~ 50% compilation time.
[Example](https://gist.github.com/Haskellmouse/b05db12de9e9fdc8cfa9b02f436eccc0#file1profilingwopatchtxt).
2. Writing base type families could cause one of two unwanted consequences:
1. In the case of adding them as builtin type families code base of GHC could be terribly grown.
[First char kind MR for example](https://gitlab.haskell.org/ghc/ghc//merge_requests/3598).
This MR includes many useful type families, but it was decided to make a smaller MR with only a few TFs to
avoid increasing GHC codebase for \~ 2000 lines mostly because of TFs.
2. Adding them via plugins is a painful process for developers at least because they have to track all changes in unstable GHC plugin API.
In both cases, developers have to learn many implementation details and internals of GHC.
## Proposal
I want to add a new **TYPEFUN** pragma, which works in the following way:
```type IsAlphaNum :: Char > Bool
type family IsAlphaNum c
{# TYPEFUN IsAlphaNum = Data.Char.isAlphaNum #}
```
1. This pragma says which termlevel function use for reducing type family.
2. It reduces only when inputs contain no type variables.
3. It works only when all types (both arguments and result) are promotable in any way.
The main idea is to use precompiled to bytecode termlevel functions
in process of type checking which should solve both problems from the motivation part:
accelerate type family reduction and make writing TFs much easier.9.4.1https://gitlab.haskell.org/ghc/ghc//issues/19559The GHCi debugger loses type constraints20210415T01:20:56ZRoland SennThe GHCi debugger loses type constraints## Summary
The GHCi debugger loses the type constraints of the breakpoint variables..
## Steps to reproduce
`Foo.hs` is a simplified version of testcase `break012`:
````
foo :: (Num a1, Num a2) => a2 > (a2, a1 > a1 > a1)
foo i = let incr = i + 1
add = (+)
in (incr,add)
````
Observe the following GHCi session:
````
$ ghci Foo.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Ok, one module loaded.
ghci> :st foo 5 `seq` ()
Stopped in Main.foo, Foo.hs:4:1221
_result :: (a2, a1 > a1 > a1) = _
add :: a1 > a1 > a1 = _
incr :: a2 = _
[Foo.hs:4:1221] ghci> add 40 2
<interactive>:2:5: error:
• No instance for (Num a1) arising from the literal ‘40’
Cannot resolve unknown runtime type ‘a1’
Use :print or :force to determine these types
Relevant bindings include it :: a1 (bound at <interactive>:2:1)
These potential instances exist:
instance Num Integer  Defined in ‘GHC.Num’
instance Num Double  Defined in ‘GHC.Float’
instance Num Float  Defined in ‘GHC.Float’
...plus two others
...plus one instance involving outofscope types
(use fprintpotentialinstances to see them all)
• In the first argument of ‘add’, namely ‘40’
In the expression: add 40 2
In an equation for ‘it’: it = add 40 2
[Foo.hs:4:1221] ghci>
````
The types of all breakpoint variables lack `Num` contraints!
## Expected behavior
The types of all 3 breakpoint variables (`_result`, `add`, `incr`) should have one or two `Num` constraints. The correct types are:
````
_result :: (Num a1, Num a2) => a2 > (a2, a1 > a1 > a1) = _ ( or _result :: Integer = _ )
add :: Num a1 => a1 > a1 > a1 = _
incr :: Num a1 => a2 = _
````
The result of `add 40 2` should be `42` and not an error message.
## Environment
* GHC versions used: 7.10.3, 8.10.2, 9.0.1, HEAD
(in 7.10.3 only the `_result` breakpoint variable is shown)
* Operating System: Linux Debian 10
* System Architecture: x86_64## Summary
The GHCi debugger loses the type constraints of the breakpoint variables..
## Steps to reproduce
`Foo.hs` is a simplified version of testcase `break012`:
````
foo :: (Num a1, Num a2) => a2 > (a2, a1 > a1 > a1)
foo i = let incr = i + 1
add = (+)
in (incr,add)
````
Observe the following GHCi session:
````
$ ghci Foo.hs
GHCi, version 9.0.1: https://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( Foo.hs, interpreted )
Ok, one module loaded.
ghci> :st foo 5 `seq` ()
Stopped in Main.foo, Foo.hs:4:1221
_result :: (a2, a1 > a1 > a1) = _
add :: a1 > a1 > a1 = _
incr :: a2 = _
[Foo.hs:4:1221] ghci> add 40 2
<interactive>:2:5: error:
• No instance for (Num a1) arising from the literal ‘40’
Cannot resolve unknown runtime type ‘a1’
Use :print or :force to determine these types
Relevant bindings include it :: a1 (bound at <interactive>:2:1)
These potential instances exist:
instance Num Integer  Defined in ‘GHC.Num’
instance Num Double  Defined in ‘GHC.Float’
instance Num Float  Defined in ‘GHC.Float’
...plus two others
...plus one instance involving outofscope types
(use fprintpotentialinstances to see them all)
• In the first argument of ‘add’, namely ‘40’
In the expression: add 40 2
In an equation for ‘it’: it = add 40 2
[Foo.hs:4:1221] ghci>
````
The types of all breakpoint variables lack `Num` contraints!
## Expected behavior
The types of all 3 breakpoint variables (`_result`, `add`, `incr`) should have one or two `Num` constraints. The correct types are:
````
_result :: (Num a1, Num a2) => a2 > (a2, a1 > a1 > a1) = _ ( or _result :: Integer = _ )
add :: Num a1 => a1 > a1 > a1 = _
incr :: Num a1 => a2 = _
````
The result of `add 40 2` should be `42` and not an error message.
## Environment
* GHC versions used: 7.10.3, 8.10.2, 9.0.1, HEAD
(in 7.10.3 only the `_result` breakpoint variable is shown)
* Operating System: Linux Debian 10
* System Architecture: x86_64https://gitlab.haskell.org/ghc/ghc//issues/19503Dead suggestion for XUnliftedNewtypes in checkNewDataCon20210308T17:40:04ZSebastian 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.
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 kindmismatch
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 typecheck, 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 SubNote? That Note is awfully long and has many many sub items.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 kindmismatch
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 typecheck, 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 SubNote? That Note is awfully long and has many many sub items.https://gitlab.haskell.org/ghc/ghc//issues/19487Relax Note [Phantom type variables in kinds] to allow for phantom levity vars20210506T20:01:36ZSebastian 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 kind20210329T08:52:40ZRinat 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/19428Deprecate `Winaccessiblecode`20210505T21:40:43ZSebastian 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/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/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/19060Make the canonicaliser do unification20201214T15:23:24ZSimon Peyton JonesMake the canonicaliser do unificationLook at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `checkTyVarEq`
* All this just gets the orientation right. Then we forget all that, and later, in `tryToSolveByUnification` we call `unifyTest` again. What a mess.
One thing that discouraged me was the miasma of `rewriteEqEvidence` and `rewriteCastedEquality` and doswap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.Look at `canEqTyVarFunEqCan`
* This function calls `unifyTest`, and `checkTyVarEq`, both of which are fairly elaborate tests.
* Then we go to `canEqCanLHSFinish`, which calls `canEqOK` which calls `checkTypeEq`, repeating that `checkTyVarEq`
* All this just gets the orientation right. Then we forget all that, and later, in `tryToSolveByUnification` we call `unifyTest` again. What a mess.
One thing that discouraged me was the miasma of `rewriteEqEvidence` and `rewriteCastedEquality` and doswap stuff. I just can't get my head round it. In some of my traces (eg EqCanOccursCheck) we seem to swap and swap back. Bizarre.
@rae and I agree that the canonicaliser should just do unification on the spot. This ticket is to track that point.https://gitlab.haskell.org/ghc/ghc//issues/19051Allow named wildcards in constraints20201223T15:23:55ZsheafAllow named wildcards in constraints```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)```haskell
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE NamedWildCards #}
{# LANGUAGE PartialTypeSignatures #}
module Test where
class C a where
meth :: a
unnamed :: _ => a
unnamed = meth
named :: _c => a
named = meth
```
The `unnamed` version causes no problems, however `named` causes the following error:
```
* Could not deduce: _0
from the context: _
bound by the inferred type for `named':
forall a (_ :: Constraint). _ => a
at Test.hs:14:112
* In the ambiguity check for the inferred type for `named'
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
When checking the inferred type
named :: forall a (_ :: Constraint). _ => a

14  named = meth
 ^^^^^^^^^^^^
```
That is, in this example, `_c` is **not** a named wildcard, but is instead universally quantified. So GHC unsurprisingly throws the same error as if we had written
```haskell
universal :: c => a
universal = meth
```
I would have expected that the named wildcard `_c` behave just like the wildcard `_`, except that it would give me the ability to refer to the inferred constraint at the typelevel inside the body of `named`.
(I came across this while thinking about #19010.)