GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20210416T00:27:00Zhttps://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.220210413T17:11:53ZAndres 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 vars20210408T09:49:22ZSebastian 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`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/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.)https://gitlab.haskell.org/ghc/ghc//issues/19013Type wildcard infers differently than no type signature20201210T00:22:10ZdminuosoType wildcard infers differently than no type signature```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.```haskell
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE PartialTypeSignatures #}
module Main where
import Optics
main :: IO ()
main = putStrLn "Hello, Haskell!"
g :: Lens' String Char
g = undefined
f :: _
f o = "foo" & (g%o) .~ 10
```
Full source code of the test case at: https://gitlab.haskell.org/dminuoso/ghcwildcardbug/
The above code fails to type check with:
Without the wildcard type annotation on `f` it compiles and infers the following type for `f`:
```
*Main> :t f
f :: (Is (Join A_Lens l) A_Setter, Is l (Join A_Lens l),
Is A_Lens (Join A_Lens l), Num b) =>
Optic l js Char Char a b > String
*Main>
```
Leaving the wildcard in, the type checker bails out.
```
[nixshell:~/git/ghcwildcardbug]$ cabal build
Build profile: w ghc8.8.4 O1
In order, the following will be built (use v for more details):
 ghcwildcardbug0.1.0.0 (exe:ghcwildcardbug) (file Main.hs changed)
Preprocessing executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
Building executable 'ghcwildcardbug' for ghcwildcardbug0.1.0.0..
[1 of 1] Compiling Main ( Main.hs, /home/dminuoso/git/ghcwildcardbug/distnewstyle/build/x86_64linux/ghc8.8.4/ghcwildcardbug0.1.0.0/x/ghcwildcardbug/build/ghcwildcardbug/ghcwildcardbugtmp/Main.o )
Main.hs:15:15: error:
• Overlapping instances for Is (Join A_Lens l0) A_Setter
arising from a use of ‘.~’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Lens A_Setter
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus four others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10
In an equation for ‘f’: f o = "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10
 ^^^^^^^^^^^
Main.hs:15:16: error:
• Overlapping instances for Is l0 (Join A_Lens l0)
arising from a use of ‘%’
Matching instances:
instance [overlappable] (TypeError ...) => Is k l
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is k k
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
instance Is A_Getter A_Fold
 Defined in ‘opticscore0.3.0.1:Optics.Internal.Optic.Subtyping’
