GHC issueshttps://gitlab.haskell.org/ghc/ghc//issues20201219T14:16:12Zhttps://gitlab.haskell.org/ghc/ghc//issues/19044Regression: HEAD requires FlexibleContexts because of inferred, redundant con...20201219T14:16:12ZRyan ScottRegression: HEAD requires FlexibleContexts because of inferred, redundant constraint_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7287)._
The following code, minimized from the `pandoc2.11.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b where
m :: a > b
instance C a a where
m = id
instance C a (Maybe a) where
m _ = Nothing
f :: a > Maybe a
f = g
where
g x = h (m x) x
h :: Maybe a > a > Maybe a
h = const
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc9.1.0.20201208/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:17:5: error:
• Non typevariable argument in the constraint: C a1 (Maybe a1)
(Use FlexibleContexts to permit this)
• When checking the inferred type
g :: forall {a}. C a (Maybe a) => a > Maybe a
In an equation for ‘f’:
f = g
where
g x = h (m x) x

17  g x = h (m x) x
 ^^^^^^^^^^^^^^^
```
Previous versions of GHC would accept this program because the inferred type of `g` was `forall {a}. a > Maybe a`, not `g :: forall {a}. C a (Maybe a) => a > Maybe a`. The presence of this extra `C a (Maybe a)` constraint (which seems redundant?) is suspicious, so I opted to open an issue about it._Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7287)._
The following code, minimized from the `pandoc2.11.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE FlexibleInstances #}
{# LANGUAGE MultiParamTypeClasses #}
module Bug where
class C a b where
m :: a > b
instance C a a where
m = id
instance C a (Maybe a) where
m _ = Nothing
f :: a > Maybe a
f = g
where
g x = h (m x) x
h :: Maybe a > a > Maybe a
h = const
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc9.1.0.20201208/bin/ghc Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
Bug.hs:17:5: error:
• Non typevariable argument in the constraint: C a1 (Maybe a1)
(Use FlexibleContexts to permit this)
• When checking the inferred type
g :: forall {a}. C a (Maybe a) => a > Maybe a
In an equation for ‘f’:
f = g
where
g x = h (m x) x

17  g x = h (m x) x
 ^^^^^^^^^^^^^^^
```
Previous versions of GHC would accept this program because the inferred type of `g` was `forall {a}. a > Maybe a`, not `g :: forall {a}. C a (Maybe a) => a > Maybe a`. The presence of this extra `C a (Maybe a)` constraint (which seems redundant?) is suspicious, so I opted to open an issue about it.9.2.1https://gitlab.haskell.org/ghc/ghc//issues/19042Regression: HEAD incurs a reduction stack overflow on program involving type ...20210210T21:11:55ZRyan ScottRegression: HEAD incurs a reduction stack overflow on program involving type equality_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7936)._
The following code, minimized from the `plots0.1.1.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Plots.Types where
import Data.Functor
import Data.Typeable
type family N a
data StyledPlot n where
StyledPlot :: Typeable p => p > StyledPlot (N p)
styledPlot :: forall p f.
(Typeable p, Applicative f)
=> (p > f p)
> StyledPlot (N p) > f (StyledPlot (N p))
styledPlot f s@(StyledPlot p) =
case eq p of
Just Refl > f p <&> \p' > StyledPlot p'
Nothing > pure s
where eq :: Typeable a => a > Maybe (a :~: p)
eq _ = eqT
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Plots.Types ( Bug.hs, Bug.o )
Bug.hs:21:33: error:
• Reduction stack overflow; size = 201
When simplifying the following type: N p1
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: StyledPlot p'
In the second argument of ‘(<&>)’, namely ‘\ p' > StyledPlot p'’
In the expression: f p <&> \ p' > StyledPlot p'

21  Just Refl > f p <&> \p' > StyledPlot p'
 ^^^^^^^^^^^^^
```_Originally observed in a `head.hackage` build [here](https://gitlab.haskell.org/ghc/head.hackage//jobs/519572#L7936)._
The following code, minimized from the `plots0.1.1.2` library, fails to typecheck on GHC HEAD (I tried using commit 62ed6957463a9c0f711ea698d7ed4371e00fb122) but does typecheck with GHC 8.10.2 and 9.0.1alpha1:
```hs
{# LANGUAGE GADTs #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE TypeOperators #}
module Plots.Types where
import Data.Functor
import Data.Typeable
type family N a
data StyledPlot n where
StyledPlot :: Typeable p => p > StyledPlot (N p)
styledPlot :: forall p f.
(Typeable p, Applicative f)
=> (p > f p)
> StyledPlot (N p) > f (StyledPlot (N p))
styledPlot f s@(StyledPlot p) =
case eq p of
Just Refl > f p <&> \p' > StyledPlot p'
Nothing > pure s
where eq :: Typeable a => a > Maybe (a :~: p)
eq _ = eqT
```
On HEAD, this produces the following error:
```
$ ~/Software/ghc2/inplace/bin/ghcstage2 Bug.hs
[1 of 1] Compiling Plots.Types ( Bug.hs, Bug.o )
Bug.hs:21:33: error:
• Reduction stack overflow; size = 201
When simplifying the following type: N p1
Use freductiondepth=0 to disable this check
(any upper bound you could choose might fail unpredictably with
minor updates to GHC, so disabling the check is recommended if
you're sure that type checking should terminate)
• In the expression: StyledPlot p'
In the second argument of ‘(<&>)’, namely ‘\ p' > StyledPlot p'’
In the expression: f p <&> \ p' > StyledPlot p'

21  Just Refl > f p <&> \p' > StyledPlot p'
 ^^^^^^^^^^^^^
```9.2.1https://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/18987Quick Look does not zonk return types20201221T11:00:00ZRichard Eisenbergrae@richarde.devQuick Look does not zonk return typesTest case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.Test case `impredicative/T17332`:
```hs
data Dict c where
MkDict :: c => Dict c
aux :: Dict (forall a. a)
aux = MkDict
```
The constraint `c` ends up in the solver as an `IrredPred`, which reveals the polytype `forall a. a`. But zonking to reveal a polytype should never happen outside of Quick Look, as `Note [Quick Look]` in GHC.Tc.Gen.App tells us.
A quick look didn't reveal exactly where to put the zonk, and I don't want to add yet another wrinkle to !4149. But when this bug is fixed, the `ForAllPred` case in `canIrred` should never happen.https://gitlab.haskell.org/ghc/ghc//issues/18929Investigate touchable metavariables in Givens20210102T14:14:41ZRichard Eisenbergrae@richarde.devInvestigate touchable metavariables in Givens@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.@simonpj believes it would be disastrous to ever have a touchable metavariable in a Given. I'm not quite as sure what the disaster would be, but I admit such a situation is suspect. But we can concoct such a thing:
```hs
{# LANGUAGE PolyKinds, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class C a where
meth :: Proxy a > ()
f :: C a => Proxy a > _
f p = meth p
```
The partial signature for `f` is not kindgeneralized (the fact that it is partial means that we might want the definition of `f` to inform the kind of `a`) and thus the kind of `a` remains as a metavariable `kappa`. In the body of `f`, we have `[G] C kappa a`. We can see this in this snippet of `ddumptctrace` (with `fprintexplicitkinds` enabled):
```
tclevel = 1
work item = [WD] $dC_aoV {0}:: C @{k_aoT[tau:1]}
a_aoU[tau:1] (CNonCanonical)
inerts = {Dictionaries = [G] $dC_aoX {0}:: C @{k_aoT[tau:1]}
a_aoJ[tyv:1] (CDictCan)
```
The variable `k_aoT[tau:1]` is touchable and is not yet filled in. (It ends up being skolemised and quantified over, quite correctly.)
This ticket is to determine whether this situation is pernicious, and, if it is, figure out a way to rule it out.https://gitlab.haskell.org/ghc/ghc//issues/18920ghc8.8 does not infer kind20201109T14:13:59Zjwaldmannghc8.8 does not infer kindRejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```Rejected by ghc8.8.4 with
```
should.hs:27:12: error:
• Expected kind ‘* > *’, but ‘solver’ has kind ‘*’
• In the first argument of ‘Solver’, namely ‘solver’
In the type ‘(Solver solver, Queue q, Transformer t) =>
Int > q > t > EvalState t > solver (Int, [a])’
In the type declaration for ‘ContinueSig’
```
but accepted by 8.6.5, 8.10.2. 9.0.1alpha1.
```
{# LANGUAGE TypeFamilies #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE Rank2Types #}
{# LANGUAGE MultiParamTypeClasses #}
{# LANGUAGE GADTs #}
class Monad solver => Solver solver where
type Constraint solver :: *
type Label solver :: *
class Queue q
data Tree s a where
NewVar :: Term s t => (t > Tree s a) > Tree s a
class Solver solver => Term solver term
class Transformer t where
type EvalState t :: *
type TreeState t :: *
type ForSolver t :: (* > *)
type ForResult t :: *
nextT :: SearchSig (ForSolver t) q t (ForResult t)
returnT :: ContinueSig solver q t (ForResult t)
type ContinueSig solver q t a =
( Solver solver, Queue q, Transformer t )
=> Int > q > t > EvalState t
> solver (Int, [a])
type SearchSig solver q t a =
(Solver solver, Queue q, Transformer t )
=> Int > Tree solver a > q > t > EvalState t > TreeState t
> solver (Int,[a])
```
8.8 accepts this after introducing this:
```
type ContinueSig (solver :: * > *) q t a =
...
```8.10.1https://gitlab.haskell.org/ghc/ghc//issues/18910Orderdependent type inference due to Note [Instance and Given overlap]20210106T03:39:21ZRichard Eisenbergrae@richarde.devOrderdependent type inference due to Note [Instance and Given overlap]With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.With some effort, I have produced
```hs
{# LANGUAGE ScopedTypeVariables, AllowAmbiguousTypes, TypeApplications,
TypeFamilies, PolyKinds, DataKinds, FlexibleInstances,
MultiParamTypeClasses, FlexibleContexts, PartialTypeSignatures #}
module Bug where
import Data.Proxy
class P a
class Q a
class R a b
newtype Tagged (t :: k) a = Tagged a
type family F a
type instance F (Tagged @Bool t a) = [a]
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
wob = undefined
it'sABoolNow :: forall (t :: Bool). Int
it'sABoolNow = undefined
class HasBoolKind t
instance k ~ Bool => HasBoolKind (t :: k)
it'sABoolLater :: forall t. HasBoolKind t => Int
it'sABoolLater = undefined
g :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g _ x = it'sABoolNow @t + wob x
g2 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g2 _ x = wob x + it'sABoolNow @t
g3 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g3 _ x = it'sABoolLater @t + wob x
g4 :: forall t a. Q (F (Tagged t a)) => Proxy t > [a] > _
g4 _ x = wob x + it'sABoolLater @t
```
All of `g`, `g2`, and `g3` are accepted. `g4` is rejected. Note that `g4` is identical to `g3` except for changing the order of the summands.
What's going on:
Here is an excerpt from `Note [Instance and Given overlap]`:
```
Example, from the OutsideIn(X) paper:
instance P x => Q [x]
instance (x ~ y) => R y [x]
wob :: forall a b. (Q [b], R b a) => a > Int
g :: forall a. Q [a] => [a] > Int
g x = wob x
From 'g' we get the implication constraint:
forall a. Q [a] => (Q [beta], R beta [a])
If we react (Q [beta]) with its toplevel axiom, we end up with a
(P beta), which we have no way of discharging. On the other hand,
if we react R beta [a] with the toplevel we get (beta ~ a), which
is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
now solvable by the given Q [a].
```
Here is the scenario in the Note, when typechecking the Note's `g`:
```
[G] Q [a]
[W] Q [beta]
[W] R beta [a]
```
When we process the first Wanted, we might be tempted to use the instance, simplifying the Wanted to `P beta`. Doing this leads to failure. What we'd prefer is to recognize that the Given might be helpful later, and just to leave the Wanted asis. Then, processing the `[W] R beta [a]` tells us that `beta ~ a`, and we go home happy.
The scenario in this ticket is rather more complicated. The instances are unchanged, but now we have a type family `F` in the mix. It all looks like
```
t :: kappa
[G] Q (F (Tagged @kappa t a))
[W] Q [beta]
[W] R beta [a]
```
The question is: when processing the first Wanted, should the Given block GHC from using the global instance? (Sidenote: I've used partial type signatures and polykinds here as a sneaky way of getting a metavariable into a Given. The partial type signature stops GHC from kindgeneralizing the type, and thus `t`'s kind remains as `kappa` when processing the body.) If `kappa` is `Bool`, then the Given will eventually match and should block us from using the instance. If `kappa` is not `Bool`, then the Given will not apply. Yet in all of `g`..`g4`, `kappa` turns out to be `Bool`.
In `g`, we have `it'sABoolNow @t`, and the eager unifier sets `kappa := Bool` before the constraint solver gets a crack. The application of `F` reduces and the Given is recognized as relevant, blocking the use of the global instance.
In `g2`, the same happens.
In `g3`, we get a new `[W] HasBoolKind @kappa t`. This gets processed *before* the `Q [beta]` Wanted, and processing this sets `kappa := Bool`, leading the Given to reduce and block the use of the global instance.
In `g4`, however, the new `[W] HasBoolKind @kappa t` comes *after* the others. So we process `Q [beta]` *before* learning about `kappa`. The global instance is used, and we are left stuck with `[W] P a` that cannot be solved.
This all boils down to the `not (isFskTyVar tv)` check in `GHC.Tc.Solver.Monad.mightMatchLater`, which (effectively) says that type family applications in Givens match only themselves, not any arbitrary type. Removing that check fixes this problem. But it introduces another. The following program is accepted today:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, FlexibleContexts #}
module Bug2 where
class C a where
meth :: a > ()
instance C Int where
meth _ = ()
type family F a
foo :: C (F a) => a > Int > ()
foo _ n = meth n
```
If we strike that check from `mightMatchLater`, we get
```
• Overlapping instances for C Int arising from a use of ‘meth’
Matching instances:
instance C Int  Defined at CbvOverlap.hs:10:10
There exists a (perhaps superclass) match:
from the context: C (F a)
bound by the type signature for:
foo :: forall a. C (F a) => a > Int > ()
at CbvOverlap.hs:15:132
(The choice depends on the instantiation of ‘’
To pick the first instance above, use IncoherentInstances
when compiling the other instance declarations)
• In the expression: meth n
In an equation for ‘foo’: foo _ n = meth n
```
The (unrelated) `[G] C (F a)` blocks the useful `instance C Int`. Worse, the error message says that the overlap depends on the instantiation of <<empty list>>.
This new problem is not just theoretical. In my !4149 patch, I essentially made this change unintentionally, and GHC's Parser.hs stopped compiling (in stage 2), due to its `DisambECP` shenanigans. It's easy for me to replicate the current behavior, so my branch can continue, but this bug will remain.
I'm not sure what the solution is. If we allow type family applications in Givens to match any potential type, we will unavoidably cause the second bug. So perhaps the best course of action is to let sleeping dogs lie. Yet I was uncomfortable reinstating the old behavior, because it smelled off... and I wanted to understand it better. Thus this ticket.https://gitlab.haskell.org/ghc/ghc//issues/18891Kind inference for newtypes in GADT syntax is deeply broken20201208T21:03:16ZRichard Eisenbergrae@richarde.devKind inference for newtypes in GADT syntax is deeply brokenHere are some tales of destruction, all with `XUnliftedNewtypes` and `XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N > N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k > TYPE k
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.Here are some tales of destruction, all with `XUnliftedNewtypes` and `XNoCUSKs`:
```hs
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:34:3: error:
• Expected a type, but ‘N’ has kind ‘*’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k. TYPE k
newtype N :: forall k. TYPE k where
MkN :: N > N
```
gives
```
Scratch.hs:35:3: error:
• A newtype constructor must have a return type of form T a1 ... an
MkN :: N > N
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
gives
```
Scratch.hs:35:3: error:
• Expected a type, but ‘N m’ has kind ‘TYPE m’
• In the definition of data constructor ‘MkN’
In the newtype declaration for ‘N’
```

```hs
type N :: forall k > TYPE k
newtype N :: forall k > TYPE k where
MkN :: N m > N m
```
succeeds.
I think all these examples should succeed. All but the last cause a DEBUG build of GHC to panic.
I think the problem is that the `res_kind` passed to `kcConArgTys` has the wrong scope: it mentions variables in the type head, but these are utterly distinct from the variables in the constructor type.9.2.1https://gitlab.haskell.org/ghc/ghc//issues/18875Occurschecky Givens rewrite once, but not twice20201204T22:10:52ZRichard Eisenbergrae@richarde.devOccurschecky Givens rewrite once, but not twiceGHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurscheck failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flatteningskolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e > f
h (Just x) = x
```
Here, `h` has a similar given with an occurscheck failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.GHC remarkably accepts this program:
```hs
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```
This is remarkable because satisfying the `C e` constraint arising from the use of `meth` requires using the `e ~ Maybe (UnMaybe e)` given, despite the fact that it has an occurscheck failure. That is, GHC must rewrite `e` to `Maybe (UnMaybe e)` to solve the class constraint, yet not fall into a look trying to expand `e` further. This works due to the way GHC currently uses flatteningskolems to deal with type family applications. (The program above does not work on the current tip of !4149, which avoids this flattening mechanism.)
However, GHC rejects this program:
```hs
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e > f
h (Just x) = x
```
Here, `h` has a similar given with an occurscheck failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have
```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```
Using the Given for rewriting once gives us
```
[W] Maybe (G e f) ~ Maybe f
```
which decomposes to
```
[W] G e f ~ f
```
But now, we must use the given *again* to get
```
[W] G (Maybe (G e f)) f ~ f
```
so that can reduce to
```
[W] f ~ f
```
and be solved.
I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.
The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.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/18863Visibility mismatch between data declaration and kind signature, accepted!20201031T11:08:25ZIcelandjackVisibility mismatch between data declaration and kind signature, accepted!```haskell
{# Language PolyKinds #}
{# Language RankNTypes #}
{# Language StandaloneKindSignatures #}
import Data.Kind
type ID :: forall i > i > Type
data ID :: forall i > i > Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall>` to `forall.` we get an error. Obviously?
```haskell
 • Couldn't match expected kind ‘forall i1 > i1 > *’
 with actual kind ‘i > *’
 • In the data type declaration for ‘ID’
 
 8  data ID :: forall i > i > Type
  ^^^^^^^
type ID :: forall i. i > Type
data ID :: forall i > i > Type
```
But then why does this compile
```haskell
type ID :: forall i > i > Type
data ID :: forall i. i > Type
``````haskell
{# Language PolyKinds #}
{# Language RankNTypes #}
{# Language StandaloneKindSignatures #}
import Data.Kind
type ID :: forall i > i > Type
data ID :: forall i > i > Type
```
This compiles on 8.10.0.20191123, if we change the standalone kind signature `forall>` to `forall.` we get an error. Obviously?
```haskell
 • Couldn't match expected kind ‘forall i1 > i1 > *’
 with actual kind ‘i > *’
 • In the data type declaration for ‘ID’
 
 8  data ID :: forall i > i > Type
  ^^^^^^^
type ID :: forall i. i > Type
data ID :: forall i > i > Type
```
But then why does this compile
```haskell
type ID :: forall i > i > Type
data ID :: forall i. i > Type
```9.2.1https://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.)https://gitlab.haskell.org/ghc/ghc//issues/18850Instance/given overlap trips up the ambiguity check20201029T19:00:42ZRichard Eisenbergrae@richarde.devInstance/given overlap trips up the ambiguity checkThursday is a good day to abuse GHC. So I said this:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:632
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted  no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an overeager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is errorfree. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
 not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
 xopt LangExt.MonoLocalBinds dflags
= return ()
 ...
```
where the `...` includes generating a warning. Of course, I *do* have `XMonoLocalBinds`, as implied by `XTypeFamilies`. What happens when I disable this (with an explicit `XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [Wsimplifiableclassconstraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
 Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.Thursday is a good day to abuse GHC. So I said this:
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
```
To me, `f`'s type is unambiguous: the `IsBool bool` constraint fixes the type variable `bool` to be `Bool`. But GHC says
```
/Users/rae/temp/Bug2.hs:11:6: error:
• Could not deduce (C bool0)
from the context: (C bool, IsBool bool)
bound by the type signature for:
f :: forall bool. (C bool, IsBool bool) => ()
at /Users/rae/temp/Bug2.hs:11:632
The type variable ‘bool0’ is ambiguous
• In the ambiguity check for ‘f’
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
But maybe I'm wrong. Is the type really ambiguous? No. When I say
```hs
{# LANGUAGE TypeFamilies, FlexibleInstances, AllowAmbiguousTypes #}
module Bug where
class IsBool bool
instance bool ~ Bool => IsBool bool
class C a
instance C Bool
f :: (C bool, IsBool bool) => ()
f = ()
g = f
```
my program is accepted. I've added `AllowAmbiguousTypes` and the binding `g = f`. That binding is accepted  no type applications or other funny business. This suggests that `f`'s type is not actually ambiguous.
What's going on is an overeager instance/given overlap; see `Note [Instance and Given overlap]` in `GHC.Tc.Solver.Interact`. That Note ends with
```
All of this is disgustingly delicate, so to discourage people from writing
simplifiable class givens, we warn about signatures that contain them;
see GHC.Tc.Validity Note [Simplifiable given constraints].
```
But I don't get the warning! Even in my second program, which is errorfree. Hunting further into `GHC.Tc.Validity`, I find this code:
```hs
checkSimplifiableClassConstraint env dflags ctxt cls tys
 not (wopt Opt_WarnSimplifiableClassConstraints dflags)
= return ()
 xopt LangExt.MonoLocalBinds dflags
= return ()
 ...
```
where the `...` includes generating a warning. Of course, I *do* have `XMonoLocalBinds`, as implied by `XTypeFamilies`. What happens when I disable this (with an explicit `XNoMonoLocalBinds`)?
```
/Users/rae/temp/Bug2.hs:11:6: warning: [Wsimplifiableclassconstraints]
• The constraint ‘IsBool bool’ matches
instance (bool ~ Bool) => IsBool bool
 Defined at /Users/rae/temp/Bug2.hs:6:10
This makes type inference for inner bindings fragile;
either use MonoLocalBinds, or simplify it using the instance
• In the type signature: f :: (C bool, IsBool bool) => ()

11  f :: (C bool, IsBool bool) => ()
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^
```
Good. The warning fires.
My conclusions:
1. My first program really ought to be accepted. The type is not ambiguous. I'm willing to concede this point to "disgustingly delicate", though, if we don't see an easy way to fix.
2. It looks the warning should fire even when `XMonoLocalBinds` is in effect. My program has no local generalization involved. How would users disable the warnings? By not writing a simplifiable Given.https://gitlab.haskell.org/ghc/ghc//issues/18802Typecheck record update via desugaring20201005T20:51:46ZSimon Peyton JonesTypecheck record update via desugaringThere are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Reengineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc//issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our recordupdate tickets.There are quite a few tickets relating to inadequacies of record update, including
* #18311
* #10856
* #2595
* #10808
* #3632: updating existentials if you do all of them at once
* #16501
Record update is a place where our general plan of typechecking the source syntax seems particularly hard to do. It wold be much easier (and correct by construction) to desugar (but still in HsSyn) and typecheck that.
Fortunately we now have a way to do that: our [Reengineer rebindable syntax](https://gitlab.haskell.org/ghc/ghc//issues/17582) ticket, #17582. A lot of attention is paid there to maintaining good error messages, which is the main challenge of this approach.
So this ticket is to propose: let's use the work on #17582 to solve our recordupdate tickets.https://gitlab.haskell.org/ghc/ghc//issues/18758Remove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc20200930T20:28:26ZVladislav ZavialovRemove NoGhcTc, allow HsType GhcTc, HsDecl GhcTc## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
 HsAppType (XAppTypeE p)  After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p))  ^ Visible type application
```
The primary reason for this is that kindchecking and desugaring of types are intertwined. We mostly work with `TcType` instead of `HsType GhcTc` because it's more convenient in some places (e.g. in `unifyKind` and `unifyType`).
## Motivation A
A better architecture would be to have similar pipelines for terms and types:
* `HsExpr GhcPs > HsExpr GhcRn > HsExpr GhcTc`
* `HsType GhcPs > HsType GhcRn > HsType GhcTc`
This would allow us to talk about e.g. `HsDecl GhcTc`. For example, when discussing #12088, there was an idea of a refactoring that would separate `tcTyClDecl` and zonking. But then we'd like the type of `tcTyClDecl` to be:
```haskell
tcTyClDecl :: LTyClDecl GhcRn > TcM (LTyClDecl GhcTc)
```
And that's not currently possible.
## Motivation B
This would facilitate fixing #15824, for instance, as we could use `HsType GhcTc` as the input to `GHC.Tc.Gen.Splice.reifyType`. This way, we would retain the `HsOpTy` and `HsAppTy` distinction.
## Partial Solution
In order to address Motivation B, we would need to properly embed coercions into `HsType GhcTc` and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following `XXType` instance:
```
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
```
Then `HsType GhcTc` would only ever use `XHsType (HsTypeTc ty doc)`. The fields are as follows:
* `TcType` is the kindchecked, desugared type
* `SDoc` is the result of pretty printing `HsType GhcRn`, before parentheses and infix operators were discarded
This is sufficient to let us talk about `HsType GhcTc` and `HsDecl GhcTc`, and remove the `NoGhcTc` type family.
## Full Solution
The full solution would involve using `HsType GhcTc` throughout the type checker, rewriting zonking and unification to work over `HsType GhcTc`, and so on. It would address Motivation A, and also let us remove the notion of `TcType`: the type checker would work with `HsType GhcTc`, and `Type` would be only used in Core. That would be a nice improvement, as we could remove `TcTyVar` and `AnonArgFlag` (maybe something else?) from the syntax of Core.
## Completion
1. The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.## Background
Currently, we carefully avoid `HsType GhcTc` or `HsDecl GhcTc`, by means of the `NoGhcTc` type family:
```
 HsAppType (XAppTypeE p)  After typechecking: the type argument
(LHsExpr p)
(LHsWcType (NoGhcTc p))  ^ Visible type application
```
The primary reason for this is that kindchecking and desugaring of types are intertwined. We mostly work with `TcType` instead of `HsType GhcTc` because it's more convenient in some places (e.g. in `unifyKind` and `unifyType`).
## Motivation A
A better architecture would be to have similar pipelines for terms and types:
* `HsExpr GhcPs > HsExpr GhcRn > HsExpr GhcTc`
* `HsType GhcPs > HsType GhcRn > HsType GhcTc`
This would allow us to talk about e.g. `HsDecl GhcTc`. For example, when discussing #12088, there was an idea of a refactoring that would separate `tcTyClDecl` and zonking. But then we'd like the type of `tcTyClDecl` to be:
```haskell
tcTyClDecl :: LTyClDecl GhcRn > TcM (LTyClDecl GhcTc)
```
And that's not currently possible.
## Motivation B
This would facilitate fixing #15824, for instance, as we could use `HsType GhcTc` as the input to `GHC.Tc.Gen.Splice.reifyType`. This way, we would retain the `HsOpTy` and `HsAppTy` distinction.
## Partial Solution
In order to address Motivation B, we would need to properly embed coercions into `HsType GhcTc` and start using it throughout the type checker. However, that would be a very major, intrusive refactoring. Before we do that, there's a stopgap solution that could be used to address Motivation A.
Define the following `XXType` instance:
```
type instance XXType GhcTc = HsTypeTc
data HsTypeTc = HsTypeTc TcType SDoc
```
Then `HsType GhcTc` would only ever use `XHsType (HsTypeTc ty doc)`. The fields are as follows:
* `TcType` is the kindchecked, desugared type
* `SDoc` is the result of pretty printing `HsType GhcRn`, before parentheses and infix operators were discarded
This is sufficient to let us talk about `HsType GhcTc` and `HsDecl GhcTc`, and remove the `NoGhcTc` type family.
## Full Solution
The full solution would involve using `HsType GhcTc` throughout the type checker, rewriting zonking and unification to work over `HsType GhcTc`, and so on. It would address Motivation A, and also let us remove the notion of `TcType`: the type checker would work with `HsType GhcTc`, and `Type` would be only used in Core. That would be a nice improvement, as we could remove `TcTyVar` and `AnonArgFlag` (maybe something else?) from the syntax of Core.
## Completion
1. The partial solution is implemented.
I think we should start with the partial solution, so that's what this ticket is about. The full solution will require much more thought and design effort, so we can get back to it later.9.2.1Vladislav ZavialovVladislav Zavialovhttps://gitlab.haskell.org/ghc/ghc//issues/18753Tighten up the treatment of loose types in the solver20200930T16:21:20ZRichard Eisenbergrae@richarde.devTighten up the treatment of loose types in the solver`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.`GHC.Tc.Solver.Monad` includes
```
Note [Use loose types in inert set]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Say we know (Eq (a > c1)) and we need (Eq (a > c2)). One is clearly
solvable from the other. So, we do lookup in the inert set using
loose types, which omits the kindcheck.
We must be careful when using the result of a lookup because it may
not match the requested info exactly!
```
There are several problems.
* We aren't always careful. For example, `lookupInInerts` tries `lookupSolvedDict` and then `lookupInertDict`, both of which use this "loose" lookup. Yet the result of `lookupInInerts` just uses the result, without any special handling to take the fact that the types might not match exactly.
* The Note doesn't actually make sense. The only difference between `Eq (a > c1)` and `Eq (a > c2)` is the coercion. But I sincerely hope we never care about the contents of a coercion. So even if we use evidence of type `Eq (a > c1)` where GHC is expecting `Eq (a > c2)` (assuming `c1` and `c2` have the same type), all will be well.
* What I think the Note is trying to say will never happen. That is, the actual implementation of the inertset lookup tries to match types while ignoring their kinds. (Normal type matching requires that the kind matches also.) So a better example would be something like comparing `Eq (a :: k1)` with `Eq (a :: k2)`. But that's impossible, even with casts: all type families and classes have *closed* kinds, meaning that any variables that appear in the kinds of arguments must themselves be earlier arguments. In other words, if I have welltyped `T blah1 (... :: kind1)` and `T blah2 (... :: kind2)`, then either `kind1` equals `kind2` or `blah1` and `blah2` must differ. We use this logic elsewhere  in particular, in the pure unifier.
Conclusions:
* Using "loose" matching (that is, ignoring kinds) in the solver is the right thing.
* We should update the Note with my argument above.
* No special care needs to be taken when using loose matching in this way. This means we can drop a few redundant equality checks (e.g. in `lookupFlatCache`).
I'm pretty confident about this all, but I'd like a doublecheck before I commit a fix.https://gitlab.haskell.org/ghc/ghc//issues/18739Infer multiplicity of let expression20200928T12:06:59ZArnaud SpiwackInfer multiplicity of let expression## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .## Motivation
In a let expression `let x = rhs in u`, `x` is always bound with multiplicity `Many` (and, correspondingly, `u` is consumed with multiplicity `Many`).
This also holds of where expression `u where x = rhs`.
The situation is similar to that of case expression as in #18738 .
In #18461 , we are adding a syntax to force polymorphism, but programmers expect let expressions to know their multiplicity on their own (in particular, they expect `let x = y in u` to be the same as `u[x\y]`, but if the latter consumes `y` linearly, the former never does in the current GHC).
## Proposal
Infer the multiplicity of `let` binders instead of choosing `Many` systematically. The multiplicity would be a variable.
A small detail to pay attention to is that, in `let pat = rhs in u`, the outermost pattern of `pat` is lazy. Lazy pattern are only permissible in unrestricted patterns (one way to think about it is that the desugaring of lazy pattern is not linear).
The typechecker doesn't make this property very apparent, so we will have to be careful about it. I suppose the same issue arises in #18461 .https://gitlab.haskell.org/ghc/ghc//issues/18738Infer multiplicity of case expression20210218T10:48:10ZArnaud SpiwackInfer multiplicity of case expression## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidal## Motivation
As it stands, the following expression
```haskell
case u of {…}
```
is always understood by the typechecker as consuming `u` with multiplicity `Many`. This was done in the first iteration of patch in order to ensure being fully compatible with regular Haskell without having to delve too much into inference issue.
This applies to case expressions and to pattern guards creating a pattern:
```haskell
 pat < u, … = …
```
here u is also consumed with multiplicity `Many`.
(In a `\case` or a function definition by equations, the multiplicity is decided by the type that it is checked against, if any. So it may be any multiplicity.)
Core is already equipped to deal with arbitrary multiplicities here.
## Proposal
These expressions should infer the appropriate multiplicity. So typechecking such a case expression should emit a multiplicity variable instead of choosing `Many` systematically.
One somewhat subtle point to keep in mind is that some patterns require that the scrutinee be consumed unrestrictedly. That's the case, for instance, of wildcard patterns (`_`). I believe that the current implementation will handle a variable for the pattern's multiplicity smoothly (see `checkManyPattern` in `GHC.Tc.Gen.Pat` ([currently](https://gitlab.haskell.org/ghc/ghc//blob/d7385f7077c6258c2a76ae51b4ea80f6fa9c7015/compiler/GHC/Tc/Gen/Pat.hs#L348349)). But it's worth doublechecking.
For pattern guard the relevant code is the `BindStmt` case of `tcGuardStmt` in `GHC.Tc.Gen.Match`.
cc @monoidalhttps://gitlab.haskell.org/ghc/ghc//issues/18715ThBrackCtxt is unused20200921T21:17:06ZRyan ScottThBrackCtxt is unusedThe [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L5792) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
 ThBrackCtxt  Template Haskell type brackets [t ... ]
 ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
 a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ 2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt > ContextKind
 Depending on the context, we might accept any kind (for instance, in a TH
 splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
 The types in a 'default' decl can have varying kinds
 See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
 a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ 92,7 +92,6 @@ data UserTypeCtxt
 True: standalone deriving
 False: vanilla instance declaration
 SpecInstCtxt  SPECIALISE instance pragma
  ThBrackCtxt  Template Haskell type brackets [t ... ]
 GenSigCtxt  Higherrank or impredicative situations
 e.g. (f e) where f has a higherrank type
 We might want to elaborate this
@@ 136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t...]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ > rank1
SpecInstCtxt > rank1
 ThBrackCtxt > rank1
GhciCtxt {} > ArbitraryRank
TyVarBndrKindCtxt _ > rank0
@@ 500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt > Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ 1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True  ??
okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?The [`UserTypeCtxt`](https://gitlab.haskell.org/ghc/ghc//blob/a1f34d37b47826e86343e368a5c00f1a4b1f2bce/compiler/GHC/Tc/Types/Origin.hs#L5792) data type defines a context for TH brackets:
```hs
data UserTypeCtxt
= ...
 ThBrackCtxt  Template Haskell type brackets [t ... ]
 ...
```
However, this does not appear to actually be used anywhere and can be removed relatively easily:
<details>
```diff
diff git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 3a1ab09c9b..e81a87c3a8 100644
 a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ 2831,7 +2831,6 @@ expectedKindInCtxt :: UserTypeCtxt > ContextKind
 Depending on the context, we might accept any kind (for instance, in a TH
 splice), or only certain kinds (like in type signatures).
expectedKindInCtxt (TySynCtxt _) = AnyKind
expectedKindInCtxt ThBrackCtxt = AnyKind
expectedKindInCtxt (GhciCtxt {}) = AnyKind
 The types in a 'default' decl can have varying kinds
 See Note [Extended defaults]" in GHC.Tc.Utils.Env
diff git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b2fdefa4cd..cc63f7a5c5 100644
 a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ 92,7 +92,6 @@ data UserTypeCtxt
 True: standalone deriving
 False: vanilla instance declaration
 SpecInstCtxt  SPECIALISE instance pragma
  ThBrackCtxt  Template Haskell type brackets [t ... ]
 GenSigCtxt  Higherrank or impredicative situations
 e.g. (f e) where f has a higherrank type
 We might want to elaborate this
@@ 136,7 +135,6 @@ pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature fo
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
pprUserTypeCtxt ThBrackCtxt = text "a Template Haskell quotation [t...]"
pprUserTypeCtxt PatSigCtxt = text "a pattern type signature"
pprUserTypeCtxt ResSigCtxt = text "a result type signature"
pprUserTypeCtxt (ForSigCtxt n) = text "the foreign declaration for" <+> quotes (ppr n)
diff git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index fba45562b7..05dcb28643 100644
 a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ 372,7 +372,6 @@ checkValidType ctxt ty
ForSigCtxt _ > rank1
SpecInstCtxt > rank1
 ThBrackCtxt > rank1
GhciCtxt {} > ArbitraryRank
TyVarBndrKindCtxt _ > rank0
@@ 500,7 +499,6 @@ vdqAllowed :: UserTypeCtxt > Bool
vdqAllowed (KindSigCtxt {}) = True
vdqAllowed (StandaloneKindSigCtxt {}) = True
vdqAllowed (TySynCtxt {}) = True
vdqAllowed (ThBrackCtxt {}) = True
vdqAllowed (GhciCtxt {}) = True
vdqAllowed (TyVarBndrKindCtxt {}) = True
vdqAllowed (DataKindCtxt {}) = True
@@ 1333,7 +1331,6 @@ okIPCtxt ResSigCtxt = True
okIPCtxt GenSigCtxt = True
okIPCtxt (ConArgCtxt {}) = True
okIPCtxt (ForSigCtxt {}) = True  ??
okIPCtxt ThBrackCtxt = True
okIPCtxt (GhciCtxt {}) = True
okIPCtxt SigmaCtxt = True
okIPCtxt (DataTyCtxt {}) = True
```
</details>
Is there a good reason to keep this around?