...plus 35 others
(use fprintpotentialinstances to see them all)
(The choice depends on the instantiation of ‘l0’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the first argument of ‘(.~)’, namely ‘(g % o)’
In the second argument of ‘(&)’, namely ‘(g % o) .~ 10’
In the expression: "foo" & (g % o) .~ 10

15  f o = "foo" & (g%o) .~ 10

```
Also tried enabling NoMonomorphismRestriction to no avail.https://gitlab.haskell.org/ghc/ghc//issues/19010Partial type signature algorithm fails to infer constraints in the presence o...20201220T03:26:43ZsheafPartial type signature algorithm fails to infer constraints in the presence of GADTsI've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).I've been running into a few issues with partial type signatures as of late.
In my [graphics shader library](https://gitlab.com/sheaf/fir), users write programs using an indexed monad which keeps track of various pieces of information as they write the program, which are used to perform validation using type families. It would be impossible for the user to manually write the types of the indexed monad (they can become very large), so partial type signatures are a crucial tool in this situation.
However, I'm running into some situations in which GHC fails to infer a constraint, even though it is happy to report error messages that say exactly which constraints are missing.
After a fair bit of effort, I've finally managed to come up with a small reproducer:
```haskell
{# LANGUAGE DataKinds #}
{# LANGUAGE GADTs #}
{# LANGUAGE PartialTypeSignatures #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE ScopedTypeVariables #}
module Bug where
data SBool ( bool :: Bool ) where
STrue :: SBool True
SFalse :: SBool False
class C a where
methC :: a > Float
class D a where
methD :: a > Float
foo :: forall bool a. _ => SBool bool > a > Float
foo sBool a = meth a
where
meth :: _ => a > Float
meth = case sBool of
STrue > methC
SFalse > methD
```
produces the following error:
```
[1 of 1] Compiling Bug ( bug.hs, bug.o )
bug.hs:23:17: error:
* Could not deduce (C a) arising from a use of `methC'
from the context: bool ~ 'True
bound by a pattern with constructor: STrue :: SBool 'True,
in a case alternative
at bug.hs:23:711
Possible fix:
add (C a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methC
In a case alternative: STrue > methC
In the expression:
case sBool of
STrue > methC
SFalse > methD

23  STrue > methC
 ^^^^^
bug.hs:24:17: error:
* Could not deduce (D a) arising from a use of `methD'
from the context: bool ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in a case alternative
at bug.hs:24:712
Possible fix:
add (D a) to the context of
the inferred type of foo :: SBool bool > a > Float
* In the expression: methD
In a case alternative: SFalse > methD
In the expression:
case sBool of
STrue > methC
SFalse > methD

24  SFalse > methD
 ^^^^^
```
If one follows the error messages that GHC provides, by adding the constraint `( C a, D a )` to `meth`, then the program compiles. So it's curious that GHC is able to pinpoint the missing constraints, but not actually put them in the hole.
I also notice that this issue remains if one uses `methC` in both branches. If one changes `SBool` to `Bool` then of course it works fine.
I assume that this happens because the partial type signature algorithm is conservative in the presence of GADTs: one could potentially learn information upon matching a GADT that would help solve the constraints, and one would not want that evidence to float out in any way. However, in this case, I think we can agree that the evidence provided by the GADT match doesn't interact in any way with the constraints on the RHS (as nothing involves `bool`), i.e. it's as if we had just matched on a `Bool`.
<hr>
Versions of GHC tried: 8.8, 8.10, 9.0 (all with the same result).https://gitlab.haskell.org/ghc/ghc//issues/18873Quantified equality constraints are not used for rewriting20201210T20:30:27ZRichard Eisenbergrae@richarde.devQuantified equality constraints are not used for rewritingIf I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.If I say
```hs
type family F a b where
F [_] b = b
f :: forall a b. (a ~ [b]) => F a b > b
f x = x
```
GHC smiles upon me: the equality constraint rewrites `a` to `[b]`, and then `F [b] b` can reduce to `b`, and all is well.
But if I say
```hs
type family F a b where
F [_] b = b
class Truth
instance Truth
f :: forall a b. (Truth => a ~ [b]) => F a b > b
f x = x
```
I get an error, saying `F a b` does not match `b`. This is because the equality, hidden behind `Truth`, is not used for rewriting, and thus GHC cannot figure out that `F a b` can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.https://gitlab.haskell.org/ghc/ghc//issues/18851Nonconfluence in the solver20210104T22:12:36ZRichard Eisenbergrae@richarde.devNonconfluence in the solverIn #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can. (EDIT: Furthermore, more hammering in this direction discovered nonconfluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc//issues/18851#note_318471.)
Here is the example:
```hs
{# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #}
module Bug where
class C a b  a > b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic nonconfluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)In #18759 (starting at https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306441 and then refined in https://gitlab.haskell.org/ghc/ghc//issues/18759#note_306722, but you don't need to read that ticket to understand this one), we explored various ways of disabling the coverage condition for functional dependencies. In https://gitlab.haskell.org/ghc/ghc//issues/18759#note_307486, @simonpj asks whether these techniques can disrupt confluence.
They can. (EDIT: Furthermore, more hammering in this direction discovered nonconfluence even *without* functional dependencies. See https://gitlab.haskell.org/ghc/ghc//issues/18851#note_318471.)
Here is the example:
```hs
{# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances,
ScopedTypeVariables, TypeFamilies, TypeApplications,
FlexibleContexts, AllowAmbiguousTypes #}
module Bug where
class C a b  a > b
instance C Int b => C Int b
class IsInt int
instance int ~ Int => IsInt int
data A
instance Show A where
show _ = "A"
data B
instance Show B where
show _ = "B"
f :: forall a b c int. (Show a, Show b, Show c, C int a, C int b, C int c, IsInt int) => String
f = show (undefined :: c)
g = f @A @B
```
`g` evaluates to `"B"`. If I switch the order of the `C int a` and `C int b` constraints in the type of `f`, `g` will evaluate to `"A"`. Urgh.
(Sidenote: this file needs `AllowAmbiguousTypes`, but there are no ambiguous types here. That bug is reported as #18850.)
What's going on? When calling `f` from `g`, GHC needs to figure out how to instantiate the type variables `a`, `b`, `c`, and `int`, and GHC must find dictionaries to supply for all the class constraints. First, GHC creates unification variables `a0`, `b0`, `c0`, and `int0`. The type applications tell us `a0 := A` and `b0 := B`. Good. Then we have these constraints:
```
[W] w1 : Show A
[W] w2 : Show B
[W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
[W] w6 : C int0 c0
[W] w7 : IsInt int0
```
GHC processes these in the order given. `w1` and `w2` are easily despatched. `w3` doesn't make any progress at all. Neither does `w4` or `w5`. So we're then in this state:
```
worklist: [W] w6 : C int0 c0
[W] w7 : IsInt int0
inerts: [W] w3 : Show c0
[W] w4 : C int0 A
[W] w5 : C int0 B
```
We then look at `w6`. It doesn't make progress. But then GHC looks at the inerts, and sees that `w4` and `w5` have the same first argument to `C` (`int0`) as the work item `w6`. Because of the functional dependency on `C`, this means that `c0` must match the second argument to `C` in the inert. The problem is that there are *two* such inerts! GHC chooses the last one, arbitrarily. Thus, we get `c0 := B` and carry on. If the constraints were processed in a different order, we'd end up with `c0 := A`. This is classic nonconfluence.
Why have `IsInt` here? It's to slow down GHC. If we just wrote an explicit `Int` in the type signature for `f`, then GHC would eagerly solve `w4' : C Int A` and `w5' : C Int B`. When processing `w6' : C Int c0`, GHC wouldn't have any inerts to look at. Instead, it would look at the instance for `C`, which is unhelpful in this case. Indeed, moving the `IsInt int` constraint earlier (before the `C` constraints) in `f`'s type signature causes GHC to error, as it doesn't know how to instantiate `c0`, having lost the hints from the inerts. (More nonconfluence!)
What to do? I think the next step is to compare this to the [constrainthandling rules paper](https://www.researchgate.net/profile/Martin_Sulzmann/publication/213885702_Understanding_Functional_Dependencies_via_Constraint_Handling_Rules/links/09e41511297969891f000000.pdf), which proves confluence, and see whether that paper has a mistake, or where GHC violates an assumption in that paper. (Probably the latter: my instance for `C` is very naughty.)